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 -- | Like 'expr_from' but for a root expression.
  33 root_expr_from
  34  :: forall lam ast root.
  35  ( Expr_from ast root
  36  , Root_of_Expr root ~ root )
  37  => Proxy root -> Proxy lam -> ast
  38  -> Either (Error_of_Expr ast root)
  39            (Exists_Type_and_Repr (Type_Root_of_Expr root)
  40                                  (Forall_Repr root))
  41 root_expr_from _ex _lam ast =
  42         expr_from (Proxy::Proxy root) ast
  43          Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
  44                 Right $ Exists_Type_and_Repr ty $
  45                         Forall_Repr $ repr Context_Empty
  46
  47 -- ** Type 'Expr_From'
  48 type Expr_From ast ex hs ret
  49  = Proxy ex
  50  -- ^ Select the 'Expr_from' instance.
  51  -> ast
  52  -- ^ The input data to parse.
  53  -> Context (Lambda_Var (Type_Root_of_Expr ex)) hs
  54  -- ^ The bound variables in scope and their types:
  55  -- held in the heterogeneous list @hs@,
  56  -- from the closest including lambda abstraction to the farest.
  57  -> ( forall h
  58     .  Type_Root_of_Expr ex h
  59     -> Forall_Repr_with_Context ex hs h
  60     -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
  61  -- ^ The accumulating continuation.
  62  ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
  63
  64 -- | Parse a literal.
  65 lit_from
  66  :: forall ty lit ex ast hs ret.
  67  ( ty ~ Type_Root_of_Expr ex
  68  , Read lit
  69  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  70                    (Error_of_Expr ast (Root_of_Expr ex))
  71  ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
  72  -> ty lit -> Lambda_Var_Name
  73  -> Expr_From ast ex hs ret
  74 lit_from lit ty_lit toread ex ast _ctx k =
  75         case read_safe toread of
  76          Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
  77          Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
  78
  79 -- | Parse a unary operator.
  80 op1_from
  81  :: forall root ty lit ex ast hs ret.
  82  ( ty ~ Type_Root_of_Expr ex
  83  , root ~ Root_of_Expr ex
  84  , Eq_Type (Type_Root_of_Expr root)
  85  , Expr_from ast root
  86  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  87                    (Error_of_Expr ast root)
  88  , Root_of_Expr root ~ root
  89  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
  90  -> ty lit -> ast
  91  -> Expr_From ast ex hs ret
  92 op1_from op ty_lit ast_x ex ast ctx k =
  93         expr_from (Proxy::Proxy root) ast_x ctx $
  94          \ty_x (Forall_Repr_with_Context x) ->
  95         check_eq_type ex ast ty_lit ty_x $ \Refl ->
  96                 k ty_x $ Forall_Repr_with_Context (op . x)
  97
  98 -- | Parse a binary operator.
  99 op2_from
 100  :: forall root ty lit ex ast hs ret.
 101  ( ty ~ Type_Root_of_Expr ex
 102  , root ~ Root_of_Expr ex
 103  , Eq_Type (Type_Root_of_Expr root)
 104  , Expr_from ast root
 105  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 106                    (Error_of_Expr ast root)
 107  , Root_of_Expr root ~ root
 108  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 109  -> ty lit -> ast -> ast
 110  -> Expr_From ast ex hs ret
 111 op2_from op ty_lit ast_x ast_y ex ast ctx k =
 112         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 113         expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
 114         check_eq_type ex ast ty_lit ty_x $ \Refl ->
 115         check_eq_type ex ast ty_lit ty_y $ \Refl ->
 116                 k ty_x $ Forall_Repr_with_Context $
 117                  \c -> x c `op` y c
 118
 119 -- ** Type 'Context'
 120
 121 -- | GADT for a typing context,
 122 -- accumulating an @item@ at each lambda;
 123 -- used to accumulate object-types (in 'Expr_from')
 124 -- or host-terms (in 'Repr_Host')
 125 -- associated with the 'Lambda_Var's in scope.
 126 data Context :: (* -> *) -> [*] -> * where
 127         Context_Empty :: Context item '[]
 128         Context_Next  :: item h -> Context item hs -> Context item (h ': hs)
 129 infixr 5 `Context_Next`
 130
 131 -- ** Type 'Lambda_Var'
 132 -- | Join a name and a type.
 133 --
 134 -- This data type is used to handle lambda variables by name
 135 -- (instead of DeBruijn indices for instance).
 136 data Lambda_Var ty h
 137  =   Lambda_Var Lambda_Var_Name (ty h)
 138 type Lambda_Var_Name = Text
 139
 140 -- ** Type 'Forall_Repr_with_Context'
 141 -- | A data type embedding a universal quantification
 142 -- over an interpreter @repr@
 143 -- and qualified by the symantics of an expression.
 144 --
 145 -- Moreover the expression is abstracted by a 'Context'
 146 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
 147 -- for lambda abstractions.
 148 --
 149 -- This data type is used to keep a parsed expression polymorphic enough
 150 -- to stay interpretable by different interpreters.
 151 --
 152 -- NOTE: 'Sym_of_Expr'@ ex repr@
 153 -- is needed to be able to use symantic methods of the parsed expression
 154 -- into a 'Forall_Repr_with_Context'@ ex@.
 155 --
 156 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
 157 -- is needed to be able to use an expression
 158 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
 159 -- into a 'Forall_Repr_with_Context'@ ex@,
 160 -- which happens when a symantic method includes a polymorphic type
 161 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
 162 data Forall_Repr_with_Context ex hs h
 163  =   Forall_Repr_with_Context
 164  (   forall repr. ( Sym_of_Expr ex repr
 165                   , Sym_of_Expr (Root_of_Expr ex) repr
 166                   ) => Context repr hs -> repr h )
 167
 168 -- ** Type 'Forall_Repr'
 169 data Forall_Repr ex h
 170  =   Forall_Repr
 171  { unForall_Repr :: forall repr
 172                  .  ( Sym_of_Expr ex repr
 173                     , Sym_of_Expr (Root_of_Expr ex) repr )
 174                  => repr h }
 175
 176 -- ** Type family 'Root_of_Expr'
 177 -- | The root expression of an expression.
 178 type family Root_of_Expr (ex:: *) :: *
 179
 180 -- ** Type family 'Sym_of_Expr'
 181 -- | The symantic of an expression.
 182 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
 183
 184 -- ** Type family 'Error_of_Expr'
 185 -- | The error(s) of an expression.
 186 type family Error_of_Expr (ast:: *) (ex:: *) :: *
 187
 188 -- ** Type family 'Type_of_Expr'
 189 -- | The type of an expression, parameterized by a root type.
 190 type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
 191
 192 -- ** Type 'Type_Root_of_Expr'
 193 -- | Convenient alias.
 194 --
 195 -- NOTE: include 'Type_Var' only to use it
 196 -- within 'Error_Expr_Type_mismatch' so far.
 197 type Type_Root_of_Expr (ex:: *)
 198  =   Type_Root (Type_Var :|: Type_of_Expr (Root_of_Expr ex))
 199
 200 -- * Type 'Expr_Root'
 201 -- | The root expression, passing itself as parameter to the given expression.
 202 newtype Expr_Root (ex:: * -> *)
 203  =      Expr_Root (ex (Expr_Root ex))
 204 type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
 205 type instance Type_of_Expr (Expr_Root ex)
 206  =            Type_of_Expr (ex (Expr_Root ex))
 207 type instance Error_of_Expr ast (Expr_Root ex)
 208  =            Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
 209                                          (Type_Root_of_Expr (ex (Expr_Root ex)))
 210                                          ast)
 211                              (Error_of_Expr ast (ex (Expr_Root ex)))
 212 type instance Sym_of_Expr (Expr_Root ex) repr
 213  =            Sym_of_Expr (ex (Expr_Root ex)) repr
 214 instance -- Expr_from
 215  ( Expr_from ast (ex (Expr_Root ex))
 216  , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
 217  ) => Expr_from ast (Expr_Root ex) where
 218         expr_from _ex ctx ast k =
 219                 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
 220                  ctx ast $ \ty (Forall_Repr_with_Context repr) ->
 221                         k ty (Forall_Repr_with_Context repr)
 222
 223 {- NOTE: useless code so far.
 224 -- ** Class 'Expr_Root_Lift'
 225 -- | Lift a given expression to a given root expression.
 226 class Expr_Root_Lift ex root where
 227         expr_root_lift :: ex root -> root
 228 instance
 229  Lift_Expr ex root =>
 230  Expr_Root_Lift ex (Expr_Root root) where
 231         expr_root_lift = Expr_Root . lift_expr
 232 -}
 233
 234 -- * Type 'Expr_Alt'
 235 -- | Expression making an alternative between two expressions.
 236 data Expr_Alt curr next (root:: *)
 237  =   Expr_Alt_Curr (curr root)
 238  |   Expr_Alt_Next (next root)
 239 -- | Convenient alias. Requires @TypeOperators@.
 240 --
 241 -- TODO: see if using a type-level list is better.
 242 type (.|.) = Expr_Alt
 243 infixr 5 .|.
 244 type instance Root_of_Expr (Expr_Alt curr next root) = root
 245 type instance Sym_of_Expr (Expr_Alt curr next root) repr
 246  = ( Sym_of_Expr (curr root) repr
 247    , Sym_of_Expr (next root) repr
 248    )
 249 type instance Type_of_Expr (Expr_Alt curr next root)
 250  = Type_of_Expr_Alt (Type_of_Expr (curr root))
 251                     (Type_of_Expr (next root))
 252 -- ** Type family 'Type_of_Expr_Alt'
 253 -- | Remove 'No_Type' type when building 'Type_of_Expr'.
 254 type family Type_of_Expr_Alt
 255  (type_curr:: (* -> *) -> * -> *)
 256  (type_next:: (* -> *) -> * -> *)
 257  where
 258         Type_of_Expr_Alt No_Type next    = next
 259         Type_of_Expr_Alt curr    No_Type = curr
 260         Type_of_Expr_Alt curr    next    = Type_Alt curr next
 261
 262 type instance Error_of_Expr ast (Expr_Alt curr next root)
 263  = Error_of_Expr_Alt ast (Error_of_Expr ast (curr root))
 264                          (Error_of_Expr ast (next root))
 265 -- ** Type family 'Error_of_Expr_Alt'
 266 -- | Remove 'No_Error_Expr' type when building the error of an expression.
 267 type family Error_of_Expr_Alt ast curr next where
 268         Error_of_Expr_Alt ast No_Error_Expr next          = next
 269         Error_of_Expr_Alt ast curr          No_Error_Expr = curr
 270         Error_of_Expr_Alt ast curr          next          = Error_Expr_Alt curr next
 271
 272 -- ** Type 'No_Error_Expr'
 273 -- | A discarded error.
 274 data No_Error_Expr
 275  =   No_Error_Expr
 276  deriving (Eq, Show)
 277
 278 instance -- Expr_from
 279  ( Expr_from ast (curr root)
 280  , Expr_from ast (next root)
 281  , Root_of_Expr (curr root) ~ root
 282  , Root_of_Expr (next root) ~ root
 283  , Unlift_Error_Expr (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
 284                                  (Type_Root_of_Expr root) ast)
 285                      (Error_of_Expr ast root)
 286  ) => Expr_from ast (Expr_Alt curr next root) where
 287         expr_from _ex ctx ast k =
 288                 case expr_from (Proxy::Proxy (curr root)) ctx ast $
 289                  \ty (Forall_Repr_with_Context repr) ->
 290                         Right $ k ty (Forall_Repr_with_Context repr) of
 291                  Right ret -> ret
 292                  Left err ->
 293                         case unlift_error_expr err of
 294                          Just (Error_Expr_Unsupported_here _
 295                           :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
 296                                         (Type_Root_of_Expr root) ast) ->
 297                                 expr_from (Proxy::Proxy (next root)) ctx ast $
 298                                  \ty (Forall_Repr_with_Context repr) ->
 299                                         k ty (Forall_Repr_with_Context repr)
 300                          _ -> Left err
 301
 302 {- NOTE: useless code so far.
 303 -- ** Type 'Lift_Expr'
 304 -- | Apply 'Peano_of_Expr' on 'Lift_ExprP'.
 305 type Lift_Expr ex exs
 306  =   Lift_ExprP (Peano_of_Expr ex exs) ex exs
 307
 308 -- | Convenient wrapper around 'expr_liftN',
 309 -- passing it the 'Peano' number from 'Peano_of_Expr'.
 310 lift_expr
 311  :: forall ex exs (root:: *).
 312  Lift_Expr ex exs =>
 313  ex root -> exs root
 314 lift_expr = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
 315
 316 -- *** Type family 'Peano_of_Expr'
 317 -- | Return a 'Peano' number derived from the location
 318 -- of a given expression within a given expression stack,
 319 -- which is used to avoid @OverlappingInstances@.
 320 type family Peano_of_Expr
 321  (ex::  * -> *)
 322  (exs:: * -> *) :: * where
 323         Peano_of_Expr ex    ex                   = Zero
 324         Peano_of_Expr ex    (Expr_Alt ex   next) = Zero
 325         Peano_of_Expr other (Expr_Alt curr next) = Succ (Peano_of_Expr other next)
 326
 327 -- *** Class 'Lift_ExprP'
 328 -- | Lift a given expression to the top of a given expression stack including it,
 329 -- by constructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
 330 class Lift_ExprP (p:: *) ex exs where
 331         expr_liftN :: forall (root:: *). Proxy p -> ex root -> exs root
 332 instance Lift_ExprP Zero curr curr where
 333         expr_liftN _ = id
 334 instance Lift_ExprP Zero curr (Expr_Alt curr next) where
 335         expr_liftN _ = Expr_Alt_Curr
 336 instance
 337  Lift_ExprP p other next =>
 338  Lift_ExprP (Succ p) other (Expr_Alt curr next) where
 339         expr_liftN _ = Expr_Alt_Next . expr_liftN (Proxy::Proxy p)
 340
 341 -- ** Type 'Unlift_Expr'
 342 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
 343 type Unlift_Expr ex exs
 344  =   Expr_UnliftN (Peano_of_Expr ex exs) ex exs
 345
 346 -- | Convenient wrapper around 'expr_unliftN',
 347 -- passing it the 'Peano' number from 'Peano_of_Expr'.
 348 expr_unlift
 349  :: forall ex exs (root:: *).
 350  Unlift_Expr ex exs =>
 351  exs root -> Maybe (ex root)
 352 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
 353
 354 -- *** Class 'Expr_UnliftN'
 355 -- | Try to unlift a given expression out of a given expression stack including it,
 356 -- by deconstructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
 357 class Expr_UnliftN (p:: *) ex exs where
 358         expr_unliftN :: forall (root:: *). Proxy p -> exs root -> Maybe (ex root)
 359 instance Expr_UnliftN Zero curr curr where
 360         expr_unliftN _ = Just
 361 instance Expr_UnliftN Zero curr (Expr_Alt curr next) where
 362         expr_unliftN _ (Expr_Alt_Curr x) = Just x
 363         expr_unliftN _ (Expr_Alt_Next _) = Nothing
 364 instance
 365  Expr_UnliftN p other next =>
 366  Expr_UnliftN (Succ p) other (Expr_Alt curr next) where
 367         expr_unliftN _ (Expr_Alt_Next x) = expr_unliftN (Proxy::Proxy p) x
 368         expr_unliftN _ (Expr_Alt_Curr _) = Nothing
 369 -}
 370
 371 -- ** Type family 'Is_Last_Expr'
 372 -- | Return whether a given expression is the last one in a given expression stack.
 373 --
 374 -- NOTE: each expression parser uses this type family
 375 -- when it encounters unsupported syntax:
 376 -- to know if it is the last expression parser component that will be tried
 377 -- (and thus return 'Error_Expr_Unsupported')
 378 -- or if some other expression parser component shall be tried
 379 -- (and thus return 'Error_Expr_Unsupported_here',
 380 -- which is then handled accordingly by the 'Expr_from' instance of 'Expr_Alt').
 381 type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
 382         Is_Last_Expr ex        ex                        = 'True
 383         Is_Last_Expr ex        (Expr_Root exs)           = Is_Last_Expr ex (exs (Expr_Root exs))
 384         Is_Last_Expr (ex root) (Expr_Alt ex   next root) = 'False
 385         Is_Last_Expr other     (Expr_Alt curr next root) = Is_Last_Expr other (next root)
 386
 387 -- * Type 'Error_Expr_Alt'
 388 -- | Error expression making an alternative between two error expressions.
 389 data Error_Expr_Alt curr next
 390  =   Error_Expr_Alt_Curr curr
 391  |   Error_Expr_Alt_Next next
 392  deriving (Eq, Show)
 393
 394 -- ** Type 'Lift_Error_Expr'
 395 -- | Apply 'Peano_of_Error_Expr' on 'Lift_Error_ExprP'.
 396 type Lift_Error_Expr err errs
 397  =   Lift_Error_ExprP (Peano_of_Error_Expr err errs) err errs
 398
 399 -- | Convenient wrapper around 'lift_error_exprP',
 400 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
 401 lift_error_expr
 402  :: forall err errs.
 403  Lift_Error_Expr err errs => err -> errs
 404 lift_error_expr = lift_error_exprP (Proxy::Proxy (Peano_of_Error_Expr err errs))
 405
 406 -- *** Type family 'Peano_of_Error_Expr'
 407 -- | Return a 'Peano' number derived from the location
 408 -- of a given error expression within a given error expression stack,
 409 -- which is used to avoid @OverlappingInstances@.
 410 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: * where
 411         Peano_of_Error_Expr err   err                        = Zero
 412         Peano_of_Error_Expr err   (Error_Expr_Alt err  next) = Zero
 413         Peano_of_Error_Expr other (Error_Expr_Alt curr next) = Succ (Peano_of_Error_Expr other next)
 414
 415 -- *** Class 'Lift_Error_ExprP'
 416 -- | Lift a given expression to the top of a given expression stack including it,
 417 -- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
 418 class Lift_Error_ExprP (p:: *) err errs where
 419         lift_error_exprP :: Proxy p -> err -> errs
 420 instance Lift_Error_ExprP Zero curr curr where
 421         lift_error_exprP _ = id
 422 instance Lift_Error_ExprP Zero curr (Error_Expr_Alt curr next) where
 423         lift_error_exprP _ = Error_Expr_Alt_Curr
 424 instance
 425  Lift_Error_ExprP p other next =>
 426  Lift_Error_ExprP (Succ p) other (Error_Expr_Alt curr next) where
 427         lift_error_exprP _ = Error_Expr_Alt_Next . lift_error_exprP (Proxy::Proxy p)
 428
 429 -- ** Type 'Unlift_Error_Expr'
 430 -- | Apply 'Peano_of_Error_Expr' on 'Unlift_Error_ExprP'.
 431 type Unlift_Error_Expr ex exs
 432  =   Unlift_Error_ExprP (Peano_of_Error_Expr ex exs) ex exs
 433
 434 -- | Convenient wrapper around 'unlift_error_exprP',
 435 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
 436 unlift_error_expr
 437  :: forall ex exs.
 438  Unlift_Error_Expr ex exs => exs -> Maybe ex
 439 unlift_error_expr = unlift_error_exprP (Proxy::Proxy (Peano_of_Error_Expr ex exs))
 440
 441 -- *** Class 'Unlift_Error_ExprP'
 442 -- | Try to unlift a given expression error out of a given expression error stack including it,
 443 -- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
 444 class Unlift_Error_ExprP (p:: *) ex exs where
 445         unlift_error_exprP :: Proxy p -> exs -> Maybe ex
 446 instance Unlift_Error_ExprP Zero curr curr where
 447         unlift_error_exprP _ = Just
 448 instance Unlift_Error_ExprP Zero curr (Error_Expr_Alt curr next) where
 449         unlift_error_exprP _ (Error_Expr_Alt_Curr x) = Just x
 450         unlift_error_exprP _ (Error_Expr_Alt_Next _) = Nothing
 451 instance
 452  Unlift_Error_ExprP p other next =>
 453  Unlift_Error_ExprP (Succ p) other (Error_Expr_Alt curr next) where
 454         unlift_error_exprP _ (Error_Expr_Alt_Next x) = unlift_error_exprP (Proxy::Proxy p) x
 455         unlift_error_exprP _ (Error_Expr_Alt_Curr _) = Nothing
 456
 457 -- * Type 'Error_Expr_Read'
 458 -- | Common expression errors.
 459 data Error_Expr err_ty ty ast
 460  =   Error_Expr_Wrong_number_of_arguments ast Int
 461  -- ^ Wrong number of arguments applied to a term,
 462  -- the integer is the number of arguments expected.
 463  |   Error_Expr_Type_mismatch ast (Exists_Type ty) (Exists_Type ty)
 464  -- ^ Mismatch between respectively expected and actual type.
 465  |   Error_Expr_Constraint_missing ast {-Exists_Dict-} (Exists_Type ty)
 466  -- ^ A 'Constraint' is missing.
 467  |   Error_Expr_Read Error_Read ast
 468  -- ^ Error when reading a literal.
 469  |   Error_Expr_Type err_ty ast
 470  -- ^ Error when parsing a type.
 471  |   Error_Expr_Unsupported ast
 472  -- ^ Given syntax is supported by none
 473  -- of the expression parser components
 474  -- of the expression stack.
 475  |   Error_Expr_Unsupported_here ast
 476  -- ^ Given syntax not supported by
 477  -- the current expression parser component.
 478  deriving (Eq, Show)
 479
 480 -- | Convenient type alias.
 481 type Error_Expr_of_Root ast root
 482  =   Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
 483                 (Type_Root_of_Expr root)
 484                 ast
 485
 486 -- | Convenient wrapper around 'lift_error_expr',
 487 -- passing the type family boilerplate.
 488 error_expr
 489  :: forall ast ex ty.
 490  (ty ~ Type_Root_of_Expr ex)
 491  => Lift_Error_Expr
 492    (Error_Expr (Error_of_Type ast ty) ty ast)
 493    (Error_of_Expr ast (Root_of_Expr ex))
 494  => Proxy ex
 495  -> Error_Expr (Error_of_Type ast ty) ty ast
 496  -> Error_of_Expr ast (Root_of_Expr ex)
 497 error_expr _ = lift_error_expr
 498
 499 -- | Parsing utility to return 'Error_Expr_Unsupported'
 500 -- or 'Error_Expr_Unsupported_here'
 501 -- according to the given expression.
 502 error_expr_unsupported
 503  :: forall ast ex ty root.
 504  ( root ~ Root_of_Expr ex
 505  , ty ~ Type_Root_of_Expr ex
 506  , Implicit_HBool (Is_Last_Expr ex root)
 507  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 508                    (Error_of_Expr ast root)
 509  ) => Proxy ex -> ast
 510  -> Error_of_Expr ast (Root_of_Expr ex)
 511 error_expr_unsupported ex ast =
 512         case hbool :: HBool (Is_Last_Expr ex root) of
 513          HTrue  -> error_expr ex $ Error_Expr_Unsupported ast
 514          HFalse -> error_expr ex $ Error_Expr_Unsupported_here ast
 515
 516 -- | Parsing utility to check that two types are equal,
 517 -- or raise 'Error_Expr_Type_mismatch'.
 518 check_eq_type
 519  :: forall ast ex root ty x y ret.
 520  ( root ~ Root_of_Expr ex
 521  , ty ~ Type_Root_of_Expr ex
 522  , Eq_Type ty
 523  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 524                    (Error_of_Expr ast root)
 525  )
 526  => Proxy ex -> ast -> ty x -> ty y
 527  -> (x :~: y -> Either (Error_of_Expr ast root) ret)
 528  -> Either (Error_of_Expr ast root) ret
 529 check_eq_type ex ast x y k =
 530         case x `eq_type` y of
 531          Just Refl -> k Refl
 532          Nothing -> Left $ error_expr ex $
 533                 Error_Expr_Type_mismatch ast
 534                  (Exists_Type x)
 535                  (Exists_Type y)
 536 check_eq_type1
 537  :: forall ast ex root ty h1 h2 a1 a2 ret.
 538  ( root ~ Root_of_Expr ex
 539  , ty ~ Type_Root_of_Expr ex
 540  , Eq_Type1 ty
 541  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 542                    (Error_of_Expr ast root)
 543  )
 544  => Proxy ex -> ast -> ty (h1 a1) -> ty (h2 a2)
 545  -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
 546  -> Either (Error_of_Expr ast root) ret
 547 check_eq_type1 ex ast h1 h2 k =
 548         case h1 `eq_type1` h2 of
 549          Just Refl -> k Refl
 550          Nothing -> Left $ error_expr ex $
 551                 Error_Expr_Type_mismatch ast
 552                  (Exists_Type h1)
 553                  (Exists_Type h2)
 554
 555 -- | Parsing utility to check that a type is has instance of a given 'Constraint',
 556 -- or raise 'Error_Expr_Constraint_missing'.
 557 check_constraint_type
 558  :: forall ast ex c root ty h ret.
 559  ( root ~ Root_of_Expr ex
 560  , ty ~ Type_Root_of_Expr ex
 561  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 562                    (Error_of_Expr ast root)
 563  , Constraint_Type c ty
 564  )
 565  => Proxy ex -> Proxy c -> ast -> ty h
 566  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 567  -> Either (Error_of_Expr ast root) ret
 568 check_constraint_type ex c ast ty k =
 569         case constraint_type c ty of
 570          Just Dict -> k Dict
 571          Nothing -> Left $ error_expr ex $
 572                 Error_Expr_Constraint_missing ast
 573                  {-(Exists_Dict c)-}
 574                  -- FIXME: not easy to report the constraint
 575                  -- and still support 'Eq' and 'Show' deriving.
 576                  (Exists_Type ty)
 577
 578 -- | Parsing utility to check that a type is has instance of a given 'Constraint'1,
 579 -- or raise 'Error_Expr_Constraint_missing'.
 580 check_constraint1_type
 581  :: forall ast ex c root ty h a ret.
 582  ( root ~ Root_of_Expr ex
 583  , ty ~ Type_Root_of_Expr ex
 584  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 585                    (Error_of_Expr ast root)
 586  , Constraint_Type1 c ty
 587  )
 588  => Proxy ex -> Proxy c -> ast -> ty (h a)
 589  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 590  -> Either (Error_of_Expr ast root) ret
 591 check_constraint1_type ex c ast ty k =
 592         case constraint_type1 c ty of
 593          Just Dict -> k Dict
 594          Nothing -> Left $ error_expr ex $
 595                 Error_Expr_Constraint_missing ast
 596                  (Exists_Type ty)
 597
 598 -- | Parsing utility to check that the given type is a 'Type_Maybe'
 599 -- or raise 'Error_Expr_Type_mismatch'.
 600 check_type1
 601  :: forall ast ex root ty h ret.
 602  ( root ~ Root_of_Expr ex
 603  , ty ~ Type_Root_of_Expr ex
 604  , Unlift_Type1 (Type_of_Expr root)
 605  , String_from_Type ty
 606  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 607                    (Error_of_Expr ast root)
 608  )
 609  => Proxy ex -> ast -> ty h
 610  -> (forall (f:: * -> *).
 611      ( Type_Type1 f ty h
 612      , Lift_Type1 f (Type_Var :|: Type_of_Expr root)
 613      ) -> Either (Error_of_Expr ast root) ret)
 614  -> Either (Error_of_Expr ast root) ret
 615 check_type1 ex ast ty k =
 616         case unlift_type1 (unType_Root ty) $ Just . k of
 617          Just x -> x
 618          Nothing -> undefined
 619                 {-
 620          Just x -> k x
 621          Nothing ->
 622                 error ("check_type1: " ++ show ty)
 623                 Left $
 624                 error_expr ex $
 625                 Error_Expr_Type_mismatch ast
 626                  (Exists_Type (lift_type_root (Type_Type1 $ type_var SZero) -- $ type_var SZero
 627                  :: Type_Root_of_Expr ex (Zero1 Zero)))
 628                  (Exists_Type ty)
 629                 -}
 630 data Zero1 a
 631
 632 -- * Type 'Error_Read'
 633 -- | Error parsing a host-term.
 634 data Error_Read
 635  =   Error_Read Text
 636  deriving (Eq, Show)
 637
 638 -- | Parse a host-term.
 639 read_safe :: Read h => Text -> Either Error_Read h
 640 read_safe t =
 641         case reads $ Text.unpack t of
 642          [(x, "")] -> Right x
 643          _         -> Left $ Error_Read t