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_IfacesR is)
 179
 180 -- ** Type family 'TyConsts_of_IfacesR'
 181 type family TyConsts_of_IfacesR (is::[*]) where
 182         TyConsts_of_IfacesR '[] = '[]
 183         TyConsts_of_IfacesR (i ': is) = TyConsts_of_Iface i ++ TyConsts_of_IfacesR is
 184
 185 {- NOTE: failed attempt to recursively collect TyConsts.
 186 -- ** Type family 'TyConsts_imported_byR'
 187 type family TyConsts_imported_byR (done::[*]) (cs::[*]) where
 188         TyConsts_imported_byR done '[] = done
 189         TyConsts_imported_byR done (c ': cs) =
 190                 If (Exists c done)
 191                  (TyConsts_imported_byR done cs)
 192                  (TyConsts_imported_byR (c ': done) (TyConsts_imported_by c ++ TyConsts_imported_byR done cs))
 193 -}
 194
 195 -- ** Type family 'TyConsts_of_Iface'
 196 type family TyConsts_of_Iface (i:: *) :: [*]
 197
 198 -- ** Type family 'TyConsts_imported_by'
 199 -- | Return the /type constant/s that a given /type constant/
 200 -- wants to be part of the final list of /type constants/.
 201 type family TyConsts_imported_by (c:: *) :: [*]
 202
 203 -- * Type 'TyCtx'
 204 -- | GADT for a typing context:
 205 -- accumulating at each /lambda abstraction/
 206 -- the 'Type' of the introduced variable.
 207 data TyCtx (name:: *) (cs::[*]) (hs::[*]) where
 208         TyCtxZ :: TyCtx name cs '[]
 209         TyCtxS :: name
 210                -> Type cs h
 211                -> TyCtx name cs hs
 212                -> TyCtx name cs (h ': hs)
 213 infixr 5 `TyCtxS`
 214
 215 -- * Type 'TeCtx'
 216 -- | GADT for an evaluating context:
 217 -- accumulating at each /lambda abstraction/
 218 -- the @term@ of the introduced variable.
 219 data TeCtx (term:: * -> *) (hs::[*]) where
 220         TeCtxZ :: TeCtx term '[]
 221         TeCtxS :: term h
 222                -> TeCtx term hs
 223                -> TeCtx term (h ': hs)
 224 infixr 5 `TeCtxS`
 225
 226 -- * Type 'Error_Term'
 227 data Error_Term meta (cs::[*]) (is::[*])
 228  =   Error_Term_unbound TeName
 229  |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
 230  |   Error_Term_Con_Type
 231      (Either
 232        (Con_Type meta cs '[Proxy Token_Type])
 233        (Con_Type meta cs is))
 234  |   Error_Term_Con_Kind (Con_Kind meta is)
 235 deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta cs is)
 236 deriving instance (Show meta, Show_Token meta is, Show_TyConst cs) => Show (Error_Term meta cs is)
 237
 238 -- * Type 'Con_Type'
 239 data Con_Type meta cs ts
 240  =   Con_TyEq  (Either (At meta '[Proxy Token_Type] (EType cs))
 241                        (At meta ts (EType cs)))
 242                (At meta ts (EType cs))
 243  |   Con_TyApp (At meta ts (EType cs))
 244  |   Con_TyCon (At meta ts (KType cs Constraint))
 245  |   Con_TyFam (At meta ts TyFamName) [EType cs]
 246 deriving instance
 247  ( Eq meta
 248  , Eq_Token meta ts
 249  ) => Eq (Con_Type meta cs ts)
 250 deriving instance
 251  ( Show meta
 252  , Show_Token meta ts
 253  , Show_TyConst cs
 254  ) => Show (Con_Type meta cs ts)
 255
 256 instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta cs ts) where
 257         olift = Error_Term_Typing . olift
 258 instance MonoLift (Error_Term meta cs ts) (Error_Term meta cs ts) where
 259         olift = id
 260 instance
 261  MonoLift (Con_Type meta cs is) (Error_Term meta cs is) where
 262         olift = Error_Term_Con_Type . Right
 263 instance
 264  MonoLift (Con_Type meta cs '[Proxy Token_Type]) (Error_Term meta cs is) where
 265         olift = Error_Term_Con_Type . Left
 266 instance MonoLift (Con_Kind meta '[Proxy Token_Type]) (Error_Term meta cs is) where
 267         olift = Error_Term_Typing . Error_Type_Con_Kind
 268 instance MonoLift (Con_Kind meta is) (Error_Term meta cs is) where
 269         olift = Error_Term_Con_Kind
 270
 271 -- ** Checks
 272 check_TyEq
 273  :: MonoLift (Con_Type meta cs ts) err
 274  => At meta ts (Type cs x)
 275  -> At meta ts (Type cs y)
 276  -> ((x :~: y) -> Either err ret) -> Either err ret
 277 check_TyEq x y k =
 278         case unAt x `eq_Type` unAt y of
 279          Just Refl -> k Refl
 280          Nothing -> Left $ olift $
 281                 Con_TyEq (Right $ EType <$> x) (EType <$> y)
 282
 283 check_Type_is
 284  :: MonoLift (Con_Type meta cs ts) err
 285  => At meta '[Proxy Token_Type] (Type cs x)
 286  -> At meta ts (Type cs y)
 287  -> ((x :~: y) -> Either err ret) -> Either err ret
 288 check_Type_is x y k =
 289         case unAt x `eq_Type` unAt y of
 290          Just Refl -> k Refl
 291          Nothing -> Left $ olift $
 292                 Con_TyEq (Left $ EType <$> x) (EType <$> y)
 293
 294 check_TyApp
 295  :: MonoLift (Con_Type meta cs ts) err
 296  => At meta ts (Type cs (fa::kfa))
 297  -> (forall ka f a. (fa :~: f a)
 298   -> Type cs (f::ka -> kfa)
 299   -> Type cs (a::ka)
 300   -> Either err ret)
 301  -> Either err ret
 302 check_TyApp typ k =
 303         case unAt typ of
 304          a :$ b -> k Refl a b
 305          _ -> Left $ olift $
 306                 Con_TyApp (EType <$> typ)
 307
 308 check_TyEq1
 309  :: ( MonoLift (Con_Type meta cs ts) err
 310     , MonoLift (Con_Kind meta ts) err )
 311  => Type cs (f:: * -> *)
 312  -> At meta ts (Type cs fa)
 313  -> (forall a. (fa :~: f a)
 314   -> Type cs a
 315   -> Either err ret)
 316  -> Either err ret
 317 check_TyEq1 typ ty_fa k =
 318         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 319         check_Kind
 320          (At Nothing $ SKiType `SKiArrow` SKiType)
 321          (kind_of ty_f <$ ty_fa) $ \Refl ->
 322         check_TyEq
 323          (At Nothing typ)
 324          (ty_f <$ ty_fa) $ \Refl ->
 325         k Refl ty_a
 326
 327 check_TyEq2
 328  :: ( MonoLift (Con_Type meta cs ts) err
 329     , MonoLift (Con_Kind meta ts) err )
 330  => Type cs (f:: * -> * -> *)
 331  -> At meta ts (Type cs fab)
 332  -> (forall a b. (fab :~: f a b)
 333   -> Type cs a
 334   -> Type cs b
 335   -> Either err ret)
 336  -> Either err ret
 337 check_TyEq2 typ ty_fab k =
 338         check_TyApp ty_fab            $ \Refl ty_fa ty_b ->
 339         check_TyApp (ty_fa <$ ty_fab) $ \Refl ty_f  ty_a ->
 340         check_Kind
 341          (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 342          (kind_of ty_f <$ ty_fab) $ \Refl ->
 343         check_TyEq
 344          (At Nothing typ)
 345          (ty_f <$ ty_fab) $ \Refl ->
 346         k Refl ty_a ty_b
 347
 348 check_TyCon
 349  :: ( Proj_TyCon cs
 350     , MonoLift (Con_Type meta cs ts) err )
 351  => At meta ts (Type cs (q::Constraint))
 352  -> (TyCon q -> Either err ret)
 353  -> Either err ret
 354 check_TyCon typ k =
 355         case proj_TyCon $ unAt typ of
 356          Just TyCon -> k TyCon
 357          Nothing -> Left $ olift $
 358                 Con_TyCon (KType <$> typ)
 359
 360 check_TyCon1
 361  :: ( Proj_TyCon cs
 362     , MonoLift (Con_Type meta cs ts) err
 363     , MonoLift (Con_Kind meta ts) err )
 364  => Type cs con
 365  -> At meta ts (Type cs (fa:: *))
 366  -> (forall f a. (fa :~: f a)
 367   -> TyCon (con f)
 368   -> Type cs (f:: * -> *)
 369   -> Type cs (a:: *)
 370   -> Either err ret)
 371  -> Either err ret
 372 check_TyCon1 con ty_fa k =
 373         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 374         check_Kind
 375          (At Nothing (SKiType `SKiArrow` SKiType))
 376          (kind_of ty_f <$ ty_fa) $ \Refl ->
 377         check_TyCon ((con :$ ty_f) <$ ty_fa) $ \TyCon ->
 378         k Refl TyCon ty_f ty_a
 379
 380 check_TyFam
 381  :: ( MonoLift (Con_Type meta cs ts) err
 382     , Proj_TyFam cs fam
 383     , Show fam )
 384  => At meta ts fam
 385  -> Types cs hs
 386  -> (Type cs (TyFam fam hs) -> Either err ret)
 387  -> Either err ret
 388 check_TyFam fam tys k =
 389         case proj_TyFam (unAt fam) tys of
 390          Just t -> k t
 391          Nothing -> Left $ olift $
 392                 Con_TyFam
 393                  (Text.pack . show <$> fam)
 394                  (eTypes tys)