From c10d7703ad8e5bb3634b51f8aaf018b01dd5e85c Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Mon, 13 Feb 2023 19:03:06 +0100 Subject: [PATCH] Progression on type checker ;) --- Grammar.cf | 11 +- src/Main.hs | 11 +- src/TypeChecker/TypeChecker.hs | 172 +++++++++++++++++++------------ src/TypeChecker/TypeCheckerIr.hs | 12 +-- test_program | 2 +- 5 files changed, 126 insertions(+), 82 deletions(-) diff --git a/Grammar.cf b/Grammar.cf index b58dbea..45021c1 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -7,16 +7,19 @@ EAnn. Exp5 ::= Exp5 ":" Type ; EId. Exp4 ::= Ident; EConst. Exp4 ::= Const; EApp. Exp3 ::= Exp3 Exp4; -ELet. Exp2 ::= "let" Bind "in" Exp; EAdd. Exp1 ::= Exp1 "+" Exp2; +ELet. Exp ::= "let" Ident "=" Exp "in" Exp; EAbs. Exp ::= "\\" Ident "." Exp; CInt. Const ::= Integer ; CStr. Const ::= String ; -TMono. Type1 ::= Ident ; -TPoly. Type1 ::= Ident ; -TFun. Type ::= Type1 "->" Type ; +TMono. Type1 ::= UIdent ; +TPoly. Type1 ::= LIdent ; +TArrow. Type ::= Type "->" Type1 ; + +token UIdent (upper (letter | digit | '_')*) ; +token LIdent (lower (letter | digit | '_')*) ; separator Bind ";"; separator Ident " "; diff --git a/src/Main.hs b/src/Main.hs index e55afe9..27802b7 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -5,6 +5,7 @@ import Grammar.Par (myLexer, pProgram) import Grammar.Print (printTree) import System.Environment (getArgs) import System.Exit (exitFailure, exitSuccess) +import TypeChecker.TypeChecker (typecheck) main :: IO () main = getArgs >>= \case @@ -16,4 +17,12 @@ main = getArgs >>= \case putStrLn "SYNTAX ERROR" putStrLn err exitFailure - Right prg -> putStrLn "NO SYNTAX ERROR" + Right prg -> case typecheck prg of + Right prg -> do + putStrLn "TYPE CHECK SUCCESSFUL" + putStrLn . show $ prg + Left err -> do + putStrLn "TYPE CHECK ERROR" + putStrLn . show $ err + exitFailure + diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs index c98ad66..9c3ac70 100644 --- a/src/TypeChecker/TypeChecker.hs +++ b/src/TypeChecker/TypeChecker.hs @@ -1,14 +1,18 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase, OverloadedStrings #-} -module TypeChecker.TypeChecker where +module TypeChecker.TypeChecker (typecheck) where + +import Control.Monad (when, void) +import Control.Monad.Except (ExceptT, throwError, runExceptT) -import Control.Monad (when) -import Control.Monad.Except (throwError) import Control.Monad.Reader (ReaderT) import qualified Control.Monad.Reader as R + import Control.Monad.Writer (WriterT) import qualified Control.Monad.Writer as W +import Data.Functor.Identity (Identity, runIdentity) + import Data.Map (Map) import qualified Data.Map as M import Data.Set (Set) @@ -24,66 +28,88 @@ data Ctx = Ctx , sig :: Map Ident Bind , typs :: Set Ident } + deriving Show -type Check a = WriterT String (ReaderT Ctx Err) a +type Check = ReaderT Ctx (ExceptT Error Identity) + +initEnv :: Ctx +initEnv = + Ctx { env = mempty + , sig = mempty + , typs = mempty + } + +run :: Check Type -> Either Error Type +run = runIdentity . runExceptT . flip R.runReaderT initEnv + +typecheck :: Old.Program -> Either Error () +typecheck = runIdentity . runExceptT . flip R.runReaderT initEnv . inferPrg + +inferPrg :: Old.Program -> Check () +inferPrg (Program [x]) = void $ inferBind x + +inferBind :: Old.Bind -> Check () +inferBind (Bind _ _ e) = void $ inferExp e inferExp :: Old.Exp -> Check Type inferExp = \case + + Old.EId i -> undefined + Old.EAnn e t -> do infT <- inferExp e - when (t /= infT) (throwError $ show (AnnotatedMismatch (show e) (show t) (show infT))) + when (t /= infT) (throwError AnnotatedMismatch) return infT + Old.EConst c -> case c of - (CInt i) -> return (TMono $ Old.Ident "Int") - (CStr s) -> return (TMono $ Old.Ident "String") - Old.EId i -> lookupEnv i + (Old.CInt i) -> return (TMono $ UIdent "Int") + (Old.CStr s) -> return (TMono $ UIdent "String") + Old.EAdd e1 e2 -> do t1 <- inferExp e1 t2 <- inferExp e2 case (t1, t2) of - (TMono (Old.Ident "Int"), TMono (Old.Ident "Int")) -> return t1 - _ -> throwError $ show (NotNumber (show t1)) + (TMono (UIdent "Int"), TMono (UIdent "Int")) -> return t1 + _ -> throwError NotNumber return t1 - -- This is wrong currently. (a -> b) should be able to take String Old.EApp e1 e2 -> do inferExp e1 >>= \case - TFun mono@(TMono i) t2 -> do + TArrow mono@(TMono i) t2 -> do t <- inferExp e2 - when (t /= mono) (throwError $ show $ TypeMismatch (show t) (show mono)) - return t + when (t /= mono) (throwError TypeMismatch) + return t2 - -- Not entirely correct. Should sometimes be able to provide mono types where poly expected. - -- i.e id : a -> a; id "string" - TFun poly@(TPoly f) t2 -> do - t <- inferExp e2 - when (t /= poly) (throwError $ show (TypeMismatch (show t) (show poly))) - return t - t -> throwError $ show (NotFunction "Expected a function, but got:" (show t)) + TArrow poly@(TPoly f) t2 -> do + t <- inferExp e2 + when (not $ t `subtype` t) (throwError TypeMismatch) + return t2 - Old.EAbs i e -> undefined +-- This is not entirely correct. The assumed type can change. + Old.EAbs i e -> do + let assume = (TPoly "a") + infT <- R.local (insertEnv i assume) (inferExp e) + return (TArrow assume infT) - Old.ELet b e -> undefined + Old.ELet i e1 e2 -> undefined -- Aux -lookupEnv :: Ident -> Check Type -lookupEnv i = - R.asks env >>= \case - [] -> throwError $ show (UnboundVar "Variable not found" (show i)) - xs -> lookupEnv' i xs - where - lookupEnv' :: Ident -> [Map Ident Type] -> Check Type - lookupEnv' i [] = throwError $ show (UnboundVar "Variable not found" (show i)) - lookupEnv' i (x : xs) = case M.lookup i x of - Just t -> return t - Nothing -> lookupEnv' i xs +subtype :: Type -> Type -> Bool +subtype (TMono t1) (TMono t2) = t1 == t2 +subtype (TMono t1) (TPoly t2) = True +subtype (TPoly t2) (TMono t1) = False +subtype (TArrow t1 t2) (TArrow t3 t4) = t1 `subtype` t3 && t2 `subtype` t4 -lookupSig :: Ident -> Check Bind -lookupSig b = - R.asks sig >>= \m -> case M.lookup b m of - Nothing -> undefined - Just b -> return b +lookupEnv :: Ident -> Ctx -> Maybe Type +lookupEnv i c = case env c of + [] -> Nothing + x : xs -> case M.lookup i x of + Nothing -> lookupEnv i (Ctx { env = xs }) + Just x -> Just x + +lookupSig :: Ident -> Ctx -> Maybe Bind +lookupSig i = M.lookup i . sig insertEnv :: Ident -> Type -> Ctx -> Ctx insertEnv i t c = @@ -92,31 +118,45 @@ insertEnv i t c = (x : xs) -> Ctx{env = M.insert i t x : xs} data Error - = TypeMismatch String String - | NotNumber String - | FunctionTypeMismatch String String String - | NotFunction String String - | UnboundVar String String - | AnnotatedMismatch String String String - | Default String + = TypeMismatch + | NotNumber + | FunctionTypeMismatch + | NotFunction + | UnboundVar + | AnnotatedMismatch + | Default + deriving Show -showErr :: Error -> String -showErr = \case - TypeMismatch expected found -> unwords ["Expected type:", show expected, "but got", show found] - NotNumber mess -> "Expected a number, but got: " <> mess - NotFunction mess func -> mess <> ": " <> func - FunctionTypeMismatch func expected found -> unwords ["Function:", show func, "expected:", show expected, "but got:", show found] - UnboundVar mess var -> mess <> ": " <> var - AnnotatedMismatch expression expected found -> - unwords - [ "Expression" - , expression - , "expected type" - , expected - , "but was inferred as type" - , found - ] - Default mess -> mess +-- showErr :: Error -> String +-- showErr = \case +-- TypeMismatch expected found -> unwords ["Expected type:", show expected, "but got", show found] +-- NotNumber mess -> "Expected a number, but got: " <> mess +-- NotFunction mess func -> mess <> ": " <> func +-- FunctionTypeMismatch func expected found -> unwords ["Function:", show func, "expected:", show expected, "but got:", show found] +-- UnboundVar mess var -> mess <> ": " <> var +-- AnnotatedMismatch expression expected found -> +-- unwords +-- [ "Expression" +-- , expression +-- , "expected type" +-- , expected +-- , "but was inferred as type" +-- , found +-- ] +-- Default mess -> mess -instance Show Error where - show = showErr + +-- Tests + +number :: Old.Exp +number = Old.EConst (CInt 3) + +lambda :: Old.Exp +lambda = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EConst (Old.CInt 3)) (Old.EConst (Old.CInt 3))) + +apply :: Old.Exp +apply = Old.EApp lambda (Old.EConst (Old.CInt 3)) + +{-# WARNING todo "TODO IN CODE" #-} +todo :: a +todo = error "TODO in code" diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs index 3bca405..7fb93fe 100644 --- a/src/TypeChecker/TypeCheckerIr.hs +++ b/src/TypeChecker/TypeCheckerIr.hs @@ -1,16 +1,8 @@ {-# LANGUAGE LambdaCase #-} -module TypeChecker.TypeCheckerIr - ( Program(..) - , Bind(..) - , Ident - , Type(..) - , Const(..) - , Exp(..) - ) - where +module TypeChecker.TypeCheckerIr (module Grammar.Abs, Exp) where -import Grammar.Abs (Program(..), Bind(..), Ident, Type(..), Const(..)) +import Grammar.Abs (Program(..), Ident(..), Bind(..), Const(..), Type(..), UIdent(..), LIdent(..)) data Exp = EAnn Exp Type diff --git a/test_program b/test_program index 4a7b634..14077bd 100644 --- a/test_program +++ b/test_program @@ -1 +1 @@ -main = \x. x + (3 : Int) +test y = y