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 GHC.Prim (Constraint)
  17 import Data.Text (Text)
  18 import Data.Peano
  19
  20 import Language.LOL.Symantic.AST
  21 import Language.LOL.Symantic.Type
  22
  23 -- * Class 'Expr_from'
  24
  25 class Expr_from ast (ex:: *) where
  26         expr_from
  27          :: forall hs ret
  28          .  Proxy ex
  29          -- ^ Select the 'Expr_from' instance for the expression @ex@.
  30          -> Context (Var (Type_Root_of_Expr ex)) hs
  31          -- ^ The bound variables in scope and their types:
  32          -- held in the heterogeneous list @hs@,
  33          -- from the closest including lambda abstraction to the farest.
  34          -> ast
  35          -- ^ The input data to parse.
  36          -> ( forall h
  37             .  Type_Root_of_Expr ex h
  38             -> Forall_Repr_with_Context ex hs h
  39             -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
  40          -- ^ The accumulating continuation.
  41          ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
  42
  43 -- ** Type 'Context'
  44
  45 -- | GADT for a typing context,
  46 -- accumulating an @item@ at each lambda;
  47 -- used to accumulate object-types of lambda variables in 'Expr_from'
  48 -- or host-terms of lambda variables in 'Repr_Host'.
  49 data Context :: (* -> *) -> [*] -> * where
  50         Context_Empty :: Context item '[]
  51         Context_Alt_Next  :: item h -> Context item hs -> Context item (h ': hs)
  52 infixr 5 `Context_Alt_Next`
  53
  54 -- ** Type 'Var'
  55 -- | Join a name and a type.
  56 --
  57 -- This data type is used to handle lambda variables by name
  58 -- (instead of DeBruijn indices for instance).
  59 data Var ty h
  60  =   Var Var_Name (ty h)
  61 type Var_Name = Text
  62
  63 -- ** Type 'Forall_Repr_with_Context'
  64 -- | A data type embedding a universal quantification
  65 -- over an interpreter @repr@
  66 -- and qualified by the symantics of an expression.
  67 --
  68 -- Moreover the expression is abstracted by a 'Context'
  69 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
  70 -- for lambda abstractions.
  71 --
  72 -- This data type is used to keep a parsed expression polymorphic enough
  73 -- to stay interpretable by different interpreters.
  74 --
  75 -- NOTE: 'Sym_of_Expr'@ ex repr@
  76 -- is needed to be able to use symantic methods of the parsed expression
  77 -- into a 'Forall_Repr_with_Context' @ex@.
  78 --
  79 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
  80 -- is needed to be able to use an expression
  81 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
  82 -- into a 'Forall_Repr_with_Context'@ ex@,
  83 -- which happens when a symantic method includes a polymorphic type
  84 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
  85 data Forall_Repr_with_Context ex hs h
  86  =   Forall_Repr_with_Context
  87  (   forall repr. ( Sym_of_Expr ex repr
  88                   , Sym_of_Expr (Root_of_Expr ex) repr
  89                   ) => Context repr hs -> repr h )
  90
  91 -- ** Type 'Forall_Repr'
  92 data Forall_Repr ex h
  93  =   Forall_Repr
  94  { unForall_Repr :: forall repr
  95                  .  Sym_of_Expr ex repr
  96                  => repr h }
  97
  98 -- ** Type family 'Root_of_Expr'
  99 -- | The root expression, closing an expression with itself.
 100 type family Root_of_Expr (ex:: *) :: *
 101
 102 -- ** Type family 'Sym_of_Expr'
 103 -- | The symantic of an expression.
 104 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
 105
 106 -- ** Type family 'Error_of_Expr'
 107 -- | The error(s) of an expression.
 108 type family Error_of_Expr (ast:: *) (ex:: *) :: *
 109
 110 -- ** Type family 'Type_of_Expr'
 111 -- | The type of an expression, parameterized by a root type.
 112 type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
 113
 114 -- ** Type 'Type_Root_of_Expr'
 115 -- | Convenient alias.
 116 type Type_Root_of_Expr ex
 117  =   Type_Root (Type_of_Expr (Root_of_Expr ex))
 118
 119 -- * Type 'Expr_Root'
 120 -- | The root expression, passing itself as parameter to the given expression.
 121 newtype Expr_Root (ex:: * -> *)
 122  =      Expr_Root (ex (Expr_Root ex))
 123 type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
 124 type instance Type_of_Expr (Expr_Root ex)
 125  =            Type_of_Expr (ex (Expr_Root ex))
 126  -- NOTE: require UndecidableInstances.
 127 type instance Error_of_Expr ast (Expr_Root ex)
 128  =            Error_Expr_Alt (Error_Expr ast)
 129                               (Error_of_Expr ast (ex (Expr_Root ex)))
 130  -- NOTE: require UndecidableInstances.
 131 type instance Sym_of_Expr (Expr_Root ex) repr
 132  =            Sym_of_Expr (ex (Expr_Root ex)) repr
 133  -- NOTE: require UndecidableInstances.
 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 -- | Combine two expressions into one.
 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 ast) (Error_of_Expr ast root)
 176  ) => Expr_from ast (Expr_Alt curr next root) where
 177         expr_from _px_ex ctx ast k =
 178                 case expr_from (Proxy::Proxy (curr root)) ctx ast $
 179                  \ty (Forall_Repr_with_Context repr) ->
 180                         Right $ k ty (Forall_Repr_with_Context repr) of
 181                  Right ret -> ret
 182                  Left err ->
 183                         case error_expr_unlift err of
 184                          Just (Error_Expr_Unsupported_here (_::ast)) ->
 185                                 expr_from (Proxy::Proxy (next root)) ctx ast $
 186                                  \ty (Forall_Repr_with_Context repr) ->
 187                                         k ty (Forall_Repr_with_Context repr)
 188                          _ -> Left err
 189
 190 {- NOTE: useless code so far.
 191 -- ** Type 'Expr_Lift'
 192 -- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
 193 type Expr_Lift ex exs
 194  =   Expr_LiftN (Peano_of_Expr ex exs) ex exs
 195
 196 -- | Convenient wrapper around 'expr_liftN',
 197 -- passing it the 'Peano' number from 'Peano_of_Expr'.
 198 expr_lift
 199  :: forall ex exs (root:: *).
 200  Expr_Lift ex exs =>
 201  ex root -> exs root
 202 expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
 203
 204 -- *** Type family 'Peano_of_Expr'
 205 -- | Return a 'Peano' number derived from the location
 206 -- of a given expression within a given expression stack,
 207 -- which is used to avoid @OverlappingInstances@.
 208 type family Peano_of_Expr
 209  (ex::  * -> *)
 210  (exs:: * -> *) :: Peano where
 211         Peano_of_Expr ex ex                      = 'Zero
 212         Peano_of_Expr ex (Expr_Alt ex next)      = 'Zero
 213         Peano_of_Expr other (Expr_Alt curr next) = 'Succ (Peano_of_Expr other next)
 214
 215 -- *** Class 'Expr_LiftN'
 216 -- | Lift a given expression to the top of a given expression stack including it,
 217 -- by constructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
 218 class Expr_LiftN (n::Peano) ex exs where
 219         expr_liftN :: forall (root:: *). Proxy n -> ex root -> exs root
 220 instance Expr_LiftN 'Zero curr curr where
 221         expr_liftN _ = id
 222 instance Expr_LiftN 'Zero curr (Expr_Alt curr next) where
 223         expr_liftN _ = Expr_Alt_Curr
 224 instance
 225  Expr_LiftN n other next =>
 226  Expr_LiftN ('Succ n) other (Expr_Alt curr next) where
 227         expr_liftN _ = Expr_Alt_Next . expr_liftN (Proxy::Proxy n)
 228 -}
 229
 230 {- NOTE: useless code so far.
 231 -- ** Type 'Expr_Unlift'
 232 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
 233 type Expr_Unlift ex exs
 234  =   Expr_UnliftN (Peano_of_Expr ex exs) ex exs
 235
 236 -- | Convenient wrapper around 'expr_unliftN',
 237 -- passing it the 'Peano' number from 'Peano_of_Expr'.
 238 expr_unlift
 239  :: forall ex exs (root:: *).
 240  Expr_Unlift ex exs =>
 241  exs root -> Maybe (ex root)
 242 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
 243
 244 -- *** Class 'Expr_UnliftN'
 245 -- | Try to unlift a given expression out of a given expression stack including it,
 246 -- by deconstructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
 247 class Expr_UnliftN (n::Peano) ex exs where
 248         expr_unliftN :: forall (root:: *). Proxy n -> exs root -> Maybe (ex root)
 249 instance Expr_UnliftN 'Zero curr curr where
 250         expr_unliftN _ = Just
 251 instance Expr_UnliftN 'Zero curr (Expr_Alt curr next) where
 252         expr_unliftN _ (Expr_Alt_Curr x) = Just x
 253         expr_unliftN _ (Expr_Alt_Next _) = Nothing
 254 instance
 255  Expr_UnliftN n other next =>
 256  Expr_UnliftN ('Succ n) other (Expr_Alt curr next) where
 257         expr_unliftN _ (Expr_Alt_Next x) = expr_unliftN (Proxy::Proxy n) x
 258         expr_unliftN _ (Expr_Alt_Curr _) = Nothing
 259 -}
 260
 261 -- * Type 'Error_Expr_Alt'
 262 -- | Combine two expression errors into one.
 263 data Error_Expr_Alt curr next
 264  =   Error_Expr_Alt_Curr curr
 265  |   Error_Expr_Alt_Next next
 266  deriving (Eq, Show)
 267
 268 -- ** Type 'Error_Expr_Lift'
 269 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftN'.
 270 type Error_Expr_Lift err errs
 271  =   Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
 272
 273 -- | Convenient wrapper around 'error_expr_liftN',
 274 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
 275 error_expr_lift
 276  :: forall err errs.
 277  Error_Expr_Lift err errs =>
 278  err -> errs
 279 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
 280
 281 -- * Type family 'Is_Last_Expr'
 282 type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
 283         Is_Last_Expr ex ex                                = 'True
 284         Is_Last_Expr ex        (Expr_Root exs)            = Is_Last_Expr ex (exs (Expr_Root exs))
 285         Is_Last_Expr (ex root) (Expr_Alt ex   next root) = 'False
 286         Is_Last_Expr other     (Expr_Alt curr next root) = Is_Last_Expr other (next root)
 287
 288 -- *** Type family 'Peano_of_Error_Expr'
 289 -- | Return a 'Peano' number derived from the location
 290 -- of a given error expression within a given error expression stack,
 291 -- which is used to avoid @OverlappingInstances@.
 292 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: Peano where
 293         Peano_of_Error_Expr err err                          = 'Zero
 294         Peano_of_Error_Expr err (Error_Expr_Alt err next)    = 'Zero
 295         Peano_of_Error_Expr other (Error_Expr_Alt curr next) = 'Succ (Peano_of_Error_Expr other next)
 296
 297 -- *** Class 'Error_Expr_LiftN'
 298 -- | Lift a given expression to the top of a given expression stack including it,
 299 -- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
 300 class Error_Expr_LiftN (n::Peano) err errs where
 301         error_expr_liftN :: Proxy n -> err -> errs
 302 instance Error_Expr_LiftN 'Zero curr curr where
 303         error_expr_liftN _ = id
 304 instance Error_Expr_LiftN 'Zero curr (Error_Expr_Alt curr next) where
 305         error_expr_liftN _ = Error_Expr_Alt_Curr
 306 instance
 307  Error_Expr_LiftN n other next =>
 308  Error_Expr_LiftN ('Succ n) other (Error_Expr_Alt curr next) where
 309         error_expr_liftN _ = Error_Expr_Alt_Next . error_expr_liftN (Proxy::Proxy n)
 310
 311 -- ** Type 'Error_Expr_Unlift'
 312 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftN'.
 313 type Error_Expr_Unlift ex exs
 314  =   Error_Expr_UnliftN (Peano_of_Error_Expr ex exs) ex exs
 315
 316 -- | Convenient wrapper around 'error_expr_unliftN',
 317 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
 318 error_expr_unlift
 319  :: forall ex exs.
 320  Error_Expr_Unlift ex exs =>
 321  exs -> Maybe ex
 322 error_expr_unlift = error_expr_unliftN (Proxy::Proxy (Peano_of_Error_Expr ex exs))
 323
 324 -- *** Class 'Error_Expr_UnliftN'
 325 -- | Try to unlift a given expression error out of a given expression error stack including it,
 326 -- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
 327 class Error_Expr_UnliftN (n::Peano) ex exs where
 328         error_expr_unliftN :: Proxy n -> exs -> Maybe ex
 329 instance Error_Expr_UnliftN 'Zero curr curr where
 330         error_expr_unliftN _ = Just
 331 instance Error_Expr_UnliftN 'Zero curr (Error_Expr_Alt curr next) where
 332         error_expr_unliftN _ (Error_Expr_Alt_Curr x) = Just x
 333         error_expr_unliftN _ (Error_Expr_Alt_Next _) = Nothing
 334 instance
 335  Error_Expr_UnliftN n other next =>
 336  Error_Expr_UnliftN ('Succ n) other (Error_Expr_Alt curr next) where
 337         error_expr_unliftN _ (Error_Expr_Alt_Next x) = error_expr_unliftN (Proxy::Proxy n) x
 338         error_expr_unliftN _ (Error_Expr_Alt_Curr _) = Nothing
 339
 340 -- ** Type 'Error_Expr_Read'
 341 -- | Common expression errors.
 342 data Error_Expr ast
 343  =   Error_Expr_Read Error_Read ast
 344  |   Error_Expr_Unsupported ast
 345  -- ^ Given syntax is supported by none
 346  -- of the expression parser components
 347  -- of the expression stack.
 348  |   Error_Expr_Unsupported_here ast
 349  -- ^ Given syntax not supported by the current expression parser component.
 350  deriving (Eq, Show)