Language/Symantic/Compiling/Term.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE DefaultSignatures #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE KindSignatures #-}
   8 {-# LANGUAGE MultiParamTypeClasses #-}
   9 {-# LANGUAGE OverloadedStrings #-}
  10 {-# LANGUAGE PolyKinds #-}
  11 {-# LANGUAGE Rank2Types #-}
  12 {-# LANGUAGE ScopedTypeVariables #-}
  13 {-# LANGUAGE StandaloneDeriving #-}
  14 {-# LANGUAGE TypeFamilies #-}
  15 {-# LANGUAGE TypeInType #-}
  16 {-# LANGUAGE TypeOperators #-}
  17 {-# LANGUAGE UndecidableInstances #-}
  18 {-# OPTIONS_GHC -fno-warn-orphans #-}
  19 module Language.Symantic.Compiling.Term where
  20
  21 import qualified Data.Function as Fun
  22 import qualified Data.Kind as Kind
  23 import Data.Kind hiding (Type)
  24 import Data.Monoid ((<>))
  25 import Data.Proxy (Proxy(..))
  26 import Data.String (IsString)
  27 import Data.Text (Text)
  28 import qualified Data.Text as Text
  29 import Data.Type.Equality
  30 import GHC.Exts (Constraint)
  31 import Prelude hiding (not)
  32
  33 import Language.Symantic.Lib.Data.Type.List
  34 import Language.Symantic.Typing
  35 import Language.Symantic.Interpreting
  36 import Language.Symantic.Transforming.Trans
  37
  38 -- * Type 'Term'
  39 -- | 'TermLC' applied on a 'LamCtx_Type'.
  40 data Term is h
  41  =   Term
  42  (forall term. ( Sym_of_Ifaces is term
  43                , Sym_Lambda term
  44                ) => term h)
  45
  46 -- ** Type 'TermLC'
  47 -- | A data type embedding a universal quantification
  48 -- over an interpreter @term@
  49 -- and qualified by the symantics of a term.
  50 --
  51 -- Moreover the term is abstracted by a 'LamCtx_Term'
  52 -- built top-down at parsing time
  53 -- to build a /Higher-Order Abstract Syntax/ (HOAS)
  54 -- for /lambda abstractions/ ('lam').
  55 --
  56 -- This data type is used to keep a parsed term polymorphic enough
  57 -- to stay interpretable by different interpreters.
  58 --
  59 -- * @(@'Sym_of_Ifaces'@ is term)@
  60 -- is needed when a symantic method includes a polymorphic type
  61 -- and thus calls: 'term_from'.
  62 --
  63 -- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
  64 -- are needed to be able to write the instance:
  65 -- @(@'Term_fromR'@ is ls (i ': rs) ast)@.
  66 --
  67 -- * @(@'Sym_Lambda'@ term)@
  68 -- is needed to be able to parse partially applied functions
  69 -- (when their type is knowable).
  70 data TermLC ctx h is ls rs
  71  =   TermLC
  72  (forall term. ( Sym_of_Ifaces is term
  73                , Sym_of_Ifaces ls term
  74                , Sym_of_Ifaces rs term
  75                , Sym_Lambda term
  76                ) => LamCtx_Term term ctx -> term h)
  77
  78 -- * Type 'ETerm'
  79 -- | Existential 'Term', with its 'Type'.
  80 data ETerm is
  81  = forall (h::Kind.Type). ETerm
  82    (Type (Consts_of_Ifaces is) h)
  83    (Term is h)
  84
  85 -- | Like 'term_from' but for a term with an empty /lambda context/.
  86 root_term_from
  87  :: Term_from is ast
  88  => ast -> Either (Error_Term is ast) (ETerm is)
  89 root_term_from ast =
  90         term_from ast LamCtx_TypeZ $ \ty (TermLC te) ->
  91         Right $ ETerm ty $ Term $ te LamCtx_TermZ
  92
  93 -- * Type 'Term_from'
  94 -- | Convenient type synonym wrapping 'Term_fromR'
  95 -- to initiate its recursion.
  96 class Term_from is ast where
  97         term_from :: Term_fromT ast ctx ret is '[] is
  98 instance
  99  ( AST ast
 100  , Eq (Lexem ast)
 101  , Term_fromR is '[] is ast
 102  ) => Term_from is ast where
 103         term_from ast ctx k =
 104                 case replace_var (ast_lexem ast) ctx k of
 105                  Left Error_Term_unsupported -> term_fromR ast ctx k
 106                  x -> x
 107                 where
 108                 replace_var :: forall lc ret.
 109                       Lexem ast
 110                    -> LamCtx_Type is (Lexem ast) lc
 111                    -> ( forall h.
 112                          Type (Consts_of_Ifaces is) (h::Kind.Type)
 113                       -> TermLC lc h is '[] is
 114                       -> Either (Error_Term is ast) ret )
 115                    -> Either (Error_Term is ast) ret
 116                 replace_var name lc k' =
 117                         case lc of
 118                          LamCtx_TypeZ -> Left $ Error_Term_unsupported
 119                          LamCtx_TypeS n ty _ | n == name ->
 120                                 k' ty $ TermLC $ \(te `LamCtx_TermS` _) -> te
 121                          LamCtx_TypeS _n _ty lc' ->
 122                                 replace_var name lc' $ \ty (TermLC te::TermLC lc' h is '[] is) ->
 123                                 k' ty $ TermLC $ \(_ `LamCtx_TermS` c) -> te c
 124
 125 -- ** Type 'Term_fromT'
 126 -- | Convenient type synonym defining a term parser.
 127 type Term_fromT ast ctx ret is ls rs
 128  = ast
 129  -> LamCtx_Type is (Lexem ast) ctx
 130  -- ^ The bound variables in scope and their types:
 131  -- built top-down in the heterogeneous list @ctx@,
 132  -- from the closest including /lambda abstraction/ to the farest.
 133  -> ( forall h.
 134        Type (Consts_of_Ifaces is) (h::Kind.Type)
 135     -> TermLC ctx h is ls rs
 136     -> Either (Error_Term is ast) ret )
 137  -- ^ The accumulating continuation called bottom-up.
 138  -> Either (Error_Term is ast) ret
 139
 140 -- ** Class 'Term_fromR'
 141 -- | Intermediate type class to construct an instance of 'Term_from'
 142 -- from many instances of 'Term_fromI', one for each item of @is@.
 143 --
 144 -- * @is@: starting  list of /term constants/.
 145 -- * @ls@: done      list of /term constants/.
 146 -- * @rs@: remaining list of /term constants/.
 147 class Term_fromR (is::[*]) (ls::[*]) (rs::[*]) ast where
 148         term_fromR :: Term_fromT ast ctx ret is ls rs
 149         default term_fromR :: AST ast => Term_fromT ast ctx ret is ls rs
 150         term_fromR ast _ctx _k =
 151                 Left $ Error_Term_unknown $
 152                 At (Just ast) $ ast_lexem ast
 153
 154 -- | Test whether @i@ handles the work of 'Term_from' or not,
 155 -- or recurse on @rs@, preserving the starting list of /term constants/,
 156 -- and keeping a list of those done to construct 'TermLC'.
 157 instance
 158  ( Term_fromI is i ast
 159  , Term_fromR is (i ': ls) rs ast
 160  ) => Term_fromR is ls (i ': rs) ast where
 161         term_fromR ast ctx k =
 162                 case term_fromI ast ctx $ \ty (TermLC te
 163                  ::TermLC ctx h is ls (i ': rs)) ->
 164                         k ty (TermLC te) of
 165                  Left Error_Term_unsupported ->
 166                         term_fromR ast ctx $ \ty (TermLC te
 167                          ::TermLC ctx h is (i ': ls) rs) ->
 168                                 k ty (TermLC te
 169                                  ::TermLC ctx h is ls (i ': rs))
 170                  x -> x
 171 -- | End the recursion.
 172 instance AST ast => Term_fromR is ls '[] ast
 173
 174 -- ** Class 'Term_fromI'
 175 -- | Handle the work of 'Term_from' for a given /interface/ @i@,
 176 -- that is: maybe it handles the given /interface/,
 177 -- and if so, maybe the term can be parsed.
 178 class Term_fromI (is::[*]) (i:: *) ast where
 179         term_fromI :: Term_fromT ast ctx ret is ls (i ': rs)
 180         term_fromI _ast _ctx _k = Left $ Error_Term_unsupported
 181
 182 -- * Type family 'Sym_of_Ifaces'
 183 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
 184         Sym_of_Ifaces '[] term = ()
 185         Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
 186
 187 -- ** Type family 'Sym_of_Iface'
 188 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
 189
 190 -- * Type 'Consts_of_Ifaces'
 191 type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)
 192
 193 -- ** Type family 'Consts_of_IfaceR'
 194 type family Consts_of_IfaceR (is::[*]) where
 195         Consts_of_IfaceR '[] = '[]
 196         Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
 197
 198 -- ** Type family 'Consts_of_Iface'
 199 type family   Consts_of_Iface (i::k) :: [*]
 200 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
 201
 202 -- * Type 'LamCtx_Type'
 203 -- | GADT for a typing context,
 204 -- accumulating an @item@ at each lambda;
 205 -- used to accumulate object-types (in 'Expr_From')
 206 -- or host-terms (in 'HostI')
 207 -- associated with the 'LamVar's in scope.
 208 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
 209         LamCtx_TypeZ :: LamCtx_Type is name '[]
 210         LamCtx_TypeS :: name
 211                      -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 212                      -> LamCtx_Type is name hs
 213                      -> LamCtx_Type is name (h ': hs)
 214 infixr 5 `LamCtx_TypeS`
 215
 216 -- ** Type 'LamVarName'
 217 type LamVarName = Text
 218
 219 -- * Type 'LamCtx_Term'
 220 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 221         LamCtx_TermZ :: LamCtx_Term term '[]
 222         LamCtx_TermS :: term h
 223                      -> LamCtx_Term term hs
 224                      -> LamCtx_Term term (h ': hs)
 225 infixr 5 `LamCtx_TermS`
 226
 227 -- * Type 'Error_Term'
 228 data Error_Term (is::[*]) ast
 229  =   Error_Term_unknown (At ast (Lexem ast))
 230  |   Error_Term_unsupported
 231  |   Error_Term_Syntax (Error_Syntax ast)
 232  |   Error_Term_Constraint_not_deductible (At ast (KType (Consts_of_Ifaces is) Constraint))
 233  |   Error_Term_Typing (At ast (Error_Type (Consts_of_Ifaces is) ast))
 234  |   Error_Term_Type_mismatch (At ast (EType (Consts_of_Ifaces is)))
 235                               (At ast (EType (Consts_of_Ifaces is)))
 236  |   Error_Term_Type_is_not_an_application (At ast (EType (Consts_of_Ifaces is)))
 237 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Term is ast)
 238 deriving instance (Show ast, Show (Lexem ast), Show_Const (Consts_of_Ifaces is)) => Show (Error_Term is ast)
 239
 240 instance Lift_Error_Syntax (Error_Term is) where
 241         lift_error_syntax = Error_Term_Syntax
 242
 243 -- ** Checks
 244
 245 -- | Check that the 'kind_of' a given 'Type's equals a given kind,
 246 -- or fail with 'Error_Type_Kind_mismatch'.
 247 check_kind
 248  :: ast -> SKind k
 249  -> At ast (Type (Consts_of_Ifaces is) (t::kt))
 250  -> ((k :~: kt) -> Either (Error_Term is ast) ret)
 251  -> Either (Error_Term is ast) ret
 252 check_kind ast ki (At at_ty ty) k =
 253         let ki_ty = kind_of ty in
 254         case eq_skind ki ki_ty of
 255          Just Refl -> k Refl
 256          Nothing -> Left $ Error_Term_Typing $
 257                 At (Just ast) $
 258                 Error_Type_Kind_mismatch
 259                  (At Nothing $ EKind SKiType)
 260                  (At at_ty $ EKind ki_ty)
 261
 262 -- | Check that a given 'Type' is a /type application/,
 263 -- or fail with 'Error_Term_Type_is_not_an_application'.
 264 check_app
 265  :: ast -> Type (Consts_of_Ifaces is) (fx::kfx)
 266  -> (forall kx f x. (fx :~: f x)
 267   -> Type (Consts_of_Ifaces is) (f::kx -> kfx)
 268   -> Type (Consts_of_Ifaces is) (x::kx)
 269   -> Either (Error_Term is ast) ret)
 270  -> Either (Error_Term is ast) ret
 271 check_app ast ty_fx k =
 272         case ty_fx of
 273          ty_f :$ ty_x -> k Refl ty_f ty_x
 274          _ -> Left $ Error_Term_Type_is_not_an_application $
 275                 At (Just ast) $ EType ty_fx
 276
 277 -- | Check that two given 'Type's are equal,
 278 -- or fail with 'Error_Term_Type_mismatch'.
 279 check_type
 280  :: At ast (Type (Consts_of_Ifaces is) x)
 281  -> At ast (Type (Consts_of_Ifaces is) y)
 282  -> ((x :~: y) -> Either (Error_Term is ast) ret)
 283  -> Either (Error_Term is ast) ret
 284 check_type (At at_x x) (At at_y y) k =
 285         case eq_type x y of
 286          Just Refl -> k Refl
 287          Nothing -> Left $ Error_Term_Type_mismatch
 288                  (At at_x $ EType x)
 289                  (At at_y $ EType y)
 290
 291 -- | Convenient wrapper to check for a 'Type' of kind: @* -> *@.
 292 check_type1
 293  :: Type (Consts_of_Ifaces is) ty
 294  -> ast
 295  -> Type (Consts_of_Ifaces is) (fx:: *)
 296  -> (forall x. (fx :~: ty x)
 297   -> Type (Consts_of_Ifaces is) (x:: *)
 298   -> Either (Error_Term is ast) ret)
 299  -> Either (Error_Term is ast) ret
 300 check_type1 ty ast_ta ty_ta k =
 301         check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
 302         check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 303         check_type (At Nothing ty) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 304         k Refl ty_ta_a
 305
 306 -- | Convenient wrapper to check for a 'Type' of kind: @* -> * -> *@.
 307 check_type2
 308  :: Type (Consts_of_Ifaces is) (ty:: * -> * -> *)
 309  -> ast -> Type (Consts_of_Ifaces is) a2b
 310  -> (forall a b. (a2b :~: (ty a b))
 311   -> Type (Consts_of_Ifaces is) a
 312   -> Type (Consts_of_Ifaces is) b
 313   -> Either (Error_Term is ast) ret)
 314  -> Either (Error_Term is ast) ret
 315 check_type2 ty ast ty_a2b k =
 316         check_app ast ty_a2b $ \Refl ty_a2b_a2 ty_a2b_b ->
 317         check_app ast ty_a2b_a2 $ \Refl ty_a2b_ty ty_a2b_a ->
 318         check_kind ast (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) (At (Just ast) ty_a2b_ty) $ \Refl ->
 319         check_type (At Nothing ty) (At (Just ast) ty_a2b_ty) $ \Refl ->
 320         k Refl ty_a2b_a ty_a2b_b
 321
 322 -- | Check that a given 'Constraint' holds,
 323 -- or fail with 'Error_Term_Constraint_not_deductible'.
 324 check_constraint
 325  :: Proj_Con (Consts_of_Ifaces is)
 326  => At ast (Type (Consts_of_Ifaces is) (q::Constraint))
 327  -> (Con q -> Either (Error_Term is ast) ret)
 328  -> Either (Error_Term is ast) ret
 329 check_constraint (At at_q q) k =
 330         case proj_con q of
 331          Just Con -> k Con
 332          Nothing -> Left $ Error_Term_Constraint_not_deductible $
 333                 At at_q $ KType q
 334
 335 -- | Convenient wrapper to check for a 'Constraint'
 336 -- over a 'Type' of kind: @* -> *@.
 337 check_constraint1
 338  :: Proj_Con (Consts_of_Ifaces is)
 339  => Type (Consts_of_Ifaces is) con
 340  -> ast -> Type (Consts_of_Ifaces is) (fx:: *)
 341  -> (forall f x. (fx :~: f x)
 342   -> Con (con f)
 343   -> Type (Consts_of_Ifaces is) (f:: * -> *)
 344   -> Type (Consts_of_Ifaces is) (x:: *)
 345   -> Either (Error_Term is ast) ret)
 346  -> Either (Error_Term is ast) ret
 347 check_constraint1 con ast_ta ty_ta k =
 348         check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
 349         check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 350         check_constraint (At (Just ast_ta) (con :$ ty_ta_t)) $ \Con ->
 351         k Refl Con ty_ta_t ty_ta_a
 352
 353 -- * Class 'Sym_Lambda'
 354 class Sym_Lambda term where
 355         -- | /Lambda abstraction/.
 356         lam :: (term arg -> term res) -> term ((->) arg res)
 357         default lam :: Trans t term
 358          => (t term arg -> t term res)
 359          -> t term ((->) arg res)
 360         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
 361
 362         -- | /Lambda application/.
 363         (.$) :: term ((->) arg res) -> term arg -> term res
 364         default (.$) :: Trans t term
 365          => t term ((->) arg res) -> t term arg -> t term res
 366         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
 367
 368         -- | Convenient 'lam' and '.$' wrapper.
 369         let_ :: term var -> (term var -> term res) -> term res
 370         let_ x y = lam y .$ x
 371
 372         id :: term a -> term a
 373         id a = lam Fun.id .$ a
 374
 375         const :: term a -> term b -> term a
 376         const a b = lam (lam . Fun.const) .$ a .$ b
 377
 378         -- | /Lambda composition/.
 379         (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
 380         (#) f g = lam $ \a -> f .$ (g .$ a)
 381
 382         flip :: term (a -> b -> c) -> term (b -> a -> c)
 383         flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
 384
 385 infixl 0 .$
 386 infixr 9 #
 387
 388 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
 389 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
 390 type instance Consts_imported_by (->) =
 391  [ Proxy Applicative
 392  , Proxy Functor
 393  , Proxy Monad
 394  , Proxy Monoid
 395  ]
 396
 397 instance Sym_Lambda HostI where
 398         lam f = HostI (unHostI . f . HostI)
 399         (.$)  = (<*>)
 400 instance Sym_Lambda TextI where
 401         lam f = TextI $ \p v ->
 402                 let p' = Precedence 1 in
 403                 let x = "x" <> Text.pack (show v) in
 404                 paren p p' $ "\\" <> x <> " -> "
 405                  <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
 406         -- (.$) = textI_infix "$" (Precedence 0)
 407         (.$) (TextI a1) (TextI a2) =
 408                 TextI $ \p v ->
 409                         let p' = precedence_App in
 410                         paren p p' $ a1 p' v <> " " <> a2 p' v
 411         let_ e in_ =
 412                 TextI $ \p v ->
 413                         let p' = Precedence 2 in
 414                         let x = "x" <> Text.pack (show v) in
 415                         paren p p' $ "let" <> " " <> x <> " = "
 416                          <> unTextI e (Precedence 0) (succ v) <> " in "
 417                          <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
 418         (#)   = textI_infix "." (Precedence 9)
 419         id    = textI_app1 "id"
 420         const = textI_app2 "const"
 421         flip  = textI_app1 "flip"
 422 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
 423         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
 424                 where lam_f = lam f
 425         (.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
 426
 427 instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
 428         const_from "(->)" k = k (ConstZ kind)
 429         const_from s k = const_from s $ k . ConstS
 430 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 431         show_const ConstZ{} = "(->)"
 432         show_const (ConstS c) = show_const c
 433
 434 instance -- Proj_ConC (->)
 435  ( Proj_Const cs (->)
 436  , Proj_Consts cs (Consts_imported_by (->))
 437  , Proj_Con cs
 438  ) => Proj_ConC cs (Proxy (->)) where
 439         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 440          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 441          , Just Refl <- proj_const c (Proxy::Proxy (->))
 442          = Just $ case () of
 443                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 444                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 445                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 446                  _ -> Nothing
 447         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 448          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 449          , Just Refl <- proj_const c (Proxy::Proxy (->))
 450          = Just $ case () of
 451                  _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 452                    , Just Con  <- proj_con (t :$ b) -> Just Con
 453                  _ -> Nothing
 454         proj_conC _c _q = Nothing
 455 instance -- Term_fromI (->)
 456  ( AST ast
 457  , Lexem ast ~ LamVarName
 458  , Inj_Const  (Consts_of_Ifaces is) (->)
 459  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 460  , Term_from is ast
 461  ) => Term_fromI is (Proxy (->)) ast where
 462         term_fromI ast ctx k =
 463                 case ast_lexem ast of
 464                  "\\" ->
 465                         from_ast3 ast $ \ast_name ast_ty_arg ast_body ->
 466                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 467                         type_from ast_ty_arg $ \ty_arg -> Right $
 468                         check_kind ast SKiType (At (Just ast) ty_arg) $ \Refl ->
 469                         term_from ast_body
 470                          (LamCtx_TypeS (ast_lexem ast_name) ty_arg ctx) $
 471                          \ty_res (TermLC res) ->
 472                         k (ty_arg ~> ty_res) $ TermLC $
 473                          \c -> lam $ \arg ->
 474                                 res (arg `LamCtx_TermS` c)
 475                  " " ->
 476                         from_ast2 ast $ \ast_lam ast_arg_actual ->
 477                         term_from ast_lam ctx $ \ty_lam (TermLC lam_) ->
 478                         term_from ast_arg_actual ctx $ \ty_arg_actual (TermLC arg_actual) ->
 479                         check_type2 tyFun ast_lam ty_lam $ \Refl ty_arg ty_res ->
 480                         check_type
 481                          (At (Just ast_lam) ty_arg)
 482                          (At (Just ast_arg_actual) ty_arg_actual) $ \Refl ->
 483                         k ty_res $ TermLC $
 484                          \c -> lam_ c .$ arg_actual c
 485                  "let" ->
 486                         from_ast3 ast $ \ast_name ast_bound ast_body ->
 487                         term_from ast_bound ctx $ \ty_bound (TermLC bound) ->
 488                         term_from ast_body (LamCtx_TypeS (ast_lexem ast_name) ty_bound ctx) $
 489                          \ty_res (TermLC res) ->
 490                         k ty_res $ TermLC $
 491                          \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
 492                  _ -> Left $ Error_Term_unsupported
 493
 494 -- | The '(->)' 'Type'
 495 tyFun :: Inj_Const cs (->) => Type cs (->)
 496 tyFun = TyConst inj_const
 497
 498 -- | The function 'Type' @(->)@,
 499 -- with an infix notation more readable.
 500 (~>) :: forall cs a b. Inj_Const cs (->)
 501  => Type cs a -> Type cs b -> Type cs (a -> b)
 502 (~>) a b = tyFun :$ a :$ b
 503 infixr 5 ~>
 504
 505 syFun :: IsString a => [Syntax a] -> Syntax a
 506 syFun = Syntax "(->)"
 507
 508 (.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
 509 a .> b = syFun [a, b]
 510 infixr 3 .>
 511
 512 syLam :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
 513 syLam arg ty body = Syntax "\\" [arg, ty, body]
 514
 515 syApp :: IsString a => Syntax a -> Syntax a -> Syntax a
 516 syApp lam_ arg = Syntax " " [lam_, arg]
 517 infixl 0 `syApp`
 518
 519 syLet :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
 520 syLet name bound body = Syntax "let" [name, bound, body]
 521
 522 {-
 523 -- * Checks
 524
 525 -- | Parsing utility to check that the type resulting
 526 -- from the application of a given type family to a given type
 527 -- is within the type stack,
 528 -- or raise 'Error_Term_Type_mismatch'.
 529 check_type0_family
 530  :: forall ast is tf root ty h ret.
 531  ( root ~ Root_of_Expr is
 532  , ty ~ Type_Root_of_Expr is
 533  , Type0_Family tf ty
 534  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 535                    (Error_of_Expr ast root)
 536  ) => Proxy tf -> Proxy is -> ast -> ty h
 537  -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
 538  -> Either (Error_of_Expr ast root) ret
 539 check_type0_family tf is ast ty k =
 540         case type0_family tf ty of
 541          Just t -> k t
 542          Nothing -> Left $ error_expr is $
 543                 Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
 544
 545 -}