diff options
Diffstat (limited to 'typecheck/CC/Typecheck.hs')
-rw-r--r-- | typecheck/CC/Typecheck.hs | 182 |
1 files changed, 115 insertions, 67 deletions
diff --git a/typecheck/CC/Typecheck.hs b/typecheck/CC/Typecheck.hs index f61103e..824a714 100644 --- a/typecheck/CC/Typecheck.hs +++ b/typecheck/CC/Typecheck.hs @@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeSynonymInstances #-} module CC.Typecheck(runPass) where @@ -10,59 +11,47 @@ import Data.Maybe import qualified Data.Set as Set import Data.Set (Set) +import Debug.Trace + import qualified CC.AST.Source as S import qualified CC.AST.Typed as T import CC.Context -import CC.Pretty import CC.Types +import CC.Typecheck.Typedefs +import CC.Typecheck.Types -- Inspiration: https://github.com/kritzcreek/fby19 -data TCError = TypeError SourceRange T.Type T.Type - | RefError SourceRange Name +data Env = + Env (Map Name T.TypeScheme) -- Definitions in scope + (Map Name T.TypeDef) -- Type definitions + (Map Name S.AliasDef) -- Type aliases deriving (Show) -instance Pretty TCError where - pretty (TypeError sr real expect) = - "Type error: Expression at " ++ pretty sr ++ - " has type " ++ pretty real ++ - ", but should have type " ++ pretty expect - pretty (RefError sr name) = - "Reference error: Variable '" ++ name ++ "' out of scope at " ++ pretty sr - -type TM a = ExceptT TCError (State Int) a - -genId :: TM Int -genId = state (\idval -> (idval, idval + 1)) - -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 T.TypeScheme) - newtype Subst = Subst (Map Int T.Type) class FreeTypeVars a where - freeTypeVars :: a -> Set Int + -- Free instantiable type variables + freeInstTypeVars :: a -> Set Int 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 + freeInstTypeVars (T.TFun t1 t2) = freeInstTypeVars t1 <> freeInstTypeVars t2 + freeInstTypeVars T.TInt = mempty + freeInstTypeVars (T.TTup ts) = Set.unions (map freeInstTypeVars ts) + freeInstTypeVars (T.TNamed _ ts) = Set.unions (map freeInstTypeVars ts) + freeInstTypeVars (T.TUnion ts) = Set.unions (map freeInstTypeVars (Set.toList ts)) + freeInstTypeVars (T.TyVar T.Instantiable var) = Set.singleton var + freeInstTypeVars (T.TyVar T.Rigid _) = mempty instance FreeTypeVars T.TypeScheme where - freeTypeVars (T.TypeScheme bnds ty) = foldr Set.delete (freeTypeVars ty) bnds + freeInstTypeVars (T.TypeScheme bnds ty) = + foldr Set.delete (freeInstTypeVars ty) bnds instance FreeTypeVars Env where - freeTypeVars (Env mp) = foldMap freeTypeVars (Map.elems mp) + freeInstTypeVars (Env mp _ _) = foldMap freeInstTypeVars (Map.elems mp) infixr >>! @@ -74,14 +63,20 @@ instance Substitute T.Type where 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) + T.TNamed n ts -> T.TNamed n (map (theta >>!) ts) + T.TUnion ts -> T.TUnion (Set.map (theta >>!) ts) + T.TyVar T.Instantiable i -> fromMaybe ty (Map.lookup i mp) + T.TyVar T.Rigid i + | i `Map.member` mp -> error "Attempt to substitute a rigid type variable" + | otherwise -> 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) + theta >>! Env mp tdefs aliases = + Env (Map.map (theta >>!) mp) tdefs aliases -- TODO: make this instance unnecessary instance Substitute T.Expr where @@ -94,6 +89,7 @@ instance Substitute T.Expr where _ >>! 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)) + theta >>! T.Constr ty n = T.Constr (theta >>! ty) n instance Semigroup Subst where @@ -103,20 +99,43 @@ instance Monoid Subst where mempty = Subst mempty emptyEnv :: Env -emptyEnv = Env mempty +emptyEnv = Env mempty mempty mempty + +envAddDef :: Name -> T.TypeScheme -> Env -> Env +envAddDef name sty (Env mp tmp aliases) + | name `Map.member` mp = error "envAddDef on name already in environment" + | otherwise = + Env (Map.insert name sty mp) tmp aliases + +envFindDef :: Name -> Env -> Maybe T.TypeScheme +envFindDef name (Env mp _ _) = Map.lookup name mp + +envAddTypes :: Map Name T.TypeDef -> Env -> Env +envAddTypes l (Env mp tdefs aliases) = + let combined = l <> tdefs + in if Map.size combined == Map.size l + Map.size tdefs + then Env mp combined aliases + else error "envAddTypes on duplicate type names" + +envFindType :: Name -> Env -> Maybe T.TypeDef +envFindType name (Env _ tdefs _) = Map.lookup name tdefs -envAdd :: Name -> T.TypeScheme -> Env -> Env -envAdd name sty (Env mp) = Env (Map.insert name sty mp) +envAddAliases :: Map Name S.AliasDef -> Env -> Env +envAddAliases l (Env mp tdefs aliases) = + let combined = l <> aliases + in if Map.size combined == Map.size l + Map.size aliases + then Env mp tdefs combined + else error "envAddAliaes on duplicate type names" -envFind :: Name -> Env -> Maybe T.TypeScheme -envFind name (Env mp) = Map.lookup name mp +envAliases :: Env -> Map Name S.AliasDef +envAliases (Env _ _ aliases) = aliases substVar :: Int -> T.Type -> Subst substVar var ty = Subst (Map.singleton var ty) generalise :: Env -> T.Type -> T.TypeScheme generalise env ty = - T.TypeScheme (Set.toList (freeTypeVars ty Set.\\ freeTypeVars env)) ty + T.TypeScheme (Set.toList (freeInstTypeVars ty Set.\\ freeInstTypeVars env)) ty instantiate :: T.TypeScheme -> TM T.Type instantiate (T.TypeScheme bnds ty) = do @@ -124,6 +143,9 @@ instantiate (T.TypeScheme bnds ty) = do let theta = Subst (Map.fromList (zip bnds vars)) return (theta >>! ty) +freshenFrees :: Env -> T.Type -> TM T.Type +freshenFrees env = instantiate . generalise env + data UnifyContext = UnifyContext SourceRange T.Type T.Type unify :: SourceRange -> T.Type -> T.Type -> TM Subst @@ -131,25 +153,22 @@ unify sr t1 t2 = unify' (UnifyContext sr t1 t2) t1 t2 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.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' _ (T.TyVar var) ty = return (substVar var ty) -unify' _ ty (T.TyVar var) = return (substVar var ty) +unify' _ (T.TyVar T.Instantiable var) ty = return (substVar var ty) +unify' _ ty (T.TyVar T.Instantiable var) = return (substVar var ty) +-- TODO: fix unify unify' (UnifyContext sr t1 t2) _ _ = throwError (TypeError sr t1 t2) -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 -> S.Expr -> TM (Subst, T.Expr) infer env expr = case expr of 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 (T.TypeScheme [] argVar) env + let augEnv = envAddDef arg (T.TypeScheme [] argVar) env (theta, body') <- infer augEnv body let argType = theta >>! argVar return (theta, T.Lam (T.TFun argType (T.exprType body')) @@ -157,7 +176,7 @@ infer env expr = case expr of S.Let _ (name, _) rhs body -> do (theta1, rhs') <- infer env rhs let varType = T.exprType rhs' - let augEnv = envAdd name (T.TypeScheme [] varType) env + let augEnv = envAddDef name (T.TypeScheme [] varType) env (theta2, body') <- infer augEnv body return (theta2 <> theta1, T.Let (T.Occ name varType) rhs' body') S.Call sr func arg -> do @@ -173,14 +192,22 @@ infer env expr = case expr of 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 + | Just sty <- envFindDef name env -> do ty <- instantiate sty return (mempty, T.Var (T.Occ name ty)) | otherwise -> throwError (RefError sr name) + S.Constr sr name -> case envFindType name env of + Just (T.TypeDef typname params typ) -> do + restyp <- freshenFrees emptyEnv + (T.TNamed typname (map (T.TyVar T.Instantiable) params)) + return (mempty, T.Constr (T.TFun typ restyp) name) + _ -> + throwError (RefError sr name) S.Annot sr subex ty -> do (theta1, subex') <- infer env subex - theta2 <- unify sr (T.exprType subex') (convertType ty) + ty' <- convertType (envAliases env) sr ty + theta2 <- unify sr (T.exprType subex') ty' return (theta2 <> theta1, theta2 >>! subex') -- TODO: quadratic complexity inferList :: Env -> [S.Expr] -> TM (Subst, [T.Expr]) @@ -192,23 +219,44 @@ inferList env (expr : exprs) = do runPass :: Context -> S.Program -> Either TCError T.Program -runPass (Context _ (Builtins builtins)) prog = - let env = Env (Map.map (generalise emptyEnv) builtins) +runPass (Context _ (Builtins builtins _)) prog = + let env = Env (Map.map (generalise emptyEnv) builtins) mempty mempty in runTM (typeCheck env prog) typeCheck :: Env -> S.Program -> TM T.Program -typeCheck startEnv (S.Program decls) = - let defs = [(name, ty) - | S.Def (S.Function (Just ty) (name, _) _ _) <- decls] - env = foldl (\env' (name, ty) -> envAdd name (generalise env' (convertType ty)) env') - startEnv defs - 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 +typeCheck startEnv (S.Program decls) = do + traceM (show decls) + + let aliasdefs = [(n, def) + | S.DeclAlias def@(S.AliasDef (n, _) _ _) <- decls] + env1 = envAddAliases (Map.fromList aliasdefs) startEnv + + typedefs' <- checkTypedefs (envAliases env1) [def | S.DeclType def <- decls] + let typedefsMap = Map.fromList [(n, def) | def@(T.TypeDef n _ _) <- typedefs'] + + let funcdefs = [def | S.DeclFunc def <- decls] + typedfuncs <- sequence + [(name,) <$> convertType (envAliases env1) sr ty + | S.FuncDef (Just ty) (name, sr) _ _ <- funcdefs] + + let env2 = envAddTypes typedefsMap env1 + + traceM (show typedefsMap) + + let env = foldl (\env' (name, ty) -> + envAddDef name (generalise env' ty) env') + env2 typedfuncs + + traceM (show env) + + funcdefs' <- mapM (typeCheckFunc env) funcdefs + return (T.Program funcdefs' typedefsMap) + +typeCheckFunc :: Env -> S.FuncDef -> TM T.Def +typeCheckFunc env (S.FuncDef mannot (name, sr) args@(_:_) body) = + typeCheckFunc env (S.FuncDef mannot (name, sr) [] (S.Lam sr args body)) +typeCheckFunc env (S.FuncDef (Just annot) (name, sr) [] body) = + typeCheckFunc env (S.FuncDef Nothing (name, sr) [] (S.Annot sr body annot)) +typeCheckFunc env (S.FuncDef Nothing (name, _) [] body) = do (_, body') <- infer env body return (T.Def name body') |