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 cs is
  65  = forall (h::Kind.Type). ETerm
  66    (Type cs h)
  67    (Term is h)
  68
  69 -- * Type 'Compile'
  70 -- | Convenient class wrapping 'CompileR' to initiate its recursion.
  71 class Compile cs is where
  72         compileO :: EToken meta is -> CompileT meta ctx ret cs is '[] is
  73 instance CompileR cs is '[] is => Compile cs 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 cs is
  79  => EToken meta is
  80  -> Either (Error_Term meta cs is) (ETerm cs 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 cs is ls rs
  88  = LamCtx_Type cs 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 cs (h::Kind.Type)
  94     -> TermO ctx h is ls rs
  95     -> Either (Error_Term meta cs is) ret )
  96  -- ^ The accumulating continuation called bottom-up.
  97  -> Either (Error_Term meta cs 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 (cs::[*]) (is::[*]) (ls::[*]) (rs::[*]) where
 107         compileR :: TokenR meta is rs i -> CompileT meta ctx ret cs 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 cs is i
 114  , CompileR cs is (i ': ls) (r ': rs)
 115  ) => CompileR cs 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 cs is i =>
 125  CompileR cs 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 (cs::[*]) (is::[*]) (i:: *) where
 132         compileI :: TokenT meta is i -> CompileT meta ctx ret cs 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 (cs::[*]) (is::[*]) (name:: *) (ctx::[*]) where
 160         LamCtx_TypeZ :: LamCtx_Type cs is name '[]
 161         LamCtx_TypeS :: name
 162                      -> Type cs (h::Kind.Type)
 163                      -> LamCtx_Type cs is name hs
 164                      -> LamCtx_Type cs 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 (cs::[*]) (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 cs '[Proxy Token_Type])
 182        (Con_Type meta cs is))
 183  |   Error_Term_Con_Kind (Con_Kind meta is)
 184 deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta cs is)
 185 deriving instance (Show meta, Show_Token meta is, Show_TyConst cs) => Show (Error_Term meta cs is)
 186
 187 -- * Type 'Con_Type'
 188 data Con_Type meta cs ts
 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 cs ts)
 199 deriving instance
 200  ( Show meta
 201  , Show_Token meta ts
 202  , Show_TyConst cs
 203  ) => Show (Con_Type meta cs ts)
 204
 205 instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta cs ts) where
 206         olift = Error_Term_Typing . olift
 207 instance MonoLift (Error_Term meta cs ts) (Error_Term meta cs ts) where
 208         olift = id
 209 instance
 210  MonoLift (Con_Type meta cs is) (Error_Term meta cs is) where
 211         olift = Error_Term_Con_Type . Right
 212 instance
 213  MonoLift (Con_Type meta cs '[Proxy Token_Type]) (Error_Term meta cs is) where
 214         olift = Error_Term_Con_Type . Left
 215 instance MonoLift (Con_Kind meta '[Proxy Token_Type]) (Error_Term meta cs is) where
 216         olift = Error_Term_Typing . Error_Type_Con_Kind
 217 instance MonoLift (Con_Kind meta is) (Error_Term meta cs is) where
 218         olift = Error_Term_Con_Kind
 219
 220 -- ** Checks
 221 check_TyEq
 222  :: MonoLift (Con_Type meta cs ts) err
 223  => At meta ts (Type cs x)
 224  -> At meta ts (Type cs y)
 225  -> ((x :~: y) -> Either err ret) -> Either err ret
 226 check_TyEq x y k =
 227         case unAt x `eq_Type` unAt y of
 228          Just Refl -> k Refl
 229          Nothing -> Left $ olift $
 230                 Con_TyEq (Right $ EType <$> x) (EType <$> y)
 231
 232 check_Type_is
 233  :: MonoLift (Con_Type meta cs ts) err
 234  => At meta '[Proxy Token_Type] (Type cs x)
 235  -> At meta ts (Type cs y)
 236  -> ((x :~: y) -> Either err ret) -> Either err ret
 237 check_Type_is x y k =
 238         case unAt x `eq_Type` unAt y of
 239          Just Refl -> k Refl
 240          Nothing -> Left $ olift $
 241                 Con_TyEq (Left $ EType <$> x) (EType <$> y)
 242
 243 check_TyApp
 244  :: MonoLift (Con_Type meta cs ts) err
 245  => At meta ts (Type cs (fa::kfa))
 246  -> (forall ka f a. (fa :~: f a)
 247   -> Type cs (f::ka -> kfa)
 248   -> Type cs (a::ka)
 249   -> Either err ret)
 250  -> Either err ret
 251 check_TyApp typ k =
 252         case unAt typ of
 253          a :$ b -> k Refl a b
 254          _ -> Left $ olift $
 255                 Con_TyApp (EType <$> typ)
 256
 257 check_TyEq1
 258  :: ( MonoLift (Con_Type meta cs ts) err
 259     , MonoLift (Con_Kind meta ts) err )
 260  => Type cs (f:: * -> *)
 261  -> At meta ts (Type cs fa)
 262  -> (forall a. (fa :~: f a)
 263   -> Type cs a
 264   -> Either err ret)
 265  -> Either err ret
 266 check_TyEq1 typ ty_fa k =
 267         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 268         check_Kind
 269          (At Nothing $ SKiType `SKiArrow` SKiType)
 270          (kind_of ty_f <$ ty_fa) $ \Refl ->
 271         check_TyEq
 272          (At Nothing typ)
 273          (ty_f <$ ty_fa) $ \Refl ->
 274         k Refl ty_a
 275
 276 check_TyEq2
 277  :: ( MonoLift (Con_Type meta cs ts) err
 278     , MonoLift (Con_Kind meta ts) err )
 279  => Type cs (f:: * -> * -> *)
 280  -> At meta ts (Type cs fab)
 281  -> (forall a b. (fab :~: f a b)
 282   -> Type cs a
 283   -> Type cs b
 284   -> Either err ret)
 285  -> Either err ret
 286 check_TyEq2 typ ty_fab k =
 287         check_TyApp ty_fab            $ \Refl ty_fa ty_b ->
 288         check_TyApp (ty_fa <$ ty_fab) $ \Refl ty_f  ty_a ->
 289         check_Kind
 290          (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 291          (kind_of ty_f <$ ty_fab) $ \Refl ->
 292         check_TyEq
 293          (At Nothing typ)
 294          (ty_f <$ ty_fab) $ \Refl ->
 295         k Refl ty_a ty_b
 296
 297 check_TyCon
 298  :: ( Proj_TyCon cs
 299     , MonoLift (Con_Type meta cs ts) err )
 300  => At meta ts (Type cs (q::Constraint))
 301  -> (TyCon q -> Either err ret)
 302  -> Either err ret
 303 check_TyCon typ k =
 304         case proj_TyCon $ unAt typ of
 305          Just TyCon -> k TyCon
 306          Nothing -> Left $ olift $
 307                 Con_TyCon (KType <$> typ)
 308
 309 check_TyCon1
 310  :: ( Proj_TyCon cs
 311     , MonoLift (Con_Type meta cs ts) err
 312     , MonoLift (Con_Kind meta ts) err )
 313  => Type cs con
 314  -> At meta ts (Type cs (fa:: *))
 315  -> (forall f a. (fa :~: f a)
 316   -> TyCon (con f)
 317   -> Type cs (f:: * -> *)
 318   -> Type cs (a:: *)
 319   -> Either err ret)
 320  -> Either err ret
 321 check_TyCon1 con ty_fa k =
 322         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 323         check_Kind
 324          (At Nothing (SKiType `SKiArrow` SKiType))
 325          (kind_of ty_f <$ ty_fa) $ \Refl ->
 326         check_TyCon ((con :$ ty_f) <$ ty_fa) $ \TyCon ->
 327         k Refl TyCon ty_f ty_a
 328
 329 check_TyFam
 330  :: ( MonoLift (Con_Type meta cs ts) err
 331     , Proj_TyFam cs fam
 332     , Show fam )
 333  => At meta ts fam
 334  -> Types cs hs
 335  -> (Type cs (TyFam fam hs) -> Either err ret)
 336  -> Either err ret
 337 check_TyFam fam tys k =
 338         case proj_TyFam (unAt fam) tys of
 339          Just t -> k t
 340          Nothing -> Left $ olift $
 341                 Con_TyFam
 342                  (Text.pack . show <$> fam)
 343                  (eTypes tys)