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