Language/Symantic/Expr/Common.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE GADTs #-}
   6 {-# LANGUAGE KindSignatures #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 module Language.Symantic.Expr.Common where
  14
  15 import Data.Proxy (Proxy(..))
  16 import Data.Text (Text)
  17 import qualified Data.Text as Text
  18 import Data.Type.Equality ((:~:)(Refl))
  19 import GHC.Prim (Constraint)
  20
  21 import Language.Symantic.Type
  22
  23 -- * Class 'Expr_from'
  24
  25 -- | Parse given @ast@ into
  26 -- a 'Type_Root_of_Expr' and
  27 -- a 'Forall_Repr_with_Context',
  28 -- or return an 'Error_of_Expr'.
  29 class Expr_from ast (ex:: *) where
  30         expr_from :: Expr_From ast ex hs ret
  31
  32 -- ** Type 'Expr_From'
  33 type Expr_From ast ex hs ret
  34  = Proxy ex
  35  -- ^ Select the 'Expr_from' instance.
  36  -> ast
  37  -- ^ The input data to parse.
  38  -> Context (Lambda_Var (Type_Root_of_Expr ex)) hs
  39  -- ^ The bound variables in scope and their types:
  40  -- held in the heterogeneous list @hs@,
  41  -- from the closest including lambda abstraction to the farest.
  42  -> ( forall h
  43     .  Type_Root_of_Expr ex h
  44     -> Forall_Repr_with_Context ex hs h
  45     -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
  46  -- ^ The accumulating continuation.
  47  ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
  48
  49 -- | Parse a literal.
  50 lit_from
  51  :: forall ty lit ex ast hs ret.
  52  ( ty ~ Type_Root_of_Expr ex
  53  , Read lit
  54  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  55                    (Error_of_Expr ast (Root_of_Expr ex))
  56  ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
  57  -> ty lit -> Lambda_Var_Name
  58  -> Expr_From ast ex hs ret
  59 lit_from lit ty_lit toread ex ast _ctx k =
  60         case read_safe toread of
  61          Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
  62          Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
  63
  64 -- | Parse a unary operator.
  65 op1_from
  66  :: forall root ty lit ex ast hs ret.
  67  ( ty ~ Type_Root_of_Expr ex
  68  , root ~ Root_of_Expr ex
  69  , Type_Eq (Type_Root_of_Expr root)
  70  , Expr_from ast root
  71  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  72                    (Error_of_Expr ast root)
  73  , Root_of_Expr root ~ root
  74  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
  75  -> ty lit -> ast
  76  -> Expr_From ast ex hs ret
  77 op1_from op ty_lit ast_x ex ast ctx k =
  78         expr_from (Proxy::Proxy root) ast_x ctx $
  79          \ty_x (Forall_Repr_with_Context x) ->
  80         when_type_eq ex ast ty_lit ty_x $ \Refl ->
  81                 k ty_x $ Forall_Repr_with_Context (op . x)
  82
  83 -- | Parse a binary operator.
  84 op2_from
  85  :: forall root ty lit ex ast hs ret.
  86  ( ty ~ Type_Root_of_Expr ex
  87  , root ~ Root_of_Expr ex
  88  , Type_Eq (Type_Root_of_Expr root)
  89  , Expr_from ast root
  90  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  91                    (Error_of_Expr ast root)
  92  , Root_of_Expr root ~ root
  93  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
  94  -> ty lit -> ast -> ast
  95  -> Expr_From ast ex hs ret
  96 op2_from op ty_lit ast_x ast_y ex ast ctx k =
  97         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
  98         expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
  99         when_type_eq ex ast ty_lit ty_x $ \Refl ->
 100         when_type_eq ex ast ty_lit ty_y $ \Refl ->
 101                 k ty_x $ Forall_Repr_with_Context $
 102                  \c -> x c `op` y c
 103
 104 -- ** Type 'Context'
 105
 106 -- | GADT for a typing context,
 107 -- accumulating an @item@ at each lambda;
 108 -- used to accumulate object-types (in 'Expr_from')
 109 -- or host-terms (in 'Repr_Host')
 110 -- associated with the 'Lambda_Var's in scope.
 111 data Context :: (* -> *) -> [*] -> * where
 112         Context_Empty :: Context item '[]
 113         Context_Next  :: item h -> Context item hs -> Context item (h ': hs)
 114 infixr 5 `Context_Next`
 115
 116 -- ** Type 'Lambda_Var'
 117 -- | Join a name and a type.
 118 --
 119 -- This data type is used to handle lambda variables by name
 120 -- (instead of DeBruijn indices for instance).
 121 data Lambda_Var ty h
 122  =   Lambda_Var Lambda_Var_Name (ty h)
 123 type Lambda_Var_Name = Text
 124
 125 -- ** Type 'Forall_Repr_with_Context'
 126 -- | A data type embedding a universal quantification
 127 -- over an interpreter @repr@
 128 -- and qualified by the symantics of an expression.
 129 --
 130 -- Moreover the expression is abstracted by a 'Context'
 131 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
 132 -- for lambda abstractions.
 133 --
 134 -- This data type is used to keep a parsed expression polymorphic enough
 135 -- to stay interpretable by different interpreters.
 136 --
 137 -- NOTE: 'Sym_of_Expr'@ ex repr@
 138 -- is needed to be able to use symantic methods of the parsed expression
 139 -- into a 'Forall_Repr_with_Context'@ ex@.
 140 --
 141 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
 142 -- is needed to be able to use an expression
 143 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
 144 -- into a 'Forall_Repr_with_Context'@ ex@,
 145 -- which happens when a symantic method includes a polymorphic type
 146 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
 147 data Forall_Repr_with_Context ex hs h
 148  =   Forall_Repr_with_Context
 149  (   forall repr. ( Sym_of_Expr ex repr
 150                   , Sym_of_Expr (Root_of_Expr ex) repr
 151                   ) => Context repr hs -> repr h )
 152
 153 -- ** Type 'Forall_Repr'
 154 data Forall_Repr ex h
 155  =   Forall_Repr
 156  { unForall_Repr :: forall repr
 157                  .  Sym_of_Expr ex repr
 158                  => repr h }
 159
 160 -- ** Type family 'Root_of_Expr'
 161 -- | The root expression of an expression.
 162 type family Root_of_Expr (ex:: *) :: *
 163
 164 -- ** Type family 'Sym_of_Expr'
 165 -- | The symantic of an expression.
 166 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
 167
 168 -- ** Type family 'Error_of_Expr'
 169 -- | The error(s) of an expression.
 170 type family Error_of_Expr (ast:: *) (ex:: *) :: *
 171
 172 -- ** Type family 'Type_of_Expr'
 173 -- | The type of an expression, parameterized by a root type.
 174 type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
 175
 176 -- ** Type 'Type_Root_of_Expr'
 177 -- | Convenient alias.
 178 --
 179 -- NOTE: include 'Type_Var' only to use it
 180 -- within 'Error_Expr_Type_mismatch' so far.
 181 type Type_Root_of_Expr (ex:: *)
 182  =   Type_Root (Type_Alt Type_Var (Type_of_Expr (Root_of_Expr ex)))
 183
 184 -- * Type 'Expr_Root'
 185 -- | The root expression, passing itself as parameter to the given expression.
 186 newtype Expr_Root (ex:: * -> *)
 187  =      Expr_Root (ex (Expr_Root ex))
 188 type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
 189 type instance Type_of_Expr (Expr_Root ex)
 190  =            Type_of_Expr (ex (Expr_Root ex))
 191 type instance Error_of_Expr ast (Expr_Root ex)
 192  =            Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
 193                                          (Type_Root_of_Expr (ex (Expr_Root ex)))
 194                                          ast)
 195                              (Error_of_Expr ast (ex (Expr_Root ex)))
 196 type instance Sym_of_Expr (Expr_Root ex) repr
 197  =            Sym_of_Expr (ex (Expr_Root ex)) repr
 198 instance -- Expr_from
 199  ( Expr_from ast (ex (Expr_Root ex))
 200  , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
 201  ) => Expr_from ast (Expr_Root ex) where
 202         expr_from _ex ctx ast k =
 203                 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
 204                  ctx ast $ \ty (Forall_Repr_with_Context repr) ->
 205                         k ty (Forall_Repr_with_Context repr)
 206
 207 {- NOTE: useless code so far.
 208 -- ** Class 'Expr_Root_Lift'
 209 -- | Lift a given expression to a given root expression.
 210 class Expr_Root_Lift ex root where
 211         expr_root_lift :: ex root -> root
 212 instance
 213  Expr_Lift ex root =>
 214  Expr_Root_Lift ex (Expr_Root root) where
 215         expr_root_lift = Expr_Root . expr_lift
 216 -}
 217
 218 -- * Type 'Expr_Alt'
 219 -- | Expression making an alternative between two expressions.
 220 data Expr_Alt curr next (root:: *)
 221  =   Expr_Alt_Curr (curr root)
 222  |   Expr_Alt_Next (next root)
 223 type instance Root_of_Expr (Expr_Alt curr next root) = root
 224 type instance Sym_of_Expr (Expr_Alt curr next root) repr
 225  = ( Sym_of_Expr (curr root) repr
 226    , Sym_of_Expr (next root) repr
 227    )
 228 type instance Type_of_Expr (Expr_Alt curr next root)
 229  = Type_of_Expr_Alt
 230   (Type_of_Expr (curr root))
 231   (Type_of_Expr (next root))
 232   curr next root
 233 -- ** Type family 'Type_of_Expr_Alt'
 234 -- | Remove 'No_Type' type when building 'Type_of_Expr'.
 235 type family Type_of_Expr_Alt
 236  (type_curr:: (* -> *) -> * -> *)
 237  (type_next:: (* -> *) -> * -> *)
 238  curr next root where
 239         Type_of_Expr_Alt No_Type type_next curr next root = Type_of_Expr (next root)
 240         Type_of_Expr_Alt type_curr No_Type curr next root = Type_of_Expr (curr root)
 241         Type_of_Expr_Alt type_curr type_next curr next root
 242          = Type_Alt (Type_of_Expr (curr root))
 243                     (Type_of_Expr (next root))
 244
 245 type instance Error_of_Expr ast (Expr_Alt curr next root)
 246  = Error_of_Expr_Alt ast (curr root) (next root)
 247 -- ** Type family 'Error_of_Expr_Alt'
 248 -- | Remove 'No_Error_Expr' type when building the error of an expression.
 249 type family Error_of_Expr_Alt ast curr next where
 250         Error_of_Expr_Alt ast No_Error_Expr next = Error_of_Expr ast next
 251         Error_of_Expr_Alt ast curr No_Error_Expr = Error_of_Expr ast curr
 252         Error_of_Expr_Alt ast curr next
 253          = Error_Expr_Alt (Error_of_Expr ast curr)
 254                           (Error_of_Expr ast next)
 255 -- ** Type 'No_Error_Expr'
 256 -- | A discarded error.
 257 data No_Error_Expr
 258  =   No_Error_Expr
 259  deriving (Eq, Show)
 260
 261 instance -- Expr_from
 262  ( Expr_from ast (curr root)
 263  , Expr_from ast (next root)
 264  , Root_of_Expr (curr root) ~ root
 265  , Root_of_Expr (next root) ~ root
 266  , Error_Expr_Unlift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
 267                                  (Type_Root_of_Expr root) ast)
 268                      (Error_of_Expr ast root)
 269  ) => Expr_from ast (Expr_Alt curr next root) where
 270         expr_from _ex ctx ast k =
 271                 case expr_from (Proxy::Proxy (curr root)) ctx ast $
 272                  \ty (Forall_Repr_with_Context repr) ->
 273                         Right $ k ty (Forall_Repr_with_Context repr) of
 274                  Right ret -> ret
 275                  Left err ->
 276                         case error_expr_unlift err of
 277                          Just (Error_Expr_Unsupported_here _
 278                           :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
 279                                         (Type_Root_of_Expr root) ast) ->
 280                                 expr_from (Proxy::Proxy (next root)) ctx ast $
 281                                  \ty (Forall_Repr_with_Context repr) ->
 282                                         k ty (Forall_Repr_with_Context repr)
 283                          _ -> Left err
 284
 285 {- NOTE: useless code so far.
 286 -- ** Type 'Expr_Lift'
 287 -- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
 288 type Expr_Lift ex exs
 289  =   Expr_LiftN (Peano_of_Expr ex exs) ex exs
 290
 291 -- | Convenient wrapper around 'expr_liftN',
 292 -- passing it the 'Peano' number from 'Peano_of_Expr'.
 293 expr_lift
 294  :: forall ex exs (root:: *).
 295  Expr_Lift ex exs =>
 296  ex root -> exs root
 297 expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
 298
 299 -- *** Type family 'Peano_of_Expr'
 300 -- | Return a 'Peano' number derived from the location
 301 -- of a given expression within a given expression stack,
 302 -- which is used to avoid @OverlappingInstances@.
 303 type family Peano_of_Expr
 304  (ex::  * -> *)
 305  (exs:: * -> *) :: * where
 306         Peano_of_Expr ex    ex                   = Zero
 307         Peano_of_Expr ex    (Expr_Alt ex   next) = Zero
 308         Peano_of_Expr other (Expr_Alt curr next) = Succ (Peano_of_Expr other next)
 309
 310 -- *** Class 'Expr_LiftN'
 311 -- | Lift a given expression to the top of a given expression stack including it,
 312 -- by constructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
 313 class Expr_LiftN (p:: *) ex exs where
 314         expr_liftN :: forall (root:: *). Proxy p -> ex root -> exs root
 315 instance Expr_LiftN Zero curr curr where
 316         expr_liftN _ = id
 317 instance Expr_LiftN Zero curr (Expr_Alt curr next) where
 318         expr_liftN _ = Expr_Alt_Curr
 319 instance
 320  Expr_LiftN p other next =>
 321  Expr_LiftN (Succ p) other (Expr_Alt curr next) where
 322         expr_liftN _ = Expr_Alt_Next . expr_liftN (Proxy::Proxy p)
 323
 324 -- ** Type 'Expr_Unlift'
 325 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
 326 type Expr_Unlift ex exs
 327  =   Expr_UnliftN (Peano_of_Expr ex exs) ex exs
 328
 329 -- | Convenient wrapper around 'expr_unliftN',
 330 -- passing it the 'Peano' number from 'Peano_of_Expr'.
 331 expr_unlift
 332  :: forall ex exs (root:: *).
 333  Expr_Unlift ex exs =>
 334  exs root -> Maybe (ex root)
 335 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
 336
 337 -- *** Class 'Expr_UnliftN'
 338 -- | Try to unlift a given expression out of a given expression stack including it,
 339 -- by deconstructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
 340 class Expr_UnliftN (p:: *) ex exs where
 341         expr_unliftN :: forall (root:: *). Proxy p -> exs root -> Maybe (ex root)
 342 instance Expr_UnliftN Zero curr curr where
 343         expr_unliftN _ = Just
 344 instance Expr_UnliftN Zero curr (Expr_Alt curr next) where
 345         expr_unliftN _ (Expr_Alt_Curr x) = Just x
 346         expr_unliftN _ (Expr_Alt_Next _) = Nothing
 347 instance
 348  Expr_UnliftN p other next =>
 349  Expr_UnliftN (Succ p) other (Expr_Alt curr next) where
 350         expr_unliftN _ (Expr_Alt_Next x) = expr_unliftN (Proxy::Proxy p) x
 351         expr_unliftN _ (Expr_Alt_Curr _) = Nothing
 352 -}
 353
 354 -- ** Type family 'Is_Last_Expr'
 355 -- | Return whether a given expression is the last one in a given expression stack.
 356 --
 357 -- NOTE: each expression parser uses this type family
 358 -- when it encounters unsupported syntax:
 359 -- to know if it is the last expression parser component that will be tried
 360 -- (and thus return 'Error_Expr_Unsupported')
 361 -- or if some other expression parser component shall be tried
 362 -- (and thus return 'Error_Expr_Unsupported_here',
 363 -- which is then handled accordingly by the 'Expr_from' instance of 'Expr_Alt').
 364 type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
 365         Is_Last_Expr ex        ex                        = 'True
 366         Is_Last_Expr ex        (Expr_Root exs)           = Is_Last_Expr ex (exs (Expr_Root exs))
 367         Is_Last_Expr (ex root) (Expr_Alt ex   next root) = 'False
 368         Is_Last_Expr other     (Expr_Alt curr next root) = Is_Last_Expr other (next root)
 369
 370 -- * Type 'Error_Expr_Alt'
 371 -- | Error expression making an alternative between two error expressions.
 372 data Error_Expr_Alt curr next
 373  =   Error_Expr_Alt_Curr curr
 374  |   Error_Expr_Alt_Next next
 375  deriving (Eq, Show)
 376
 377 -- ** Type 'Error_Expr_Lift'
 378 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftN'.
 379 type Error_Expr_Lift err errs
 380  =   Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
 381
 382 -- | Convenient wrapper around 'error_expr_liftN',
 383 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
 384 error_expr_lift
 385  :: forall err errs.
 386  Error_Expr_Lift err errs => err -> errs
 387 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
 388
 389 -- *** Type family 'Peano_of_Error_Expr'
 390 -- | Return a 'Peano' number derived from the location
 391 -- of a given error expression within a given error expression stack,
 392 -- which is used to avoid @OverlappingInstances@.
 393 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: * where
 394         Peano_of_Error_Expr err   err                        = Zero
 395         Peano_of_Error_Expr err   (Error_Expr_Alt err  next) = Zero
 396         Peano_of_Error_Expr other (Error_Expr_Alt curr next) = Succ (Peano_of_Error_Expr other next)
 397
 398 -- *** Class 'Error_Expr_LiftN'
 399 -- | Lift a given expression to the top of a given expression stack including it,
 400 -- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
 401 class Error_Expr_LiftN (p:: *) err errs where
 402         error_expr_liftN :: Proxy p -> err -> errs
 403 instance Error_Expr_LiftN Zero curr curr where
 404         error_expr_liftN _ = id
 405 instance Error_Expr_LiftN Zero curr (Error_Expr_Alt curr next) where
 406         error_expr_liftN _ = Error_Expr_Alt_Curr
 407 instance
 408  Error_Expr_LiftN p other next =>
 409  Error_Expr_LiftN (Succ p) other (Error_Expr_Alt curr next) where
 410         error_expr_liftN _ = Error_Expr_Alt_Next . error_expr_liftN (Proxy::Proxy p)
 411
 412 -- ** Type 'Error_Expr_Unlift'
 413 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftN'.
 414 type Error_Expr_Unlift ex exs
 415  =   Error_Expr_UnliftN (Peano_of_Error_Expr ex exs) ex exs
 416
 417 -- | Convenient wrapper around 'error_expr_unliftN',
 418 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
 419 error_expr_unlift
 420  :: forall ex exs.
 421  Error_Expr_Unlift ex exs => exs -> Maybe ex
 422 error_expr_unlift = error_expr_unliftN (Proxy::Proxy (Peano_of_Error_Expr ex exs))
 423
 424 -- *** Class 'Error_Expr_UnliftN'
 425 -- | Try to unlift a given expression error out of a given expression error stack including it,
 426 -- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
 427 class Error_Expr_UnliftN (p:: *) ex exs where
 428         error_expr_unliftN :: Proxy p -> exs -> Maybe ex
 429 instance Error_Expr_UnliftN Zero curr curr where
 430         error_expr_unliftN _ = Just
 431 instance Error_Expr_UnliftN Zero curr (Error_Expr_Alt curr next) where
 432         error_expr_unliftN _ (Error_Expr_Alt_Curr x) = Just x
 433         error_expr_unliftN _ (Error_Expr_Alt_Next _) = Nothing
 434 instance
 435  Error_Expr_UnliftN p other next =>
 436  Error_Expr_UnliftN (Succ p) other (Error_Expr_Alt curr next) where
 437         error_expr_unliftN _ (Error_Expr_Alt_Next x) = error_expr_unliftN (Proxy::Proxy p) x
 438         error_expr_unliftN _ (Error_Expr_Alt_Curr _) = Nothing
 439
 440 -- * Type 'Error_Expr_Read'
 441 -- | Common expression errors.
 442 data Error_Expr err_ty ty ast
 443  =   Error_Expr_Wrong_number_of_arguments ast Int
 444  -- ^ Wrong number of arguments applied to a term,
 445  -- the integer is the number of arguments expected.
 446  |   Error_Expr_Type_mismatch ast (Exists_Type ty) (Exists_Type ty)
 447  -- ^ Mismatch between respectively expected and actual type.
 448  |   Error_Expr_Constraint_missing ast {-Exists_Dict-} (Exists_Type ty)
 449  -- ^ A 'Constraint' is missing.
 450  |   Error_Expr_Read Error_Read ast
 451  -- ^ Error when reading a literal.
 452  |   Error_Expr_Type err_ty ast
 453  -- ^ Error when parsing a type.
 454  |   Error_Expr_Unsupported ast
 455  -- ^ Given syntax is supported by none
 456  -- of the expression parser components
 457  -- of the expression stack.
 458  |   Error_Expr_Unsupported_here ast
 459  -- ^ Given syntax not supported by
 460  -- the current expression parser component.
 461  deriving (Eq, Show)
 462
 463 -- | Convenient wrapper around 'error_expr_lift',
 464 -- passing the type family boilerplate.
 465 error_expr
 466  :: forall ast ex ty.
 467  (ty ~ Type_Root_of_Expr ex)
 468  => Error_Expr_Lift
 469    (Error_Expr (Error_of_Type ast ty) ty ast)
 470    (Error_of_Expr ast (Root_of_Expr ex))
 471  => Proxy ex
 472  -> Error_Expr (Error_of_Type ast ty) ty ast
 473  -> Error_of_Expr ast (Root_of_Expr ex)
 474 error_expr _ = error_expr_lift
 475
 476 -- | Utility to return 'Error_Expr_Unsupported'
 477 -- or 'Error_Expr_Unsupported_here'
 478 -- according to the given expression.
 479 error_expr_unsupported
 480  :: forall ast ex ty root.
 481  ( root ~ Root_of_Expr ex
 482  , ty ~ Type_Root_of_Expr ex
 483  , Implicit_HBool (Is_Last_Expr ex root)
 484  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 485                    (Error_of_Expr ast root)
 486  ) => Proxy ex -> ast
 487  -> Error_of_Expr ast (Root_of_Expr ex)
 488 error_expr_unsupported ex ast =
 489         case hbool :: HBool (Is_Last_Expr ex root) of
 490          HTrue  -> error_expr ex $ Error_Expr_Unsupported ast
 491          HFalse -> error_expr ex $ Error_Expr_Unsupported_here ast
 492
 493 -- | Utility to check that two types are equal
 494 -- or raise 'Error_Expr_Type_mismatch'.
 495 when_type_eq
 496  :: forall ast ex root ty x y ret.
 497  ( root ~ Root_of_Expr ex
 498  , ty ~ Type_Root_of_Expr ex
 499  , Type_Eq ty
 500  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 501                    (Error_of_Expr ast root)
 502  )
 503  => Proxy ex -> ast -> ty x -> ty y
 504  -> (x :~: y -> Either (Error_of_Expr ast root) ret)
 505  -> Either (Error_of_Expr ast root) ret
 506 when_type_eq ex ast x y k =
 507         case x `type_eq` y of
 508          Just Refl -> k Refl
 509          Nothing -> Left $ error_expr ex $
 510                 Error_Expr_Type_mismatch ast
 511                  (Exists_Type x)
 512                  (Exists_Type y)
 513
 514 when_type_constraint
 515  :: forall ast ex c root ty h ret.
 516  ( root ~ Root_of_Expr ex
 517  , ty ~ Type_Root_of_Expr ex
 518  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 519                    (Error_of_Expr ast root)
 520  , Type_Constraint c ty
 521  )
 522  => Proxy ex -> Proxy c -> ast -> ty h
 523  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 524  -> Either (Error_of_Expr ast root) ret
 525 when_type_constraint ex c ast ty k =
 526         case type_constraint c ty of
 527          Just Dict -> k Dict
 528          Nothing -> Left $ error_expr ex $
 529                 Error_Expr_Constraint_missing ast
 530                  {-(Exists_Dict c)-}
 531                  (Exists_Type ty)
 532
 533 -- * Type 'Error_Read'
 534 -- | Error parsing a host-term.
 535 data Error_Read
 536  =   Error_Read Text
 537  deriving (Eq, Show)
 538
 539 -- | Parse a host-term.
 540 read_safe :: Read h => Text -> Either Error_Read h
 541 read_safe t =
 542         case reads $ Text.unpack t of
 543          [(x, "")] -> Right x
 544          _         -> Left $ Error_Read t