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
 109                  :: forall lc ret.
 110                     Lexem ast
 111                  -> LamCtx_Type is (Lexem ast) lc
 112                  -> ( forall h.
 113                        Type (Consts_of_Ifaces is) (h::Kind.Type)
 114                     -> TermLC lc h is '[] is
 115                     -> Either (Error_Term is ast) ret )
 116                  -> Either (Error_Term is ast) ret
 117                 replace_var name lc k' =
 118                         case lc of
 119                          LamCtx_TypeZ -> Left $ Error_Term_unsupported
 120                          LamCtx_TypeS n ty _ | n == name ->
 121                                 k' ty $ TermLC $ \(te `LamCtx_TermS` _) -> te
 122                          LamCtx_TypeS _n _ty lc' ->
 123                                 replace_var name lc' $ \ty (TermLC te::TermLC lc' h is '[] is) ->
 124                                 k' ty $ TermLC $ \(_ `LamCtx_TermS` c) -> te c
 125
 126 -- ** Type 'Term_fromT'
 127 -- | Convenient type synonym defining a term parser.
 128 type Term_fromT ast ctx ret is ls rs
 129  = ast
 130  -> LamCtx_Type is (Lexem ast) ctx
 131  -- ^ The bound variables in scope and their types:
 132  -- built top-down in the heterogeneous list @ctx@,
 133  -- from the closest including /lambda abstraction/ to the farest.
 134  -> ( forall h.
 135        Type (Consts_of_Ifaces is) (h::Kind.Type)
 136     -> TermLC ctx h is ls rs
 137     -> Either (Error_Term is ast) ret )
 138  -- ^ The accumulating continuation called bottom-up.
 139  -> Either (Error_Term is ast) ret
 140
 141 -- ** Type 'Term_fromIT'
 142 -- | Almost like 'Term_fromT', but with the remaining 'ast_nodes'
 143 -- given to the continuation so that 'term_apply' can be used within
 144 -- the instance 'Term_fromR'@ is ls (i ': rs) ast@.
 145 type Term_fromIT ast ctx ret is ls rs
 146  = ast
 147  -> LamCtx_Type is (Lexem ast) ctx
 148  -> ( forall h.
 149        [ast]
 150     -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 151     -> TermLC ctx h is ls rs
 152     -> Either (Error_Term is ast) ret )
 153  -> Either (Error_Term is ast) ret
 154
 155 -- ** Class 'Term_fromR'
 156 -- | Intermediate type class to construct an instance of 'Term_from'
 157 -- from many instances of 'Term_fromI', one for each item of @is@.
 158 --
 159 -- * @is@: starting  list of /term constants/.
 160 -- * @ls@: done      list of /term constants/.
 161 -- * @rs@: remaining list of /term constants/.
 162 class Term_fromR (is::[*]) (ls::[*]) (rs::[*]) ast where
 163         term_fromR :: Term_fromT ast ctx ret is ls rs
 164         default term_fromR :: AST ast => Term_fromT ast ctx ret is ls rs
 165         term_fromR ast _ctx _k =
 166                 Left $ Error_Term_unknown $
 167                 At (Just ast) $ ast_lexem ast
 168
 169 -- | Test whether @i@ handles the work of 'Term_from' or not,
 170 -- or recurse on @rs@, preserving the starting list of /term constants/,
 171 -- and keeping a list of those done to construct 'TermLC'.
 172 instance
 173  ( Term_fromI is i ast
 174  , Term_fromR is (i ': ls) rs ast
 175  , Term_from is ast
 176  , Inj_Const (Consts_of_Ifaces is) (->)
 177  ) => Term_fromR is ls (i ': rs) ast where
 178         term_fromR ast ctx k =
 179                 case term_fromI ast ctx $ \as ty (TermLC te
 180                  ::TermLC ctx h is ls (i ': rs)) ->
 181                         term_apply ast as ctx ty (TermLC te) k of
 182                  Left Error_Term_unsupported ->
 183                         term_fromR ast ctx $ \ty (TermLC te
 184                          ::TermLC ctx h is (i ': ls) rs) ->
 185                                 k ty (TermLC te
 186                                  ::TermLC ctx h is ls (i ': rs))
 187                  x -> x
 188 -- | End the recursion.
 189 instance AST ast => Term_fromR is ls '[] ast
 190
 191 -- | Apply the given @ast@s to the given 'TermLC',
 192 -- or return an 'Error_Term'.
 193 term_apply ::
 194  ( Term_from is ast
 195  , Inj_Const (Consts_of_Ifaces is) (->)
 196  ) => ast -> [ast]
 197  -> LamCtx_Type is (Lexem ast) ctx
 198  -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 199  -> TermLC ctx h is ls rs
 200  -> ( forall h'.
 201        Type (Consts_of_Ifaces is) (h' ::Kind.Type)
 202     -> TermLC ctx h' is ls rs
 203     -> Either (Error_Term is ast) ret )
 204  -> Either (Error_Term is ast) ret
 205 term_apply ast_f args ctx ty_f te_f@(TermLC f) k =
 206         case args of
 207          [] -> k ty_f te_f
 208          ast_a:as ->
 209                 term_from ast_a ctx $ \ty_a (TermLC a) ->
 210                 check_type2 tyFun ast_f ty_f $ \Refl ty_arg ty_res ->
 211                 check_type (At (Just ast_f) ty_arg) (At (Just ast_a) ty_a) $ \Refl ->
 212                 term_apply ast_f as ctx ty_res (TermLC $ \c -> f c .$ a c) k
 213
 214 -- ** Class 'Term_fromI'
 215 -- | Handle the work of 'Term_from' for a given /interface/ @i@,
 216 -- that is: maybe it handles the given /interface/,
 217 -- and if so, maybe the term can be parsed.
 218 class Term_fromI (is::[*]) (i:: *) ast where
 219         term_fromI :: Term_fromIT ast ctx ret is ls (i ': rs)
 220         term_fromI _ast _ctx _k = Left $ Error_Term_unsupported
 221
 222 -- * Type family 'Sym_of_Ifaces'
 223 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
 224         Sym_of_Ifaces '[] term = ()
 225         Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
 226
 227 -- ** Type family 'Sym_of_Iface'
 228 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
 229
 230 -- * Type 'Consts_of_Ifaces'
 231 type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)
 232
 233 -- ** Type family 'Consts_of_IfaceR'
 234 type family Consts_of_IfaceR (is::[*]) where
 235         Consts_of_IfaceR '[] = '[]
 236         Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
 237
 238 -- ** Type family 'Consts_of_Iface'
 239 type family   Consts_of_Iface (i::k) :: [*]
 240 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
 241
 242 -- * Type 'LamCtx_Type'
 243 -- | GADT for a typing context,
 244 -- accumulating an @item@ at each lambda;
 245 -- used to accumulate object-types (in 'Expr_From')
 246 -- or host-terms (in 'HostI')
 247 -- associated with the 'LamVar's in scope.
 248 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
 249         LamCtx_TypeZ :: LamCtx_Type is name '[]
 250         LamCtx_TypeS :: name
 251                      -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 252                      -> LamCtx_Type is name hs
 253                      -> LamCtx_Type is name (h ': hs)
 254 infixr 5 `LamCtx_TypeS`
 255
 256 -- ** Type 'LamVarName'
 257 type LamVarName = Text
 258
 259 -- * Type 'LamCtx_Term'
 260 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 261         LamCtx_TermZ :: LamCtx_Term term '[]
 262         LamCtx_TermS :: term h
 263                      -> LamCtx_Term term hs
 264                      -> LamCtx_Term term (h ': hs)
 265 infixr 5 `LamCtx_TermS`
 266
 267 -- * Type 'Error_Term'
 268 data Error_Term (is::[*]) ast
 269  =   Error_Term_unknown (At ast (Lexem ast))
 270  |   Error_Term_unsupported
 271  |   Error_Term_Syntax (Error_Syntax ast)
 272  |   Error_Term_Constraint_not_deductible (At ast (KType (Consts_of_Ifaces is) Constraint))
 273  |   Error_Term_Typing (At ast (Error_Type (Consts_of_Ifaces is) ast))
 274  |   Error_Term_Type_mismatch (At ast (EType (Consts_of_Ifaces is)))
 275                               (At ast (EType (Consts_of_Ifaces is)))
 276  |   Error_Term_Type_is_not_an_application (At ast (EType (Consts_of_Ifaces is)))
 277 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Term is ast)
 278 deriving instance (Show ast, Show (Lexem ast), Show_Const (Consts_of_Ifaces is)) => Show (Error_Term is ast)
 279
 280 instance Lift_Error_Syntax (Error_Term is) where
 281         lift_error_syntax = Error_Term_Syntax
 282
 283 -- ** Checks
 284
 285 -- | Check that the 'kind_of' a given 'Type's equals a given kind,
 286 -- or fail with 'Error_Type_Kind_mismatch'.
 287 check_kind
 288  :: ast -> SKind k
 289  -> At ast (Type (Consts_of_Ifaces is) (t::kt))
 290  -> ((k :~: kt) -> Either (Error_Term is ast) ret)
 291  -> Either (Error_Term is ast) ret
 292 check_kind ast ki (At at_ty ty) k =
 293         let ki_ty = kind_of ty in
 294         case eq_skind ki ki_ty of
 295          Just Refl -> k Refl
 296          Nothing -> Left $ Error_Term_Typing $
 297                 At (Just ast) $
 298                 Error_Type_Kind_mismatch
 299                  (At Nothing $ EKind SKiType)
 300                  (At at_ty $ EKind ki_ty)
 301
 302 -- | Check that a given 'Type' is a /type application/,
 303 -- or fail with 'Error_Term_Type_is_not_an_application'.
 304 check_app
 305  :: ast -> Type (Consts_of_Ifaces is) (fx::kfx)
 306  -> (forall kx f x. (fx :~: f x)
 307   -> Type (Consts_of_Ifaces is) (f::kx -> kfx)
 308   -> Type (Consts_of_Ifaces is) (x::kx)
 309   -> Either (Error_Term is ast) ret)
 310  -> Either (Error_Term is ast) ret
 311 check_app ast ty_fx k =
 312         case ty_fx of
 313          ty_f :$ ty_x -> k Refl ty_f ty_x
 314          _ -> Left $ Error_Term_Type_is_not_an_application $
 315                 At (Just ast) $ EType ty_fx
 316
 317 -- | Check that two given 'Type's are equal,
 318 -- or fail with 'Error_Term_Type_mismatch'.
 319 check_type
 320  :: At ast (Type (Consts_of_Ifaces is) x)
 321  -> At ast (Type (Consts_of_Ifaces is) y)
 322  -> ((x :~: y) -> Either (Error_Term is ast) ret)
 323  -> Either (Error_Term is ast) ret
 324 check_type (At at_x x) (At at_y y) k =
 325         case eq_type x y of
 326          Just Refl -> k Refl
 327          Nothing -> Left $ Error_Term_Type_mismatch
 328                  (At at_x $ EType x)
 329                  (At at_y $ EType y)
 330
 331 -- | Convenient wrapper to check for a 'Type' of kind: @* -> *@.
 332 check_type1
 333  :: Type (Consts_of_Ifaces is) ty
 334  -> ast
 335  -> Type (Consts_of_Ifaces is) (fx:: *)
 336  -> (forall x. (fx :~: ty x)
 337   -> Type (Consts_of_Ifaces is) (x:: *)
 338   -> Either (Error_Term is ast) ret)
 339  -> Either (Error_Term is ast) ret
 340 check_type1 ty ast_ta ty_ta k =
 341         check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
 342         check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 343         check_type (At Nothing ty) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 344         k Refl ty_ta_a
 345
 346 -- | Convenient wrapper to check for a 'Type' of kind: @* -> * -> *@.
 347 check_type2
 348  :: Type (Consts_of_Ifaces is) (ty:: * -> * -> *)
 349  -> ast -> Type (Consts_of_Ifaces is) a2b
 350  -> (forall a b. (a2b :~: (ty a b))
 351   -> Type (Consts_of_Ifaces is) a
 352   -> Type (Consts_of_Ifaces is) b
 353   -> Either (Error_Term is ast) ret)
 354  -> Either (Error_Term is ast) ret
 355 check_type2 ty ast ty_a2b k =
 356         check_app ast ty_a2b $ \Refl ty_a2b_a2 ty_a2b_b ->
 357         check_app ast ty_a2b_a2 $ \Refl ty_a2b_ty ty_a2b_a ->
 358         check_kind ast (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) (At (Just ast) ty_a2b_ty) $ \Refl ->
 359         check_type (At Nothing ty) (At (Just ast) ty_a2b_ty) $ \Refl ->
 360         k Refl ty_a2b_a ty_a2b_b
 361
 362 -- | Check that a given 'Constraint' holds,
 363 -- or fail with 'Error_Term_Constraint_not_deductible'.
 364 check_constraint
 365  :: Proj_Con (Consts_of_Ifaces is)
 366  => At ast (Type (Consts_of_Ifaces is) (q::Constraint))
 367  -> (Con q -> Either (Error_Term is ast) ret)
 368  -> Either (Error_Term is ast) ret
 369 check_constraint (At at_q q) k =
 370         case proj_con q of
 371          Just Con -> k Con
 372          Nothing -> Left $ Error_Term_Constraint_not_deductible $
 373                 At at_q $ KType q
 374
 375 -- | Convenient wrapper to check for a 'Constraint'
 376 -- over a 'Type' of kind: @* -> *@.
 377 check_constraint1
 378  :: Proj_Con (Consts_of_Ifaces is)
 379  => Type (Consts_of_Ifaces is) con
 380  -> ast -> Type (Consts_of_Ifaces is) (fx:: *)
 381  -> (forall f x. (fx :~: f x)
 382   -> Con (con f)
 383   -> Type (Consts_of_Ifaces is) (f:: * -> *)
 384   -> Type (Consts_of_Ifaces is) (x:: *)
 385   -> Either (Error_Term is ast) ret)
 386  -> Either (Error_Term is ast) ret
 387 check_constraint1 con ast_ta ty_ta k =
 388         check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
 389         check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 390         check_constraint (At (Just ast_ta) (con :$ ty_ta_t)) $ \Con ->
 391         k Refl Con ty_ta_t ty_ta_a
 392
 393 -- * Class 'Sym_Lambda'
 394 class Sym_Lambda term where
 395         -- | /Lambda abstraction/.
 396         lam :: (term arg -> term res) -> term ((->) arg res)
 397         default lam :: Trans t term
 398          => (t term arg -> t term res)
 399          -> t term ((->) arg res)
 400         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
 401
 402         -- | /Lambda application/.
 403         (.$) :: term ((->) arg res) -> term arg -> term res
 404         default (.$) :: Trans t term
 405          => t term ((->) arg res) -> t term arg -> t term res
 406         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
 407
 408         -- | Convenient 'lam' and '.$' wrapper.
 409         let_ :: term var -> (term var -> term res) -> term res
 410         let_ x y = lam y .$ x
 411
 412         id :: term a -> term a
 413         id a = lam Fun.id .$ a
 414
 415         const :: term a -> term b -> term a
 416         const a b = lam (lam . Fun.const) .$ a .$ b
 417
 418         -- | /Lambda composition/.
 419         (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
 420         (#) f g = lam $ \a -> f .$ (g .$ a)
 421
 422         flip :: term (a -> b -> c) -> term (b -> a -> c)
 423         flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
 424
 425 infixl 0 .$
 426 infixr 9 #
 427
 428 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
 429 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
 430 type instance Consts_imported_by (->) =
 431  [ Proxy Applicative
 432  , Proxy Functor
 433  , Proxy Monad
 434  , Proxy Monoid
 435  ]
 436
 437 instance Sym_Lambda HostI where
 438         lam f = HostI (unHostI . f . HostI)
 439         (.$)  = (<*>)
 440 instance Sym_Lambda TextI where
 441         lam f = TextI $ \p v ->
 442                 let p' = Precedence 1 in
 443                 let x = "x" <> Text.pack (show v) in
 444                 paren p p' $ "\\" <> x <> " -> "
 445                  <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
 446         -- (.$) = textI_infix "$" (Precedence 0)
 447         (.$) (TextI a1) (TextI a2) =
 448                 TextI $ \p v ->
 449                         let p' = precedence_App in
 450                         paren p p' $ a1 p' v <> " " <> a2 p' v
 451         let_ e in_ =
 452                 TextI $ \p v ->
 453                         let p' = Precedence 2 in
 454                         let x = "x" <> Text.pack (show v) in
 455                         paren p p' $ "let" <> " " <> x <> " = "
 456                          <> unTextI e (Precedence 0) (succ v) <> " in "
 457                          <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
 458         (#)   = textI_infix "." (Precedence 9)
 459         id    = textI_app1 "id"
 460         const = textI_app2 "const"
 461         flip  = textI_app1 "flip"
 462 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
 463         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
 464                 where lam_f = lam f
 465         (.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
 466
 467 instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
 468         const_from "(->)" k = k (ConstZ kind)
 469         const_from s k = const_from s $ k . ConstS
 470 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 471         show_const ConstZ{} = "(->)"
 472         show_const (ConstS c) = show_const c
 473
 474 instance -- Proj_ConC (->)
 475  ( Proj_Const cs (->)
 476  , Proj_Consts cs (Consts_imported_by (->))
 477  , Proj_Con cs
 478  ) => Proj_ConC cs (Proxy (->)) where
 479         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 480          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 481          , Just Refl <- proj_const c (Proxy::Proxy (->))
 482          = Just $ case () of
 483                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 484                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 485                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 486                  _ -> Nothing
 487         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 488          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 489          , Just Refl <- proj_const c (Proxy::Proxy (->))
 490          = Just $ case () of
 491                  _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 492                    , Just Con  <- proj_con (t :$ b) -> Just Con
 493                  _ -> Nothing
 494         proj_conC _c _q = Nothing
 495 instance -- Term_fromI (->)
 496  ( AST ast
 497  , Lexem ast ~ LamVarName
 498  , Inj_Const  (Consts_of_Ifaces is) (->)
 499  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 500  , Term_from is ast
 501  ) => Term_fromI is (Proxy (->)) ast where
 502         term_fromI ast ctx k =
 503                 case ast_lexem ast of
 504                  "\\" -> -- lambda abstration
 505                         from_ast3 ast $ \ast_name ast_ty_arg ast_body as ->
 506                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 507                         type_from ast_ty_arg $ \ty_arg -> Right $
 508                         check_kind ast SKiType (At (Just ast) ty_arg) $ \Refl ->
 509                         term_from ast_body
 510                          (LamCtx_TypeS (ast_lexem ast_name) ty_arg ctx) $
 511                          \ty_res (TermLC res) ->
 512                         k as (ty_arg ~> ty_res) $ TermLC $
 513                          \c -> lam $ \arg ->
 514                                 res (arg `LamCtx_TermS` c)
 515                  " " -> -- lambda application
 516                         from_ast2 ast $ \ast_lam ast_arg_actual as ->
 517                         term_from ast_lam ctx $ \ty_lam (TermLC lam_) ->
 518                         term_from ast_arg_actual ctx $ \ty_arg_actual (TermLC arg_actual) ->
 519                         check_type2 tyFun ast_lam ty_lam $ \Refl ty_arg ty_res ->
 520                         check_type
 521                          (At (Just ast_lam) ty_arg)
 522                          (At (Just ast_arg_actual) ty_arg_actual) $ \Refl ->
 523                         k as ty_res $ TermLC $
 524                          \c -> lam_ c .$ arg_actual c
 525                  "let" ->
 526                         from_ast3 ast $ \ast_name ast_bound ast_body as ->
 527                         term_from ast_bound ctx $ \ty_bound (TermLC bound) ->
 528                         term_from ast_body (LamCtx_TypeS (ast_lexem ast_name) ty_bound ctx) $
 529                          \ty_res (TermLC res) ->
 530                         k as ty_res $ TermLC $
 531                          \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
 532                  _ -> Left $ Error_Term_unsupported
 533
 534 -- | The '(->)' 'Type'
 535 tyFun :: Inj_Const cs (->) => Type cs (->)
 536 tyFun = TyConst inj_const
 537
 538 -- | The function 'Type' @(->)@,
 539 -- with an infix notation more readable.
 540 (~>) :: forall cs a b. Inj_Const cs (->)
 541  => Type cs a -> Type cs b -> Type cs (a -> b)
 542 (~>) a b = tyFun :$ a :$ b
 543 infixr 5 ~>
 544
 545 syFun :: IsString a => [Syntax a] -> Syntax a
 546 syFun = Syntax "(->)"
 547
 548 (.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
 549 a .> b = syFun [a, b]
 550 infixr 3 .>
 551
 552 syLam :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
 553 syLam arg ty body = Syntax "\\" [arg, ty, body]
 554
 555 syApp :: IsString a => Syntax a -> Syntax a -> Syntax a
 556 syApp lam_ arg = Syntax " " [lam_, arg]
 557 infixl 0 `syApp`
 558
 559 syLet :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
 560 syLet name bound body = Syntax "let" [name, bound, body]
 561
 562 {-
 563 -- * Checks
 564
 565 -- | Parsing utility to check that the type resulting
 566 -- from the application of a given type family to a given type
 567 -- is within the type stack,
 568 -- or raise 'Error_Term_Type_mismatch'.
 569 check_type0_family
 570  :: forall ast is tf root ty h ret.
 571  ( root ~ Root_of_Expr is
 572  , ty ~ Type_Root_of_Expr is
 573  , Type0_Family tf ty
 574  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 575                    (Error_of_Expr ast root)
 576  ) => Proxy tf -> Proxy is -> ast -> ty h
 577  -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
 578  -> Either (Error_of_Expr ast root) ret
 579 check_type0_family tf is ast ty k =
 580         case type0_family tf ty of
 581          Just t -> k t
 582          Nothing -> Left $ error_expr is $
 583                 Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
 584
 585 -}