aboutsummaryrefslogtreecommitdiff
path: root/typecheck/CC/Typecheck.hs
diff options
context:
space:
mode:
Diffstat (limited to 'typecheck/CC/Typecheck.hs')
-rw-r--r--typecheck/CC/Typecheck.hs159
1 files changed, 81 insertions, 78 deletions
diff --git a/typecheck/CC/Typecheck.hs b/typecheck/CC/Typecheck.hs
index bf1d17c..8678771 100644
--- a/typecheck/CC/Typecheck.hs
+++ b/typecheck/CC/Typecheck.hs
@@ -10,16 +10,17 @@ import Data.Maybe
import qualified Data.Set as Set
import Data.Set (Set)
-import CC.AST.Source
-import CC.AST.Typed
+import qualified CC.AST.Source as S
+import qualified CC.AST.Typed as T
import CC.Context
import CC.Pretty
+import CC.Types
-- Inspiration: https://github.com/kritzcreek/fby19
-data TCError = TypeError SourceRange TypeT TypeT
+data TCError = TypeError SourceRange T.Type T.Type
| RefError SourceRange Name
deriving (Show)
@@ -36,29 +37,29 @@ type TM a = ExceptT TCError (State Int) a
genId :: TM Int
genId = state (\idval -> (idval, idval + 1))
-genTyVar :: TM TypeT
-genTyVar = TyVar <$> genId
+genTyVar :: TM T.Type
+genTyVar = T.TyVar <$> genId
runTM :: TM a -> Either TCError a
runTM m = evalState (runExceptT m) 1
-newtype Env = Env (Map Name TypeSchemeT)
+newtype Env = Env (Map Name T.TypeScheme)
-newtype Subst = Subst (Map Int TypeT)
+newtype Subst = Subst (Map Int T.Type)
class FreeTypeVars a where
freeTypeVars :: a -> Set Int
-instance FreeTypeVars TypeT where
- freeTypeVars (TFunT t1 t2) = freeTypeVars t1 <> freeTypeVars t2
- freeTypeVars TIntT = mempty
- freeTypeVars (TTupT ts) = Set.unions (map freeTypeVars ts)
- freeTypeVars (TyVar var) = Set.singleton var
+instance FreeTypeVars T.Type where
+ freeTypeVars (T.TFun t1 t2) = freeTypeVars t1 <> freeTypeVars t2
+ freeTypeVars T.TInt = mempty
+ freeTypeVars (T.TTup ts) = Set.unions (map freeTypeVars ts)
+ freeTypeVars (T.TyVar var) = Set.singleton var
-instance FreeTypeVars TypeSchemeT where
- freeTypeVars (TypeSchemeT bnds ty) = foldr Set.delete (freeTypeVars ty) bnds
+instance FreeTypeVars T.TypeScheme where
+ freeTypeVars (T.TypeScheme bnds ty) = foldr Set.delete (freeTypeVars ty) bnds
instance FreeTypeVars Env where
freeTypeVars (Env mp) = foldMap freeTypeVars (Map.elems mp)
@@ -68,29 +69,29 @@ infixr >>!
class Substitute a where
(>>!) :: Subst -> a -> a
-instance Substitute TypeT where
+instance Substitute T.Type where
theta@(Subst mp) >>! ty = case ty of
- TFunT t1 t2 -> TFunT (theta >>! t1) (theta >>! t2)
- TIntT -> TIntT
- TTupT ts -> TTupT (map (theta >>!) ts)
- TyVar i -> fromMaybe ty (Map.lookup i mp)
+ T.TFun t1 t2 -> T.TFun (theta >>! t1) (theta >>! t2)
+ T.TInt -> T.TInt
+ T.TTup ts -> T.TTup (map (theta >>!) ts)
+ T.TyVar i -> fromMaybe ty (Map.lookup i mp)
-instance Substitute TypeSchemeT where
- Subst mp >>! TypeSchemeT bnds ty =
- TypeSchemeT bnds (Subst (foldr Map.delete mp bnds) >>! ty)
+instance Substitute T.TypeScheme where
+ Subst mp >>! T.TypeScheme bnds ty =
+ T.TypeScheme bnds (Subst (foldr Map.delete mp bnds) >>! ty)
instance Substitute Env where
theta >>! Env mp = Env (Map.map (theta >>!) mp)
-- TODO: make this instance unnecessary
-instance Substitute ExprT where
- theta >>! LamT ty (Occ name ty2) body =
- LamT (theta >>! ty) (Occ name (theta >>! ty2)) (theta >>! body)
- theta >>! CallT ty e1 e2 =
- CallT (theta >>! ty) (theta >>! e1) (theta >>! e2)
- _ >>! expr@(IntT _) = expr
- theta >>! TupT es = TupT (map (theta >>!) es)
- theta >>! VarT (Occ name ty) = VarT (Occ name (theta >>! ty))
+instance Substitute T.Expr where
+ theta >>! T.Lam ty (T.Occ name ty2) body =
+ T.Lam (theta >>! ty) (T.Occ name (theta >>! ty2)) (theta >>! body)
+ theta >>! T.Call ty e1 e2 =
+ T.Call (theta >>! ty) (theta >>! e1) (theta >>! e2)
+ _ >>! expr@(T.Int _) = expr
+ theta >>! T.Tup es = T.Tup (map (theta >>!) es)
+ theta >>! T.Var (T.Occ name ty) = T.Var (T.Occ name (theta >>! ty))
instance Semigroup Subst where
@@ -102,77 +103,79 @@ instance Monoid Subst where
emptyEnv :: Env
emptyEnv = Env mempty
-envAdd :: Name -> TypeSchemeT -> Env -> Env
+envAdd :: Name -> T.TypeScheme -> Env -> Env
envAdd name sty (Env mp) = Env (Map.insert name sty mp)
-envFind :: Name -> Env -> Maybe TypeSchemeT
+envFind :: Name -> Env -> Maybe T.TypeScheme
envFind name (Env mp) = Map.lookup name mp
-substVar :: Int -> TypeT -> Subst
+substVar :: Int -> T.Type -> Subst
substVar var ty = Subst (Map.singleton var ty)
-generalise :: Env -> TypeT -> TypeSchemeT
+generalise :: Env -> T.Type -> T.TypeScheme
generalise env ty =
- TypeSchemeT (Set.toList (freeTypeVars ty Set.\\ freeTypeVars env)) ty
+ T.TypeScheme (Set.toList (freeTypeVars ty Set.\\ freeTypeVars env)) ty
-instantiate :: TypeSchemeT -> TM TypeT
-instantiate (TypeSchemeT bnds ty) = do
+instantiate :: T.TypeScheme -> TM T.Type
+instantiate (T.TypeScheme bnds ty) = do
vars <- traverse (const genTyVar) bnds
let theta = Subst (Map.fromList (zip bnds vars))
return (theta >>! ty)
-data UnifyContext = UnifyContext SourceRange TypeT TypeT
+data UnifyContext = UnifyContext SourceRange T.Type T.Type
-unify :: SourceRange -> TypeT -> TypeT -> TM Subst
+unify :: SourceRange -> T.Type -> T.Type -> TM Subst
unify sr t1 t2 = unify' (UnifyContext sr t1 t2) t1 t2
-unify' :: UnifyContext -> TypeT -> TypeT -> TM Subst
-unify' _ TIntT TIntT = return mempty
-unify' ctx (TFunT t1 t2) (TFunT u1 u2) = (<>) <$> unify' ctx t1 u1 <*> unify' ctx t2 u2
-unify' ctx (TTupT ts) (TTupT us)
+unify' :: UnifyContext -> T.Type -> T.Type -> TM Subst
+unify' _ T.TInt T.TInt = return mempty
+unify' ctx (T.TFun t1 t2) (T.TFun u1 u2) = (<>) <$> unify' ctx t1 u1 <*> unify' ctx t2 u2
+unify' ctx (T.TTup ts) (T.TTup us)
| length ts == length us = mconcat <$> zipWithM (unify' ctx) ts us
-unify' _ (TyVar var) ty = return (substVar var ty)
-unify' _ ty (TyVar var) = return (substVar var ty)
+unify' _ (T.TyVar var) ty = return (substVar var ty)
+unify' _ ty (T.TyVar var) = return (substVar var ty)
unify' (UnifyContext sr t1 t2) _ _ = throwError (TypeError sr t1 t2)
-convertType :: Type -> TypeT
-convertType (TFun t1 t2) = TFunT (convertType t1) (convertType t2)
-convertType TInt = TIntT
-convertType (TTup ts) = TTupT (map convertType ts)
+convertType :: S.Type -> T.Type
+convertType (S.TFun t1 t2) = T.TFun (convertType t1) (convertType t2)
+convertType S.TInt = T.TInt
+convertType (S.TTup ts) = T.TTup (map convertType ts)
-infer :: Env -> Expr -> TM (Subst, ExprT)
+infer :: Env -> S.Expr -> TM (Subst, T.Expr)
infer env expr = case expr of
- Lam _ [] body -> infer env body
- Lam sr args@(_:_:_) body -> infer env (foldr (Lam sr . pure) body args)
- Lam _ [(arg, _)] body -> do
+ S.Lam _ [] body -> infer env body
+ S.Lam sr args@(_:_:_) body -> infer env (foldr (S.Lam sr . pure) body args)
+ S.Lam _ [(arg, _)] body -> do
argVar <- genTyVar
- let augEnv = envAdd arg (TypeSchemeT [] argVar) env
+ let augEnv = envAdd arg (T.TypeScheme [] argVar) env
(theta, body') <- infer augEnv body
let argType = theta >>! argVar
- return (theta, LamT (TFunT argType (exprType body')) (Occ arg argType) body')
- Call sr func arg -> do
+ return (theta, T.Lam (T.TFun argType (T.exprType body'))
+ (T.Occ arg argType) body')
+ S.Call sr func arg -> do
(theta1, func') <- infer env func
(theta2, arg') <- infer (theta1 >>! env) arg
resVar <- genTyVar
- theta3 <- unify sr (theta2 >>! exprType func') (TFunT (exprType arg') resVar)
+ theta3 <- unify sr (theta2 >>! T.exprType func')
+ (T.TFun (T.exprType arg') resVar)
return (theta3 <> theta2 <> theta1
- ,CallT (theta3 >>! resVar)
+ ,T.Call (theta3 >>! resVar)
((theta3 <> theta2) >>! func') -- TODO: quadratic complexity
(theta3 >>! arg')) -- TODO: quadratic complexity
- Int _ val -> return (mempty, IntT val)
- Tup _ es -> fmap TupT <$> inferList env es
- Var sr name
+ S.Int _ val -> return (mempty, T.Int val)
+ S.Tup _ es -> fmap T.Tup <$> inferList env es
+ S.Var sr name
| Just sty <- envFind name env -> do
ty <- instantiate sty
- return (mempty, VarT (Occ name ty))
+ return (mempty, T.Var (T.Occ name ty))
| otherwise ->
throwError (RefError sr name)
- Annot sr subex ty -> do
+ S.Annot sr subex ty -> do
(theta1, subex') <- infer env subex
- theta2 <- unify sr (exprType subex') (convertType ty)
+ theta2 <- unify sr (T.exprType subex') (convertType ty)
return (theta2 <> theta1, theta2 >>! subex') -- TODO: quadratic complexity
-inferList :: Env -> [Expr] -> TM (Subst, [ExprT])
+inferList :: Env -> [S.Expr] -> TM (Subst, [T.Expr])
inferList _ [] = return (mempty, [])
inferList env (expr : exprs) = do
(theta, expr') <- infer env expr
@@ -180,24 +183,24 @@ inferList env (expr : exprs) = do
return (theta <> theta', expr' : res)
-runPass :: Context -> Program -> Either TCError ProgramT
+runPass :: Context -> S.Program -> Either TCError T.Program
runPass (Context _ (Builtins builtins)) prog =
let env = Env (Map.fromList [(name, generalise emptyEnv ty) | (name, ty) <- builtins])
in runTM (typeCheck env prog)
-typeCheck :: Env -> Program -> TM ProgramT
-typeCheck startEnv (Program decls) =
+typeCheck :: Env -> S.Program -> TM T.Program
+typeCheck startEnv (S.Program decls) =
let defs = [(name, ty)
- | Def (Function (Just ty) (name, _) _ _) <- decls]
+ | S.Def (S.Function (Just ty) (name, _) _ _) <- decls]
env = foldl (\env' (name, ty) -> envAdd name (generalise env' (convertType ty)) env')
startEnv defs
- in ProgramT <$> mapM (typeCheckDef env . (\(Def def) -> def)) decls
-
-typeCheckDef :: Env -> Def -> TM DefT
-typeCheckDef env (Function mannot (name, sr) args@(_:_) body) =
- typeCheckDef env (Function mannot (name, sr) [] (Lam sr args body))
-typeCheckDef env (Function (Just annot) (name, sr) [] body) =
- typeCheckDef env (Function Nothing (name, sr) [] (Annot sr body annot))
-typeCheckDef env (Function Nothing (name, _) [] body) = do
+ in T.Program <$> mapM (typeCheckDef env . (\(S.Def def) -> def)) decls
+
+typeCheckDef :: Env -> S.Def -> TM T.Def
+typeCheckDef env (S.Function mannot (name, sr) args@(_:_) body) =
+ typeCheckDef env (S.Function mannot (name, sr) [] (S.Lam sr args body))
+typeCheckDef env (S.Function (Just annot) (name, sr) [] body) =
+ typeCheckDef env (S.Function Nothing (name, sr) [] (S.Annot sr body annot))
+typeCheckDef env (S.Function Nothing (name, _) [] body) = do
(_, body') <- infer env body
- return (DefT name body')
+ return (T.Def name body')
generated by cgit v1.2.3 (git 2.25.1) at 2024-05-03 15:38:56 +0200