From e094e3294e9c93fd1123b008a4b0e5f53915f5be Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Thu, 29 Feb 2024 21:13:14 +0100 Subject: Destroy fancy typing, and some work --- src/HSVIS/Typecheck.hs | 235 ++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 186 insertions(+), 49 deletions(-) (limited to 'src/HSVIS/Typecheck.hs') diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs index 23fb961..2b05793 100644 --- a/src/HSVIS/Typecheck.hs +++ b/src/HSVIS/Typecheck.hs @@ -3,25 +3,27 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TupleSections #-} module HSVIS.Typecheck where import Control.Monad -import Control.Monad.Reader -import Control.Monad.State -import Control.Monad.Writer.CPS +import Data.Bifunctor (first) import Data.Foldable (toList) +import Data.List (partition) import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map import Data.Bag import Data.List.NonEmpty.Util import HSVIS.AST import HSVIS.Parser import HSVIS.Diagnostic +import HSVIS.Pretty data StageTC -type instance X DataDef StageTC = CType +type instance X DataDef StageTC = () type instance X FunDef StageTC = CType type instance X FunEq StageTC = CType type instance X Kind StageTC = () @@ -30,8 +32,8 @@ type instance X Pattern StageTC = CType type instance X RHS StageTC = CType type instance X Expr StageTC = CType -data instance E Type StageTC = TUniVar Int - deriving (Show) +data instance E Type StageTC = TUniVar Int deriving (Show) +data instance E Kind StageTC = KUniVar Int deriving (Show) type CProgram = Program StageTC type CDataDef = DataDef StageTC @@ -54,8 +56,8 @@ type instance X Pattern StageTyped = TType type instance X RHS StageTyped = TType type instance X Expr StageTyped = TType -data instance E t StageTyped - deriving (Show) +data instance E Type StageTyped deriving (Show) +data instance E Kind StageTyped deriving (Show) type TProgram = Program StageTyped type TDataDef = DataDef StageTyped @@ -68,77 +70,203 @@ type TRHS = RHS StageTyped type TExpr = Expr StageTyped -typecheck :: FilePath -> String -> Program Range -> ([Diagnostic], Program TType) +typecheck :: FilePath -> String -> PProgram -> ([Diagnostic], Program TType) typecheck fp source prog = - let (progtc, (ds1, cs)) = - runWriter - . flip evalStateT (Env mempty mempty) - . flip evalStateT 1 - . flip runReaderT (fp, source) - . runTCM - $ tcProgram prog + let (ds1, cs, _, _, progtc) = + runTCM (tcProgram prog) (fp, source) 1 (Env mempty mempty) (ds2, sub) = solveConstrs cs in (toList (ds1 <> ds2), substProg sub progtc) -data Constr = - CEq CType CType Range -- ^ These types must be equal because of the expression here +data Constr + = CEq CType CType Range -- ^ These types must be equal because of the expression here + | CEqK CKind CKind Range -- ^ These kinds must be equal because of the type here deriving (Show) data Env = Env (Map Name CKind) (Map Name CType) deriving (Show) -newtype TCM a = TCM { runTCM :: - ReaderT (FilePath, String) - (StateT Int - (StateT Env - (Writer (Bag Diagnostic, Bag Constr)))) - a } - deriving newtype (Functor, Applicative, Monad) +newtype TCM a = TCM { + runTCM :: (FilePath, String) -- ^ reader context: file and file contents + -> Int -- ^ state: next id to generate + -> Env -- ^ state: type and value environment + -> (Bag Diagnostic -- ^ writer: diagnostics + ,Bag Constr -- ^ writer: constraints + ,Int, Env, a) + } + +instance Functor TCM where + fmap f (TCM g) = TCM $ \ctx i env -> + let (ds, cs, i', env', x) = g ctx i env + in (ds, cs, i', env', f x) + +instance Applicative TCM where + pure x = TCM $ \_ i env -> (mempty, mempty, i, env, x) + (<*>) = ap + +instance Monad TCM where + TCM f >>= g = TCM $ \ctx i1 env1 -> + let (ds2, cs2, i2, env2, x) = f ctx i1 env1 + (ds3, cs3, i3, env3, y) = runTCM (g x) ctx i2 env2 + in (ds2 <> ds3, cs2 <> cs3, i3, env3, y) raise :: Range -> String -> TCM () -raise rng@(Range (Pos y _) _) msg = do - (fp, source) <- ask - TCM $ lift $ lift $ tell (pure (Diagnostic fp rng [] (source !! y) msg), mempty) +raise rng@(Range (Pos y _) _) msg = TCM $ \(fp, source) i env -> + (pure (Diagnostic fp rng [] (lines source !! y) msg), mempty, i, env, ()) + +emit :: Constr -> TCM () +emit c = TCM $ \_ i env -> (mempty, pure c, i, env, ()) + +collectConstraints :: (Constr -> Maybe b) -> TCM a -> TCM (Bag b, a) +collectConstraints predicate (TCM f) = TCM $ \ctx i env -> + let (ds, cs, i', env', x) = f ctx i env + (yes, no) = bagPartition predicate cs + in (ds, no, i', env', (yes, x)) + +getFullEnv :: TCM Env +getFullEnv = TCM $ \_ i env -> (mempty, mempty, i, env, env) + +putFullEnv :: Env -> TCM () +putFullEnv env = TCM $ \_ i _ -> (mempty, mempty, i, env, ()) + +genId :: TCM Int +genId = TCM $ \_ i env -> (mempty, mempty, i, env, i) + +getKind :: Name -> TCM (Maybe CKind) +getKind name = do + Env tenv _ <- getFullEnv + return (Map.lookup name tenv) + +getType :: Name -> TCM (Maybe CType) +getType name = do + Env _ venv <- getFullEnv + return (Map.lookup name venv) modifyTEnv :: (Map Name CKind -> Map Name CKind) -> TCM () -modifyTEnv f = TCM $ lift $ lift $ modify (\(Env a b) -> Env (f a) b) +modifyTEnv f = do + Env tenv venv <- getFullEnv + putFullEnv (Env (f tenv) venv) modifyVEnv :: (Map Name CType -> Map Name CType) -> TCM () -modifyVEnv f = TCM $ lift $ lift $ modify (\(Env a b) -> Env a (f b)) +modifyVEnv f = do + Env tenv venv <- getFullEnv + putFullEnv (Env tenv (f venv)) + +scopeTEnv :: TCM a -> TCM a +scopeTEnv m = do + Env origtenv _ <- getFullEnv + res <- m + modifyTEnv (\_ -> origtenv) + return res + +scopeVEnv :: TCM a -> TCM a +scopeVEnv m = do + Env _ origvenv <- getFullEnv + res <- m + modifyVEnv (\_ -> origvenv) + return res + +genKUniVar :: TCM CKind +genKUniVar = KExt () . KUniVar <$> genId genUniVar :: CKind -> TCM CType -genUniVar k = TCM $ lift $ state (\i -> (TExt k (TUniVar i), i + 1)) +genUniVar k = TExt k . TUniVar <$> genId + +getKind' :: Range -> Name -> TCM CKind +getKind' rng name = getKind name >>= \case + Nothing -> do + raise rng $ "Type not in scope: " ++ pretty name + genKUniVar + Just k -> return k + +getType' :: Range -> Name -> TCM CType +getType' rng name = getType name >>= \case + Nothing -> do + raise rng $ "Variable not in scope: " ++ pretty name + genUniVar (KType ()) + Just k -> return k tcProgram :: PProgram -> TCM CProgram tcProgram (Program ddefs fdefs) = do - -- TODO: add preliminary kinds for the data definitions to the environment, - -- then solve for the kind variables in checkDataDef + (kconstrs, ddefs') <- collectConstraints isCEqK $ do + mapM_ prepareDataDef ddefs + mapM tcDataDef ddefs + + solveKindVars kconstrs + + fdefs' <- mapM tcFunDef fdefs + + return (Program ddefs' fdefs') + +prepareDataDef :: PDataDef -> TCM () +prepareDataDef (DataDef _ name params _) = do + parkinds <- mapM (\_ -> genKUniVar) params + let k = foldr (KFun ()) (KType ()) parkinds + modifyTEnv (Map.insert name k) + +-- Assumes that the kind of the name itself has already been registered with +-- the correct arity (this is doen by prepareDataDef). +tcDataDef :: PDataDef -> TCM CDataDef +tcDataDef (DataDef rng name params cons) = do + kd <- getKind' rng name + let (pkinds, kret) = splitKind kd + + -- sanity checking; would be nicer to store these in prepareDataDef already + when (length pkinds /= length params) $ error "tcDataDef: Invalid param kind list length" + case kret of Right () -> return () + _ -> error "tcDataDef: Invalid ret kind" + + cons' <- scopeTEnv $ do + modifyTEnv (Map.fromList (zip (map snd params) pkinds) <>) + mapM (\(cname, ty) -> (cname,) <$> mapM kcType ty) cons + return (DataDef () name (zip pkinds (map snd params)) cons') - Program <$> traverse checkDataDef ddefs <*> traverse tcFunDef fdefs +kcType :: PType -> TCM CType +kcType = \case + TApp rng t ts -> do + t' <- kcType t + ts' <- mapM kcType ts + retk <- genKUniVar + let expected = foldr (KFun ()) retk (map extOf ts') + emit $ CEqK (extOf t') expected rng + return (TApp retk t' ts') -checkDataDef :: PDataDef -> TCM CDataDef -checkDataDef (DataDef rng name params cons) = do - _ + TTup _ ts -> do + ts' <- mapM kcType ts + forM_ (zip (map extOf ts) ts') $ \(trng, ct) -> + emit $ CEqK (extOf ct) (KType ()) trng + return (TTup (KType ()) ts') + + TList _ t -> do + t' <- kcType t + emit $ CEqK (extOf t') (KType ()) (extOf t) + return (TList (KType ()) t') + + TFun _ t1 t2 -> do + t1' <- kcType t1 + t2' <- kcType t2 + emit $ CEqK (extOf t1') (KType ()) (extOf t1) + emit $ CEqK (extOf t2') (KType ()) (extOf t2) + return (TFun (KType ()) t1' t2') + + TCon rng n -> TCon <$> getKind' rng n <*> pure n + + TVar rng n -> TVar <$> getKind' rng n <*> pure n tcFunDef :: PFunDef -> TCM CFunDef -tcFunDef (FunDef rng name msig eqs) = do +tcFunDef (FunDef _ name msig eqs) = do when (not $ allEq (fmap (length . funeqPats) eqs)) $ raise (sconcatne (fmap extOf eqs)) "Function equations have differing numbers of arguments" typ <- case msig of - Just sig -> checkType sig - Nothing -> genUniVar (KType ()) + TypeSig sig -> kcType sig + TypeSigExt NoTypeSig -> genUniVar (KType ()) - _ + eqs' <- mapM (tcFunEq typ) eqs -checkType :: PType -> TCM CType -checkType = \case - TApp r t ts -> _ - TTup r ts -> _ - TList r t -> _ - TFun r s t -> _ - TCon r n -> _ - TVar r n -> _ + return (FunDef typ name (TypeSig typ) eqs') + +tcFunEq :: CType -> PFunEq -> TCM CFunEq +tcFunEq = _ allEq :: (Eq a, Foldable t) => t a -> Bool allEq l = case toList l of @@ -147,3 +275,12 @@ allEq l = case toList l of funeqPats :: FunEq t -> [Pattern t] funeqPats (FunEq _ _ pats _) = pats + +splitKind :: Kind s -> ([Kind s], Either (E Kind s) (X Kind s)) +splitKind (KType x) = ([], Right x) +splitKind (KFun _ k1 k2) = first (k1:) (splitKind k2) +splitKind (KExt _ e) = ([], Left e) + +isCEqK :: Constr -> Maybe (CKind, CKind, Range) +isCEqK (CEqK k1 k2 rng) = Just (k1, k2, rng) +isCEqK _ = Nothing -- cgit v1.2.3-70-g09d2