kempe 0.2.0.9 → 0.2.0.10

raw patch · 14 files changed

+94/−52 lines, 14 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• docs/manual.pdf binary
• golden/CDecl.hs +1/−1
• golden/Golden.hs +3/−1
• kempe.cabal +1/−1
• prelude/fn.kmp +5/−1
• src/Kempe/Check/Lint.hs +1/−1
• src/Kempe/Error.hs +1/−1
• src/Kempe/TyAssign.hs +68/−23
• test/Parser.hs +1/−11
• test/Type.hs +2/−10
• test/data/mutual.kmp +0/−2
• test/err/typecheck.kmp +3/−0
• test/include/num.h +3/−0

@@ -1,5 +1,10 @@ # kempe +## 0.2.0.10++  * Fix bug in typechecking against inferred signatures.+  * Fix bug in prelude+ ## 0.2.0.9    * Add `armabi` method of exporting Kempe functions, so that `kc` generates

binary file changed (217165 → 217165 bytes)

@@ -5,7 +5,7 @@ import           Data.Text.Lazy.Encoding   (encodeUtf8) import           Kempe.File import           Language.C.AST-import           Prettyprinter             (Doc, LayoutOptions (..), PageWidth (..), layoutSmart)+import           Prettyprinter             (Doc, layoutSmart) import           Prettyprinter.Render.Text (renderLazy) import           Test.Tasty                (TestTree) import           Test.Tasty.Golden         (goldenVsString)

@@ -20,7 +20,9 @@     _         -> error "Test suite must be run on x86_64 or aarch64"  headerGoldens :: [(FilePath, FilePath)]-headerGoldens = [ ("test/examples/splitmix.kmp", "test/include/splitmix.h") ]+headerGoldens = [ ("test/examples/splitmix.kmp", "test/include/splitmix.h")+                , ("lib/numbertheory.kmp", "test/include/num.h")+                ]  allGoldens :: [(FilePath, FilePath, FilePath)] allGoldens =

@@ -1,6 +1,6 @@ cabal-version:   3.0 name:            kempe-version:         0.2.0.9+version:         0.2.0.10 license:         BSD-3-Clause license-file:    LICENSE copyright:       Copyright: (c) 2020-2021 Vanessa McHale

@@ -10,7 +10,11 @@      =: [ swap dip(swap) ]  rotl : a b c -- c b a-     =: [ dip(swap) swap ]+     =: [ rotr swap ]++; from https://docs.factorcode.org/content/word-pick%2Ckernel.html+pick : a b c -- a b c a+     =: [ dip(dip(dup)) dip(swap) swap ]  over : a b -- a b a      =: [ dip(dup) swap ]

@@ -33,7 +33,7 @@ lintAtoms ((Dip l [AtBuiltin _ WordTimes]):a@(AtBuiltin _ WordTimes):_) = Just (DipAssoc l a) lintAtoms ((Dip l [AtBuiltin _ And]):a@(AtBuiltin _ And):_)             = Just (DipAssoc l a) lintAtoms ((Dip l [AtBuiltin _ Or]):a@(AtBuiltin _ Or):_)               = Just (DipAssoc l a)-lintAtoms ((Dip l [AtBuiltin _ IntEq]):a@(AtBuiltin _ IntEq):_)         = Just (DipAssoc l a)+-- lintAtoms ((Dip l [AtBuiltin _ IntEq]):a@(AtBuiltin _ IntEq):_)         = Just (DipAssoc l a) lintAtoms ((AtBuiltin l Swap):(AtBuiltin _ Swap):_)                     = Just (DoubleSwap l) lintAtoms ((AtBuiltin l Dup):a@(AtBuiltin _ And):_)                     = Just (Identity l a) lintAtoms ((AtBuiltin l Dup):a@(AtBuiltin _ Or):_)                      = Just (Identity l a)

