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_Family_instance_missing (At ast ()) {-fam-}Text [EType (Consts_of_Ifaces is)]
 274  |   Error_Term_Typing (At ast (Error_Type (Consts_of_Ifaces is) ast))
 275  |   Error_Term_Type_mismatch (At ast (EType (Consts_of_Ifaces is)))
 276                               (At ast (EType (Consts_of_Ifaces is)))
 277  |   Error_Term_Type_is_not_an_application (At ast (EType (Consts_of_Ifaces is)))
 278 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Term is ast)
 279 deriving instance (Show ast, Show (Lexem ast), Show_Const (Consts_of_Ifaces is)) => Show (Error_Term is ast)
 280
 281 instance Lift_Error_Syntax (Error_Term is) where
 282         lift_error_syntax = Error_Term_Syntax
 283
 284 -- ** Checks
 285
 286 -- | Check that the 'kind_of' a given 'Type's equals a given kind,
 287 -- or fail with 'Error_Type_Kind_mismatch'.
 288 check_kind
 289  :: ast -> SKind k
 290  -> At ast (Type (Consts_of_Ifaces is) (t::kt))
 291  -> ((k :~: kt) -> Either (Error_Term is ast) ret)
 292  -> Either (Error_Term is ast) ret
 293 check_kind ast ki (At at_ty ty) k =
 294         let ki_ty = kind_of ty in
 295         case eq_skind ki ki_ty of
 296          Just Refl -> k Refl
 297          Nothing -> Left $ Error_Term_Typing $
 298                 At (Just ast) $
 299                 Error_Type_Kind_mismatch
 300                  (At Nothing $ EKind SKiType)
 301                  (At at_ty $ EKind ki_ty)
 302
 303 -- | Check that a given 'Type' is a /type application/,
 304 -- or fail with 'Error_Term_Type_is_not_an_application'.
 305 check_app
 306  :: ast -> Type (Consts_of_Ifaces is) (fx::kfx)
 307  -> (forall kx f x. (fx :~: f x)
 308   -> Type (Consts_of_Ifaces is) (f::kx -> kfx)
 309   -> Type (Consts_of_Ifaces is) (x::kx)
 310   -> Either (Error_Term is ast) ret)
 311  -> Either (Error_Term is ast) ret
 312 check_app ast ty_fx k =
 313         case ty_fx of
 314          ty_f :$ ty_x -> k Refl ty_f ty_x
 315          _ -> Left $ Error_Term_Type_is_not_an_application $
 316                 At (Just ast) $ EType ty_fx
 317
 318 -- | Check that two given 'Type's are equal,
 319 -- or fail with 'Error_Term_Type_mismatch'.
 320 check_type
 321  :: At ast (Type (Consts_of_Ifaces is) x)
 322  -> At ast (Type (Consts_of_Ifaces is) y)
 323  -> ((x :~: y) -> Either (Error_Term is ast) ret)
 324  -> Either (Error_Term is ast) ret
 325 check_type (At at_x x) (At at_y y) k =
 326         case eq_type x y of
 327          Just Refl -> k Refl
 328          Nothing -> Left $ Error_Term_Type_mismatch
 329                  (At at_x $ EType x)
 330                  (At at_y $ EType y)
 331
 332 -- | Convenient wrapper to check for a 'Type' of kind: @* -> *@.
 333 check_type1
 334  :: Type (Consts_of_Ifaces is) ty
 335  -> ast
 336  -> Type (Consts_of_Ifaces is) (fx:: *)
 337  -> (forall x. (fx :~: ty x)
 338   -> Type (Consts_of_Ifaces is) (x:: *)
 339   -> Either (Error_Term is ast) ret)
 340  -> Either (Error_Term is ast) ret
 341 check_type1 ty ast_ta ty_ta k =
 342         check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
 343         check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 344         check_type (At Nothing ty) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 345         k Refl ty_ta_a
 346
 347 -- | Convenient wrapper to check for a 'Type' of kind: @* -> * -> *@.
 348 check_type2
 349  :: Type (Consts_of_Ifaces is) (ty:: * -> * -> *)
 350  -> ast -> Type (Consts_of_Ifaces is) a2b
 351  -> (forall a b. (a2b :~: (ty a b))
 352   -> Type (Consts_of_Ifaces is) a
 353   -> Type (Consts_of_Ifaces is) b
 354   -> Either (Error_Term is ast) ret)
 355  -> Either (Error_Term is ast) ret
 356 check_type2 ty ast ty_a2b k =
 357         check_app ast ty_a2b $ \Refl ty_a2b_a2 ty_a2b_b ->
 358         check_app ast ty_a2b_a2 $ \Refl ty_a2b_ty ty_a2b_a ->
 359         check_kind ast (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) (At (Just ast) ty_a2b_ty) $ \Refl ->
 360         check_type (At Nothing ty) (At (Just ast) ty_a2b_ty) $ \Refl ->
 361         k Refl ty_a2b_a ty_a2b_b
 362
 363 -- | Check that a given 'Constraint' holds,
 364 -- or fail with 'Error_Term_Constraint_not_deductible'.
 365 check_constraint
 366  :: Proj_Con (Consts_of_Ifaces is)
 367  => At ast (Type (Consts_of_Ifaces is) (q::Constraint))
 368  -> (Con q -> Either (Error_Term is ast) ret)
 369  -> Either (Error_Term is ast) ret
 370 check_constraint (At at_q q) k =
 371         case proj_con q of
 372          Just Con -> k Con
 373          Nothing -> Left $ Error_Term_Constraint_not_deductible $
 374                 At at_q $ KType q
 375
 376 -- | Convenient wrapper to check for a 'Constraint'
 377 -- over a 'Type' of kind: @* -> *@.
 378 check_constraint1
 379  :: Proj_Con (Consts_of_Ifaces is)
 380  => Type (Consts_of_Ifaces is) con
 381  -> ast -> Type (Consts_of_Ifaces is) (fx:: *)
 382  -> (forall f x. (fx :~: f x)
 383   -> Con (con f)
 384   -> Type (Consts_of_Ifaces is) (f:: * -> *)
 385   -> Type (Consts_of_Ifaces is) (x:: *)
 386   -> Either (Error_Term is ast) ret)
 387  -> Either (Error_Term is ast) ret
 388 check_constraint1 con ast_ta ty_ta k =
 389         check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
 390         check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
 391         check_constraint (At (Just ast_ta) (con :$ ty_ta_t)) $ \Con ->
 392         k Refl Con ty_ta_t ty_ta_a
 393
 394 -- | Check that a given /type family/ is supported,
 395 -- or fail with 'Error_Term_Family_instance_missing'.
 396 check_family ::
 397  ( Proj_Fam (Consts_of_Ifaces is) fam
 398  , Show fam
 399  ) => ast
 400  -> fam
 401  -> Types (Consts_of_Ifaces is) hs
 402  -> (Type (Consts_of_Ifaces is) (Fam fam hs) -> Either (Error_Term is ast) ret)
 403  -> Either (Error_Term is ast) ret
 404 check_family ast fam tys k =
 405         case proj_fam fam tys of
 406          Just t -> k t
 407          Nothing -> Left $ Error_Term_Family_instance_missing
 408                  (At (Just ast) ())
 409                  (Text.pack $ show fam)
 410                  (etypes tys)
 411
 412 -- * Class 'Sym_Lambda'
 413 class Sym_Lambda term where
 414         -- | /Lambda abstraction/.
 415         lam :: (term arg -> term res) -> term ((->) arg res)
 416         default lam :: Trans t term
 417          => (t term arg -> t term res)
 418          -> t term ((->) arg res)
 419         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
 420
 421         -- | /Lambda application/.
 422         (.$) :: term ((->) arg res) -> term arg -> term res
 423         default (.$) :: Trans t term
 424          => t term ((->) arg res) -> t term arg -> t term res
 425         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
 426
 427         -- | Convenient 'lam' and '.$' wrapper.
 428         let_ :: term var -> (term var -> term res) -> term res
 429         let_ x y = lam y .$ x
 430
 431         id :: term a -> term a
 432         id a = lam Fun.id .$ a
 433
 434         const :: term a -> term b -> term a
 435         const a b = lam (lam . Fun.const) .$ a .$ b
 436
 437         -- | /Lambda composition/.
 438         (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
 439         (#) f g = lam $ \a -> f .$ (g .$ a)
 440
 441         flip :: term (a -> b -> c) -> term (b -> a -> c)
 442         flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
 443
 444 infixl 0 .$
 445 infixr 9 #
 446
 447 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
 448 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
 449 type instance Consts_imported_by (->) =
 450  [ Proxy Applicative
 451  , Proxy Functor
 452  , Proxy Monad
 453  , Proxy Monoid
 454  ]
 455
 456 instance Sym_Lambda HostI where
 457         lam f = HostI (unHostI . f . HostI)
 458         (.$)  = (<*>)
 459 instance Sym_Lambda TextI where
 460         lam f = TextI $ \p v ->
 461                 let p' = Precedence 1 in
 462                 let x = "x" <> Text.pack (show v) in
 463                 paren p p' $ "\\" <> x <> " -> "
 464                  <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
 465         -- (.$) = textI_infix "$" (Precedence 0)
 466         (.$) (TextI a1) (TextI a2) =
 467                 TextI $ \p v ->
 468                         let p' = precedence_App in
 469                         paren p p' $ a1 p' v <> " " <> a2 p' v
 470         let_ e in_ =
 471                 TextI $ \p v ->
 472                         let p' = Precedence 2 in
 473                         let x = "x" <> Text.pack (show v) in
 474                         paren p p' $ "let" <> " " <> x <> " = "
 475                          <> unTextI e (Precedence 0) (succ v) <> " in "
 476                          <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
 477         (#)   = textI_infix "." (Precedence 9)
 478         id    = textI_app1 "id"
 479         const = textI_app2 "const"
 480         flip  = textI_app1 "flip"
 481 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
 482         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
 483                 where lam_f = lam f
 484         (.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
 485
 486 instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
 487         const_from "(->)" k = k (ConstZ kind)
 488         const_from s k = const_from s $ k . ConstS
 489 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 490         show_const ConstZ{} = "(->)"
 491         show_const (ConstS c) = show_const c
 492
 493 instance -- Proj_ConC (->)
 494  ( Proj_Const cs (->)
 495  , Proj_Consts cs (Consts_imported_by (->))
 496  , Proj_Con cs
 497  ) => Proj_ConC cs (Proxy (->)) where
 498         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 499          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 500          , Just Refl <- proj_const c (Proxy::Proxy (->))
 501          = case () of
 502                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 503                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 504                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 505                  _ -> Nothing
 506         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 507          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 508          , Just Refl <- proj_const c (Proxy::Proxy (->))
 509          = case () of
 510                  _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 511                    , Just Con  <- proj_con (t :$ b) -> Just Con
 512                  _ -> Nothing
 513         proj_conC _c _q = Nothing
 514 instance -- Term_fromI (->)
 515  ( AST ast
 516  , Lexem ast ~ LamVarName
 517  , Inj_Const  (Consts_of_Ifaces is) (->)
 518  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 519  , Term_from is ast
 520  ) => Term_fromI is (Proxy (->)) ast where
 521         term_fromI ast ctx k =
 522                 case ast_lexem ast of
 523                  "\\" -> -- lambda abstration
 524                         from_ast3 ast $ \ast_name ast_ty_arg ast_body as ->
 525                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 526                         type_from ast_ty_arg $ \ty_arg -> Right $
 527                         check_kind ast SKiType (At (Just ast) ty_arg) $ \Refl ->
 528                         term_from ast_body
 529                          (LamCtx_TypeS (ast_lexem ast_name) ty_arg ctx) $
 530                          \ty_res (TermLC res) ->
 531                         k as (ty_arg ~> ty_res) $ TermLC $
 532                          \c -> lam $ \arg ->
 533                                 res (arg `LamCtx_TermS` c)
 534                  " " -> -- lambda application
 535                         from_ast2 ast $ \ast_lam ast_arg_actual as ->
 536                         term_from ast_lam ctx $ \ty_lam (TermLC lam_) ->
 537                         term_from ast_arg_actual ctx $ \ty_arg_actual (TermLC arg_actual) ->
 538                         check_type2 tyFun ast_lam ty_lam $ \Refl ty_arg ty_res ->
 539                         check_type
 540                          (At (Just ast_lam) ty_arg)
 541                          (At (Just ast_arg_actual) ty_arg_actual) $ \Refl ->
 542                         k as ty_res $ TermLC $
 543                          \c -> lam_ c .$ arg_actual c
 544                  "let" ->
 545                         from_ast3 ast $ \ast_name ast_bound ast_body as ->
 546                         term_from ast_bound ctx $ \ty_bound (TermLC bound) ->
 547                         term_from ast_body (LamCtx_TypeS (ast_lexem ast_name) ty_bound ctx) $
 548                          \ty_res (TermLC res) ->
 549                         k as ty_res $ TermLC $
 550                          \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
 551                  _ -> Left $ Error_Term_unsupported
 552
 553 -- | The '(->)' 'Type'
 554 tyFun :: Inj_Const cs (->) => Type cs (->)
 555 tyFun = TyConst inj_const
 556
 557 -- | The function 'Type' @(->)@,
 558 -- with an infix notation more readable.
 559 (~>) :: forall cs a b. Inj_Const cs (->)
 560  => Type cs a -> Type cs b -> Type cs (a -> b)
 561 (~>) a b = tyFun :$ a :$ b
 562 infixr 5 ~>
 563
 564 syFun :: IsString a => [Syntax a] -> Syntax a
 565 syFun = Syntax "(->)"
 566
 567 (.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
 568 a .> b = syFun [a, b]
 569 infixr 3 .>
 570
 571 syLam :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
 572 syLam arg ty body = Syntax "\\" [arg, ty, body]
 573
 574 syApp :: IsString a => Syntax a -> Syntax a -> Syntax a
 575 syApp lam_ arg = Syntax " " [lam_, arg]
 576 infixl 0 `syApp`
 577
 578 syLet :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
 579 syLet name bound body = Syntax "let" [name, bound, body]
 580
 581 {-
 582 -- * Checks
 583
 584 -- | Parsing utility to check that the type resulting
 585 -- from the application of a given type family to a given type
 586 -- is within the type stack,
 587 -- or raise 'Error_Term_Type_mismatch'.
 588 check_type0_family
 589  :: forall ast is tf root ty h ret.
 590  ( root ~ Root_of_Expr is
 591  , ty ~ Type_Root_of_Expr is
 592  , Type0_Family tf ty
 593  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 594                    (Error_of_Expr ast root)
 595  ) => Proxy tf -> Proxy is -> ast -> ty h
 596  -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
 597  -> Either (Error_of_Expr ast root) ret
 598 check_type0_family tf is ast ty k =
 599         case type0_family tf ty of
 600          Just t -> k t
 601          Nothing -> Left $ error_expr is $
 602                 Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
 603
 604 -}