From 5d247057f56fc2ecd18323f863d59e92f34924c2 Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Tue, 14 Feb 2023 22:03:56 +0100 Subject: [PATCH] Minor rewrite of tc. Some bugs still left --- Grammar.cf | 5 +- src/Main.hs | 21 ++- src/Renamer/RenamerIr.hs | 9 +- src/TypeChecker/TypeChecker.hs | 263 ++++++++++++++++++------------- src/TypeChecker/TypeCheckerIr.hs | 81 +++++++++- test_program | 5 +- 6 files changed, 256 insertions(+), 128 deletions(-) diff --git a/Grammar.cf b/Grammar.cf index 21b563b..234b2f0 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -3,7 +3,7 @@ Program. Program ::= [Bind] ; Bind. Bind ::= Ident [Ident] "=" Exp ; -EAnn. Exp5 ::= Exp5 ":" Type ; +EAnn. Exp5 ::= "(" Exp ":" Type ")" ; EId. Exp4 ::= Ident ; EConst. Exp4 ::= Const ; EApp. Exp3 ::= Exp3 Exp4 ; @@ -16,8 +16,9 @@ CStr. Const ::= String ; TMono. Type ::= "Mono" Ident ; TPoly. Type ::= "Poly" Ident ; -TArrow. Type ::= Type "->" Type1 ; +TArrow. Type ::= Type1 "->" Type ; +-- This doesn't seem to work so we'll have to live with ugly keywords for now -- token Upper (upper (letter | digit | '_')*) ; -- token Lower (lower (letter | digit | '_')*) ; diff --git a/src/Main.hs b/src/Main.hs index 93b3edd..647ac9d 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -5,8 +5,9 @@ import Grammar.Par (myLexer, pProgram) import Grammar.Print (printTree) import System.Environment (getArgs) import System.Exit (exitFailure, exitSuccess) -import TypeChecker.TypeChecker (typecheck) -import Renamer.Renamer (rename) +import TypeChecker.TypeChecker (typecheck) +import Renamer.Renamer (rename) +import Grammar.Print (prt) main :: IO () main = getArgs >>= \case @@ -19,10 +20,14 @@ main = getArgs >>= \case putStrLn err exitFailure Right prg -> case rename prg of - Right prg -> do - putStrLn "RENAME SUCCESSFUL" - putStrLn $ printTree prg Left err -> do - putStrLn "FAILED RENAMING" - putStrLn . show $ err - exitFailure + putStrLn "FAILED RENAMING" + putStrLn . show $ err + exitFailure + Right prg -> case typecheck prg of + Left err -> do + putStrLn "TYPECHECK ERROR" + putStrLn . show $ err + exitFailure + Right prg -> do + putStrLn . printTree $ prg diff --git a/src/Renamer/RenamerIr.hs b/src/Renamer/RenamerIr.hs index 882129c..ea6f477 100644 --- a/src/Renamer/RenamerIr.hs +++ b/src/Renamer/RenamerIr.hs @@ -1,6 +1,12 @@ {-# LANGUAGE LambdaCase #-} -module Renamer.RenamerIr (module Grammar.Abs, RExp (..), RBind (..), RProgram (..)) where +module Renamer.RenamerIr ( RExp (..) + , RBind (..) + , RProgram (..) + , Const (..) + , Ident (..) + , Type (..) + ) where import Grammar.Abs ( Bind (..), @@ -43,6 +49,7 @@ instance Print RBind where instance Print RExp where prt i = \case + RAnn e t -> prPrec i 2 (concatD [prt 0 e, doc (showString ":"), prt 1 t]) RBound n _ -> prPrec i 3 (concatD [prt 0 ("var" ++ show n)]) RFree id -> prPrec i 3 (concatD [prt 0 id]) RConst n -> prPrec i 3 (concatD [prt 0 n]) diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs index ed59298..acb3132 100644 --- a/src/TypeChecker/TypeChecker.hs +++ b/src/TypeChecker/TypeChecker.hs @@ -1,6 +1,6 @@ {-# LANGUAGE LambdaCase, OverloadedStrings, OverloadedRecordDot #-} -module TypeChecker.TypeChecker (typecheck) where +module TypeChecker.TypeChecker where import Control.Monad (when, void) import Control.Monad.Except (ExceptT, throwError, runExceptT) @@ -13,15 +13,11 @@ import qualified Control.Monad.State as St import Data.Functor.Identity (Identity, runIdentity) import Data.Map (Map) import qualified Data.Map as M -import Data.Set (Set) -import qualified Data.Set as S -import Data.Bool (bool) -import qualified Grammar.Abs as Old import Grammar.ErrM (Err) import TypeChecker.TypeCheckerIr -data Ctx = Ctx { env :: Map Ident Type +data Ctx = Ctx { vars :: Map Integer Type , sigs :: Map Ident Type } deriving Show @@ -34,121 +30,165 @@ programmer. -} -type Check = StateT (Map Ident Type) (ReaderT Ctx (ExceptT Error Identity)) +type Infer = StateT Ctx (ExceptT Error Identity) initEnv :: Ctx -initEnv = - Ctx { env = mempty - , sigs = mempty - } +initEnv = Ctx mempty mempty -run :: Check Type -> Either Error Type -run = runIdentity . runExceptT . flip R.runReaderT initEnv . flip St.evalStateT mempty +run :: Infer a -> Either Error a +run = runIdentity . runExceptT . flip St.evalStateT initEnv -typecheck :: Old.Program -> Either Error () -typecheck = todo +typecheck :: RProgram -> Either Error TProgram +typecheck = run . inferPrg -inferPrg :: Old.Program -> Check () -inferPrg (Program [x]) = void $ inferBind x +inferPrg :: RProgram -> Infer TProgram +inferPrg (RProgram xs) = do + xs' <- mapM inferBind xs + return $ TProgram xs' -inferBind :: Old.Bind -> Check () -inferBind (Bind _ _ e) = void $ inferExp e +inferBind :: RBind -> Infer TBind +inferBind (RBind name e) = do + t <- inferExp e + e' <- toTExpr e + return $ TBind name t e' -inferExp :: Old.Exp -> Check Type +toTExpr :: RExp -> Infer TExp +toTExpr = \case + + re@(RAnn e t) -> do + t <- inferExp re + e' <- toTExpr e + return $ TAnn e' t + + re@(RBound num name) -> do + t <- inferExp re + return $ TBound num name t + + re@(RFree name) -> do + t <- inferExp re + return $ TFree name t + + re@(RConst con)-> do + t <- inferExp re + return $ TConst con t + + re@(RApp e1 e2) -> do + t <- inferExp re + e1' <- toTExpr e1 + e2' <- toTExpr e2 + return $ TApp e1' e2' t + + re@(RAdd e1 e2)-> do + t <- inferExp re + e1' <- toTExpr e1 + e2' <- toTExpr e2 + return $ TAdd e1' e2' t + + re@(RAbs num name e) -> do + t <- inferExp re + e' <- toTExpr e + return $ TAbs num name e' t + + +inferExp :: RExp -> Infer Type inferExp = \case - -- TODO: Fix bound variable lookup - Old.EId i -> do - st <- St.get - case lookupBound i st of - Just t -> return t - Nothing -> do - ctx <- R.ask - case lookupEnv i ctx of - Just t -> return t - Nothing -> case lookupSigs i ctx of - Just t -> return t - Nothing -> throwError UnboundVar - - Old.EAnn e t -> do - infT <- inferExp e - when (t /= infT) (throwError AnnotatedMismatch) - return infT + RAnn expr typ -> do + exprT <- inferExp expr + when (not (exprT == typ || isPoly exprT)) (throwError AnnotatedMismatch) + return typ - Old.EConst c -> case c of - (Old.CInt i) -> return (TMono "Int") - (Old.CStr s) -> return (TMono "String") + -- Name is only here for proper error messages + RBound num name -> + M.lookup num <$> St.gets vars >>= \case + Nothing -> throwError UnboundVar + Just t -> return t - Old.EAdd e1 e2 -> do - let int = TMono "Int" - updateBound e1 int - updateBound e2 int - inf1 <- inferExp e1 - inf2 <- inferExp e2 - when (not $ isInt inf1 && isInt inf2) (throwError TypeMismatch) - return int + RFree name -> do + M.lookup name <$> St.gets sigs >>= \case + Nothing -> throwError UnboundVar + Just t -> return t - -- Incomplete and probably wrong - Old.EApp e1 e2 -> do - inferExp e1 >>= \case - TArrow mono@(TMono i) t2 -> do - t <- inferExp e2 - when (t /= mono) (throwError TypeMismatch) - return t2 + RConst (CInt _) -> return $ TMono "Int" + RConst (CStr _) -> return $ TMono "Str" - TArrow poly@(TPoly f) t2 -> do - t <- inferExp e2 - when (not $ t `subtype` t) (throwError TypeMismatch) - return t2 + -- Currently does not accept using a polymorphic type as the function. + RApp expr1 expr2 -> do + typ1 <- inferExp expr1 + typ2 <- inferExp expr2 + fit typ2 typ1 - -- This is not entirely correct. The assumed type can change. - Old.EAbs i e -> do - let assume = (TPoly "a") - St.modify (M.insert i assume) - infT <- R.local (insertEnv i assume) (inferExp e) - St.gets (M.lookup i) >>= \case - Nothing -> todo - Just x -> return (TArrow x infT) + RAdd expr1 expr2 -> do + typ1 <- inferExp expr1 + typ2 <- inferExp expr2 + when (not $ (isInt typ1 || isPoly typ1) && (isInt typ2 || isPoly typ2)) (throwError TypeMismatch) + specifyType expr1 (TMono "Int") + specifyType expr2 (TMono "Int") + return (TMono "Int") - Old.ELet i e1 e2 -> todo + RAbs num name expr -> do + insertVars num (TPoly "a") + typ <- inferExp expr + newTyp <- lookupVars num + return $ TArrow newTyp typ -- Aux - --- Double check this function. It's bad and maybe wrong -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 -subtype _ _ = False - -lookupEnv :: Ident -> Ctx -> Maybe Type -lookupEnv i = M.lookup i . env - -lookupSigs :: Ident -> Ctx -> Maybe Type -lookupSigs i = M.lookup i . sigs - -insertEnv :: Ident -> Type -> Ctx -> Ctx -insertEnv i t c = Ctx { env = M.insert i t c.env - , sigs = c.sigs - } - -updateBound :: Old.Exp -> Type -> Check () -updateBound (Old.EId i) t = St.modify (M.insert i t) -updateBound _ _ = return () - -isBound :: Old.Exp -> Check Bool -isBound (Old.EId i) = (M.member i) <$> St.get -isBound _ = return False - -lookupBound :: Ident -> Map Ident Type -> Maybe Type -lookupBound = M.lookup - isInt :: Type -> Bool isInt (TMono "Int") = True -isInt (TPoly _) = True isInt _ = False +isArrow :: Type -> Bool +isArrow (TArrow _ _) = True +isArrow _ = False + +isPoly :: Type -> Bool +isPoly (TPoly _) = True +isPoly _ = False + +fit :: Type -> Type -> Infer Type +fit (TArrow t1 (TArrow t2 t3)) t4 + | t1 == t4 = return $ TArrow t2 t3 + | otherwise = fit (TArrow (TArrow t1 t2) t3) t4 +fit (TArrow t1 t2) t3 + | t1 == t3 = return t2 + | otherwise = throwError TypeMismatch +fit _ _ = throwError TypeMismatch + +-- a -> (b -> (c -> d)) +-- a -> b + +-- | Specify the type of a bound variable +-- Because in lambdas we have to assume a general type and update it +specifyType :: RExp -> Type -> Infer () +specifyType (RBound num name) typ = do + insertVars num typ + return () +specifyType _ _ = return () + +lookupVars :: Integer -> Infer Type +lookupVars i = do + st <- St.gets vars + case M.lookup i st of + Just t -> return t + Nothing -> throwError UnboundVar + +lookupSigs :: Ident -> Infer Type +lookupSigs i = do + st <- St.gets sigs + case M.lookup i st of + Just t -> return t + Nothing -> throwError UnboundVar + + +insertVars :: Integer -> Type -> Infer () +insertVars i t = do + st <- St.get + St.put ( Ctx { vars = M.insert i t st.vars, sigs = st.sigs } ) + +{-# WARNING todo "TODO IN CODE" #-} +todo :: a +todo = error "TODO in code" + data Error = TypeMismatch | NotNumber @@ -161,18 +201,17 @@ data Error -- Tests -number :: Old.Exp -number = Old.EConst (CInt 3) +lambda = RAbs 0 "x" (RAdd (RBound 0 "x") (RBound 0 "x")) +lambda2 = RAbs 0 "x" (RAnn (RBound 0 "x") (TArrow (TMono "Int") (TMono "String"))) -aToInt :: Old.Exp -aToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EConst (Old.CInt 3)) (Old.EConst (Old.CInt 3))) +pp :: Type -> String +pp (TMono (Ident x)) = x +pp (TPoly (Ident x)) = x +pp (TArrow t1 t2) = pp t1 <> " -> " <> pp t2 -intToInt :: Old.Exp -intToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EId $ Ident "x") (Old.EConst (Old.CInt 3))) +int,str :: Type +int = TMono "Int" +str = TMono "Str" -addLambda :: Old.Exp -addLambda = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EId $ Ident "x") (Old.EId $ Ident "x")) - -{-# WARNING todo "TODO IN CODE" #-} -todo :: a -todo = error "TODO in code" +arrow :: Type -> Type -> Type +arrow = TArrow diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs index 95e4108..d1aa706 100644 --- a/src/TypeChecker/TypeCheckerIr.hs +++ b/src/TypeChecker/TypeCheckerIr.hs @@ -1,12 +1,25 @@ {-# LANGUAGE LambdaCase #-} -module TypeChecker.TypeCheckerIr where +module TypeChecker.TypeCheckerIr ( TProgram(..) + , TBind(..) + , TExp(..) + , RProgram(..) + , RBind(..) + , RExp(..) + , Type(..) + , Const(..) + , Ident(..) + ) + where import Renamer.RenamerIr +import Grammar.Print data TProgram = TProgram [TBind] + deriving (Eq, Show, Read, Ord) data TBind = TBind Ident Type TExp + deriving (Eq, Show, Read, Ord) data TExp = TAnn TExp Type @@ -17,3 +30,69 @@ data TExp | TAdd TExp TExp Type | TAbs Integer Ident TExp Type deriving (Eq, Ord, Show, Read) + +instance Print TProgram where + prt i = \case + TProgram defs -> prPrec i 0 (concatD [prt 0 defs]) + +instance Print TBind where + prt i = \case + TBind x t e -> + prPrec i 0 $ + concatD + [ prt 0 x + , doc (showString ":") + , prt 0 t + , doc (showString "=") + , prt 0 e + ] + +instance Print TExp where + prt i = \case + TAnn e t -> prPrec i 2 $ concatD + [ prt 0 e + , doc (showString ":") + , prt 1 t + ] + TBound _ u t -> prPrec i 3 $ concatD + [ doc (showString "(") + , prt 0 u + , doc (showString ":") + , prt 0 t + , doc (showString ")") + ] + TFree u t -> prPrec i 3 $ concatD + [ doc (showString "(") + , prt 0 u + , doc (showString ":") + , prt 0 t + , doc (showString ")") + ] + TConst c _ -> prPrec i 3 (concatD [prt 0 c]) + TApp e e1 t -> prPrec i 2 $ concatD + [ doc (showString "(") + , prt 2 e + , prt 3 e1 + , doc (showString ")") + , doc (showString ":") + , prt 0 t + ] + TAdd e e1 t -> prPrec i 1 $ concatD + [ doc (showString "(") + , prt 1 e + , doc (showString "+") + , prt 2 e1 + , doc (showString ")") + , doc (showString ":") + , prt 0 t + ] + TAbs _ u e t -> prPrec i 0 $ concatD + [ doc (showString "(") + , doc (showString "\\") + , prt 0 u + , doc (showString ".") + , prt 0 e + , doc (showString ")") + , doc (showString ":") + , prt 0 t, doc (showString ".") + ] diff --git a/test_program b/test_program index 3fcfcea..e297617 100644 --- a/test_program +++ b/test_program @@ -1,4 +1 @@ -letters = let x = 1 - in let y = 2 - in let z = 3 - in x + y + z +testType f x = f x