Language/Symantic/Compiling/Term.hs

   1 {-# LANGUAGE GADTs #-}
   2 {-# LANGUAGE UndecidableInstances #-}
   3 {-# OPTIONS_GHC -fno-warn-orphans #-}
   4 module Language.Symantic.Compiling.Term where
   5
   6 import qualified Data.Function as Fun
   7 import qualified Data.Kind as Kind
   8 import Data.Monoid ((<>))
   9 import Data.Proxy (Proxy(..))
  10 import Data.Text (Text)
  11 import qualified Data.Text as Text
  12 import Data.Type.Equality ((:~:)(..))
  13 import GHC.Exts (Constraint)
  14 import Prelude hiding (not)
  15
  16 import Language.Symantic.Lib.Data.Type.List
  17 import Language.Symantic.Parsing
  18 import Language.Symantic.Typing
  19 import Language.Symantic.Interpreting
  20 import Language.Symantic.Transforming.Trans
  21
  22 -- * Type 'Term'
  23 -- | 'TermLC' applied on a 'LamCtx_Type'.
  24 data Term is h
  25  =   Term
  26  (forall term. ( Sym_of_Ifaces is term
  27                , Sym_Lambda term
  28                ) => term h)
  29
  30 -- ** Type 'TermLC'
  31 -- | A data type embedding a universal quantification
  32 -- over an interpreter @term@
  33 -- and qualified by the symantics of a term.
  34 --
  35 -- Moreover the term is abstracted by a 'LamCtx_Term'
  36 -- built top-down at parsing time
  37 -- to build a /Higher-Order Abstract Syntax/ (HOAS)
  38 -- for /lambda abstractions/ ('lam').
  39 --
  40 -- This data type is used to keep a parsed term polymorphic enough
  41 -- to stay interpretable by different interpreters.
  42 --
  43 -- * @(@'Sym_of_Ifaces'@ is term)@
  44 -- is needed when a symantic method includes a polymorphic type
  45 -- and thus calls: 'term_from'.
  46 --
  47 -- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
  48 -- are needed to be able to write the instance:
  49 -- @(@'Term_fromR'@ is ls (i ': rs) ast)@.
  50 --
  51 -- * @(@'Sym_Lambda'@ term)@
  52 -- is needed to be able to parse partially applied functions
  53 -- (when their type is knowable).
  54 data TermLC ctx h is ls rs
  55  =   TermLC
  56  (forall term. ( Sym_of_Ifaces is term
  57                , Sym_of_Ifaces ls term
  58                , Sym_of_Ifaces rs term
  59                , Sym_Lambda 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 -- | Like 'term_from' but for a term with an empty /lambda context/.
  70 closed_term_from
  71  :: Term_from is
  72  => EToken meta is
  73  -> Either (Error_Term meta is) (ETerm is)
  74 closed_term_from tok =
  75         term_from tok LamCtx_TypeZ $ \typ (TermLC te) ->
  76         Right $ ETerm typ $ Term $ te LamCtx_TermZ
  77
  78 -- * Type 'Term_from'
  79 -- | Convenient type synonym wrapping 'Term_fromR' to initiate its recursion.
  80 class Term_from is where
  81         term_from :: EToken meta is -> Term_fromT meta ctx ret is '[] is
  82 instance Term_fromR is '[] is => Term_from is where
  83         term_from (EToken tok) = term_fromR tok
  84
  85 -- ** Type 'Term_fromT'
  86 -- | Convenient type synonym defining a term parser.
  87 type Term_fromT meta ctx ret is ls rs
  88  = LamCtx_Type is Name_LamVar 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     -> TermLC 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 'Term_fromR'
 100 -- | Intermediate type class to construct an instance of 'Term_from'
 101 -- from many instances of 'Term_fromI', 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 Term_fromR (is::[*]) (ls::[*]) (rs::[*]) where
 107         term_fromR :: TokenR meta is rs i -> Term_fromT meta ctx ret is ls rs
 108         {-
 109         term_fromR _tok _ctx _k = Left $ Error_Term_unbound
 110         default term_fromR :: AST ast => Term_fromT meta ctx ret is ls rs
 111         term_fromR ast _ctx _k =
 112                 Left $ Error_Term_unbound $
 113                 At (Just ast) $ ast_lexem ast
 114         -}
 115
 116 -- | Test whether @i@ handles the work of 'Term_from' or not,
 117 -- or recurse on @rs@, preserving the starting list of /term constants/,
 118 -- and keeping a list of those done to construct 'TermLC'.
 119 instance
 120  ( Term_fromI is i
 121  , Term_fromR is (i ': ls) (r ': rs)
 122  ) => Term_fromR is ls (i ': r ': rs) where
 123         term_fromR tok ctx k =
 124                 case tok of
 125                  TokenZ _m t -> term_fromI t ctx k
 126                  TokenS t ->
 127                         term_fromR t ctx $ \typ (TermLC te :: TermLC ctx h is (i ': ls) (r ': rs)) ->
 128                                 k typ (TermLC te :: TermLC ctx h is ls (i ': r ': rs))
 129 -- | End the recursion.
 130 instance
 131  Term_fromI is i =>
 132  Term_fromR is ls (i ': '[]) where
 133         term_fromR (TokenZ _m t) ctx k = term_fromI t ctx k
 134         term_fromR TokenS{} _ctx _k = error "Oops, the impossible happened..."
 135
 136 -- ** Class 'Term_fromI'
 137 -- | Handle the work of 'Term_from' for a given /interface/ @i@,
 138 -- that is: maybe it handles the given /interface/,
 139 -- and if so, maybe the term type-checks.
 140 class Term_fromI (is::[*]) (i:: *) where
 141         term_fromI :: TokenT meta is i -> Term_fromT meta ctx ret is ls (i ': rs)
 142
 143 -- * Type family 'Sym_of_Ifaces'
 144 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
 145         Sym_of_Ifaces '[] term = ()
 146         Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
 147
 148 -- ** Type family 'Sym_of_Iface'
 149 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
 150
 151 -- * Type 'Consts_of_Ifaces'
 152 type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)
 153
 154 -- ** Type family 'Consts_of_IfaceR'
 155 type family Consts_of_IfaceR (is::[*]) where
 156         Consts_of_IfaceR '[] = '[]
 157         Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
 158
 159 -- ** Type family 'Consts_of_Iface'
 160 type family   Consts_of_Iface (i::k) :: [*]
 161 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
 162
 163 -- * Type 'LamCtx_Type'
 164 -- | GADT for a typing context,
 165 -- accumulating an @item@ at each lambda;
 166 -- used to accumulate object-types (in 'Expr_From')
 167 -- or host-terms (in 'HostI')
 168 -- associated with the 'LamVar's in scope.
 169 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
 170         LamCtx_TypeZ :: LamCtx_Type is name '[]
 171         LamCtx_TypeS :: name
 172                      -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 173                      -> LamCtx_Type is name hs
 174                      -> LamCtx_Type is name (h ': hs)
 175 infixr 5 `LamCtx_TypeS`
 176
 177 -- ** Type 'Name_LamVar'
 178 type Name_LamVar = Text
 179
 180 -- * Type 'LamCtx_Term'
 181 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 182         LamCtx_TermZ :: LamCtx_Term term '[]
 183         LamCtx_TermS :: term h
 184                      -> LamCtx_Term term hs
 185                      -> LamCtx_Term term (h ': hs)
 186 infixr 5 `LamCtx_TermS`
 187
 188 {-
 189 data Constraint_Type meta ts
 190  =   Constraint_Type_Eq (Constraint_Kind meta ts)
 191  -}
 192
 193 -- * Type 'Error_Term'
 194 data Error_Term meta (is::[*])
 195  =   Error_Term_unbound Name_LamVar
 196  |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
 197  |   Error_Term_Constraint_Type
 198      (Either
 199        (Constraint_Type meta '[Proxy Token_Type] (Consts_of_Ifaces is))
 200        (Constraint_Type meta is (Consts_of_Ifaces is)))
 201  |   Error_Term_Constraint_Kind (Constraint_Kind meta is)
 202 deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
 203 deriving instance (Show meta, Show_Token meta is, Show_Const (Consts_of_Ifaces is)) => Show (Error_Term meta is)
 204
 205 -- * Type 'Constraint_Type'
 206 data Constraint_Type meta ts cs
 207  =   Constraint_Type_Eq  (Either (At meta '[Proxy Token_Type] (EType cs))
 208                                  (At meta ts (EType cs)))
 209                          (At meta ts (EType cs))
 210  |   Constraint_Type_App (At meta ts (EType cs))
 211  |   Constraint_Type_Con (At meta ts (KType cs Constraint))
 212  |   Constraint_Type_Fam (At meta ts Name_Fam) [EType cs]
 213 deriving instance
 214  ( Eq meta
 215  , Eq_Token meta ts
 216  ) => Eq (Constraint_Type meta ts cs)
 217 deriving instance
 218  ( Show meta
 219  , Show_Token meta ts
 220  , Show_Const cs
 221  ) => Show (Constraint_Type meta ts cs)
 222
 223
 224 instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
 225         olift = Error_Term_Typing . olift
 226 instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
 227         olift = Prelude.id
 228 instance
 229  cs ~ Consts_of_Ifaces is =>
 230  MonoLift (Constraint_Type meta is cs) (Error_Term meta is) where
 231         olift = Error_Term_Constraint_Type . Right
 232 instance
 233  cs ~ Consts_of_Ifaces is =>
 234  MonoLift (Constraint_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
 235         olift = Error_Term_Constraint_Type . Left
 236 instance MonoLift (Constraint_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
 237         olift = Error_Term_Typing . Error_Type_Constraint_Kind
 238 instance MonoLift (Constraint_Kind meta is) (Error_Term meta is) where
 239         olift = Error_Term_Constraint_Kind
 240
 241 -- ** Checks
 242 check_type
 243  :: MonoLift (Constraint_Type meta ts cs) err
 244  => At meta ts (Type cs x)
 245  -> At meta ts (Type cs y)
 246  -> ((x :~: y) -> Either err ret) -> Either err ret
 247 check_type x y k =
 248         case unAt x `eq_type` unAt y of
 249          Just Refl -> k Refl
 250          Nothing -> Left $ olift $
 251                 Constraint_Type_Eq (Right $ EType <$> x) (EType <$> y)
 252
 253 check_type_is
 254  :: MonoLift (Constraint_Type meta ts cs) err
 255  => At meta '[Proxy Token_Type] (Type cs x)
 256  -> At meta ts (Type cs y)
 257  -> ((x :~: y) -> Either err ret) -> Either err ret
 258 check_type_is x y k =
 259         case unAt x `eq_type` unAt y of
 260          Just Refl -> k Refl
 261          Nothing -> Left $ olift $
 262                 Constraint_Type_Eq (Left $ EType <$> x) (EType <$> y)
 263
 264 check_type_app
 265  :: MonoLift (Constraint_Type meta ts cs) err
 266  => At meta ts (Type cs (fa::kfa))
 267  -> (forall ka f a. (fa :~: f a)
 268   -> Type cs (f::ka -> kfa)
 269   -> Type cs (a::ka)
 270   -> Either err ret)
 271  -> Either err ret
 272 check_type_app typ k =
 273         case unAt typ of
 274          a :$ b -> k Refl a b
 275          _ -> Left $ olift $
 276                 Constraint_Type_App (EType <$> typ)
 277
 278 check_con
 279  :: ( Proj_Con cs
 280     , MonoLift (Constraint_Type meta ts cs) err )
 281  => At meta ts (Type cs (q::Constraint))
 282  -> (Con q -> Either err ret)
 283  -> Either err ret
 284 check_con typ k =
 285         case proj_con $ unAt typ of
 286          Just Con -> k Con
 287          Nothing -> Left $ olift $
 288                 Constraint_Type_Con (KType <$> typ)
 289
 290 check_con1
 291  :: ( Proj_Con cs
 292     , MonoLift (Constraint_Type meta ts cs) err
 293     , MonoLift (Constraint_Kind meta ts) err )
 294  => Type cs con
 295  -> At meta ts (Type cs (fa:: *))
 296  -> (forall f a. (fa :~: f a)
 297   -> Con (con f)
 298   -> Type cs (f:: * -> *)
 299   -> Type cs (a:: *)
 300   -> Either err ret)
 301  -> Either err ret
 302 check_con1 con ty_fa k =
 303         check_type_app 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_con ((con :$ ty_f) <$ ty_fa) $ \Con ->
 308         k Refl Con ty_f ty_a
 309
 310 check_type1
 311  :: ( MonoLift (Constraint_Type meta ts cs) err
 312     , MonoLift (Constraint_Kind meta ts) err )
 313  => Type cs (f:: * -> *)
 314  -> At meta ts (Type cs fa)
 315  -> (forall a. (fa :~: f a)
 316   -> Type cs a
 317   -> Either err ret)
 318  -> Either err ret
 319 check_type1 typ ty_fa k =
 320         check_type_app ty_fa $ \Refl ty_f ty_a ->
 321         check_kind
 322          (At Nothing $ SKiType `SKiArrow` SKiType)
 323          (kind_of ty_f <$ ty_fa) $ \Refl ->
 324         check_type
 325          (At Nothing typ)
 326          (ty_f <$ ty_fa) $ \Refl ->
 327         k Refl ty_a
 328
 329 check_type2
 330  :: ( MonoLift (Constraint_Type meta ts cs) err
 331     , MonoLift (Constraint_Kind meta ts) err )
 332  => Type cs (f:: * -> * -> *)
 333  -> At meta ts (Type cs fab)
 334  -> (forall a b. (fab :~: f a b)
 335   -> Type cs a
 336   -> Type cs b
 337   -> Either err ret)
 338  -> Either err ret
 339 check_type2 typ ty_fab k =
 340         check_type_app ty_fab            $ \Refl ty_fa ty_b ->
 341         check_type_app (ty_fa <$ ty_fab) $ \Refl ty_f  ty_a ->
 342         check_kind
 343          (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 344          (kind_of ty_f <$ ty_fab) $ \Refl ->
 345         check_type
 346          (At Nothing typ)
 347          (ty_f <$ ty_fab) $ \Refl ->
 348         k Refl ty_a ty_b
 349
 350 check_fam
 351  :: ( MonoLift (Constraint_Type meta ts cs) err
 352     , Proj_Fam cs fam
 353     , Show fam )
 354  => At meta ts fam
 355  -> Types cs hs
 356  -> (Type cs (Fam fam hs) -> Either err ret)
 357  -> Either err ret
 358 check_fam fam tys k =
 359         case proj_fam (unAt fam) tys of
 360          Just t -> k t
 361          Nothing -> Left $ olift $
 362                 Constraint_Type_Fam
 363                  (Text.pack . show <$> fam)
 364                  (etypes tys)
 365
 366 -- * Class 'Sym_Lambda'
 367 class Sym_Lambda term where
 368         -- | /Lambda abstraction/.
 369         lam :: (term arg -> term res) -> term ((->) arg res)
 370         default lam :: Trans t term
 371          => (t term arg -> t term res)
 372          -> t term ((->) arg res)
 373         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
 374
 375         -- | /Lambda application/.
 376         (.$) :: term ((->) arg res) -> term arg -> term res
 377         default (.$) :: Trans t term
 378          => t term ((->) arg res) -> t term arg -> t term res
 379         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
 380
 381         -- | Convenient 'lam' and '.$' wrapper.
 382         let_ :: term var -> (term var -> term res) -> term res
 383         let_ x y = lam y .$ x
 384
 385         id :: term a -> term a
 386         id a = lam Fun.id .$ a
 387
 388         const :: term a -> term b -> term a
 389         const a b = lam (lam . Fun.const) .$ a .$ b
 390
 391         -- | /Lambda composition/.
 392         (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
 393         (#) f g = lam $ \a -> f .$ (g .$ a)
 394
 395         flip :: term (a -> b -> c) -> term (b -> a -> c)
 396         flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
 397
 398 infixl 0 .$
 399 infixr 9 #
 400
 401 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
 402 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
 403 type instance Consts_imported_by (->) =
 404  [ Proxy Applicative
 405  , Proxy Functor
 406  , Proxy Monad
 407  , Proxy Monoid
 408  ]
 409
 410 instance Sym_Lambda HostI where
 411         lam f = HostI (unHostI . f . HostI)
 412         (.$)  = (<*>)
 413 instance Sym_Lambda TextI where
 414         lam f = TextI $ \p v ->
 415                 let p' = Precedence 1 in
 416                 let x = "x" <> Text.pack (show v) in
 417                 paren p p' $ "\\" <> x <> " -> "
 418                  <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
 419         -- (.$) = textI_infix "$" (Precedence 0)
 420         (.$) (TextI a1) (TextI a2) =
 421                 TextI $ \p v ->
 422                         let p' = precedence_App in
 423                         paren p p' $ a1 p' v <> " " <> a2 p' v
 424         let_ e in_ =
 425                 TextI $ \p v ->
 426                         let p' = Precedence 2 in
 427                         let x = "x" <> Text.pack (show v) in
 428                         paren p p' $ "let" <> " " <> x <> " = "
 429                          <> unTextI e (Precedence 0) (succ v) <> " in "
 430                          <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
 431         (#)   = textI_infix "." (Precedence 9)
 432         id    = textI_app1 "id"
 433         const = textI_app2 "const"
 434         flip  = textI_app1 "flip"
 435 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
 436         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
 437                 where lam_f = lam f
 438         (.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
 439
 440 instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
 441         const_from "(->)" k = k (ConstZ kind)
 442         const_from s k = const_from s $ k . ConstS
 443 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 444         show_const ConstZ{} = "(->)"
 445         show_const (ConstS c) = show_const c
 446
 447 instance -- Proj_ConC (->)
 448  ( Proj_Const cs (->)
 449  , Proj_Consts cs (Consts_imported_by (->))
 450  , Proj_Con cs
 451  ) => Proj_ConC cs (Proxy (->)) where
 452         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 453          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 454          , Just Refl <- proj_const c (Proxy::Proxy (->))
 455          = case () of
 456                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 457                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 458                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 459                  _ -> Nothing
 460         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 461          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 462          , Just Refl <- proj_const c (Proxy::Proxy (->))
 463          = case () of
 464                  _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 465                    , Just Con  <- proj_con (t :$ b) -> Just Con
 466                  _ -> Nothing
 467         proj_conC _c _q = Nothing
 468 data instance TokenT meta (ts::[*]) (Proxy (->))
 469  = Token_Term_Abst Name_LamVar (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 470  | Token_Term_App              (EToken meta ts) (EToken meta ts)
 471  | Token_Term_Let  Name_LamVar (EToken meta ts) (EToken meta ts)
 472  | Token_Term_Var  Name_LamVar
 473 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
 474 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
 475 instance -- Term_fromI (->)
 476  ( Inj_Const  (Consts_of_Ifaces is) (->)
 477  , Const_from Name_LamVar (Consts_of_Ifaces is)
 478  , Term_from is
 479  ) => Term_fromI is (Proxy (->)) where
 480         term_fromI tok ctx k =
 481                 case tok of
 482                  Token_Term_Abst name_arg tok_ty_arg tok_body ->
 483                         type_from tok_ty_arg $ \(ty_arg::Type (Consts_of_Ifaces is) h) ->
 484                         check_kind
 485                          (At Nothing SKiType)
 486                          (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
 487                         term_from tok_body
 488                          (LamCtx_TypeS name_arg ty_arg ctx) $
 489                          \ty_res (TermLC res) ->
 490                         k (ty_arg ~> ty_res) $ TermLC $
 491                          \c -> lam $ \arg ->
 492                                 res (arg `LamCtx_TermS` c)
 493                  Token_Term_App tok_lam tok_arg_actual ->
 494                         term_from tok_lam ctx $ \ty_lam (TermLC lam_) ->
 495                         term_from tok_arg_actual ctx $ \ty_arg_actual (TermLC arg_actual) ->
 496                         check_type2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
 497                         check_type
 498                          (At (Just tok_lam) ty_arg)
 499                          (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
 500                         k ty_res $ TermLC $
 501                          \c -> lam_ c .$ arg_actual c
 502                  Token_Term_Let name tok_bound tok_body ->
 503                         term_from tok_bound ctx $ \ty_bound (TermLC bound) ->
 504                         term_from tok_body (LamCtx_TypeS name ty_bound ctx) $
 505                          \ty_res (TermLC res) ->
 506                         k ty_res $ TermLC $
 507                          \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
 508                  Token_Term_Var nam -> go nam ctx k
 509                         where
 510                         go :: forall meta lc ret ls rs.
 511                             Name_LamVar
 512                          -> LamCtx_Type is Name_LamVar lc
 513                          -> ( forall h.
 514                                Type (Consts_of_Ifaces is) (h::Kind.Type)
 515                             -> TermLC lc h is ls rs
 516                             -> Either (Error_Term meta is) ret )
 517                          -> Either (Error_Term meta is) ret
 518                         go name lc k' =
 519                                 case lc of
 520                                  LamCtx_TypeZ -> Left $ Error_Term_unbound name
 521                                  LamCtx_TypeS n typ _ | n == name ->
 522                                         k' typ $ TermLC $ \(te `LamCtx_TermS` _) -> te
 523                                  LamCtx_TypeS _n _ty lc' ->
 524                                         go name lc' $ \typ (TermLC te::TermLC lc' h is '[] is) ->
 525                                         k' typ $ TermLC $ \(_ `LamCtx_TermS` c) -> te c
 526
 527 -- | The function 'Type' @(->)@,
 528 -- with an infix notation more readable.
 529 (~>) :: forall cs a b. Inj_Const cs (->)
 530  => Type cs a -> Type cs b -> Type cs (a -> b)
 531 (~>) a b = ty @(->) :$ a :$ b
 532 infixr 5 ~>
 533
 534 {-
 535 -- * Class 'Sym_Type'
 536 class Sym_Type term
 537 instance Sym_Type term
 538 type instance Sym_of_Iface (Proxy Token_Type) = Sym_Type
 539 type instance Consts_of_Iface (Proxy Token_Type) = '[]
 540 type instance Consts_imported_by Token_Type = '[]
 541 instance -- Proj_ConC
 542  Proj_ConC cs (Proxy Token_Type)
 543 instance -- Term_fromI (->)
 544  Term_fromI is (Proxy Token_Type) where
 545         term_fromI _tok _ctx _k = Left $ Error_Term_unbound
 546 -}