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 TypeOperators #-}
  16 {-# LANGUAGE UndecidableInstances #-}
  17 {-# OPTIONS_GHC -fno-warn-orphans #-}
  18 module Language.Symantic.Compiling.Term where
  19
  20 import Data.Proxy (Proxy(..))
  21 import Data.Text (Text)
  22 import qualified Data.Function as Fun
  23 import Data.Monoid ((<>))
  24 import qualified Data.Text as Text
  25 import Data.Type.Equality
  26 import GHC.Exts (Constraint)
  27 import Prelude hiding (not)
  28
  29 import Language.Symantic.Lib.Data.Type.List
  30 import Language.Symantic.Typing
  31 import Language.Symantic.Interpreting
  32 import Language.Symantic.Transforming.Trans
  33
  34 -- * Type 'Term'
  35 -- | 'Term_of_LamCtx' applied on a 'LamCtx_Type'.
  36 data Term is h
  37  =   Term
  38  (forall term. ( Sym_of_Ifaces is term
  39                , Sym_Lambda term
  40                ) => term (UnProxy h))
  41
  42 -- ** Type 'Term_of_LamCtx'
  43 -- | A data type embedding a universal quantification
  44 -- over an interpreter @term@
  45 -- and qualified by the symantics of a term.
  46 --
  47 -- Moreover the term is abstracted by a 'LamCtx_Term'
  48 -- built top-down at parsing time
  49 -- to build a /Higher-Order Abstract Syntax/ (HOAS)
  50 -- for /lambda abstractions/ ('lam').
  51 --
  52 -- This data type is used to keep a parsed term polymorphic enough
  53 -- to stay interpretable by different interpreters.
  54 --
  55 -- * @(@'Sym_of_Ifaces'@ is term)@
  56 -- is needed to be able to use a term
  57 -- out of a @(@'Term_of_LamCtx'@ (@'Root_of_Expr'@ is))@
  58 -- into a @(@'Term_of_LamCtx'@ is)@,
  59 -- which happens when a symantic method includes a polymorphic type
  60 -- and thus calls: 'term_from'@ (Proxy::Proxy (@'Root_of_Expr'@ is))@.
  61 --
  62 -- * @'@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
  63 -- are needed to be able to write the instance:
  64 -- @(@'Term_fromR'@ is ls (i ': rs) ast)@.
  65 --
  66 -- * @(@'Sym_Lambda'@ term)@
  67 -- is needed to be able to parse partially applied functions
  68 -- (when their type is knowable).
  69 data Term_of_LamCtx ctx h is ls rs
  70  =   Term_of_LamCtx
  71  (forall term. ( Sym_of_Ifaces is term
  72                , Sym_of_Ifaces ls term
  73                , Sym_of_Ifaces rs term
  74                , Sym_Lambda term
  75                ) => LamCtx_Term term ctx -> term (UnProxy h))
  76
  77 -- ** Type 'ETerm'
  78 -- | Existential 'Term', with its 'Type'.
  79 data ETerm is
  80  = forall h. ETerm
  81    (Type (Consts_of_Ifaces is) 'KiTerm h)
  82    (Term is h)
  83
  84 -- | Like 'term_from' but for a term with empty /lambda context/.
  85 root_term_from
  86  :: Term_from is ast
  87  => ast -> Either (Error_Term is ast) (ETerm is)
  88 root_term_from ast =
  89         term_from ast LamCtx_TypeZ $ \ty (Term_of_LamCtx te) ->
  90         Right $ ETerm ty $ Term $ te LamCtx_TermZ
  91
  92 -- * Type 'Term_from'
  93 -- | Convenient type synonym wrapping 'Term_fromR'
  94 -- to initiate its recursion.
  95 class Term_from is ast where
  96         term_from :: Term_fromT ast ctx ret is '[] is
  97 instance
  98  ( AST ast
  99  , Eq (Lexem ast)
 100  , Term_fromR is '[] is ast
 101  ) => Term_from is ast where
 102         term_from ast ctx k =
 103                 case replace_var (ast_lexem ast) ctx k of
 104                  Left Error_Term_unsupported -> term_fromR ast ctx k
 105                  x -> x
 106                 where
 107                 replace_var :: forall lc ret.
 108                       Lexem ast
 109                    -> LamCtx_Type is (Lexem ast) lc
 110                    -> ( forall h.
 111                          Type (Consts_of_Ifaces is) 'KiTerm h
 112                       -> Term_of_LamCtx lc h is '[] is
 113                       -> Either (Error_Term is ast) ret )
 114                    -> Either (Error_Term is ast) ret
 115                 replace_var name lc k' =
 116                         case lc of
 117                          LamCtx_TypeZ -> Left $ Error_Term_unsupported
 118                          LamCtx_TypeS n ty _ | n == name ->
 119                                 k' ty $ Term_of_LamCtx $ \(te `LamCtx_TermS` _) -> te
 120                          LamCtx_TypeS _n _ty lc' ->
 121                                 replace_var name lc' $ \ty (Term_of_LamCtx te::Term_of_LamCtx lc' h is '[] is) ->
 122                                 k' ty $ Term_of_LamCtx $ \(_ `LamCtx_TermS` c) -> te c
 123
 124 -- ** Type 'Term_fromT'
 125 -- | Convenient type synonym defining a term parser.
 126 type Term_fromT ast ctx ret is ls rs
 127  = ast
 128  -> LamCtx_Type is (Lexem ast) ctx
 129  -- ^ The bound variables in scope and their types:
 130  -- built top-down in the heterogeneous list @ctx@,
 131  -- from the closest including /lambda abstraction/ to the farest.
 132  -> ( forall h.
 133        Type (Consts_of_Ifaces is) 'KiTerm h
 134     -> Term_of_LamCtx ctx h is ls rs
 135     -> Either (Error_Term is ast) ret )
 136  -- ^ The accumulating continuation called bottom-up.
 137  -> Either (Error_Term is ast) ret
 138
 139 -- ** Class 'Term_fromR'
 140 -- | Intermediate type class to construct an instance of 'Term_from'
 141 -- from many instances of 'Term_fromI', one for each item of @is@.
 142 --
 143 -- * @is@: starting  list of /term constants/.
 144 -- * @ls@: done      list of /term constants/.
 145 -- * @rs@: remaining list of /term constants/.
 146 class AST ast => Term_fromR (is::[*]) (ls::[*]) (rs::[*]) ast where
 147         term_fromR :: Term_fromT ast ctx ret is ls rs
 148         term_fromR ast _ctx _k =
 149                 Left $ Error_Term_unknown $
 150                 At (Just ast) $ ast_lexem ast
 151
 152 -- | Test whether @i@ handles the work of 'Term_from' or not,
 153 -- or recurse on @rs@, preserving the starting list of /term constants/,
 154 -- and keeping a list of those done to construct 'Term_of_LamCtx'.
 155 instance
 156  ( Term_fromI is i ast
 157  , Term_fromR is (i ': ls) rs ast
 158  ) => Term_fromR is ls (i ': rs) ast where
 159         term_fromR ast ctx k =
 160                 case term_fromI ast ctx $ \ty (Term_of_LamCtx te
 161                  ::Term_of_LamCtx ctx h is ls (i ': rs)) ->
 162                         k ty (Term_of_LamCtx te) of
 163                  Left Error_Term_unsupported ->
 164                         term_fromR ast ctx $ \ty (Term_of_LamCtx te
 165                          ::Term_of_LamCtx ctx h is (i ': ls) rs) ->
 166                                 k ty (Term_of_LamCtx te
 167                                  ::Term_of_LamCtx ctx h is ls (i ': rs))
 168                  x -> x
 169 -- | End the recursion.
 170 instance AST ast => Term_fromR is ls '[] ast
 171
 172 -- * Type family 'Sym_of_Ifaces'
 173 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
 174         Sym_of_Ifaces '[] term = ()
 175         Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
 176
 177 -- ** Type family 'Sym_of_Iface'
 178 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
 179 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
 180
 181 -- ** Class 'Term_fromI'
 182 -- | Handle the work of 'Term_from' for a given /instance/ @i@,
 183 -- that is: maybe it handles the given /instance/,
 184 -- and if so, maybe the 'Constraint' holds.
 185 class AST ast => Term_fromI (is::[*]) (i:: *) ast where
 186         term_fromI :: Term_fromT ast ctx ret is ls (i ': rs)
 187         term_fromI _ast _ctx _k =
 188                 Left $ Error_Term_unsupported
 189 instance -- (->)
 190  ( AST ast
 191  , Lexem ast ~ LamVarName
 192  , Inj_Const (Consts_of_Ifaces is) (->)
 193  , Proj_Const (Consts_of_Ifaces is) (Proxy (->))
 194  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 195  , Term_from is ast
 196  ) => Term_fromI is (Proxy (->)) ast where
 197         term_fromI ast ctx k =
 198                 case ast_lexem ast of
 199                  "\\" ->
 200                         from_ast3 ast $ \ast_name ast_ty_arg ast_body ->
 201                                 either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 202                                 type_from ast_ty_arg $ \ty_arg -> Right $
 203                                 check_kind ast SKiTerm (At (Just ast) ty_arg) $ \Refl ->
 204                                 term_from ast_body
 205                                  (LamCtx_TypeS (ast_lexem ast_name) ty_arg ctx) $
 206                                  \ty_res (Term_of_LamCtx res) ->
 207                                 k (ty_arg ~> ty_res) $ Term_of_LamCtx $
 208                                  \c -> lam $ \arg ->
 209                                         res (arg `LamCtx_TermS` c)
 210                  " " ->
 211                         from_ast2 ast $ \ast_lam ast_arg_actual ->
 212                                 term_from ast_lam ctx $ \ty_lam (Term_of_LamCtx lam_) ->
 213                                 term_from ast_arg_actual ctx $ \ty_arg_actual (Term_of_LamCtx arg_actual) ->
 214                                 case ty_lam of
 215                                  TyConst co_fun :$ ty_arg :$ ty_res
 216                                   | Just Refl <- proj_const co_fun (Proxy::Proxy (->)) ->
 217                                         check_type
 218                                          (At (Just ast_lam) ty_arg)
 219                                          (At (Just ast_arg_actual) ty_arg_actual) $ \Refl ->
 220                                         k ty_res $ Term_of_LamCtx $
 221                                          \c -> lam_ c .$ arg_actual c
 222                                  _ -> Left $ Error_Term_not_applicable $
 223                                         At (Just ast) $ EType ty_lam
 224                  "let" ->
 225                         from_ast3 ast $ \ast_name ast_var ast_body ->
 226                                 term_from ast_var ctx $ \ty_var (Term_of_LamCtx var) ->
 227                                 term_from ast_body (LamCtx_TypeS (ast_lexem ast_name) ty_var ctx) $
 228                                  \ty_res (Term_of_LamCtx res) ->
 229                                 k ty_res $ Term_of_LamCtx $
 230                                  \c -> let_ (var c) $ \arg -> res (arg `LamCtx_TermS` c)
 231                  _ -> Left $ Error_Term_unsupported
 232 instance -- Applicative
 233  AST ast =>
 234  Term_fromI is (Proxy Applicative) ast
 235
 236 check_type
 237  :: AST ast
 238  => At ast (Type (Consts_of_Ifaces is) ki_x x)
 239  -> At ast (Type (Consts_of_Ifaces is) ki_y y)
 240  -> ((x :~: y) -> Either (Error_Term is ast) ret)
 241  -> Either (Error_Term is ast) ret
 242 check_type (At at_x x) (At at_y y) k =
 243         case eq_type x y of
 244          Just Refl -> k Refl
 245          Nothing -> Left $ Error_Term_Type_mismatch
 246                  (At at_x $ EType x)
 247                  (At at_y $ EType y)
 248
 249 check_kind
 250  :: AST ast
 251  => ast -> SKind ki
 252  -> At ast (Type (Consts_of_Ifaces is) ki_x x)
 253  -> ((ki :~: ki_x) -> Either (Error_Term is ast) ret)
 254  -> Either (Error_Term is ast) ret
 255 check_kind ast ki (At at_ty ty) k =
 256         let ki_ty = kind_of ty in
 257         case testEquality ki ki_ty of
 258          Just Refl -> k Refl
 259          Nothing -> Left $ Error_Term_Typing $
 260                 At (Just ast) $
 261                 Error_Type_Kind_mismatch
 262                  (At Nothing $ EKind SKiTerm)
 263                  (At at_ty $ EKind ki_ty)
 264
 265 check_constraint
 266  :: (AST ast, Proj_Con (Consts_of_Ifaces is))
 267  => At ast (Type (Consts_of_Ifaces is) 'KiCon q)
 268  -> (Con (UnProxy q) -> Either (Error_Term is ast) ret)
 269  -> Either (Error_Term is ast) ret
 270 check_constraint (At at_q q) k =
 271         case proj_con q of
 272          Just Con -> k Con
 273          Nothing -> Left $ Error_Term_Constraint_not_deductible $
 274                 At at_q $ KType q
 275
 276 -- * Type 'Error_Term'
 277 data Error_Term (is::[*]) ast
 278  =   Error_Term_unknown (At ast (Lexem ast))
 279  |   Error_Term_unsupported
 280  |   Error_Term_Syntax (Error_Syntax ast)
 281  |   Error_Term_Constraint_not_deductible (At ast (KType (Consts_of_Ifaces is) 'KiCon))
 282  |   Error_Term_Typing (At ast (Error_Type (Consts_of_Ifaces is) ast))
 283  |   Error_Term_Type_mismatch (At ast (EType (Consts_of_Ifaces is)))
 284                               (At ast (EType (Consts_of_Ifaces is)))
 285  |   Error_Term_not_applicable (At ast (EType (Consts_of_Ifaces is)))
 286 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Term is ast)
 287 deriving instance (Show ast, Show (Lexem ast), Show_Const (Consts_of_Ifaces is)) => Show (Error_Term is ast)
 288
 289 instance Lift_Error_Syntax (Error_Term is) where
 290         lift_error_syntax = Error_Term_Syntax
 291
 292 -- * Type 'Consts_of_Ifaces'
 293 type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)
 294
 295 -- ** Type family 'Consts_of_IfaceR'
 296 type family Consts_of_IfaceR (is::[*]) where
 297         Consts_of_IfaceR '[] = '[]
 298         Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
 299
 300 -- ** Type family 'Consts_of_Iface'
 301 type family   Consts_of_Iface (i:: *) :: [*]
 302 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
 303 type instance Consts_of_Iface (Proxy Bool) = Proxy Bool ': Consts_imported_by Bool
 304 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
 305 type instance Consts_of_Iface (Proxy Eq)   = Proxy Eq   ': Consts_imported_by Eq
 306 type instance Consts_of_Iface (Proxy Ord)  = Proxy Ord  ': Consts_imported_by Ord
 307
 308 -- * Type 'LamCtx_Type'
 309 -- | GADT for a typing context,
 310 -- accumulating an @item@ at each lambda;
 311 -- used to accumulate object-types (in 'Expr_From')
 312 -- or host-terms (in 'HostI')
 313 -- associated with the 'LamVar's in scope.
 314 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
 315         LamCtx_TypeZ :: LamCtx_Type is name '[]
 316         LamCtx_TypeS :: name
 317                      -> Type (Consts_of_Ifaces is) 'KiTerm h
 318                      -> LamCtx_Type is name hs
 319                      -> LamCtx_Type is name (h ': hs)
 320 infixr 5 `LamCtx_TypeS`
 321
 322 -- ** Type 'LamVarName'
 323 type LamVarName = Text
 324
 325 -- * Type 'LamCtx_Term'
 326 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 327         LamCtx_TermZ :: LamCtx_Term term '[]
 328         LamCtx_TermS :: term (UnProxy h)
 329                      -> LamCtx_Term term hs
 330                      -> LamCtx_Term term (h ': hs)
 331 infixr 5 `LamCtx_TermS`
 332
 333 -- * Class 'Sym_Lambda'
 334 class Sym_Lambda term where
 335         -- | /Lambda abstraction/.
 336         lam :: (term arg -> term res) -> term ((->) arg res)
 337         default lam :: Trans t term
 338          => (t term arg -> t term res)
 339          -> t term ((->) arg res)
 340         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
 341
 342         -- | /Lambda application/.
 343         (.$) :: term ((->) arg res) -> term arg -> term res
 344         default (.$) :: Trans t term
 345          => t term ((->) arg res) -> t term arg -> t term res
 346         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
 347
 348         -- | Convenient 'lam' and '.$' wrapper.
 349         let_ :: term var -> (term var -> term res) -> term res
 350         let_ x y = lam y .$ x
 351
 352         id :: term a -> term a
 353         id a = lam Fun.id .$ a
 354
 355         const :: term a -> term b -> term a
 356         const a b = lam (lam . Fun.const) .$ a .$ b
 357
 358         -- | /Lambda composition/.
 359         (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
 360         (#) f g = lam $ \a -> f .$ (g .$ a)
 361
 362         flip :: term (a -> b -> c) -> term (b -> a -> c)
 363         flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
 364
 365 infixl 0 .$
 366 infixr 9 #
 367
 368 instance Sym_Lambda HostI where
 369         lam f = HostI (unHostI . f . HostI)
 370         (.$)  = (<*>)
 371 instance Sym_Lambda TextI where
 372         lam f = TextI $ \p v ->
 373                 let p' = Precedence 1 in
 374                 let x = "x" <> Text.pack (show v) in
 375                 paren p p' $ "\\" <> x <> " -> "
 376                  <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
 377         -- (.$) = textI_infix "$" (Precedence 0)
 378         (.$) (TextI a1) (TextI a2) =
 379                 TextI $ \p v ->
 380                         let p' = precedence_App in
 381                         paren p p' $ a1 p' v <> " " <> a2 p' v
 382         let_ e in_ =
 383                 TextI $ \p v ->
 384                         let p' = Precedence 2 in
 385                         let x = "x" <> Text.pack (show v) in
 386                         paren p p' $ "let" <> " " <> x <> " = "
 387                          <> unTextI e (Precedence 0) (succ v) <> " in "
 388                          <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
 389         (#)   = textI_infix "." (Precedence 9)
 390         id    = textI_app1 "id"
 391         const = textI_app2 "const"
 392         flip  = textI_app1 "flip"
 393 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
 394         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
 395                 where lam_f = lam f
 396         (.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
 397
 398
 399 {-
 400 class IProxy (ty::ki) where
 401         proxy :: Proxy ty
 402         proxy = (Proxy::Proxy ty)
 403 instance IProxy ty
 404
 405 -}
 406
 407 {-
 408 -- * Checks
 409
 410 -- | Parsing utility to check that the type resulting
 411 -- from the application of a given type family to a given type
 412 -- is within the type stack,
 413 -- or raise 'Error_Term_Type_mismatch'.
 414 check_type0_family
 415  :: forall ast is tf root ty h ret.
 416  ( root ~ Root_of_Expr is
 417  , ty ~ Type_Root_of_Expr is
 418  , Type0_Family tf ty
 419  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 420                    (Error_of_Expr ast root)
 421  ) => Proxy tf -> Proxy is -> ast -> ty h
 422  -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
 423  -> Either (Error_of_Expr ast root) ret
 424 check_type0_family tf is ast ty k =
 425         case type0_family tf ty of
 426          Just t -> k t
 427          Nothing -> Left $ error_expr is $
 428                 Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
 429
 430 -- | Parsing utility to check that two types are equal,
 431 -- or raise 'Error_Term_Type_mismatch'.
 432 check_type0_eq
 433  :: forall ast is root ty x y ret.
 434  ( root ~ Root_of_Expr is
 435  , ty ~ Type_Root_of_Expr is
 436  , Type0_Eq ty
 437  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 438                    (Error_of_Expr ast root)
 439  ) => Proxy is -> ast -> ty x -> ty y
 440  -> (x :~: y -> Either (Error_of_Expr ast root) ret)
 441  -> Either (Error_of_Expr ast root) ret
 442 check_type0_eq is ast x y k =
 443         case x `type0_eq` y of
 444          Just Refl -> k Refl
 445          Nothing -> Left $ error_expr is $
 446                 Error_Term_Type_mismatch ast
 447                  (Exists_Type0 x)
 448                  (Exists_Type0 y)
 449
 450 -- | Parsing utility to check that two 'Type1' are equal,
 451 -- or raise 'Error_Term_Type_mismatch'.
 452 check_type1_eq
 453  :: forall ast is root ty h1 h2 a1 a2 ret.
 454  ( root ~ Root_of_Expr is
 455  , ty ~ Type_Root_of_Expr is
 456  , Type1_Eq ty
 457  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 458                    (Error_of_Expr ast root)
 459  )
 460  => Proxy is -> ast -> ty (h1 a1) -> ty (h2 a2)
 461  -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
 462  -> Either (Error_of_Expr ast root) ret
 463 check_type1_eq is ast h1 h2 k =
 464         case h1 `type1_eq` h2 of
 465          Just Refl -> k Refl
 466          Nothing -> Left $ error_expr is $
 467                 Error_Term_Type_mismatch ast
 468                  (Exists_Type0 h1)
 469                  (Exists_Type0 h2)
 470
 471 -- | Parsing utility to check that a 'Type0' or higher
 472 -- is an instance of a given 'Constraint',
 473 -- or raise 'Error_Term_Constraint_missing'.
 474 check_type0_constraint
 475  :: forall ast is c root ty h ret.
 476  ( root ~ Root_of_Expr is
 477  , ty ~ Type_Root_of_Expr is
 478  , Type0_Constraint c ty
 479  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 480                    (Error_of_Expr ast root)
 481  )
 482  => Proxy is -> Proxy c -> ast -> ty h
 483  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 484  -> Either (Error_of_Expr ast root) ret
 485 check_type0_constraint is c ast ty k =
 486         case type0_constraint c ty of
 487          Just Dict -> k Dict
 488          Nothing -> Left $ error_expr is $
 489                 Error_Term_Constraint_missing ast
 490                  {-(Exists_Dict c)-}
 491                  -- FIXME: not easy to report the constraint
 492                  -- and still support 'Eq' and 'Show' deriving.
 493                  (Exists_Type0 ty)
 494
 495 -- | Parsing utility to check that a 'Type1' or higher
 496 -- is an instance of a given 'Constraint',
 497 -- or raise 'Error_Term_Constraint_missing'.
 498 check_type1_constraint
 499  :: forall ast is c root ty h a ret.
 500  ( root ~ Root_of_Expr is
 501  , ty ~ Type_Root_of_Expr is
 502  , Type1_Constraint c ty
 503  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 504                    (Error_of_Expr ast root)
 505  ) => Proxy is -> Proxy c -> ast -> ty (h a)
 506  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 507  -> Either (Error_of_Expr ast root) ret
 508 check_type1_constraint is c ast ty k =
 509         case type1_constraint c ty of
 510          Just Dict -> k Dict
 511          Nothing -> Left $ error_expr is $
 512                 Error_Term_Constraint_missing ast
 513                  (Exists_Type0 ty)
 514
 515 -- | Parsing utility to check that the given type is at least a 'Type1'
 516 -- or raise 'Error_Term_Type_mismatch'.
 517 check_type1
 518  :: forall ast is root ty h ret.
 519  ( root ~ Root_of_Expr is
 520  , ty ~ Type_Root_of_Expr is
 521  , Type1_Unlift (Type_of_Expr root)
 522  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 523                    (Error_of_Expr ast root)
 524  ) => Proxy is -> ast -> ty h
 525  -> (forall (t1:: *).
 526      ( Type1 t1 ty h
 527      , Type1_Lift t1 ty (Type_Var0 :|: Type_Var1 :|: Type_of_Expr root)
 528      ) -> Either (Error_of_Expr ast root) ret)
 529  -> Either (Error_of_Expr ast root) ret
 530 check_type1 is ast ty k =
 531         (`fromMaybe` type1_unlift (unType_Root ty) (Just . k)) $
 532         Left $ error_expr is $
 533         Error_Term_Type_mismatch ast
 534          (Exists_Type0 (type_var1 SZero (type_var0 SZero)
 535          :: ty (Var1 Var0)))
 536          (Exists_Type0 ty)
 537
 538 -- * Parsers
 539
 540 -- | Like 'expr_from' but for a root expression.
 541 root_expr_from
 542  :: forall ast root.
 543  ( Expr_From ast root
 544  , Root_of_Expr root ~ root
 545  ) => Proxy root -> ast
 546  -> Either (Error_of_Expr ast root)
 547            (Exists_Type0_and_Repr (Type_Root_of_Expr root)
 548                                   (Term root))
 549 root_expr_from _ex ast =
 550         expr_from (Proxy::Proxy root) ast
 551          LamCtxZ $ \ty (Term_of_LamCtx term) ->
 552         Right $ Exists_Type0_and_Repr ty $
 553                 Term $ term LamCtxZ
 554
 555 -- | Parse a literal.
 556 lit_from
 557  :: forall ty lit is ast hs ret.
 558  ( ty ~ Type_Root_of_Expr is
 559  , Read lit
 560  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 561                    (Error_of_Expr ast (Root_of_Expr is))
 562  ) => (forall term. Sym_of_Iface is term => lit -> term lit)
 563  -> ty lit -> Text
 564  -> Term_fromT ast is hs ret
 565 lit_from lit ty_lit toread is ast _ctx k =
 566         case read_safe toread of
 567          Left err -> Left $ error_expr is $ Error_Term_Read err ast
 568          Right (i::lit) -> k ty_lit $ Term_of_LamCtx $ const $ lit i
 569
 570 -- | Parse a unary class operator.
 571 class_op1_from
 572  :: forall root ty cl is ast hs ret.
 573  ( ty ~ Type_Root_of_Expr is
 574  , root ~ Root_of_Expr is
 575  , Type0_Eq ty
 576  , Expr_From ast root
 577  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 578                    (Error_of_Expr ast root)
 579  , Root_of_Expr root ~ root
 580  , Type0_Constraint cl ty
 581  ) => (forall lit term. (cl lit, Sym_of_Iface is term) => term lit -> term lit)
 582  -> Proxy cl -> ast
 583  -> Term_fromT ast is hs ret
 584 class_op1_from op cl ast_x is _ast ctx k =
 585         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 586         check_type0_constraint is cl ast_x ty_x $ \Dict ->
 587         k ty_x $ Term_of_LamCtx (op . x)
 588
 589 -- | Parse a binary class operator.
 590 class_op2_from
 591  :: forall root ty cl is ast hs ret.
 592  ( ty ~ Type_Root_of_Expr is
 593  , root ~ Root_of_Expr is
 594  , Type0_Eq ty
 595  , Expr_From ast root
 596  , Type0_Constraint cl ty
 597  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 598                    (Error_of_Expr ast root)
 599  , Root_of_Expr root ~ root
 600  ) => (forall lit term. (cl lit, Sym_of_Iface is term) => term lit -> term lit -> term lit)
 601  -> Proxy cl -> ast -> ast
 602  -> Term_fromT ast is hs ret
 603 class_op2_from op cl ast_x ast_y is ast ctx k =
 604         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 605         expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
 606         check_type0_constraint is cl ast_x ty_x $ \Dict ->
 607         check_type0_constraint is cl ast_y ty_y $ \Dict ->
 608         check_type0_eq is ast ty_x ty_y $ \Refl ->
 609         k ty_x $ Term_of_LamCtx $
 610          \c -> x c `op` y c
 611
 612 -- | Parse a binary class operator, partially applied.
 613 class_op2_from1
 614  :: forall root ty cl is ast hs ret.
 615  ( ty ~ Type_Root_of_Expr is
 616  , root ~ Root_of_Expr is
 617  , Type0_Eq ty
 618  , Type0_Constraint cl ty
 619  , Type0_Lift Type_Fun (Type_of_Expr root)
 620  , Expr_From ast root
 621  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 622                    (Error_of_Expr ast root)
 623  , Root_of_Expr root ~ root
 624  ) => (forall lit term. (cl lit, Sym_of_Iface is term) => term lit -> term lit -> term lit)
 625  -> Proxy cl -> ast
 626  -> Term_fromT ast is hs ret
 627 class_op2_from1 op cl ast_x is _ast ctx k =
 628         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 629         check_type0_constraint is cl ast_x ty_x $ \Dict ->
 630         k (type_fun ty_x ty_x) $ Term_of_LamCtx $
 631          \c -> lam $ \y -> x c `op` y
 632
 633 -- | Parse a unary operator.
 634 op1_from
 635  :: forall root ty lit is ast hs ret.
 636  ( ty ~ Type_Root_of_Expr is
 637  , root ~ Root_of_Expr is
 638  , Type0_Eq ty
 639  , Expr_From ast root
 640  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 641                    (Error_of_Expr ast root)
 642  , Root_of_Expr root ~ root
 643  ) => (forall term. Sym_of_Iface is term => term lit -> term lit)
 644  -> ty lit -> ast
 645  -> Term_fromT ast is hs ret
 646 op1_from op ty_lit ast_x is ast ctx k =
 647         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 648         check_type0_eq is ast ty_lit ty_x $ \Refl ->
 649         k ty_x $ Term_of_LamCtx (op . x)
 650
 651 -- | Parse a unary operator, partially applied.
 652 op1_from0
 653  :: forall root ty lit is ast hs ret.
 654  ( ty ~ Type_Root_of_Expr is
 655  , root ~ Root_of_Expr is
 656  , Type0_Eq ty
 657  , Type0_Lift Type_Fun (Type_of_Expr root)
 658  , Expr_From ast root
 659  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 660                    (Error_of_Expr ast root)
 661  , Root_of_Expr root ~ root
 662  ) => (forall term. Sym_of_Iface is term => term lit -> term lit)
 663  -> ty lit
 664  -> Term_fromT ast is hs ret
 665 op1_from0 op ty_lit _ex _ast _ctx k =
 666         k (type_fun ty_lit ty_lit) $ Term_of_LamCtx $
 667          \_c -> lam op
 668
 669 -- | Parse a binary operator.
 670 op2_from
 671  :: forall root ty lit is ast hs ret.
 672  ( ty ~ Type_Root_of_Expr is
 673  , root ~ Root_of_Expr is
 674  , Type0_Eq ty
 675  , Expr_From ast root
 676  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 677                    (Error_of_Expr ast root)
 678  , Root_of_Expr root ~ root
 679  ) => (forall term. Sym_of_Iface is term => term lit -> term lit -> term lit)
 680  -> ty lit -> ast -> ast
 681  -> Term_fromT ast is hs ret
 682 op2_from op ty_lit ast_x ast_y is ast ctx k =
 683         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 684         expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
 685         check_type0_eq is ast ty_lit ty_x $ \Refl ->
 686         check_type0_eq is ast ty_lit ty_y $ \Refl ->
 687         k ty_x $ Term_of_LamCtx $
 688          \c -> x c `op` y c
 689
 690 -- | Parse a binary operator, partially applied.
 691 op2_from1
 692  :: forall root ty lit is ast hs ret.
 693  ( ty ~ Type_Root_of_Expr is
 694  , root ~ Root_of_Expr is
 695  , Type0_Eq ty
 696  , Type0_Lift Type_Fun (Type_of_Expr root)
 697  , Expr_From ast root
 698  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 699                    (Error_of_Expr ast root)
 700  , Root_of_Expr root ~ root
 701  ) => (forall term. Sym_of_Iface is term => term lit -> term lit -> term lit)
 702  -> ty lit -> ast
 703  -> Term_fromT ast is hs ret
 704 op2_from1 op ty_lit ast_x is ast ctx k =
 705         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 706         check_type0_eq is ast ty_lit ty_x $ \Refl ->
 707                 k (type_fun ty_x ty_x) $ Term_of_LamCtx $
 708                  \c -> lam $ \y -> x c `op` y
 709
 710 -- | Parse a binary operator, partially applied.
 711 op2_from0
 712  :: forall root ty lit is ast hs ret.
 713  ( ty ~ Type_Root_of_Expr is
 714  , root ~ Root_of_Expr is
 715  , Type0_Eq ty
 716  , Type0_Lift Type_Fun (Type_of_Expr root)
 717  , Expr_From ast root
 718  , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
 719                    (Error_of_Expr ast root)
 720  , Root_of_Expr root ~ root
 721  ) => (forall term. Sym_of_Iface is term => term lit -> term lit -> term lit)
 722  -> ty lit
 723  -> Term_fromT ast is hs ret
 724 op2_from0 op ty_lit _ex _ast _ctx k =
 725         k (type_fun ty_lit $ type_fun ty_lit ty_lit) $ Term_of_LamCtx $
 726          \_c -> lam $ \x -> lam $ \y -> x `op` y
 727 -}