symantic/Language/Symantic/Compiling/Term.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6 module Language.Symantic.Compiling.Term
   7  ( module Language.Symantic.Compiling.Term
   8  , module Language.Symantic.Compiling.Term.Grammar
   9  ) where
  10
  11 import qualified Data.Kind as Kind
  12 import Data.Proxy (Proxy(..))
  13 import qualified Data.Text as Text
  14 import Data.Type.Equality ((:~:)(..))
  15 import GHC.Exts (Constraint)
  16
  17 import Language.Symantic.Helper.Data.Type.List
  18 import Language.Symantic.Parsing
  19 import Language.Symantic.Typing
  20
  21 import Language.Symantic.Compiling.Term.Grammar
  22
  23 -- * Type 'Term'
  24 -- | Closed 'TermO'.
  25 data Term is h
  26  =   Term
  27  (forall term. ( Sym_of_Ifaces is term
  28                , Sym_of_Iface (Proxy (->)) term
  29                ) => term h)
  30
  31 -- ** Type 'TermO'
  32 -- | An open term (i.e. with a /lambda context/).
  33 -- The data type wraps a universal quantification
  34 -- over an interpreter @term@
  35 -- qualified by the symantics of a term.
  36 --
  37 -- Moreover the term is abstracted by a 'LamCtx_Term'
  38 -- built top-down by 'compileO',
  39 -- to enable a /Higher-Order Abstract Syntax/ (HOAS)
  40 -- for /lambda abstractions/ ('lam').
  41 --
  42 -- This data type is used to keep a parsed term polymorphic enough
  43 -- to stay interpretable by different interpreters.
  44 --
  45 -- * @(@'Sym_of_Ifaces'@ is term)@
  46 -- is needed when a symantic method includes a polymorphic type
  47 -- and thus calls: 'compileO'.
  48 --
  49 -- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
  50 -- make a zipper needed to be able to write the recursing 'CompileR' instance.
  51 --
  52 -- * @(@'Sym_of_Iface'@ (@'Proxy'@ (->)) term)@
  53 -- is needed to handle partially applied functions.
  54 data TermO ctx h is ls rs
  55  =   TermO
  56  (forall term. ( Sym_of_Ifaces is term
  57                , Sym_of_Ifaces ls term
  58                , Sym_of_Ifaces rs term
  59                , Sym_of_Iface (Proxy (->)) term
  60                ) => LamCtx_Term term ctx -> term h)
  61
  62 -- * Type 'ETerm'
  63 -- | Existential 'Term', with its 'Type'.
  64 data ETerm is
  65  = forall (h::Kind.Type). ETerm
  66    (Type (TyConsts_of_Ifaces is) h)
  67    (Term is h)
  68
  69 -- * Type 'Compile'
  70 -- | Convenient class wrapping 'CompileR' to initiate its recursion.
  71 class Compile is where
  72         compileO :: EToken meta is -> CompileT meta ctx ret is '[] is
  73 instance CompileR is '[] is => Compile is where
  74         compileO (EToken tok) = compileR tok
  75
  76 -- | Like 'compileO' but for a term with an empty /lambda context/.
  77 compile
  78  :: Compile is
  79  => EToken meta is
  80  -> Either (Error_Term meta is) (ETerm is)
  81 compile tok =
  82         compileO tok LamCtx_TypeZ $ \typ (TermO te) ->
  83         Right $ ETerm typ $ Term $ te LamCtx_TermZ
  84
  85 -- ** Type 'CompileT'
  86 -- | Convenient type synonym defining a term parser.
  87 type CompileT meta ctx ret is ls rs
  88  = LamCtx_Type is Term_Name ctx
  89  -- ^ The bound variables in scope and their types:
  90  -- built top-down in the heterogeneous list @ctx@,
  91  -- from the closest including /lambda abstraction/ to the farest.
  92  -> ( forall h.
  93        Type (TyConsts_of_Ifaces is) (h::Kind.Type)
  94     -> TermO ctx h is ls rs
  95     -> Either (Error_Term meta is) ret )
  96  -- ^ The accumulating continuation called bottom-up.
  97  -> Either (Error_Term meta is) ret
  98
  99 -- ** Class 'CompileR'
 100 -- | Intermediate type class to construct an instance of 'Compile'
 101 -- from many instances of 'CompileI', one for each item of @is@.
 102 --
 103 -- * @is@: starting  list of /term constants/.
 104 -- * @ls@: done      list of /term constants/.
 105 -- * @rs@: remaining list of /term constants/.
 106 class CompileR (is::[*]) (ls::[*]) (rs::[*]) where
 107         compileR :: TokenR meta is rs i -> CompileT meta ctx ret is ls rs
 108
 109 -- | Recurse into into the given 'TokenR'
 110 -- to call the 'compileI' instance associated
 111 -- to the 'TokenT' it contains.
 112 instance
 113  ( CompileI is i
 114  , CompileR is (i ': ls) (r ': rs)
 115  ) => CompileR is ls (i ': r ': rs) where
 116         compileR tok ctx k =
 117                 case tok of
 118                  TokenZ _m t -> compileI t ctx k
 119                  TokenS t ->
 120                         compileR t ctx $ \typ (TermO te :: TermO ctx h is (i ': ls) (r ': rs)) ->
 121                                 k typ (TermO te :: TermO ctx h is ls (i ': r ': rs))
 122 -- | End the recursion.
 123 instance
 124  CompileI is i =>
 125  CompileR is ls (i ': '[]) where
 126         compileR (TokenZ _m t) ctx k = compileI t ctx k
 127         compileR TokenS{} _ctx _k = error "Oops, the impossible happened..."
 128
 129 -- ** Class 'CompileI'
 130 -- | Handle the work of 'Compile' for a given /interface/ @i@.
 131 class CompileI (is::[*]) (i:: *) where
 132         compileI :: TokenT meta is i -> CompileT meta ctx ret is ls (i ': rs)
 133
 134 -- * Type family 'Sym_of_Ifaces'
 135 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
 136         Sym_of_Ifaces '[] term = ()
 137         Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
 138
 139 -- ** Type family 'Sym_of_Iface'
 140 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
 141
 142 -- * Type 'TyConsts_of_Ifaces'
 143 type TyConsts_of_Ifaces is = {-Nub-} (TyConsts_of_IfaceR is)
 144
 145 -- ** Type family 'TyConsts_of_IfaceR'
 146 type family TyConsts_of_IfaceR (is::[*]) where
 147         TyConsts_of_IfaceR '[] = '[]
 148         TyConsts_of_IfaceR (i ': is) = TyConsts_of_Iface i ++ TyConsts_of_IfaceR is
 149
 150 -- ** Type family 'TyConsts_of_Iface'
 151 type family TyConsts_of_Iface (i:: *) :: [*]
 152
 153 -- * Type 'LamCtx_Type'
 154 -- | GADT for a typing context,
 155 -- accumulating an @item@ at each lambda;
 156 -- used to accumulate object-types (in 'Expr_From')
 157 -- or host-terms (in 'HostI')
 158 -- associated with the 'LamVar's in scope.
 159 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
 160         LamCtx_TypeZ :: LamCtx_Type is name '[]
 161         LamCtx_TypeS :: name
 162                      -> Type (TyConsts_of_Ifaces is) (h::Kind.Type)
 163                      -> LamCtx_Type is name hs
 164                      -> LamCtx_Type is name (h ': hs)
 165 infixr 5 `LamCtx_TypeS`
 166
 167 -- * Type 'LamCtx_Term'
 168 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 169         LamCtx_TermZ :: LamCtx_Term term '[]
 170         LamCtx_TermS :: term h
 171                      -> LamCtx_Term term hs
 172                      -> LamCtx_Term term (h ': hs)
 173 infixr 5 `LamCtx_TermS`
 174
 175 -- * Type 'Error_Term'
 176 data Error_Term meta (is::[*])
 177  =   Error_Term_unbound Term_Name
 178  |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
 179  |   Error_Term_Con_Type
 180      (Either
 181        (Con_Type meta '[Proxy Token_Type] (TyConsts_of_Ifaces is))
 182        (Con_Type meta is (TyConsts_of_Ifaces is)))
 183  |   Error_Term_Con_Kind (Con_Kind meta is)
 184 deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
 185 deriving instance (Show meta, Show_Token meta is, Show_TyConst (TyConsts_of_Ifaces is)) => Show (Error_Term meta is)
 186
 187 -- * Type 'Con_Type'
 188 data Con_Type meta ts cs
 189  =   Con_TyEq  (Either (At meta '[Proxy Token_Type] (EType cs))
 190                        (At meta ts (EType cs)))
 191                (At meta ts (EType cs))
 192  |   Con_TyApp (At meta ts (EType cs))
 193  |   Con_TyCon (At meta ts (KType cs Constraint))
 194  |   Con_TyFam (At meta ts TyFamName) [EType cs]
 195 deriving instance
 196  ( Eq meta
 197  , Eq_Token meta ts
 198  ) => Eq (Con_Type meta ts cs)
 199 deriving instance
 200  ( Show meta
 201  , Show_Token meta ts
 202  , Show_TyConst cs
 203  ) => Show (Con_Type meta ts cs)
 204
 205 instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
 206         olift = Error_Term_Typing . olift
 207 instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
 208         olift = id
 209 instance
 210  cs ~ TyConsts_of_Ifaces is =>
 211  MonoLift (Con_Type meta is cs) (Error_Term meta is) where
 212         olift = Error_Term_Con_Type . Right
 213 instance
 214  cs ~ TyConsts_of_Ifaces is =>
 215  MonoLift (Con_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
 216         olift = Error_Term_Con_Type . Left
 217 instance MonoLift (Con_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
 218         olift = Error_Term_Typing . Error_Type_Con_Kind
 219 instance MonoLift (Con_Kind meta is) (Error_Term meta is) where
 220         olift = Error_Term_Con_Kind
 221
 222 -- ** Checks
 223 check_TyEq
 224  :: MonoLift (Con_Type meta ts cs) err
 225  => At meta ts (Type cs x)
 226  -> At meta ts (Type cs y)
 227  -> ((x :~: y) -> Either err ret) -> Either err ret
 228 check_TyEq x y k =
 229         case unAt x `eq_Type` unAt y of
 230          Just Refl -> k Refl
 231          Nothing -> Left $ olift $
 232                 Con_TyEq (Right $ EType <$> x) (EType <$> y)
 233
 234 check_Type_is
 235  :: MonoLift (Con_Type meta ts cs) err
 236  => At meta '[Proxy Token_Type] (Type cs x)
 237  -> At meta ts (Type cs y)
 238  -> ((x :~: y) -> Either err ret) -> Either err ret
 239 check_Type_is x y k =
 240         case unAt x `eq_Type` unAt y of
 241          Just Refl -> k Refl
 242          Nothing -> Left $ olift $
 243                 Con_TyEq (Left $ EType <$> x) (EType <$> y)
 244
 245 check_TyApp
 246  :: MonoLift (Con_Type meta ts cs) err
 247  => At meta ts (Type cs (fa::kfa))
 248  -> (forall ka f a. (fa :~: f a)
 249   -> Type cs (f::ka -> kfa)
 250   -> Type cs (a::ka)
 251   -> Either err ret)
 252  -> Either err ret
 253 check_TyApp typ k =
 254         case unAt typ of
 255          a :$ b -> k Refl a b
 256          _ -> Left $ olift $
 257                 Con_TyApp (EType <$> typ)
 258
 259 check_TyEq1
 260  :: ( MonoLift (Con_Type meta ts cs) err
 261     , MonoLift (Con_Kind meta ts) err )
 262  => Type cs (f:: * -> *)
 263  -> At meta ts (Type cs fa)
 264  -> (forall a. (fa :~: f a)
 265   -> Type cs a
 266   -> Either err ret)
 267  -> Either err ret
 268 check_TyEq1 typ ty_fa k =
 269         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 270         check_Kind
 271          (At Nothing $ SKiType `SKiArrow` SKiType)
 272          (kind_of ty_f <$ ty_fa) $ \Refl ->
 273         check_TyEq
 274          (At Nothing typ)
 275          (ty_f <$ ty_fa) $ \Refl ->
 276         k Refl ty_a
 277
 278 check_TyEq2
 279  :: ( MonoLift (Con_Type meta ts cs) err
 280     , MonoLift (Con_Kind meta ts) err )
 281  => Type cs (f:: * -> * -> *)
 282  -> At meta ts (Type cs fab)
 283  -> (forall a b. (fab :~: f a b)
 284   -> Type cs a
 285   -> Type cs b
 286   -> Either err ret)
 287  -> Either err ret
 288 check_TyEq2 typ ty_fab k =
 289         check_TyApp ty_fab            $ \Refl ty_fa ty_b ->
 290         check_TyApp (ty_fa <$ ty_fab) $ \Refl ty_f  ty_a ->
 291         check_Kind
 292          (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 293          (kind_of ty_f <$ ty_fab) $ \Refl ->
 294         check_TyEq
 295          (At Nothing typ)
 296          (ty_f <$ ty_fab) $ \Refl ->
 297         k Refl ty_a ty_b
 298
 299 check_TyCon
 300  :: ( Proj_TyCon cs
 301     , MonoLift (Con_Type meta ts cs) err )
 302  => At meta ts (Type cs (q::Constraint))
 303  -> (TyCon q -> Either err ret)
 304  -> Either err ret
 305 check_TyCon typ k =
 306         case proj_TyCon $ unAt typ of
 307          Just TyCon -> k TyCon
 308          Nothing -> Left $ olift $
 309                 Con_TyCon (KType <$> typ)
 310
 311 check_TyCon1
 312  :: ( Proj_TyCon cs
 313     , MonoLift (Con_Type meta ts cs) err
 314     , MonoLift (Con_Kind meta ts) err )
 315  => Type cs con
 316  -> At meta ts (Type cs (fa:: *))
 317  -> (forall f a. (fa :~: f a)
 318   -> TyCon (con f)
 319   -> Type cs (f:: * -> *)
 320   -> Type cs (a:: *)
 321   -> Either err ret)
 322  -> Either err ret
 323 check_TyCon1 con ty_fa k =
 324         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 325         check_Kind
 326          (At Nothing (SKiType `SKiArrow` SKiType))
 327          (kind_of ty_f <$ ty_fa) $ \Refl ->
 328         check_TyCon ((con :$ ty_f) <$ ty_fa) $ \TyCon ->
 329         k Refl TyCon ty_f ty_a
 330
 331 check_TyFam
 332  :: ( MonoLift (Con_Type meta ts cs) err
 333     , Proj_TyFam cs fam
 334     , Show fam )
 335  => At meta ts fam
 336  -> Types cs hs
 337  -> (Type cs (TyFam fam hs) -> Either err ret)
 338  -> Either err ret
 339 check_TyFam fam tys k =
 340         case proj_TyFam (unAt fam) tys of
 341          Just t -> k t
 342          Nothing -> Left $ olift $
 343                 Con_TyFam
 344                  (Text.pack . show <$> fam)
 345                  (eTypes tys)