From 05313652f9951a157bd9599118502a5f1793e620 Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Tue, 28 Feb 2023 17:15:48 +0100 Subject: [PATCH] unit tests, started on pattern matching --- Grammar.cf | 41 +++++------- language.cabal | 2 +- src/Main.hs | 24 +++---- src/Renamer/Renamer.hs | 1 - src/TypeChecker/CheckInj.hs | 27 ++++++++ src/TypeChecker/TypeChecker.hs | 78 ++++++++++++----------- src/TypeChecker/TypeCheckerIr.hs | 44 ++++++++++--- test_program | 22 +++---- tests/Tests.hs | 106 +++++++++++++++++++++---------- 9 files changed, 212 insertions(+), 133 deletions(-) create mode 100644 src/TypeChecker/CheckInj.hs diff --git a/Grammar.cf b/Grammar.cf index 96554bb..dda87b4 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -8,6 +8,18 @@ separator Def ";" ; Bind. Bind ::= Ident ":" Type ";" Ident [Ident] "=" Exp ; +Data. Data ::= "data" Type "where" "{" + [Constructor] "}" ; + +separator nonempty Constructor "" ; + +Constructor. Constructor ::= Ident ":" Type ; + +TMono. Type1 ::= "_" Ident ; +TPol. Type1 ::= "'" Ident ; +TConstr. Type1 ::= Ident "(" [Type] ")" ; +TArr. Type ::= Type1 "->" Type ; + EAnn. Exp5 ::= "(" Exp ":" Type ")" ; EId. Exp4 ::= Ident ; ELit. Exp4 ::= Literal ; @@ -15,43 +27,24 @@ EApp. Exp3 ::= Exp3 Exp4 ; EAdd. Exp1 ::= Exp1 "+" Exp2 ; ELet. Exp ::= "let" Ident "=" Exp "in" Exp ; EAbs. Exp ::= "\\" Ident "." Exp ; -ECase. Exp ::= "case" Exp "of" "{" [Inj] "}"; +ECase. Exp ::= "case" Exp "of" "{" [Inj] "}"; LInt. Literal ::= Integer ; Inj. Inj ::= Init "=>" Exp ; -terminator Inj ";" ; +separator nonempty Inj ";" ; -InitLit. Init ::= Literal ; -InitConstr. Init ::= Ident [Match] ; -InitCatch. Init ::= "_" ; - -LMatch. Match ::= Literal ; -IMatch. Match ::= Ident ; -InitMatch. Match ::= Ident Match ; -separator Match " " ; - -TMono. Type1 ::= "_" Ident ; -TPol. Type1 ::= "'" Ident ; -TConstr. Type1 ::= Ident "(" [Type] ")" ; -TArr. Type ::= Type1 "->" Type ; +InitLit. Init ::= Literal ; +InitConstr. Init ::= Ident [Ident] ; +InitCatch. Init ::= "_" ; separator Type " " ; coercions Type 2 ; --- shift/reduce problem here -Data. Data ::= "data" Type "where" ";" - [Constructor]; - -separator Constructor "," ; - -Constructor. Constructor ::= Ident ":" Type ; - -- This doesn't seem to work so we'll have to live with ugly keywords for now -- token Poly upper (letter | digit | '_')* ; -- token Mono lower (letter | digit | '_')* ; -separator Bind ";" ; separator Ident " "; coercions Exp 5 ; diff --git a/language.cabal b/language.cabal index 3556367..637d9f7 100644 --- a/language.cabal +++ b/language.cabal @@ -47,7 +47,6 @@ executable language , either , extra , array - , QuickCheck default-language: GHC2021 @@ -76,6 +75,7 @@ Test-suite language-testsuite , either , extra , array + , hspec , QuickCheck default-language: GHC2021 diff --git a/src/Main.hs b/src/Main.hs index 316c599..8e62f2b 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -3,7 +3,6 @@ module Main where -- import Codegen.Codegen (compile) -import GHC.IO.Handle.Text (hPutStrLn) import Grammar.ErrM (Err) import Grammar.Par (myLexer, pProgram) import Grammar.Print (printTree) @@ -12,7 +11,6 @@ import Grammar.Print (printTree) import Renamer.Renamer (rename) import System.Environment (getArgs) import System.Exit (exitFailure, exitSuccess) -import System.IO (stderr) import TypeChecker.TypeChecker (typecheck) main :: IO () @@ -25,32 +23,28 @@ main' :: String -> IO () main' s = do file <- readFile s - printToErr "-- Parse Tree -- " + putStrLn "-- Parse Tree -- " parsed <- fromSyntaxErr . pProgram $ myLexer file - printToErr $ printTree parsed + putStrLn $ printTree parsed - printToErr "\n-- Renamer --" + putStrLn "\n-- Renamer --" let renamed = rename parsed - printToErr $ printTree renamed + putStrLn $ printTree renamed - printToErr "\n-- TypeChecker --" + putStrLn "\n-- TypeChecker --" typechecked <- fromTypeCheckerErr $ typecheck renamed - printToErr $ printTree typechecked + putStrLn $ printTree typechecked - -- printToErr "\n-- Lambda Lifter --" + -- putStrLn "\n-- Lambda Lifter --" -- let lifted = lambdaLift typechecked - -- printToErr $ printTree lifted + -- putStrLn $ printTree lifted - -- printToErr "\n -- Printing compiler output to stdout --" + -- putStrLn "\n -- Printing compiler output to stdout --" -- compiled <- fromCompilerErr $ compile lifted -- putStrLn compiled - -- writeFile "llvm.ll" compiled exitSuccess -printToErr :: String -> IO () -printToErr = hPutStrLn stderr - fromCompilerErr :: Err a -> IO a fromCompilerErr = either diff --git a/src/Renamer/Renamer.hs b/src/Renamer/Renamer.hs index 1ea892c..24582f6 100644 --- a/src/Renamer/Renamer.hs +++ b/src/Renamer/Renamer.hs @@ -28,7 +28,6 @@ rename (Program bs) = Program $ evalState (runRn $ mapM (renameSc initNames) bs) pure . DBind $ Bind name t name parms' rhs' renameSc _ def = pure def --- -- | Rename monad. State holds the number of renamed names. newtype Rn a = Rn { runRn :: State Int a } diff --git a/src/TypeChecker/CheckInj.hs b/src/TypeChecker/CheckInj.hs new file mode 100644 index 0000000..c5845df --- /dev/null +++ b/src/TypeChecker/CheckInj.hs @@ -0,0 +1,27 @@ +{-# OPTIONS_GHC -Wno-unused-imports #-} +module TypeChecker.CheckInj where + +import TypeChecker.TypeChecker +import qualified TypeChecker.TypeCheckerIr as T +import TypeChecker.TypeCheckerIr (Infer) + +import Control.Monad.Except +import Control.Monad.Reader +import Control.Monad.State +import Data.Functor.Identity (Identity, runIdentity) +import Data.Map (Map) +import qualified Data.Map as M + +import Grammar.Abs +import Grammar.Print (printTree) + + +checkInj :: Inj -> Infer T.Inj +checkInj (Inj it expr) = do + (_, e') <- inferExp expr + t' <- initType it + return $ T.Inj (it, t') e' + +initType :: Init -> Infer Type +initType = undefined + diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs index b938477..80a5289 100644 --- a/src/TypeChecker/TypeChecker.hs +++ b/src/TypeChecker/TypeChecker.hs @@ -1,10 +1,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# HLINT ignore "Use traverse_" #-} -{-# OPTIONS_GHC -Wno-overlapping-patterns #-} -{-# HLINT ignore "Use zipWithM" #-} +-- | A module for type checking and inference using algorithm W, Hindley-Milner module TypeChecker.TypeChecker where import Control.Monad.Except @@ -21,23 +18,9 @@ import Data.Foldable (traverse_) import Grammar.Abs import Grammar.Print (printTree) import qualified TypeChecker.TypeCheckerIr as T +import TypeChecker.TypeCheckerIr (Ctx (..), Env (..), Error, Infer, + Poly (..), Subst) --- | A data type representing type variables -data Poly = Forall [Ident] Type - deriving Show - -newtype Ctx = Ctx { vars :: Map Ident Poly - } - -data Env = Env { count :: Int - , sigs :: Map Ident Type - , dtypes :: Map Ident Type - } - -type Error = String -type Subst = Map Ident Type - -type Infer = StateT Env (ReaderT Ctx (ExceptT Error Identity)) initCtx = Ctx mempty initEnv = Env 0 mempty mempty @@ -98,7 +81,11 @@ checkBind (Bind n t _ args e) = do (t', e') <- inferExp $ makeLambda e (reverse args) s <- unify t t' let t'' = apply s t - unless (t `typeEq` t'') (throwError $ unwords ["Top level signature", printTree t, "does not match body with type:", printTree t'']) + unless (t `typeEq` t'') (throwError $ unwords ["Top level signature" + , printTree t + , "does not match body with inferred type:" + , printTree t'' + ]) return $ T.Bind (n, t) [] e' where makeLambda :: Exp -> [Ident] -> Exp @@ -109,12 +96,17 @@ checkBind (Bind n t _ args e) = do typeEq :: Type -> Type -> Bool typeEq (TArr l r) (TArr l' r') = typeEq l l' && typeEq r r' typeEq (TMono a) (TMono b) = a == b -typeEq (TConstr name a) (TConstr name' b) = if length a == length b - then name == name' && and (zipWith typeEq a b) - else False +typeEq (TConstr name a) (TConstr name' b) = length a == length b + && name == name' + && and (zipWith typeEq a b) typeEq (TPol _) (TPol _) = True typeEq _ _ = False +isMoreGeneral :: Type -> Type -> Bool +isMoreGeneral _ (TPol _) = True +isMoreGeneral (TArr a b) (TArr c d) = isMoreGeneral a c && isMoreGeneral b d +isMoreGeneral a b = a == b + inferExp :: Exp -> Infer (Type, T.Exp) inferExp e = do (s, t, e') <- algoW e @@ -123,24 +115,30 @@ inferExp e = do replace :: Type -> T.Exp -> T.Exp replace t = \case - T.ELit _ e -> T.ELit t e - T.EId (n, _) -> T.EId (n, t) - T.EAbs _ name e -> T.EAbs t name e - T.EApp _ e1 e2 -> T.EApp t e1 e2 - T.EAdd _ e1 e2 -> T.EAdd t e1 e2 + T.ELit _ e -> T.ELit t e + T.EId (n, _) -> T.EId (n, t) + T.EAbs _ name e -> T.EAbs t name e + T.EApp _ e1 e2 -> T.EApp t e1 e2 + T.EAdd _ e1 e2 -> T.EAdd t e1 e2 T.ELet (T.Bind (n, _) args e1) e2 -> T.ELet (T.Bind (n, t) args e1) e2 algoW :: Exp -> Infer (Subst, Type, T.Exp) algoW = \case + -- | TODO: Reason more about this one. Could be wrong EAnn e t -> do (s1, t', e') <- algoW e + unless (t `isMoreGeneral` t') (throwError $ unwords + ["Annotated type:" + , printTree t + , "does not match inferred type:" + , printTree t' ]) applySt s1 $ do - s2 <- unify (apply s1 t) t' + s2 <- unify t t' return (s2 `compose` s1, t, e') -- | ------------------ --- | Γ ⊢ e₀ : Int, ∅ +-- | Γ ⊢ i : Int, ∅ ELit (LInt n) -> return (nullSubst, TMono "Int", T.ELit (TMono "Int") (LInt n)) @@ -159,7 +157,7 @@ algoW = \case case M.lookup i sig of Just t -> return (nullSubst, t, T.EId (i, t)) Nothing -> do - constr <- gets dtypes + constr <- gets constructors case M.lookup i constr of Just t -> return (nullSubst, t, T.EId (i, t)) Nothing -> throwError $ "Unbound variable: " ++ show i @@ -220,9 +218,9 @@ algoW = \case (s2, t2, e1') <- algoW e1 return (s2 `compose` s1, t2, T.ELet (T.Bind (name,t2) [] e0') e1' ) - ECase a b -> error $ "NOT IMPLEMENTED YET: ECase" ++ show a ++ " " ++ show b + ECase e0 injs -> undefined --- | Unify two types producing a new substitution (constraint) +-- | Unify two types producing a new substitution unify :: Type -> Type -> Infer Subst unify t0 t1 = case (t0, t1) of (TArr a b, TArr c d) -> do @@ -235,9 +233,15 @@ unify t0 t1 = case (t0, t1) of -- | TODO: Figure out a cleaner way to express the same thing (TConstr name t, TConstr name' t') -> if name == name' && length t == length t' then do - xs <- sequence $ zipWith unify t t' + xs <- zipWithM unify t t' return $ foldr compose nullSubst xs - else throwError $ unwords ["Type constructor:", printTree name, "(" ++ printTree t ++ ")", "does not match with:", printTree name', "(" ++ printTree t' ++ ")"] + else throwError $ unwords + ["Type constructor:" + , printTree name + , "(" ++ printTree t ++ ")" + , "does not match with:" + , printTree name' + , "(" ++ printTree t' ++ ")"] (a, b) -> throwError . unwords $ ["Type:", printTree a, "can't be unified with:", printTree b] -- | Check if a type is contained in another type. @@ -324,4 +328,4 @@ insertSig i t = modify (\st -> st { sigs = M.insert i t (sigs st) }) -- | Insert a constructor with its data type insertConstr :: Ident -> Type -> Infer () -insertConstr i t = modify (\st -> st { dtypes = M.insert i t (dtypes st) }) +insertConstr i t = modify (\st -> st { constructors = M.insert i t (constructors st) }) diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs index ee02416..82956b8 100644 --- a/src/TypeChecker/TypeCheckerIr.hs +++ b/src/TypeChecker/TypeCheckerIr.hs @@ -1,14 +1,33 @@ {-# LANGUAGE LambdaCase #-} -module TypeChecker.TypeCheckerIr - ( module Grammar.Abs - , module TypeChecker.TypeCheckerIr - ) where +module TypeChecker.TypeCheckerIr where -import Grammar.Abs (Data (..), Ident (..), Literal (..), Type (..)) +import Control.Monad.Except +import Control.Monad.Reader +import Control.Monad.State +import Data.Functor.Identity (Identity) +import Data.Map (Map) +import Grammar.Abs (Data (..), Ident (..), Init (..), + Literal (..), Type (..)) import Grammar.Print import Prelude -import qualified Prelude as C (Eq, Ord, Read, Show) +import qualified Prelude as C (Eq, Ord, Read, Show) + +-- | A data type representing type variables +data Poly = Forall [Ident] Type + deriving Show + +newtype Ctx = Ctx { vars :: Map Ident Poly } + +data Env = Env { count :: Int + , sigs :: Map Ident Type + , constructors :: Map Ident Type + } + +type Error = String +type Subst = Map Ident Type + +type Infer = StateT Env (ReaderT Ctx (ExceptT Error Identity)) newtype Program = Program [Def] deriving (C.Eq, C.Ord, C.Show, C.Read) @@ -22,6 +41,9 @@ data Exp | EAbs Type Id Exp deriving (C.Eq, C.Ord, C.Read, C.Show) +data Inj = Inj (Init, Type) Exp + deriving (C.Eq, C.Ord, C.Read, C.Show) + data Def = DBind Bind | DData Data deriving (C.Eq, C.Ord, C.Read, C.Show) @@ -30,6 +52,10 @@ type Id = (Ident, Type) data Bind = Bind Id [Id] Exp deriving (C.Eq, C.Ord, C.Show, C.Read) +instance Print [Def] where + prt _ [] = concatD [] + prt _ (x:xs) = concatD [prt 0 x, doc (showString "\n"), prt 0 xs] + instance Print Def where prt i (DBind bind) = prt i bind prt i (DData d) = prt i d @@ -41,16 +67,16 @@ instance Print Bind where prt i (Bind (t, name) parms rhs) = prPrec i 0 $ concatD [ prt 0 name , doc $ showString ":" - , prt 0 t + , prt 1 t , prtIdPs 0 parms , doc $ showString "=" - , prt 0 rhs + , prt 2 rhs ] instance Print [Bind] where prt _ [] = concatD [] prt _ [x] = concatD [prt 0 x] - prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), doc (showString "\n"), prt 0 xs] prtIdPs :: Int -> [Id] -> Doc prtIdPs i = prPrec i 0 . concatD . map (prtIdP i) diff --git a/test_program b/test_program index 5c2a164..0cc17b3 100644 --- a/test_program +++ b/test_program @@ -1,14 +1,12 @@ -data List ('a) where; - Nil : List ('a), - Cons : 'a -> List ('a) -> List ('a) ; +data List ('a) where { + Nil : List ('a) + Cons : 'a -> List ('a) -> List ('a) +}; -main : List (_Int) ; +data Bool () where { + True : Bool () + False : Bool () +}; + +main : List ('a) ; main = Cons 1 (Cons 0 Nil) ; - -data Bool () where; - True : Bool (), - False : Bool (); - -boolean : Bool (_Int); -boolean = True ; - diff --git a/tests/Tests.hs b/tests/Tests.hs index 46a9a3f..5c52939 100644 --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -1,56 +1,94 @@ {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use <$>" #-} +{-# HLINT ignore "Use camelCase" #-} module Main where -import Control.Monad.Except +import Data.Either (isLeft, isRight) +import Data.Map (Map) +import qualified Data.Map as M import Grammar.Abs +import Test.Hspec import Test.QuickCheck import TypeChecker.TypeChecker import qualified TypeChecker.TypeCheckerIr as T +import TypeChecker.TypeCheckerIr (Ctx (..), Env (..), Error, Infer, + Poly (..)) main :: IO () -main = do - quickCheck prop_isInt - quickCheck prop_idAbs_generic +main = hspec $ do + infer_elit + infer_eann + infer_eid + infer_eabs + infer_eapp -newtype AbsExp = AE Exp deriving Show -newtype EIntExp = EI Exp deriving Show +infer_elit = describe "algoW used on ELit" $ do + it "infers the type mono Int" $ do + getType (ELit (LInt 0)) `shouldBe` Right (TMono "Int") -instance Arbitrary EIntExp where - arbitrary = genInt + it "infers the type mono Int" $ do + getType (ELit (LInt 9999)) `shouldBe` Right (TMono "Int") -instance Arbitrary AbsExp where - arbitrary = genLambda +infer_eann = describe "algoW used on EAnn" $ do + it "infers the type and checks if the annotated type matches" $ do + getType (EAnn (ELit $ LInt 0) (TMono "Int")) `shouldBe` Right (TMono "Int") -getType :: Infer (Type, T.Exp) -> Either Error Type -getType ie = case run ie of - Left err -> Left err - Right (t,e) -> return t + it "fails if the annotated type does not match with the inferred type" $ do + getType (EAnn (ELit $ LInt 0) (TPol "a")) `shouldSatisfy` isLeft -genInt :: Gen EIntExp -genInt = EI . ELit . LInt <$> arbitrary + it "should be possible to annotate with a more specific type" $ do + let annotated_lambda = EAnn (EAbs "x" (EId "x")) (TArr (TMono "Int") (TMono "Int")) + in getType annotated_lambda `shouldBe` Right (TArr (TMono "Int") (TMono "Int")) -genLambda :: Gen AbsExp -genLambda = do - str <- arbitrary @String - let str' = Ident str - return $ AE $ EAbs str' (EId str') + it "should fail if the annotated type is more general than the inferred type" $ do + getType (EAnn (ELit (LInt 0)) (TPol "a")) `shouldSatisfy` isLeft -prop_idAbs_generic :: AbsExp -> Bool -prop_idAbs_generic (AE e) = case getType (inferExp e) of - Left _ -> False - Right t -> isGenericArr t + it "should fail if the annotated type is an arrow but the annotated type is not" $ do + getType (EAnn (EAbs "x" (EId "x")) (TPol "a")) `shouldSatisfy` isLeft -prop_isInt :: EIntExp -> Bool -prop_isInt (EI e) = case getType (inferExp e) of - Left _ -> False - Right t -> t == int +infer_eid = describe "algoW used on EId" $ do + it "should fail if the variable is not added to the environment" $ do + property $ \x -> getType (EId (Ident (x :: String))) `shouldSatisfy` isLeft -int :: Type -int = TMono "Int" + it "should succeed if the type exist in the environment" $ do + property $ \x -> do + let env = Env 0 mempty mempty + let t = Forall [] (TPol "a") + let ctx = Ctx (M.singleton (Ident (x :: String)) t) + getTypeC env ctx (EId (Ident x)) `shouldBe` Right (TPol "a") -isGenericArr :: Type -> Bool -isGenericArr (TArr (TPol a) (TPol b)) = a == b -isGenericArr _ = False +infer_eabs = describe "algoW used on EAbs" $ do + it "should infer the argument type as int if the variable is used as an int" $ do + let lambda = EAbs "x" (EAdd (EId "x") (ELit (LInt 0))) + getType lambda `shouldBe` Right (TArr (TMono "Int") (TMono "Int")) + + it "should infer the argument type as polymorphic if it is not used in the lambda" $ do + let lambda = EAbs "x" (ELit (LInt 0)) + getType lambda `shouldSatisfy` isArrowPolyToMono + it "should infer a variable as function if used as one" $ do + let lambda = EAbs "f" (EAbs "x" (EApp (EId "f") (EId "x"))) + let isOk (Right (TArr (TArr (TPol _) (TPol _)) (TArr (TPol _) (TPol _)))) = True + isOk _ = False + getType lambda `shouldSatisfy` isOk + +infer_eapp = describe "algoW used on EApp" $ do + it "should fail if a variable is applied to itself (occurs check)" $ do + property $ \x -> do + let env = Env 0 mempty mempty + let t = Forall [] (TPol "a") + let ctx = Ctx (M.singleton (Ident (x :: String)) t) + getTypeC env ctx (EApp (EId (Ident x)) (EId (Ident x))) `shouldBe` Left "Occurs check failed" + +isArrowPolyToMono :: Either Error Type -> Bool +isArrowPolyToMono (Right (TArr (TPol _) (TMono _))) = True +isArrowPolyToMono _ = False + +-- | Empty environment +getType :: Exp -> Either Error Type +getType e = pure fst <*> run (inferExp e) + +-- | Custom environment +getTypeC :: Env -> Ctx -> Exp -> Either Error Type +getTypeC env ctx e = pure fst <*> runC env ctx (inferExp e)