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 +++++++++++++++++++++++++++++-------------------------- 1 file changed, 92 insertions(+), 80 deletions(-) (limited to 'src/HSVIS/AST.hs') 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) -- cgit v1.2.3-70-g09d2