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