diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/docs/manual.pdf b/docs/manual.pdf Binary files a/docs/manual.pdf and b/docs/manual.pdf differ diff --git a/golden/CDecl.hs b/golden/CDecl.hs --- a/golden/CDecl.hs +++ b/golden/CDecl.hs @@ -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) diff --git a/golden/Golden.hs b/golden/Golden.hs --- a/golden/Golden.hs +++ b/golden/Golden.hs @@ -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 = diff --git a/kempe.cabal b/kempe.cabal --- a/kempe.cabal +++ b/kempe.cabal @@ -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 diff --git a/prelude/fn.kmp b/prelude/fn.kmp --- a/prelude/fn.kmp +++ b/prelude/fn.kmp @@ -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 ] diff --git a/src/Kempe/Check/Lint.hs b/src/Kempe/Check/Lint.hs --- a/src/Kempe/Check/Lint.hs +++ b/src/Kempe/Check/Lint.hs @@ -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) diff --git a/src/Kempe/Error.hs b/src/Kempe/Error.hs --- a/src/Kempe/Error.hs +++ b/src/Kempe/Error.hs @@ -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." diff --git a/src/Kempe/TyAssign.hs b/src/Kempe/TyAssign.hs --- a/src/Kempe/TyAssign.hs +++ b/src/Kempe/TyAssign.hs @@ -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 diff --git a/test/Parser.hs b/test/Parser.hs --- a/test/Parser.hs +++ b/test/Parser.hs @@ -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" ] diff --git a/test/Type.hs b/test/Type.hs --- a/test/Type.hs +++ b/test/Type.hs @@ -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 diff --git a/test/data/mutual.kmp b/test/data/mutual.kmp --- a/test/data/mutual.kmp +++ b/test/data/mutual.kmp @@ -1,5 +1,3 @@ -import "lib/bool.kmp" - odd : Int -- Bool =: [ dup 0 = if( drop False diff --git a/test/err/typecheck.kmp b/test/err/typecheck.kmp new file mode 100644 --- /dev/null +++ b/test/err/typecheck.kmp @@ -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)) ] diff --git a/test/include/num.h b/test/include/num.h new file mode 100644 --- /dev/null +++ b/test/include/num.h @@ -0,0 +1,3 @@ +#include +extern int k_gcd (void*, int, int); +extern bool is_prime (void*, int);