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