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 (Consts_of_Ifaces is) h)
  67    (Term is h)
  68
  69 -- * Type 'Compile'
  70 -- | Convenient type synonym 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' minus 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 (Consts_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 'Consts_of_Ifaces'
 143 type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)
 144
 145 -- ** Type family 'Consts_of_IfaceR'
 146 type family Consts_of_IfaceR (is::[*]) where
 147         Consts_of_IfaceR '[] = '[]
 148         Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
 149
 150 -- ** Type family 'Consts_of_Iface'
 151 type family   Consts_of_Iface (i:: *) :: [*]
 152 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
 153
 154 -- * Type 'LamCtx_Type'
 155 -- | GADT for a typing context,
 156 -- accumulating an @item@ at each lambda;
 157 -- used to accumulate object-types (in 'Expr_From')
 158 -- or host-terms (in 'HostI')
 159 -- associated with the 'LamVar's in scope.
 160 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
 161         LamCtx_TypeZ :: LamCtx_Type is name '[]
 162         LamCtx_TypeS :: name
 163                      -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 164                      -> LamCtx_Type is name hs
 165                      -> LamCtx_Type is name (h ': hs)
 166 infixr 5 `LamCtx_TypeS`
 167
 168 -- * Type 'LamCtx_Term'
 169 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 170         LamCtx_TermZ :: LamCtx_Term term '[]
 171         LamCtx_TermS :: term h
 172                      -> LamCtx_Term term hs
 173                      -> LamCtx_Term term (h ': hs)
 174 infixr 5 `LamCtx_TermS`
 175
 176 -- * Type 'Error_Term'
 177 data Error_Term meta (is::[*])
 178  =   Error_Term_unbound Term_Name
 179  |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
 180  |   Error_Term_Constraint_Type
 181      (Either
 182        (Constraint_Type meta '[Proxy Token_Type] (Consts_of_Ifaces is))
 183        (Constraint_Type meta is (Consts_of_Ifaces is)))
 184  |   Error_Term_Constraint_Kind (Constraint_Kind meta is)
 185 deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
 186 deriving instance (Show meta, Show_Token meta is, Show_Const (Consts_of_Ifaces is)) => Show (Error_Term meta is)
 187
 188 -- * Type 'Constraint_Type'
 189 data Constraint_Type meta ts cs
 190  =   Constraint_Type_Eq  (Either (At meta '[Proxy Token_Type] (EType cs))
 191                                  (At meta ts (EType cs)))
 192                          (At meta ts (EType cs))
 193  |   Constraint_Type_App (At meta ts (EType cs))
 194  |   Constraint_Type_Con (At meta ts (KType cs Constraint))
 195  |   Constraint_Type_Fam (At meta ts Name_Fam) [EType cs]
 196 deriving instance
 197  ( Eq meta
 198  , Eq_Token meta ts
 199  ) => Eq (Constraint_Type meta ts cs)
 200 deriving instance
 201  ( Show meta
 202  , Show_Token meta ts
 203  , Show_Const cs
 204  ) => Show (Constraint_Type meta ts cs)
 205
 206 instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
 207         olift = Error_Term_Typing . olift
 208 instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
 209         olift = Prelude.id
 210 instance
 211  cs ~ Consts_of_Ifaces is =>
 212  MonoLift (Constraint_Type meta is cs) (Error_Term meta is) where
 213         olift = Error_Term_Constraint_Type . Right
 214 instance
 215  cs ~ Consts_of_Ifaces is =>
 216  MonoLift (Constraint_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
 217         olift = Error_Term_Constraint_Type . Left
 218 instance MonoLift (Constraint_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
 219         olift = Error_Term_Typing . Error_Type_Constraint_Kind
 220 instance MonoLift (Constraint_Kind meta is) (Error_Term meta is) where
 221         olift = Error_Term_Constraint_Kind
 222
 223 -- ** Checks
 224 check_type
 225  :: MonoLift (Constraint_Type meta ts cs) err
 226  => At meta ts (Type cs x)
 227  -> At meta ts (Type cs y)
 228  -> ((x :~: y) -> Either err ret) -> Either err ret
 229 check_type x y k =
 230         case unAt x `eq_type` unAt y of
 231          Just Refl -> k Refl
 232          Nothing -> Left $ olift $
 233                 Constraint_Type_Eq (Right $ EType <$> x) (EType <$> y)
 234
 235 check_type_is
 236  :: MonoLift (Constraint_Type meta ts cs) err
 237  => At meta '[Proxy Token_Type] (Type cs x)
 238  -> At meta ts (Type cs y)
 239  -> ((x :~: y) -> Either err ret) -> Either err ret
 240 check_type_is x y k =
 241         case unAt x `eq_type` unAt y of
 242          Just Refl -> k Refl
 243          Nothing -> Left $ olift $
 244                 Constraint_Type_Eq (Left $ EType <$> x) (EType <$> y)
 245
 246 check_type_app
 247  :: MonoLift (Constraint_Type meta ts cs) err
 248  => At meta ts (Type cs (fa::kfa))
 249  -> (forall ka f a. (fa :~: f a)
 250   -> Type cs (f::ka -> kfa)
 251   -> Type cs (a::ka)
 252   -> Either err ret)
 253  -> Either err ret
 254 check_type_app typ k =
 255         case unAt typ of
 256          a :$ b -> k Refl a b
 257          _ -> Left $ olift $
 258                 Constraint_Type_App (EType <$> typ)
 259
 260 check_type1
 261  :: ( MonoLift (Constraint_Type meta ts cs) err
 262     , MonoLift (Constraint_Kind meta ts) err )
 263  => Type cs (f:: * -> *)
 264  -> At meta ts (Type cs fa)
 265  -> (forall a. (fa :~: f a)
 266   -> Type cs a
 267   -> Either err ret)
 268  -> Either err ret
 269 check_type1 typ ty_fa k =
 270         check_type_app ty_fa $ \Refl ty_f ty_a ->
 271         check_kind
 272          (At Nothing $ SKiType `SKiArrow` SKiType)
 273          (kind_of ty_f <$ ty_fa) $ \Refl ->
 274         check_type
 275          (At Nothing typ)
 276          (ty_f <$ ty_fa) $ \Refl ->
 277         k Refl ty_a
 278
 279 check_type2
 280  :: ( MonoLift (Constraint_Type meta ts cs) err
 281     , MonoLift (Constraint_Kind meta ts) err )
 282  => Type cs (f:: * -> * -> *)
 283  -> At meta ts (Type cs fab)
 284  -> (forall a b. (fab :~: f a b)
 285   -> Type cs a
 286   -> Type cs b
 287   -> Either err ret)
 288  -> Either err ret
 289 check_type2 typ ty_fab k =
 290         check_type_app ty_fab            $ \Refl ty_fa ty_b ->
 291         check_type_app (ty_fa <$ ty_fab) $ \Refl ty_f  ty_a ->
 292         check_kind
 293          (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 294          (kind_of ty_f <$ ty_fab) $ \Refl ->
 295         check_type
 296          (At Nothing typ)
 297          (ty_f <$ ty_fab) $ \Refl ->
 298         k Refl ty_a ty_b
 299
 300 check_con
 301  :: ( Proj_Con cs
 302     , MonoLift (Constraint_Type meta ts cs) err )
 303  => At meta ts (Type cs (q::Constraint))
 304  -> (Con q -> Either err ret)
 305  -> Either err ret
 306 check_con typ k =
 307         case proj_con $ unAt typ of
 308          Just Con -> k Con
 309          Nothing -> Left $ olift $
 310                 Constraint_Type_Con (KType <$> typ)
 311
 312 check_con1
 313  :: ( Proj_Con cs
 314     , MonoLift (Constraint_Type meta ts cs) err
 315     , MonoLift (Constraint_Kind meta ts) err )
 316  => Type cs con
 317  -> At meta ts (Type cs (fa:: *))
 318  -> (forall f a. (fa :~: f a)
 319   -> Con (con f)
 320   -> Type cs (f:: * -> *)
 321   -> Type cs (a:: *)
 322   -> Either err ret)
 323  -> Either err ret
 324 check_con1 con ty_fa k =
 325         check_type_app ty_fa $ \Refl ty_f ty_a ->
 326         check_kind
 327          (At Nothing (SKiType `SKiArrow` SKiType))
 328          (kind_of ty_f <$ ty_fa) $ \Refl ->
 329         check_con ((con :$ ty_f) <$ ty_fa) $ \Con ->
 330         k Refl Con ty_f ty_a
 331
 332 check_fam
 333  :: ( MonoLift (Constraint_Type meta ts cs) err
 334     , Proj_Fam cs fam
 335     , Show fam )
 336  => At meta ts fam
 337  -> Types cs hs
 338  -> (Type cs (Fam fam hs) -> Either err ret)
 339  -> Either err ret
 340 check_fam fam tys k =
 341         case proj_fam (unAt fam) tys of
 342          Just t -> k t
 343          Nothing -> Left $ olift $
 344                 Constraint_Type_Fam
 345                  (Text.pack . show <$> fam)
 346                  (etypes tys)