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