typechecker

1 files changed, 92 insertions, 80 deletions

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)