Language/LOL/Symantic/Expr/Common.hs

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