From 5014c402e63e882567bb8759cad5cbf61db1e11f Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Mon, 25 Mar 2024 22:30:33 +0100 Subject: typechecker --- src/HSVIS/AST.hs | 172 +++++++++++++++-------------- src/HSVIS/Parser.hs | 11 +- src/HSVIS/Typecheck.hs | 292 +++++++++++++++++++++++++++++++------------------ 3 files changed, 285 insertions(+), 190 deletions(-) (limited to 'src/HSVIS') diff --git a/src/HSVIS/AST.hs b/src/HSVIS/AST.hs index 91e08eb..63594bc 100644 --- a/src/HSVIS/AST.hs +++ b/src/HSVIS/AST.hs @@ -9,11 +9,11 @@ {-# LANGUAGE ConstrainedClassMethods #-} module HSVIS.AST where -import Data.Bifunctor (bimap, first, second) +-- import Data.Bifunctor (bimap, first, second) import qualified Data.Kind as DK import Data.List (intersperse) import Data.List.NonEmpty (NonEmpty) -import Data.Proxy +-- import Data.Proxy import HSVIS.Pretty @@ -32,30 +32,30 @@ class HasExt f where type HasECon f :: Bool type ContainsData f :: [ASTType] extOf :: HasXField f ~ 'True => f s -> X f s - extMap :: Proxy f -> Proxy s1 -> Proxy s2 - -> XMapperTelescope (f ': ContainsData f) s1 s2 - (EMapperTelescope (f ': ContainsData f) s1 s2 - (f s1 -> f s2)) + -- extMap :: Proxy f -> Proxy s1 -> Proxy s2 + -- -> XMapperTelescope (f ': ContainsData f) s1 s2 + -- (EMapperTelescope (f ': ContainsData f) s1 s2 + -- (f s1 -> f s2)) type family If c a b where If 'True a b = a If 'False a b = b -type family XMapperTelescope fs s1 s2 a where - XMapperTelescope '[] s1 s2 a = a - XMapperTelescope (f ': fs) s1 s2 a = - If (HasXField f) - ((X f s1 -> X f s2) -> XMapperTelescope fs s1 s2 a) - (XMapperTelescope fs s1 s2 a) +-- type family XMapperTelescope fs s1 s2 a where +-- XMapperTelescope '[] s1 s2 a = a +-- XMapperTelescope (f ': fs) s1 s2 a = +-- If (HasXField f) +-- ((X f s1 -> X f s2) -> XMapperTelescope fs s1 s2 a) +-- (XMapperTelescope fs s1 s2 a) -type family EMapperTelescope fs s1 s2 a where - EMapperTelescope '[] s1 s2 a = a - EMapperTelescope (f ': fs) s1 s2 a = - If (HasECon f) - (If (HasXField f) (X f s1 -> E f s1 -> f s2) - (E f s1 -> f s2) - -> EMapperTelescope fs s1 s2 a) - (EMapperTelescope fs s1 s2 a) +-- type family EMapperTelescope fs s1 s2 a where +-- EMapperTelescope '[] s1 s2 a = a +-- EMapperTelescope (f ': fs) s1 s2 a = +-- If (HasECon f) +-- (If (HasXField f) (X f s1 -> E f s1 -> f s2) +-- (E f s1 -> f s2) +-- -> EMapperTelescope fs s1 s2 a) +-- (EMapperTelescope fs s1 s2 a) newtype Name = Name String @@ -64,16 +64,19 @@ newtype Name = Name String data Program s = Program [DataDef s] [FunDef s] deriving instance (Show (DataDef s), Show (FunDef s)) => Show (Program s) -data DataDef s = DataDef (X DataDef s) Name [(X Type s, Name)] [(Name, [Type s])] -deriving instance (Show (X DataDef s), Show (X Type s), Show (E Type s)) => Show (DataDef s) +data DataDef s = DataDef (X DataDef s) Name [(X Type s, Name)] [(Name, [DataField s])] +deriving instance (Show (X DataDef s), Show (DataField s), Show (X Type s)) => Show (DataDef s) + +data DataField s = DataField (X DataField s) (Type s) +deriving instance (Show (X DataField s), Show (X Type s), Show (E Type s)) => Show (DataField s) data FunDef s = FunDef (X FunDef s) Name (TypeSig s) (NonEmpty (FunEq s)) deriving instance (Show (X FunDef s), Show (TypeSig s), Show (FunEq s)) => Show (FunDef s) data TypeSig s - = TypeSig (Type s) - | TypeSigExt !(E TypeSig s) -deriving instance (Show (E TypeSig s), Show (Type s)) => Show (TypeSig s) + = TypeSig (X TypeSig s) (Type s) + | TypeSigExt (X TypeSig s) !(E TypeSig s) +deriving instance (Show (X TypeSig s), Show (E TypeSig s), Show (Type s)) => Show (TypeSig s) data FunEq s = FunEq (X FunEq s) Name [Pattern s] (RHS s) deriving instance (Show (X FunEq s), Show (Pattern s), Show (RHS s)) => Show (FunEq s) @@ -171,7 +174,7 @@ instance (Pretty (X Type s), Pretty (E Type s)) => Pretty (DataDef s) where | (k, n) <- vars] . showString " = " . foldr (.) id (intersperse (showString " | ") - [prettysPrec 11 cname . foldr (.) id [showString " " . prettysPrec 11 t | t <- fields] + [prettysPrec 11 cname . foldr (.) id [showString " " . prettysPrec 11 t | DataField _ t <- fields] | (cname, fields) <- cons]) instance Pretty Operator where @@ -188,38 +191,47 @@ instance Pretty Operator where instance HasExt DataDef where type HasXField DataDef = 'True type HasECon DataDef = 'False - type ContainsData DataDef = '[Type] + type ContainsData DataDef = '[DataField, Type] extOf (DataDef x _ _ _) = x - extMap _ ps1 ps2 fdd fty gty (DataDef x n ps cs) = - DataDef (fdd x) n (map (first fty) ps) (map (second (map (extMap (Proxy @Type) ps1 ps2 fty gty))) cs) + -- extMap _ ps1 ps2 fdd fdf fty gty (DataDef x n ps cs) = + -- DataDef (fdd x) n (map (first fty) ps) + -- (map (second (map (extMap (Proxy @DataField) ps1 ps2 fdf fty gty))) cs) + +instance HasExt DataField where + type HasXField DataField = 'True + type HasECon DataField = 'False + type ContainsData DataField = '[Type] + extOf (DataField x _) = x + -- extMap _ ps1 ps2 fdf fty gty (DataField x t) = + -- DataField (fdf x) (extMap (Proxy @Type) ps1 ps2 fty gty t) instance HasExt FunDef where type HasXField FunDef = 'True type HasECon FunDef = 'False type ContainsData FunDef = '[TypeSig, FunEq, Type, Pattern, RHS, Expr] extOf (FunDef x _ _ _) = x - extMap _ ps1 ps2 ffd ffe fty fpa frh fex gts gty (FunDef x n sig es) = - FunDef (ffd x) n - (extMap (Proxy @TypeSig) ps1 ps2 fty gts gty sig) - (fmap (extMap (Proxy @FunEq) ps1 ps2 ffe ffd fty fpa frh fex gts gty) es) + -- extMap _ ps1 ps2 ffd fts ffe fty fpa frh fex gts gty (FunDef x n sig es) = + -- FunDef (ffd x) n + -- (extMap (Proxy @TypeSig) ps1 ps2 fty gts gty sig) + -- (fmap (extMap (Proxy @FunEq) ps1 ps2 ffe ffd fty fpa frh fex gts gty) es) instance HasExt TypeSig where - type HasXField TypeSig = 'False + type HasXField TypeSig = 'True type HasECon TypeSig = 'True type ContainsData TypeSig = '[Type] extOf _ = undefined - extMap _ ps1 ps2 fty _ gty (TypeSig ty) = - TypeSig (extMap (Proxy @Type) ps1 ps2 fty gty ty) - extMap _ _ _ _ gts _ (TypeSigExt e) = gts e + -- extMap _ ps1 ps2 fty _ gty (TypeSig x ty) = + -- TypeSig (extMap (Proxy @Type) ps1 ps2 fty gty ty) + -- extMap _ _ _ _ gts _ (TypeSigExt x e) = gts e instance HasExt FunEq where type HasXField FunEq = 'True type HasECon FunEq = 'False type ContainsData FunEq = '[FunDef, TypeSig, Type, Pattern, RHS, Expr] extOf (FunEq x _ _ _) = x - extMap _ ps1 ps2 ffe ffd fty fpa frh fex gts gty (FunEq x n ps rhs) = - FunEq (ffe x) n (map (extMap (Proxy @Pattern) ps1 ps2 fpa) ps) - (extMap (Proxy @RHS) ps1 ps2 frh ffd ffe fty fpa fex gts gty rhs) + -- extMap _ ps1 ps2 ffe ffd fty fpa frh fex gts gty (FunEq x n ps rhs) = + -- FunEq (ffe x) n (map (extMap (Proxy @Pattern) ps1 ps2 fpa) ps) + -- (extMap (Proxy @RHS) ps1 ps2 frh ffd ffe fty fpa fex gts gty rhs) instance HasExt Kind where type HasXField Kind = 'True @@ -228,9 +240,9 @@ instance HasExt Kind where extOf (KType x) = x extOf (KFun x _ _) = x extOf (KExt x _) = x - extMap _ _ _ f _ (KType x) = KType (f x) - extMap p ps1 ps2 f g (KFun x a b) = KFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b) - extMap _ _ _ _ g (KExt x a) = g x a + -- extMap _ _ _ f _ (KType x) = KType (f x) + -- extMap p ps1 ps2 f g (KFun x a b) = KFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b) + -- extMap _ _ _ _ g (KExt x a) = g x a instance HasExt Type where type HasXField Type = 'True @@ -245,14 +257,14 @@ instance HasExt Type where extOf (TForall x _ _) = x extOf (TExt x _) = x - extMap p ps1 ps2 f g (TApp x a b) = TApp (f x) (extMap p ps1 ps2 f g a) (map (extMap p ps1 ps2 f g) b) - extMap p ps1 ps2 f g (TTup x as) = TTup (f x) (map (extMap p ps1 ps2 f g) as) - extMap p ps1 ps2 f g (TList x a) = TList (f x) (extMap p ps1 ps2 f g a) - extMap p ps1 ps2 f g (TFun x a b) = TFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b) - extMap _ _ _ f _ (TCon x n) = TCon (f x) n - extMap _ _ _ f _ (TVar x n) = TVar (f x) n - extMap p ps1 ps2 f g (TForall x n a) = TForall (f x) n (extMap p ps1 ps2 f g a) - extMap _ _ _ _ g (TExt x e) = g x e + -- extMap p ps1 ps2 f g (TApp x a b) = TApp (f x) (extMap p ps1 ps2 f g a) (map (extMap p ps1 ps2 f g) b) + -- extMap p ps1 ps2 f g (TTup x as) = TTup (f x) (map (extMap p ps1 ps2 f g) as) + -- extMap p ps1 ps2 f g (TList x a) = TList (f x) (extMap p ps1 ps2 f g a) + -- extMap p ps1 ps2 f g (TFun x a b) = TFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b) + -- extMap _ _ _ f _ (TCon x n) = TCon (f x) n + -- extMap _ _ _ f _ (TVar x n) = TVar (f x) n + -- extMap p ps1 ps2 f g (TForall x n a) = TForall (f x) n (extMap p ps1 ps2 f g a) + -- extMap _ _ _ _ g (TExt x e) = g x e instance HasExt Pattern where type HasXField Pattern = 'True @@ -266,13 +278,13 @@ instance HasExt Pattern where extOf (PList x _) = x extOf (PTup x _) = x - extMap _ _ _ f (PWildcard x) = PWildcard (f x) - extMap _ _ _ f (PVar x n) = PVar (f x) n - extMap p ps1 ps2 f (PAs x n a) = PAs (f x) n (extMap p ps1 ps2 f a) - extMap p ps1 ps2 f (PCon x n as) = PCon (f x) n (map (extMap p ps1 ps2 f) as) - extMap p ps1 ps2 f (POp x a n b) = POp (f x) (extMap p ps1 ps2 f a) n (extMap p ps1 ps2 f b) - extMap p ps1 ps2 f (PList x as) = PList (f x) (map (extMap p ps1 ps2 f) as) - extMap p ps1 ps2 f (PTup x as) = PTup (f x) (map (extMap p ps1 ps2 f) as) + -- extMap _ _ _ f (PWildcard x) = PWildcard (f x) + -- extMap _ _ _ f (PVar x n) = PVar (f x) n + -- extMap p ps1 ps2 f (PAs x n a) = PAs (f x) n (extMap p ps1 ps2 f a) + -- extMap p ps1 ps2 f (PCon x n as) = PCon (f x) n (map (extMap p ps1 ps2 f) as) + -- extMap p ps1 ps2 f (POp x a n b) = POp (f x) (extMap p ps1 ps2 f a) n (extMap p ps1 ps2 f b) + -- extMap p ps1 ps2 f (PList x as) = PList (f x) (map (extMap p ps1 ps2 f) as) + -- extMap p ps1 ps2 f (PTup x as) = PTup (f x) (map (extMap p ps1 ps2 f) as) instance HasExt RHS where type HasXField RHS = 'True @@ -281,13 +293,13 @@ instance HasExt RHS where extOf (Guarded x _) = x extOf (Plain x _) = x - extMap _ ps1 ps2 frh ffd ffe fty fpa fex gts gty (Guarded x l) = - Guarded (frh x) - (map (bimap (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty) - (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty)) - l) - extMap _ ps1 ps2 frh ffd ffe fty fpa fex gts gty (Plain x e) = - Plain (frh x) (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty e) + -- extMap _ ps1 ps2 frh ffd ffe fty fpa fex gts gty (Guarded x l) = + -- Guarded (frh x) + -- (map (bimap (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty) + -- (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty)) + -- l) + -- extMap _ ps1 ps2 frh ffd ffe fty fpa fex gts gty (Plain x e) = + -- Plain (frh x) (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty e) instance HasExt Expr where type HasXField Expr = 'True @@ -305,18 +317,18 @@ instance HasExt Expr where extOf (ELet x _ _) = x extOf (EError x) = x - extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty = \case - ELit x l -> ELit (fex x) l - EVar x n -> EVar (fex x) n - ECon x n -> ECon (fex x) n - EList x es -> EList (fex x) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es) - ETup x es -> ETup (fex x) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es) - EApp x a es -> EApp (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es) - EOp x a n b -> EOp (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) n (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b) - EIf x a b c -> EIf (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty c) - ECase x a l -> ECase (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) - (map (bimap (extMap (Proxy @Pattern) ps1 ps2 fpa) - (extMap (Proxy @RHS) ps1 ps2 frh ffd ffe fty fpa fex gts gty)) - l) - ELet x as b -> ELet (fex x) (map (extMap (Proxy @FunDef) ps1 ps2 ffd ffe fty fpa frh fex gts gty) as) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b) - EError x -> EError (fex x) + -- extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty = \case + -- ELit x l -> ELit (fex x) l + -- EVar x n -> EVar (fex x) n + -- ECon x n -> ECon (fex x) n + -- EList x es -> EList (fex x) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es) + -- ETup x es -> ETup (fex x) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es) + -- EApp x a es -> EApp (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es) + -- EOp x a n b -> EOp (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) n (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b) + -- EIf x a b c -> EIf (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty c) + -- ECase x a l -> ECase (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) + -- (map (bimap (extMap (Proxy @Pattern) ps1 ps2 fpa) + -- (extMap (Proxy @RHS) ps1 ps2 frh ffd ffe fty fpa fex gts gty)) + -- l) + -- ELet x as b -> ELet (fex x) (map (extMap (Proxy @FunDef) ps1 ps2 ffd ffe fty fpa frh fex gts gty) as) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b) + -- EError x -> EError (fex x) diff --git a/src/HSVIS/Parser.hs b/src/HSVIS/Parser.hs index e89c679..bea0524 100644 --- a/src/HSVIS/Parser.hs +++ b/src/HSVIS/Parser.hs @@ -30,6 +30,7 @@ import Control.Monad.Chronicle import Control.Monad.Reader import Control.Monad.State.Lazy import Data.Char +import Data.Bifunctor (second) import Data.Either (partitionEithers) import Data.Foldable import Data.List.NonEmpty (NonEmpty(..)) @@ -49,7 +50,9 @@ import HSVIS.Pretty data StageParsed type instance X DataDef StageParsed = Range +type instance X DataField StageParsed = () type instance X FunDef StageParsed = Range +type instance X TypeSig StageParsed = () type instance X FunEq StageParsed = Range type instance X Type StageParsed = Range type instance X Pattern StageParsed = Range @@ -233,7 +236,7 @@ pDataDef0 = do params <- famany (inlineWhite >> ranged (pIdentifier0 InBlock Lowercase WCBacktrack)) cons <- pDatacons "=" pos2 <- gets psCur - return [DataDef (Range pos1 pos2) name params cons] + return [DataDef (Range pos1 pos2) name params (map (second (map (DataField ()))) cons)] where pDatacons :: String -> IParser [(Name, [PType])] pDatacons leader = do @@ -262,20 +265,20 @@ pFunDef0 = clauses <- concat <$> famany (pFunEq (Continue name)) let clauses' = clause1 :| clauses1 ++ clauses let rng = sigrange <> foldMapne extOf clauses' - return [FunDef rng name (TypeSig typ) clauses'] + return [FunDef rng name (TypeSig () typ) clauses'] _ -> do pos <- gets psCur raise Error $ "Expected function equation for " ++ pretty name ++ " after type signature" let rng = Range pos pos - return [FunDef sigrange name (TypeSig typ) + return [FunDef sigrange name (TypeSig () typ) (FunEq rng name [] (Plain rng (EError rng)) :| [])] ,do pFunEq FirstLine >>= \case clause1@(FunEq _ name _ _) : clauses1 -> noFail $ do clauses <- concat <$> famany (pFunEq (Continue name)) let clauses' = clause1 :| clauses1 ++ clauses let rng = foldMapne extOf clauses' - return [FunDef rng name (TypeSigExt NoTypeSig) clauses'] + return [FunDef rng name (TypeSigExt () NoTypeSig) clauses'] [] -> faempty] -- | Given the name from the type signature or a previous clause, if any. diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs index 2dd103f..1e46a99 100644 --- a/src/HSVIS/Typecheck.hs +++ b/src/HSVIS/Typecheck.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE EmptyDataDeriving #-} {-# LANGUAGE FlexibleInstances #-} @@ -7,40 +8,28 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE GADTs #-} - - - -{-# OPTIONS -Wno-unused-top-binds #-} -{-# OPTIONS -Wno-unused-imports #-} -{-# LANGUAGE DataKinds #-} - - - module HSVIS.Typecheck ( StageTyped, typecheck, -- * Typed AST synonyms - -- TProgram, TDataDef, TFunDef, TFunEq, TKind, TType, TPattern, TRHS, TExpr, + TProgram, TDataDef, TDataField, TFunDef, TFunEq, TKind, TType, TPattern, TRHS, TExpr, ) where import Control.Monad import Data.Bifunctor (first, second, bimap) import Data.Foldable (toList) -import Data.List (find, inits) +import Data.List (inits) import Data.Map.Strict (Map) import Data.Maybe (fromMaybe) -import Data.Monoid (Ap(..)) import qualified Data.Map.Strict as Map import Data.Tuple (swap) import Data.Semigroup (First(..)) import Data.Set (Set) import qualified Data.Set as Set -import GHC.Stack import Debug.Trace import Data.Bag -import Data.List.NonEmpty.Util import Data.Map.Monoidal (MMap(..)) import qualified Data.Map.Monoidal as MMap import HSVIS.AST @@ -53,13 +42,15 @@ import HSVIS.Typecheck.Solve data StageTC type instance X DataDef StageTC = CKind -type instance X FunDef StageTC = CType +type instance X DataField StageTC = Range +type instance X FunDef StageTC = Range +type instance X TypeSig StageTC = Maybe Range type instance X FunEq StageTC = () type instance X Kind StageTC = () type instance X Type StageTC = CKind -type instance X Pattern StageTC = CType +type instance X Pattern StageTC = (Range, CType) type instance X RHS StageTC = CType -type instance X Expr StageTC = CType +type instance X Expr StageTC = (Range, CType) data instance E Type StageTC = TUniVar Int deriving (Show, Eq, Ord) data instance E Kind StageTC = KUniVar Int deriving (Show, Eq, Ord) @@ -67,6 +58,7 @@ data instance E TypeSig StageTC deriving (Show) type CProgram = Program StageTC type CDataDef = DataDef StageTC +type CDataField = DataField StageTC type CFunDef = FunDef StageTC type CFunEq = FunEq StageTC type CKind = Kind StageTC @@ -78,7 +70,9 @@ type CExpr = Expr StageTC data StageTyped type instance X DataDef StageTyped = TKind -type instance X FunDef StageTyped = TType +type instance X DataField StageTyped = Range +type instance X FunDef StageTyped = () +type instance X TypeSig StageTyped = () type instance X FunEq StageTyped = () type instance X Kind StageTyped = () type instance X Type StageTyped = TKind @@ -92,6 +86,7 @@ data instance E TypeSig StageTyped deriving (Show) type TProgram = Program StageTyped type TDataDef = DataDef StageTyped +type TDataField = DataField StageTyped type TFunDef = FunDef StageTyped type TFunEq = FunEq StageTyped type TKind = Kind StageTyped @@ -251,7 +246,7 @@ tcTop :: PProgram -> TCM TProgram tcTop prog = do (cs, prog') <- collectConstraints Just (tcProgram prog) (subK, subT) <- solveConstrs cs - return $ finaliseProg (substProg subK subT prog') + finaliseProg (substProg subK subT prog') tcProgram :: PProgram -> TCM CProgram tcProgram (Program ddefs1 fdefs1) = do @@ -301,9 +296,10 @@ kcDataDef (kd, parkinds) (DataDef _ name params cons) = do -- kind-check the constructors cons' <- scopeTEnv $ do modifyTEnv (Map.fromList (zip params' parkinds) <>) - forM cons $ \(cname, fieldtys) -> do - fieldtys' <- mapM (kcType KCTMNormal (Just (KType ()))) fieldtys - return (cname, fieldtys') + forM cons $ \(cname, fields) -> do + fields' <- forM fields $ \(DataField () t) -> + DataField (extOf t) <$> kcType KCTMNormal (Just (KType ())) t + return (cname, fields') return (DataDef kd name (zip parkinds params') cons') @@ -311,7 +307,7 @@ generateInvCons :: CDataDef -> [(Name, InvCon)] generateInvCons (DataDef k tname params cons) = let tyvars = Map.fromList (map swap params) resty = TApp (KType ()) (TCon k tname) (map (uncurry TVar) params) - in [(cname, InvCon tyvars resty fields) | (cname, fields) <- cons] + in [(cname, InvCon tyvars resty (map dataFieldType fields)) | (cname, fields) <- cons] promoteDownK :: Maybe CKind -> TCM CKind promoteDownK Nothing = genKUniVar @@ -401,7 +397,7 @@ tcFunDefBlock fdefs = do -- take the actual found types for typechecking the body (and link them -- to the variables generated above) - let bound2 = map (\(FunDef ty n _ _) -> (n, ty)) defs' + let bound2 = map (\(FunDef _ n (TypeSig _ ty) _) -> (n, ty)) defs' forM_ (zip3 fdefs bound bound2) $ \(fdef, (_, tvar), (_, ty)) -> emit $ CEq ty tvar (extOf fdef) -- which is expected/observed? which range? /shrug/ @@ -412,8 +408,8 @@ tcFunDef (FunDef rng name msig eqs) = do when (not $ allEq (fmap (length . funeqPats) eqs)) $ raise SError rng "Function equations have differing numbers of arguments" - typ <- case msig of - TypeSig sig -> do + (typ, msigrng) <- case msig of + TypeSig _ sig -> do (typ, freetvars) <- kcType KCTMOpen (Just (KType ())) sig TODO -- We need to check that these free type variables do not escape. -- Perhaps with levels on unification variables? Associate a level @@ -421,14 +417,15 @@ tcFunDef (FunDef rng name msig eqs) = do -- passing below a forall. -- But how do we deal with functions without a type signature -- anyway? We should be able to infer a polymorphic type for them. - return $ foldr (\(n, k) -> TForall k n) typ (Map.assocs freetvars) - TypeSigExt NoTypeSig -> genUniVar (KType ()) + return (foldr (\(n, k) -> TForall k n) typ (Map.assocs freetvars) + ,Just (extOf sig)) + TypeSigExt _ NoTypeSig -> (,Nothing) <$> genUniVar (KType ()) eqs' <- scopeVEnv $ do modifyVEnv (Map.insert name typ) -- allow function to be recursive mapM (tcFunEq typ) eqs - return (FunDef typ name (TypeSig typ) eqs') + return (FunDef rng name (TypeSig msigrng typ) eqs') tcFunEq :: CType -> PFunEq -> TCM CFunEq tcFunEq down (FunEq rng name pats rhs) = do @@ -442,11 +439,14 @@ tcFunEq down (FunEq rng name pats rhs) = do -- | Brings the bound variables in scope tcPattern :: CType -> PPattern -> TCM CPattern tcPattern down = \case - PWildcard _ -> return $ PWildcard down + PWildcard rng -> return $ PWildcard (rng, down) - PVar _ n -> modifyVEnv (Map.insert n down) >> return (PVar down n) + PVar rng n -> modifyVEnv (Map.insert n down) >> return (PVar (rng, down) n) - PAs _ n p -> modifyVEnv (Map.insert n down) >> tcPattern down p + PAs rng n p -> do + modifyVEnv (Map.insert n down) + p' <- tcPattern down p + return $ PAs (rng, snd (extOf p')) n p' PCon rng n ps -> getInvCon n >>= \case @@ -455,10 +455,10 @@ tcPattern down = \case let match' = substType mempty mempty unisub match fields' = map (substType mempty mempty unisub) fields emit $ CEq down match' rng - PCon match' n <$> zipWithM tcPattern fields' ps + PCon (rng, match') n <$> zipWithM tcPattern fields' ps Nothing -> do raise SError rng $ "Constructor not in scope: " ++ pretty n - return (PWildcard down) + return (PWildcard (rng, down)) POp rng p1 op p2 -> case op of @@ -468,27 +468,27 @@ tcPattern down = \case emit $ CEq down listty rng p1' <- tcPattern eltty p1 p2' <- tcPattern listty p2 - return (POp listty p1' OCons p2') + return (POp (rng, listty) p1' OCons p2') _ -> do raise SError rng $ "Operator is not a constructor: " ++ pretty op - return (PWildcard down) + return (PWildcard (rng, down)) PList rng ps -> do eltty <- genUniVar (KType ()) let listty = TList (KType ()) eltty emit $ CEq down listty rng - PList listty <$> mapM (tcPattern eltty) ps + PList (rng, listty) <$> mapM (tcPattern eltty) ps PTup rng ps -> do ts <- mapM (\_ -> genUniVar (KType ())) ps emit $ CEq down (TTup (KType ()) ts) rng - PTup (TTup (KType ()) ts) <$> zipWithM tcPattern ts ps + PTup (rng, TTup (KType ()) ts) <$> zipWithM tcPattern ts ps tcRHS :: CType -> PRHS -> TCM CRHS tcRHS _ (Guarded _ _) = error "typecheck: Guards not yet supported" tcRHS down (Plain _ e) = do e' <- tcExpr down e - return $ Plain (extOf e') e' + return $ Plain (snd (extOf e')) e' tcExpr :: CType -> PExpr -> TCM CExpr tcExpr down = \case @@ -499,34 +499,34 @@ tcExpr down = \case LChar{} -> TCon (KType ()) (Name "Char") LString{} -> TList (KType ()) (TCon (KType ()) (Name "Char")) emit $ CEq down ty rng - return (ELit ty lit) + return $ ELit (rng, ty) lit EVar rng n -> do ty <- getType' rng n emit $ CEq down ty rng - return $ EVar ty n + return $ EVar (rng, ty) n ECon rng n -> do ty <- getType' rng n emit $ CEq down ty rng - return $ EVar ty n + return $ EVar (rng, ty) n EList rng es -> do eltty <- genUniVar (KType ()) let listty = TList (KType ()) eltty emit $ CEq down listty rng - EList listty <$> mapM (tcExpr listty) es + EList (rng, listty) <$> mapM (tcExpr listty) es ETup rng es -> do ts <- mapM (\_ -> genUniVar (KType ())) es emit $ CEq down (TTup (KType ()) ts) rng - ETup (TTup (KType ()) ts) <$> zipWithM tcExpr ts es + ETup (rng, TTup (KType ()) ts) <$> zipWithM tcExpr ts es - EApp _ e1 es -> do + EApp rng e1 es -> do argtys <- mapM (\_ -> genUniVar (KType ())) es let funty = foldr (TFun (KType ())) down argtys - EApp funty <$> tcExpr funty e1 - <*> zipWithM tcExpr argtys es + EApp (rng, funty) <$> tcExpr funty e1 + <*> zipWithM tcExpr argtys es -- TODO: these types are way too monomorphic and in any case these -- ~operators~ functions should not be built-in @@ -548,31 +548,31 @@ tcExpr down = \case emit $ CEq down rty rng e1' <- tcExpr aty1 e1 e2' <- tcExpr aty2 e2 - return (EOp rty e1' op e2') + return (EOp (rng, rty) e1' op e2') - EIf _ e1 e2 e3 -> do + EIf rng e1 e2 e3 -> do e1' <- tcExpr (TCon (KType ()) (Name "Bool")) e1 e2' <- tcExpr down e2 e3' <- tcExpr down e3 - return (EIf down e1' e2' e3') + return (EIf (rng, down) e1' e2' e3') - ECase _ e1 alts -> do + ECase rng e1 alts -> do ty <- genUniVar (KType ()) e1' <- tcExpr ty e1 alts' <- forM alts $ \(pat, rhs) -> scopeVEnv $ (,) <$> tcPattern ty pat <*> tcRHS down rhs - return $ ECase down e1' alts' + return $ ECase (rng, down) e1' alts' - ELet _ defs body -> do + ELet rng defs body -> do defs' <- tcFunDefBlock defs - let bound2 = map (\(FunDef ty n _ _) -> (n, ty)) defs' + let bound2 = map (\(FunDef _ n (TypeSig _ ty) _) -> (n, ty)) defs' scopeVEnv $ do modifyVEnv (Map.fromList bound2 <>) body' <- tcExpr down body - return $ ELet down defs' body' + return $ ELet (rng, down) defs' body' - EError _ -> return $ EError down + EError rng -> return $ EError (rng, down) unfoldFunTy :: Range -> Int -> CType -> TCM ([CType], CType) unfoldFunTy _ n t | n <= 0 = return ([], t) @@ -706,70 +706,65 @@ partitionConstrs = foldMap $ \case CEq t1 t2 r -> (pure (t1, t2, r), mempty) -- - an instantiation map for type unification variables (Map Int CType) -- - an instantiation map for type variables (Map Name CType) -substProg :: HasCallStack - => Map Int CKind -> Map Int CType -> CProgram -> CProgram +substProg :: Map Int CKind -> Map Int CType -> CProgram -> CProgram substProg mk mt (Program ds fs) = Program (map (substDdef mk mt) ds) (map (substFdef mk mt) fs) -substDdef :: HasCallStack - => Map Int CKind -> Map Int CType -> CDataDef -> CDataDef +substDdef :: Map Int CKind -> Map Int CType -> CDataDef -> CDataDef substDdef mk mt (DataDef k name pars cons) = DataDef (substKind mk k) name (map (first (substKind mk)) pars) - (map (second (map (substType mk mt mempty))) cons) + (map (second (map (substDataField mk mt))) cons) + +substDataField :: Map Int CKind -> Map Int CType -> CDataField -> CDataField +substDataField mk mt (DataField rng t) = DataField rng (substType mk mt mempty t) -substFdef :: HasCallStack - => Map Int CKind -> Map Int CType -> CFunDef -> CFunDef -substFdef mk mt (FunDef t n (TypeSig sig) eqs) = - FunDef (substType mk mt mempty t) n - (TypeSig (substType mk mt mempty sig)) +substFdef :: Map Int CKind -> Map Int CType -> CFunDef -> CFunDef +substFdef mk mt (FunDef rng n (TypeSig sigrng sig) eqs) = + FunDef rng n + (TypeSig sigrng (substType mk mt mempty sig)) (fmap (substFunEq mk mt) eqs) -substFunEq :: HasCallStack - => Map Int CKind -> Map Int CType -> CFunEq -> CFunEq +substFunEq :: Map Int CKind -> Map Int CType -> CFunEq -> CFunEq substFunEq mk mt (FunEq () n ps rhs) = FunEq () n (map (substPattern mk mt) ps) (substRHS mk mt rhs) -substRHS :: HasCallStack - => Map Int CKind -> Map Int CType -> CRHS -> CRHS +substRHS :: Map Int CKind -> Map Int CType -> CRHS -> CRHS substRHS _ _ (Guarded _ _) = error "typecheck: guards unsupported" substRHS mk mt (Plain t e) = Plain (substType mk mt mempty t) (substExpr mk mt e) -substPattern :: HasCallStack - => Map Int CKind -> Map Int CType -> CPattern -> CPattern +substPattern :: Map Int CKind -> Map Int CType -> CPattern -> CPattern substPattern mk mt = go where - go (PWildcard t) = PWildcard (goType t) - go (PVar t n) = PVar (goType t) n - go (PAs t n p) = PAs (goType t) n (go p) - go (PCon t n ps) = PCon (goType t) n (map go ps) - go (POp t p1 op p2) = POp (goType t) (go p1) op (go p2) - go (PList t ps) = PList (goType t) (map go ps) - go (PTup t ps) = PTup (goType t) (map go ps) - - goType = substType mk mt mempty - -substExpr :: HasCallStack - => Map Int CKind -> Map Int CType -> CExpr -> CExpr + go (PWildcard e) = PWildcard (goExt e) + go (PVar e n) = PVar (goExt e) n + go (PAs e n p) = PAs (goExt e) n (go p) + go (PCon e n ps) = PCon (goExt e) n (map go ps) + go (POp e p1 op p2) = POp (goExt e) (go p1) op (go p2) + go (PList e ps) = PList (goExt e) (map go ps) + go (PTup e ps) = PTup (goExt e) (map go ps) + + goExt (rng, t) = (rng, substType mk mt mempty t) + +substExpr :: Map Int CKind -> Map Int CType -> CExpr -> CExpr substExpr mk mt = go where - go (ELit t lit) = ELit (goType t) lit - go (EVar t n) = EVar (goType t) n - go (ECon t n) = ECon (goType t) n - go (EList t es) = EList (goType t) (map go es) - go (ETup t es) = ETup (goType t) (map go es) - go (EApp t e1 es) = EApp (goType t) (go e1) (map go es) - go (EOp t e1 op e2) = EOp (goType t) (go e1) op (go e2) - go (EIf t e1 e2 e3) = EIf (goType t) (go e1) (go e2) (go e3) - go (ECase t e1 alts) = ECase (goType t) (go e1) (map (bimap (substPattern mk mt) (substRHS mk mt)) alts) - go (ELet t defs body) = ELet (goType t) (map (substFdef mk mt) defs) (go body) - go (EError t) = EError (goType t) - - goType = substType mk mt mempty - -substType :: HasCallStack - => Map Int CKind -> Map Int CType -> Map Name CType -> CType -> CType + go (ELit e lit) = ELit (goExt e) lit + go (EVar e n) = EVar (goExt e) n + go (ECon e n) = ECon (goExt e) n + go (EList e es) = EList (goExt e) (map go es) + go (ETup e es) = ETup (goExt e) (map go es) + go (EApp e e1 es) = EApp (goExt e) (go e1) (map go es) + go (EOp e e1 op e2) = EOp (goExt e) (go e1) op (go e2) + go (EIf e e1 e2 e3) = EIf (goExt e) (go e1) (go e2) (go e3) + go (ECase e e1 alts) = ECase (goExt e) (go e1) (map (bimap (substPattern mk mt) (substRHS mk mt)) alts) + go (ELet e defs body) = ELet (goExt e) (map (substFdef mk mt) defs) (go body) + go (EError e) = EError (goExt e) + + goExt (rng, t) = (rng, substType mk mt mempty t) + +substType :: Map Int CKind -> Map Int CType -> Map Name CType -> CType -> CType substType mk mt mtv = go where go (TApp k t ts) = TApp (goKind k) (go t) (map go ts) @@ -783,8 +778,7 @@ substType mk mt mtv = go goKind = substKind mk -substKind :: HasCallStack - => Map Int CKind -> CKind -> CKind +substKind :: Map Int CKind -> CKind -> CKind substKind m = \case KType () -> KType () KFun () k1 k2 -> KFun () (substKind m k1) (substKind m k2) @@ -793,7 +787,84 @@ substKind m = \case -------------------- FINALISATION FUNCTIONS -------------------- -- These report free type unification variables. --- TODO the finalise* functions +finaliseProg :: MonadRaise m => CProgram -> m TProgram +finaliseProg (Program ds fs) = + Program <$> traverse finaliseDdef ds <*> traverse finaliseFdef fs + +finaliseDdef :: MonadRaise m => CDataDef -> m TDataDef +finaliseDdef (DataDef k name pars cons) = + DataDef <$> finaliseKind k <*> pure name + <*> traverse (firstM finaliseKind) pars + <*> traverse (secondM (traverse finaliseDataField)) cons + +finaliseDataField :: MonadRaise m => CDataField -> m TDataField +finaliseDataField (DataField rng t) = DataField rng <$> finaliseType rng t + +finaliseFdef :: MonadRaise m => CFunDef -> m TFunDef +finaliseFdef (FunDef rng n (TypeSig msigrng sig) eqs) = + FunDef () n + <$> (TypeSig () <$> finaliseType (fromMaybe rng msigrng) sig) + <*> traverse finaliseFunEq eqs + +finaliseFunEq :: MonadRaise m => CFunEq -> m TFunEq +finaliseFunEq (FunEq () n ps rhs) = + FunEq () n + <$> traverse finalisePattern ps + <*> finaliseRHS rhs + +finaliseRHS :: MonadRaise m => CRHS -> m TRHS +finaliseRHS (Guarded _ _) = error "typecheck: guards unsupported" +finaliseRHS (Plain t e) = Plain <$> finaliseType (fst (extOf e)) t <*> finaliseExpr e + +finalisePattern :: MonadRaise m => CPattern -> m TPattern +finalisePattern = \case + PWildcard e -> PWildcard <$> goExt e + PVar e n -> PVar <$> goExt e <*> pure n + PAs e n p -> PAs <$> goExt e <*> pure n <*> finalisePattern p + PCon e n ps -> PCon <$> goExt e <*> pure n <*> traverse finalisePattern ps + POp e p1 op p2 -> POp <$> goExt e <*> finalisePattern p1 <*> pure op <*> finalisePattern p2 + PList e ps -> PList <$> goExt e <*> traverse finalisePattern ps + PTup e ps -> PTup <$> goExt e <*> traverse finalisePattern ps + where + goExt (rng, t) = finaliseType rng t + +finaliseExpr :: MonadRaise m => CExpr -> m TExpr +finaliseExpr = \case + ELit e lit -> ELit <$> goExt e <*> pure lit + EVar e n -> EVar <$> goExt e <*> pure n + ECon e n -> ECon <$> goExt e <*> pure n + EList e es -> EList <$> goExt e <*> traverse finaliseExpr es + ETup e es -> ETup <$> goExt e <*> traverse finaliseExpr es + EApp e e1 es -> EApp <$> goExt e <*> finaliseExpr e1 <*> traverse finaliseExpr es + EOp e e1 op e2 -> EOp <$> goExt e <*> finaliseExpr e1 <*> pure op <*> finaliseExpr e2 + EIf e e1 e2 e3 -> EIf <$> goExt e <*> finaliseExpr e1 <*> finaliseExpr e2 <*> finaliseExpr e3 + ECase e e1 alts -> ECase <$> goExt e <*> finaliseExpr e1 <*> traverse (bimapM finalisePattern finaliseRHS) alts + ELet e defs body -> ELet <$> goExt e <*> traverse finaliseFdef defs <*> finaliseExpr body + EError e -> EError <$> goExt e + where + goExt (rng, t) = finaliseType rng t + +finaliseType :: MonadRaise m => Range -> CType -> m TType +finaliseType rng toptype = go toptype + where + go (TApp k t ts) = TApp <$> finaliseKind k <*> go t <*> traverse go ts + go (TTup k ts) = TTup <$> finaliseKind k <*> traverse go ts + go (TList k t) = TList <$> finaliseKind k <*> go t + go (TFun k t1 t2) = TFun <$> finaliseKind k <*> go t1 <*> go t2 + go (TCon k n) = TCon <$> finaliseKind k <*> pure n + go (TVar k n) = TVar <$> finaliseKind k <*> pure n + go (TForall k n t) = TForall <$> finaliseKind k <*> pure n <*> go t + go t@(TExt k TUniVar{}) = do + raise SError rng $ "Ambiguous type unification variable " ++ pretty t ++ " in type: " ++ pretty toptype + TVar <$> finaliseKind k <*> pure (Name "$_error") + +finaliseKind :: MonadRaise m => CKind -> m TKind +finaliseKind = \case + KType () -> pure (KType ()) + KFun () k1 k2 -> KFun () <$> finaliseKind k1 <*> finaliseKind k2 + k@(KExt () KUniVar{}) -> error $ "Unresolved kind variable: " ++ pretty k + +-------------------- END OF FINALISATION FUNCTIONS -------------------- typeUniVars :: CType -> Set Int typeUniVars = \case @@ -817,12 +888,21 @@ allEq l = case toList l of [] -> True x : xs -> all (== x) xs -funeqPats :: FunEq t -> [Pattern t] +funeqPats :: FunEq s -> [Pattern s] funeqPats (FunEq _ _ pats _) = pats +dataFieldType :: DataField s -> Type s +dataFieldType (DataField _ t) = t + isCEqK :: Constr -> Maybe (CKind, CKind, Range) isCEqK (CEqK k1 k2 rng) = Just (k1, k2, rng) isCEqK _ = Nothing -foldMapM :: (Applicative f, Monoid m, Foldable t) => (a -> f m) -> t a -> f m -foldMapM f = getAp . foldMap (Ap . f) +firstM :: Functor f => (a -> f b) -> (a, c) -> f (b, c) +firstM f (x, y) = (,y) <$> f x + +secondM :: Functor f => (b -> f c) -> (a, b) -> f (a, c) +secondM f (x, y) = (x,) <$> f y + +bimapM :: Applicative f => (a -> f b) -> (c -> f d) -> (a, c) -> f (b, d) +bimapM f g (x, y) = (,) <$> f x <*> g y -- cgit v1.2.3-70-g09d2