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