@@ -43,7 +43,7 @@     pretty (UnificationFailed _ ty ty')  = "could not unify type" <+> squotes (pretty ty) <+> "with" <+> squotes (pretty ty')     pretty (TyVarExt _ n)                = "Error in function" <+> pretty n <> ": type variables may not occur in external or exported functions."     pretty (MonoFailed _)                = "Monomorphization step failed"-    pretty (LessGeneral _ sty sty')      = "Type" <+> pretty sty' <+> "is not as general as type" <+> pretty sty+    pretty (LessGeneral _ sty sty')      = "Type" <+> pretty sty' <+> "is not as general as type" <+> pretty sty <+> "or does not match."     pretty (InvalidCExport _ n)          = "C export" <+> pretty n <+> "has more than one return value"     pretty (InvalidCImport _ n)          = pretty n <+> "imported functions can have at most one return value"     pretty (IllKinded _ ty)              = "Ill-kinded type:" <+> squotes (pretty ty) <> ". Note that type variables have kind ⭑ in Kempe."

@@ -11,12 +11,11 @@ import           Control.Composition        (thread, (.$)) import           Control.Monad              (foldM, replicateM, unless, when, zipWithM_) import           Control.Monad.Except       (throwError)-import           Control.Monad.State.Strict (StateT, get, gets, modify, put, runStateT)+import           Control.Monad.State.Strict (State, StateT, evalState, get, gets, modify, put, runStateT) import           Data.Bifunctor             (bimap, second) import           Data.Foldable              (traverse_) import           Data.Functor               (void, ($>)) import qualified Data.IntMap                as IM-import           Data.List                  (foldl') import           Data.List.NonEmpty         (NonEmpty (..)) import           Data.Semigroup             ((<>)) import qualified Data.Set                   as S@@ -294,14 +293,22 @@     where dropFst (_, y, z) = (y, z)  assignAtoms :: [Atom b a] -> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())-assignAtoms = foldM-    (\seed a -> do { (ty, r) <- assignAtom a ; (fst seed ++ [r] ,) <$> catTypes (snd seed) ty })-    ([], emptyStackType)+assignAtoms []  = pure ([], emptyStackType)+assignAtoms [a] = do+    (ty, a') <- assignAtom a+    pure ([a'], ty)+assignAtoms (a:as) = do+    (ty, a') <- assignAtom a+    (as', ty') <- assignAtoms as+    (a':as' ,) <$> catTypes ty ty'  tyAtoms :: [Atom b a] -> TypeM () (StackType ())-tyAtoms = foldM-    (\seed a -> do { tys' <- tyAtom a ; catTypes seed tys' })-    emptyStackType+tyAtoms [] = pure emptyStackType+tyAtoms [a] = tyAtom a+tyAtoms (a:as) = do+    ty <- tyAtom a+    tys <- tyAtoms as+    catTypes ty tys  -- from size, mkHKT :: Int -> Kind@@ -334,7 +341,7 @@     (tn $> ty, fmap void ins)  app :: KempeTy a -> [Name a] -> KempeTy a-app = foldl' (\ty n -> TyApp undefined ty (TyVar undefined n))+app = foldr (\n ty -> TyApp undefined ty (TyVar undefined n))  kindLookup :: TyName a -> TypeM a Kind kindLookup n@(Name _ (Unique i) l) = do@@ -361,14 +368,14 @@     sig <- renameStack $ voidStackType $ StackType (freeVars (ins ++ os)) ins os     (as, inferred) <- assignAtoms a     reconcile <- mergeStackTypes sig inferred-    -- assign comes after tyInsert+    when (inferred `lessGeneral` sig) $+        throwError $ LessGeneral () sig inferred     pure $ FunDecl reconcile (n $> reconcile) (void <$> ins) (void <$> os) as assignDecl (ExtFnDecl _ n ins os cn) = do     traverse_ kindOf (void <$> ins ++ os)     unless (length os <= 1) $         throwError $ InvalidCImport () (void n)     let sig = voidStackType $ StackType S.empty ins os-    -- assign always comes after tyInsert     pure $ ExtFnDecl sig (n $> sig) (void <$> ins) (void <$> os) cn assignDecl (Export _ abi n) = do     ty@(StackType _ _ os) <- tyLookup (void n)@@ -394,18 +401,56 @@     modifying tyEnvLens (IM.insert i sig) tyHeader TyDecl{} = pure () -lessGeneral :: StackType a -> StackType a -> Bool-lessGeneral (StackType _ is os) (StackType _ is' os') = lessGenerals (is ++ os) (is' ++ os')-    where lessGeneralAtom :: KempeTy a -> KempeTy a -> Bool-          lessGeneralAtom TyBuiltin{} TyVar{}                   = True-          lessGeneralAtom TyApp{} TyVar{}                       = True-          lessGeneralAtom (TyApp _ ty ty') (TyApp _ ty'' ty''') = lessGeneralAtom ty ty'' || lessGeneralAtom ty' ty''' -- lazy pattern match?-          lessGeneralAtom _ _                                   = False-          lessGenerals :: [KempeTy a] -> [KempeTy a] -> Bool-          lessGenerals [] []               = False-          lessGenerals (ty:tys) (ty':tys') = lessGeneralAtom ty ty' || lessGenerals tys tys'-          lessGenerals _ []                = False -- shouldn't happen; will be caught later-          lessGenerals [] _                = False+type Vars a = IM.IntMap (Name a)++-- TODO: do we want strict or lazy?+type EqState a = State (Vars a)++-- FIXME: this is too simple-minded.+-- a -- a b+-- checks against+-- dup+-- because it results in the constraint a = b...+--+-- NEED to check stack types are equivalent up to "alpha-equivalence"+-- (implicit binding with every space/new var!)+lessGeneral :: StackType a -- ^ Inferred type+            -> StackType a -- ^ Type from signature+            -> Bool+lessGeneral (StackType _ is os) (StackType _ is' os') =+    flip evalState mempty $+        if il > il' || ol > ol'+            then (||) <$> lessGenerals trimIs is' <*> lessGenerals trimOs os'+            else (||) <$> lessGenerals is trimIs' <*> lessGenerals os trimOs'+    where il = length is+          il' = length is'+          ol = length os+          ol' = length os'+          trimIs = drop (il-il') is+          trimIs' = drop (il'-il) is'+          trimOs = drop (ol-ol') os+          trimOs' = drop (ol'-ol) os'++          lessGeneralAtom :: KempeTy a -> KempeTy a -> EqState a Bool+          lessGeneralAtom TyBuiltin{} TyVar{}                   = pure True+          lessGeneralAtom TyApp{} TyVar{}                       = pure True+          -- FIXME: Type a_13 (Maybe_1 a_10) -- a_12 is not as general as type a_9 (Maybe_1 a_9) -- a_9+          --+          -- FIXME Type a_38 b_39 a_40 -- b_39 b_42 a_41 is not as general as type a_35 b_36 c_37 -- c_37 b_36 a_35+          lessGeneralAtom (TyApp _ ty ty') (TyApp _ ty'' ty''') = (||) <$> lessGeneralAtom ty ty'' <*> lessGeneralAtom ty' ty''' -- lazy pattern match?+          lessGeneralAtom _ _                                   = pure False+          lessGenerals :: [KempeTy a] -> [KempeTy a] -> EqState a Bool+          lessGenerals [] []                                 = pure False+          lessGenerals ((TyVar _ n):tys) ((TyVar _ n'):tys') = do+                st <- get+                let i = unUnique $ unique n+                case IM.lookup i st of+                    Nothing ->+                        modify (IM.insert i n') *>+                        lessGenerals tys tys' -- we can skip checking ty `lessGeneral` ty' at the first site+                    Just n'' ->+                        (n'' /= n' ||) <$> lessGenerals tys tys'+          lessGenerals (ty:tys) (ty':tys')                  = (||) <$> lessGeneralAtom ty ty' <*> lessGenerals tys tys'  tyInsert :: KempeDecl a c b -> TypeM () () tyInsert (TyDecl _ tn ns ls) = traverse_ (tyInsertLeaf tn (S.fromList ns)) ls

@@ -2,19 +2,11 @@               ) where  import qualified Data.ByteString.Lazy as BSL-import           Kempe.Lexer import           Kempe.Parser import           Prettyprinter        (pretty) import           Test.Tasty import           Test.Tasty.HUnit -lexNoError :: FilePath -> TestTree-lexNoError fp = testCase ("Lexing doesn't fail (" ++ fp ++ ")") $ do-    contents <- BSL.readFile fp-    case lexKempe contents of-        Left err -> assertFailure err-        Right{}  -> assertBool "Doesn't fail lexing" True- parseNoError :: FilePath -> TestTree parseNoError fp = testCase ("Parsing doesn't fail (" ++ fp ++ ")") $ do     contents <- BSL.readFile fp@@ -26,8 +18,6 @@ parserTests :: TestTree parserTests =     testGroup "Parser golden tests"-        [ lexNoError "test/data/lex.kmp"-        , lexNoError "examples/splitmix.kmp"-        , parseNoError "test/data/lex.kmp"+        [ parseNoError "test/data/lex.kmp"         , parseNoError "examples/splitmix.kmp"         ]

@@ -27,11 +27,10 @@         , tyInfer "lib/gaussian.kmp"         , tyInfer "test/data/transitive.kmp"         , tyInfer "lib/tuple.kmp"-        , badType "test/err/merge.kmp" "Type a_5 -- Int a_4 is not as general as type a_3 -- a_3 a_3"+        , badType "test/err/merge.kmp" "Type a_4 -- Int a_4 is not as general as type a_3 -- a_3 a_3 or does not match."         , badType "test/err/kind.kmp" "Ill-kinded type: '(Maybe_1 Maybe_1)'. Note that type variables have kind \11089 in Kempe."         , badType "test/err/patternMatch.kmp" "Inexhaustive pattern match."-        , detectsWarn "test/err/stupid.kmp" "4:1 'rand_1' is defined more than once."-        , detectsWarn "test/err/questionable.kmp" "3:19 'Some_3' is defined more than once."+        , badType "test/err/typecheck.kmp" "Type a_8 a_9 a_10 -- a_8 a_8 a_9 a_10 is not as general as type a_5\nb_6\nc_7 -- a_5 b_6 c_7 a_5 or does not match."         , testAssignment "test/data/ty.kmp"         , testAssignment "lib/either.kmp"         , testAssignment "prelude/fn.kmp"@@ -57,13 +56,6 @@     case res of         Left err -> assertFailure (show $ pretty err)         Right{}  -> assertBool "Doesn't fail type-checking" True--detectsWarn :: FilePath -> String -> TestTree-detectsWarn fp msg = testCase ("Warns (" ++ fp ++ ")") $ do-    res <- warnFile fp-    case res of-        Just err -> show (pretty err) @?= msg-        Nothing  -> assertFailure "Failed to warn!"  badType :: FilePath -> String -> TestTree badType fp msg = testCase ("Detects error (" ++ fp ++ ")") $ do

@@ -1,5 +1,3 @@-import "lib/bool.kmp"- odd : Int -- Bool     =: [ dup 0 =             if( drop False

@@ -0,0 +1,3 @@+; FIXME: should not typecheck (just generates constraint b = c, which should not be allowed+pick : a b c -- a b c a+     =: [ dip(dip(dup)) ]

@@ -0,0 +1,3 @@+#include <stdbool.h>+extern int k_gcd (void*, int, int);+extern bool is_prime (void*, int);