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 'Sym_from'
  25
  26 class Sym_from raw (ex:: *) where
  27         sym_from
  28          :: forall hs ret
  29          .  Proxy ex
  30          -- ^ Select the 'Sym_from' instance for the expression @ex@.
  31          -> Context (Var (Root_of_Expr ex)) hs
  32          -- ^ The bound variables and their types held in the heterogeneous list @hs@
  33          -- (types being constructed within: 'Type_Root_of_Expr' @ex@.
  34          -> raw
  35          -- ^ The input data to parse.
  36          -> ( forall h
  37             .  Type_Root_of_Expr ex h
  38             -- The type of the parsed symantic expression.
  39             -> Forall_Repr_with_Context ex hs h
  40             -- The parsed symantic expression
  41             -- (still abstracted by a 'Context' at this point).
  42             -> Either (Maybe (Error_of_Expr raw (Root_of_Expr ex))) ret
  43             )
  44          -- ^ The accumulating continuation.
  45          ->    Either (Maybe (Error_of_Expr raw (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 'Sym_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 'Var'
  59 -- | Join a name and a type;
  60 -- used to handle lambda variables by name
  61 -- (instead of DeBruijn indices for instance).
  62 data Var ex h
  63  =   Var Var_Name (Type_Root_of_Expr ex h)
  64 type Var_Name = Text
  65
  66 -- ** Type 'Forall_Repr_with_Context'
  67 -- | A data type embedding a universal quantification over @repr@
  68 -- to construct a symantic expression polymorphic enough to stay
  69 -- interpretable by different interpreters;
  70 -- moreover the symantic expression is abstracted by a 'Context'
  71 -- built at parsing time.
  72 data Forall_Repr_with_Context ex hs h
  73  =   Forall_Repr_with_Context
  74  (   forall repr. ( Sym_of_Expr ex repr
  75                   , Sym_of_Expr (Root_of_Expr ex) repr
  76                   ) => Context repr hs -> repr h )
  77
  78 -- *** Type 'Forall_Repr'
  79 data Forall_Repr ex h
  80  =   Forall_Repr
  81  { unForall_Repr :: forall repr
  82                  .  Sym_of_Expr ex repr
  83                  => repr h }
  84
  85 -- ** Type 'Root_of_Expr'
  86 -- | The root expression, closing an expression with itself.
  87 type family Root_of_Expr (ex:: *) :: *
  88
  89 -- ** Type 'Sym_of_Expr'
  90 -- | The symantic of an expression.
  91 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
  92
  93 -- ** Type 'Error_of_Expr'
  94 -- | The error(s) of an expression.
  95 type family Error_of_Expr (raw:: *) (ex:: *) :: *
  96
  97 -- ** Type 'Type_of_Expr'
  98 -- | The type of an expression, parameterized by a root type.
  99 type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
 100
 101 -- ** Type 'Type_Root_of_Expr'
 102 type Type_Root_of_Expr ex
 103  =   Type_Root (Type_of_Expr (Root_of_Expr ex))
 104
 105 -- * Type 'Expr_Root'
 106 -- | The root expression, passing itself as parameter to the given expression.
 107 newtype Expr_Root (ex:: * -> *)
 108  =      Expr_Root (ex (Expr_Root ex))
 109 type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
 110 type instance Type_of_Expr (Expr_Root ex)
 111  =            Type_of_Expr (ex (Expr_Root ex))
 112  -- NOTE: require UndecidableInstances.
 113 type instance Error_of_Expr raw (Expr_Root ex)
 114  =            Error_Expr_Cons (Error_Expr_Read raw)
 115                              (Error_of_Expr raw (ex (Expr_Root ex)))
 116  -- NOTE: require UndecidableInstances.
 117 type instance Sym_of_Expr (Expr_Root ex) repr
 118  =            Sym_of_Expr (ex (Expr_Root ex)) repr
 119  -- NOTE: require UndecidableInstances.
 120 instance -- Sym_from
 121  ( Sym_from raw (ex (Expr_Root ex))
 122  , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
 123  ) => Sym_from raw (Expr_Root ex) where
 124         sym_from _px_ex ctx raw k =
 125                 sym_from (Proxy::Proxy (ex (Expr_Root ex)))
 126                  ctx raw $ \ty (Forall_Repr_with_Context repr) ->
 127                         k ty (Forall_Repr_with_Context repr)
 128
 129 -- ** Class 'Expr_Root_Lift'
 130 -- | Lift a given type to a given root type.
 131 class Expr_Root_Lift ex root where
 132         expr_root_lift :: ex root -> root
 133 instance
 134  Expr_Lift ex root =>
 135  Expr_Root_Lift ex (Expr_Root root) where
 136         expr_root_lift = Expr_Root . expr_lift
 137
 138
 139 -- * Type 'Expr_Cons'
 140 -- | Combine two types into one.
 141 data Expr_Cons curr next (root:: *)
 142  =   Expr_Curr (curr root)
 143  |   Expr_Next (next root)
 144 type instance Root_of_Expr (Expr_Cons curr next root) = root
 145 type instance Type_of_Expr (Expr_Cons curr next root)
 146  = Type_Cons (Type_of_Expr (curr root))
 147              (Type_of_Expr (next root))
 148 type instance Error_of_Expr raw (Expr_Cons curr next root)
 149  = Error_Expr_Cons (Error_of_Expr raw (curr root))
 150                    (Error_of_Expr raw (next root))
 151 type instance Sym_of_Expr (Expr_Cons curr next root) repr
 152  = ( Sym_of_Expr (curr root) repr
 153    , Sym_of_Expr (next root) repr
 154    )
 155 instance -- Sym_from
 156  ( Sym_from raw (curr root)
 157  , Sym_from raw (next root)
 158  , Root_of_Expr (curr root) ~ root
 159  , Root_of_Expr (next root) ~ root
 160  ) => Sym_from raw (Expr_Cons curr next root) where
 161         sym_from _px_ex ctx raw k =
 162                 case sym_from (Proxy::Proxy (curr root)) ctx raw $
 163                  \ty (Forall_Repr_with_Context repr) ->
 164                         Right $ k ty (Forall_Repr_with_Context repr) of
 165                  Right ret -> ret
 166                  Left Nothing -> sym_from (Proxy::Proxy (next root)) ctx raw $
 167                          \ty (Forall_Repr_with_Context repr) ->
 168                                 k ty (Forall_Repr_with_Context repr)
 169                  Left err -> Left err
 170
 171 -- ** Type 'Peano_of_Expr'
 172 -- | Return a 'Peano' number derived from the location
 173 -- of a given extension within a given extension stack.
 174 type family Peano_of_Expr
 175  (ex::  * -> *)
 176  (exs:: * -> *) :: Peano where
 177         Peano_of_Expr ex ex                       = 'Zero
 178         Peano_of_Expr ex (Expr_Cons ex next)      = 'Zero
 179         Peano_of_Expr other (Expr_Cons curr next) = 'Succ (Peano_of_Expr other next)
 180
 181 -- ** Type 'Expr_Lift'
 182 -- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
 183 type Expr_Lift ex exs
 184  =   Expr_LiftN (Peano_of_Expr ex exs) ex exs
 185
 186 -- *** Class 'Expr_LiftN'
 187 -- | Construct the sequence of 'Expr_Curr' and 'Expr_Next'
 188 -- lifting a given extension to the top of a given extension stack.
 189 class Expr_LiftN (n::Peano) ex exs where
 190         expr_liftN :: forall (root:: *). Proxy n -> ex root -> exs root
 191 instance Expr_LiftN 'Zero curr curr where
 192         expr_liftN _ = id
 193 instance Expr_LiftN 'Zero curr (Expr_Cons curr next) where
 194         expr_liftN _ = Expr_Curr
 195 instance
 196  Expr_LiftN n other next =>
 197  Expr_LiftN ('Succ n) other (Expr_Cons curr next) where
 198         expr_liftN _ = Expr_Next . expr_liftN (Proxy::Proxy n)
 199
 200 -- | Lift an expression within an expression stack to its top,
 201 -- using a 'Peano' number calculated by 'Peano_of_Expr'
 202 -- to avoid the overlapping of the 'Expr_LiftN' instances.
 203 expr_lift
 204  :: forall ex exs (root:: *).
 205  Expr_Lift ex exs =>
 206  ex root -> exs root
 207 expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
 208
 209 -- ** Type 'Expr_Unlift'
 210 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
 211 type Expr_Unlift ex exs
 212  =   Expr_UnliftN (Peano_of_Expr ex exs) ex exs
 213
 214 -- *** Class 'Expr_UnliftN'
 215 -- | Deconstruct a sequence of 'Expr_Curr' and 'Expr_Next'
 216 -- trying to unlift a given extension out of a given extension stack.
 217 class Expr_UnliftN (n::Peano) ex exs where
 218         expr_unliftN :: forall (root:: *). Proxy n -> exs root -> Maybe (ex root)
 219 instance Expr_UnliftN 'Zero curr curr where
 220         expr_unliftN _ = Just
 221 instance Expr_UnliftN 'Zero curr (Expr_Cons curr next) where
 222         expr_unliftN _ (Expr_Curr x) = Just x
 223         expr_unliftN _ (Expr_Next _) = Nothing
 224 instance
 225  Expr_UnliftN n other next =>
 226  Expr_UnliftN ('Succ n) other (Expr_Cons curr next) where
 227         expr_unliftN _ (Expr_Next x) = expr_unliftN (Proxy::Proxy n) x
 228         expr_unliftN _ (Expr_Curr _) = Nothing
 229
 230 -- | Unlift an expression within an expression stack,
 231 -- using a 'Peano' number calculated by 'Peano_of_Expr'
 232 -- to avoid the overlapping of the 'Expr_UnliftN' instances.
 233 expr_unlift
 234  :: forall ex exs (root:: *).
 235  Expr_Unlift ex exs =>
 236  exs root -> Maybe (ex root)
 237 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
 238
 239 -- * Type 'Error_Expr_Cons'
 240 -- | Combine two error expressions into one.
 241 data Error_Expr_Cons curr next
 242  =   Error_Expr_Curr curr
 243  |   Error_Expr_Next next
 244  deriving (Eq, Show)
 245
 246 -- ** Class 'Error_Expr_LiftN'
 247 -- | Construct the sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'
 248 -- lifting a given error type to the top of a given error type stack.
 249 class Error_Expr_LiftN (n::Peano) err errs where
 250         error_expr_liftN :: Proxy n -> err -> errs
 251 instance Error_Expr_LiftN 'Zero curr curr where
 252         error_expr_liftN _ = id
 253 instance Error_Expr_LiftN 'Zero curr (Error_Expr_Cons curr next) where
 254         error_expr_liftN _ = Error_Expr_Curr
 255 instance
 256  Error_Expr_LiftN n other next =>
 257  Error_Expr_LiftN ('Succ n) other (Error_Expr_Cons curr next) where
 258         error_expr_liftN _ = Error_Expr_Next . error_expr_liftN (Proxy::Proxy n)
 259
 260 -- | Lift an error type within a type stack to its top,
 261 -- using a 'Peano' number calculated by 'Peano_of_Error_Expr'
 262 -- to avoid the overlapping of the 'Error_Expr_LiftN' instances.
 263 error_expr_lift
 264  :: forall err errs.
 265  Error_Expr_Lift err errs =>
 266  err -> errs
 267 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
 268
 269 type Error_Expr_Lift err errs
 270  =   Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
 271 -- | Return a 'Peano' number derived from the location
 272 -- of a given error type within a given error type stack.
 273 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: Peano where
 274         Peano_of_Error_Expr err err                           = 'Zero
 275         Peano_of_Error_Expr err (Error_Expr_Cons err next)    = 'Zero
 276         Peano_of_Error_Expr other (Error_Expr_Cons curr next) = 'Succ (Peano_of_Error_Expr other next)
 277
 278 -- ** Type 'Error_Expr_Read'
 279 data Error_Expr_Read raw
 280  =   Error_Expr_Read Error_Read raw
 281  deriving (Eq, Show)
 282