Language/LOL/Symantic/Expr/Common.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE ExistentialQuantification #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE KindSignatures #-}
   8 {-# LANGUAGE MultiParamTypeClasses #-}
   9 {-# LANGUAGE Rank2Types #-}
  10 {-# LANGUAGE ScopedTypeVariables #-}
  11 {-# LANGUAGE TypeFamilies #-}
  12 {-# LANGUAGE TypeOperators #-}
  13 {-# LANGUAGE UndecidableInstances #-}
  14 module Language.LOL.Symantic.Expr.Common where
  15
  16 import Data.Proxy (Proxy(..))
  17 import GHC.Prim (Constraint)
  18 import Data.Text (Text)
  19 import Data.Peano
  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 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_Cons (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 -- ** Class 'Expr_Root_Lift'
 144 -- | Lift a given expression to a given root expression.
 145 class Expr_Root_Lift ex root where
 146         expr_root_lift :: ex root -> root
 147 instance
 148  Expr_Lift ex root =>
 149  Expr_Root_Lift ex (Expr_Root root) where
 150         expr_root_lift = Expr_Root . expr_lift
 151
 152
 153 -- * Type 'Expr_Cons'
 154 -- | Combine two expressions into one.
 155 data Expr_Cons curr next (root:: *)
 156  =   Expr_Curr (curr root)
 157  |   Expr_Next (next root)
 158 type instance Root_of_Expr (Expr_Cons curr next root) = root
 159 type instance Type_of_Expr (Expr_Cons curr next root)
 160  = Type_Cons (Type_of_Expr (curr root))
 161              (Type_of_Expr (next root))
 162 type instance Error_of_Expr ast (Expr_Cons curr next root)
 163  = Error_Expr_Cons (Error_of_Expr ast (curr root))
 164                    (Error_of_Expr ast (next root))
 165 type instance Sym_of_Expr (Expr_Cons curr next root) repr
 166  = ( Sym_of_Expr (curr root) repr
 167    , Sym_of_Expr (next root) repr
 168    )
 169 instance -- Expr_from
 170  ( Expr_from ast (curr root)
 171  , Expr_from ast (next root)
 172  , Root_of_Expr (curr root) ~ root
 173  , Root_of_Expr (next root) ~ root
 174  , Error_Expr_Unlift (Error_Expr ast) (Error_of_Expr ast root)
 175  ) => Expr_from ast (Expr_Cons curr next root) where
 176         expr_from _px_ex ctx ast k =
 177                 case expr_from (Proxy::Proxy (curr root)) ctx ast $
 178                  \ty (Forall_Repr_with_Context repr) ->
 179                         Right $ k ty (Forall_Repr_with_Context repr) of
 180                  Right ret -> ret
 181                  Left err ->
 182                         case error_expr_unlift err of
 183                          Just (Error_Expr_Unsupported (_::ast)) ->
 184                                 expr_from (Proxy::Proxy (next root)) ctx ast $
 185                                  \ty (Forall_Repr_with_Context repr) ->
 186                                         k ty (Forall_Repr_with_Context repr)
 187                          _ -> Left err
 188
 189 -- ** Type 'Expr_Lift'
 190 -- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
 191 type Expr_Lift ex exs
 192  =   Expr_LiftN (Peano_of_Expr ex exs) ex exs
 193
 194 -- | Convenient wrapper around 'expr_liftN',
 195 -- passing it the 'Peano' number from 'Peano_of_Expr',
 196 -- used to avoid @OverlappingInstances@.
 197 expr_lift
 198  :: forall ex exs (root:: *).
 199  Expr_Lift ex exs =>
 200  ex root -> exs root
 201 expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
 202
 203 -- *** Type family 'Peano_of_Expr'
 204 -- | Return a 'Peano' number derived from the location
 205 -- of a given expression within a given expression stack.
 206 type family Peano_of_Expr
 207  (ex::  * -> *)
 208  (exs:: * -> *) :: Peano where
 209         Peano_of_Expr ex ex                       = 'Zero
 210         Peano_of_Expr ex (Expr_Cons ex next)      = 'Zero
 211         Peano_of_Expr other (Expr_Cons curr next) = 'Succ (Peano_of_Expr other next)
 212
 213 -- *** Class 'Expr_LiftN'
 214 -- | Lift a given expression to the top of a given expression stack including it,
 215 -- by constructing the appropriate sequence of 'Expr_Curr' and 'Expr_Next'.
 216 class Expr_LiftN (n::Peano) ex exs where
 217         expr_liftN :: forall (root:: *). Proxy n -> ex root -> exs root
 218 instance Expr_LiftN 'Zero curr curr where
 219         expr_liftN _ = id
 220 instance Expr_LiftN 'Zero curr (Expr_Cons curr next) where
 221         expr_liftN _ = Expr_Curr
 222 instance
 223  Expr_LiftN n other next =>
 224  Expr_LiftN ('Succ n) other (Expr_Cons curr next) where
 225         expr_liftN _ = Expr_Next . expr_liftN (Proxy::Proxy n)
 226
 227 {- NOTE: unused code so far
 228 -- ** Type 'Expr_Unlift'
 229 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
 230 type Expr_Unlift ex exs
 231  =   Expr_UnliftN (Peano_of_Expr ex exs) ex exs
 232
 233 -- | Convenient wrapper around 'expr_unliftN',
 234 -- passing it the 'Peano' number from 'Peano_of_Expr',
 235 -- used to avoid @OverlappingInstances@.
 236 expr_unlift
 237  :: forall ex exs (root:: *).
 238  Expr_Unlift ex exs =>
 239  exs root -> Maybe (ex root)
 240 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
 241
 242 -- *** Class 'Expr_UnliftN'
 243 -- | Try to unlift a given expression out of a given expression stack including it,
 244 -- by deconstructing the appropriate sequence of 'Expr_Curr' and 'Expr_Next'.
 245 class Expr_UnliftN (n::Peano) ex exs where
 246         expr_unliftN :: forall (root:: *). Proxy n -> exs root -> Maybe (ex root)
 247 instance Expr_UnliftN 'Zero curr curr where
 248         expr_unliftN _ = Just
 249 instance Expr_UnliftN 'Zero curr (Expr_Cons curr next) where
 250         expr_unliftN _ (Expr_Curr x) = Just x
 251         expr_unliftN _ (Expr_Next _) = Nothing
 252 instance
 253  Expr_UnliftN n other next =>
 254  Expr_UnliftN ('Succ n) other (Expr_Cons curr next) where
 255         expr_unliftN _ (Expr_Next x) = expr_unliftN (Proxy::Proxy n) x
 256         expr_unliftN _ (Expr_Curr _) = Nothing
 257 -}
 258
 259 -- * Type 'Error_Expr_Cons'
 260 -- | Combine two expression errors into one.
 261 data Error_Expr_Cons curr next
 262  =   Error_Expr_Curr curr
 263  |   Error_Expr_Next next
 264  deriving (Eq, Show)
 265
 266 -- ** Type 'Error_Expr_Lift'
 267 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftN'.
 268 type Error_Expr_Lift err errs
 269  =   Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
 270
 271 -- | Convenient wrapper around 'error_expr_liftN',
 272 -- passing it the 'Peano' number from 'Peano_of_Error_Expr',
 273 -- used to avoid @OverlappingInstances@.
 274 error_expr_lift
 275  :: forall err errs.
 276  Error_Expr_Lift err errs =>
 277  err -> errs
 278 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
 279
 280 -- *** Type family 'Peano_of_Error_Expr'
 281 -- | Return a 'Peano' number derived from the location
 282 -- of a given error type within a given error type stack.
 283 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: Peano where
 284         Peano_of_Error_Expr err err                           = 'Zero
 285         Peano_of_Error_Expr err (Error_Expr_Cons err next)    = 'Zero
 286         Peano_of_Error_Expr other (Error_Expr_Cons curr next) = 'Succ (Peano_of_Error_Expr other next)
 287
 288 -- *** Class 'Error_Expr_LiftN'
 289 -- | Lift a given expression to the top of a given expression stack including it,
 290 -- by constructing the appropriate sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'.
 291 class Error_Expr_LiftN (n::Peano) err errs where
 292         error_expr_liftN :: Proxy n -> err -> errs
 293 instance Error_Expr_LiftN 'Zero curr curr where
 294         error_expr_liftN _ = id
 295 instance Error_Expr_LiftN 'Zero curr (Error_Expr_Cons curr next) where
 296         error_expr_liftN _ = Error_Expr_Curr
 297 instance
 298  Error_Expr_LiftN n other next =>
 299  Error_Expr_LiftN ('Succ n) other (Error_Expr_Cons curr next) where
 300         error_expr_liftN _ = Error_Expr_Next . error_expr_liftN (Proxy::Proxy n)
 301
 302 -- ** Type 'Error_Expr_Unlift'
 303 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftN'.
 304 type Error_Expr_Unlift ex exs
 305  =   Error_Expr_UnliftN (Peano_of_Error_Expr ex exs) ex exs
 306
 307 -- | Convenient wrapper around 'error_expr_unliftN',
 308 -- passing it the 'Peano' number from 'Peano_of_Error_Expr',
 309 -- used to avoid @OverlappingInstances@.
 310 error_expr_unlift
 311  :: forall ex exs.
 312  Error_Expr_Unlift ex exs =>
 313  exs -> Maybe ex
 314 error_expr_unlift = error_expr_unliftN (Proxy::Proxy (Peano_of_Error_Expr ex exs))
 315
 316 -- *** Class 'Error_Expr_UnliftN'
 317 -- | Try to unlift a given expression error out of a given expression error stack including it,
 318 -- by deconstructing the appropriate sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'.
 319 class Error_Expr_UnliftN (n::Peano) ex exs where
 320         error_expr_unliftN :: Proxy n -> exs -> Maybe ex
 321 instance Error_Expr_UnliftN 'Zero curr curr where
 322         error_expr_unliftN _ = Just
 323 instance Error_Expr_UnliftN 'Zero curr (Error_Expr_Cons curr next) where
 324         error_expr_unliftN _ (Error_Expr_Curr x) = Just x
 325         error_expr_unliftN _ (Error_Expr_Next _) = Nothing
 326 instance
 327  Error_Expr_UnliftN n other next =>
 328  Error_Expr_UnliftN ('Succ n) other (Error_Expr_Cons curr next) where
 329         error_expr_unliftN _ (Error_Expr_Next x) = error_expr_unliftN (Proxy::Proxy n) x
 330         error_expr_unliftN _ (Error_Expr_Curr _) = Nothing
 331
 332 -- ** Type 'Error_Expr_Read'
 333 -- | Common expression errors.
 334 data Error_Expr ast
 335  =   Error_Expr_Read Error_Read ast
 336  |   Error_Expr_Unsupported ast
 337  deriving (Eq, Show)