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 (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          -> ast
  35          -- ^ The input data to parse.
  36          -> ( forall h
  37             .  Type_Root_of_Expr ex h
  38             -- The type of the parsed expression.
  39             -> Forall_Repr_with_Context ex hs h
  40             -- The parsed expression
  41             -- (still abstracted by a 'Context' at this point).
  42             -> Either (Maybe (Error_of_Expr ast (Root_of_Expr ex))) ret
  43             )
  44          -- ^ The accumulating continuation.
  45          ->    Either (Maybe (Error_of_Expr ast (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 'Expr_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 an expression polymorphic enough to stay
  69 -- interpretable by different interpreters;
  70 -- moreover the 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 (ast:: *) (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 ast (Expr_Root ex)
 114  =            Error_Expr_Cons (Error_Expr_Read ast)
 115                              (Error_of_Expr ast (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 -- Expr_from
 121  ( Expr_from ast (ex (Expr_Root ex))
 122  , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
 123  ) => Expr_from ast (Expr_Root ex) where
 124         expr_from _px_ex ctx ast k =
 125                 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
 126                  ctx ast $ \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 ast (Expr_Cons curr next root)
 149  = Error_Expr_Cons (Error_of_Expr ast (curr root))
 150                    (Error_of_Expr ast (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 -- Expr_from
 156  ( Expr_from ast (curr root)
 157  , Expr_from ast (next root)
 158  , Root_of_Expr (curr root) ~ root
 159  , Root_of_Expr (next root) ~ root
 160  ) => Expr_from ast (Expr_Cons curr next root) where
 161         expr_from _px_ex ctx ast k =
 162                 case expr_from (Proxy::Proxy (curr root)) ctx ast $
 163                  \ty (Forall_Repr_with_Context repr) ->
 164                         Right $ k ty (Forall_Repr_with_Context repr) of
 165                  Right ret -> ret
 166                  Left Nothing -> expr_from (Proxy::Proxy (next root)) ctx ast $
 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 -- | 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 'Expr_Unlift'
 209 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
 210 type Expr_Unlift ex exs
 211  =   Expr_UnliftN (Peano_of_Expr ex exs) ex exs
 212
 213 -- *** Class 'Expr_UnliftN'
 214 -- | Try to unlift a given expression out of a given expression stack including it,
 215 -- by deconstructing the appropriate sequence of 'Expr_Curr' and 'Expr_Next'.
 216 class Expr_UnliftN (n::Peano) ex exs where
 217         expr_unliftN :: forall (root:: *). Proxy n -> exs root -> Maybe (ex root)
 218 instance Expr_UnliftN 'Zero curr curr where
 219         expr_unliftN _ = Just
 220 instance Expr_UnliftN 'Zero curr (Expr_Cons curr next) where
 221         expr_unliftN _ (Expr_Curr x) = Just x
 222         expr_unliftN _ (Expr_Next _) = Nothing
 223 instance
 224  Expr_UnliftN n other next =>
 225  Expr_UnliftN ('Succ n) other (Expr_Cons curr next) where
 226         expr_unliftN _ (Expr_Next x) = expr_unliftN (Proxy::Proxy n) x
 227         expr_unliftN _ (Expr_Curr _) = Nothing
 228
 229 -- | Convenient wrapper around 'expr_unliftN',
 230 -- passing it the 'Peano' number from 'Peano_of_Expr'.
 231 expr_unlift
 232  :: forall ex exs (root:: *).
 233  Expr_Unlift ex exs =>
 234  exs root -> Maybe (ex root)
 235 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
 236
 237 -- * Type 'Error_Expr_Cons'
 238 -- | Combine two error expressions into one.
 239 data Error_Expr_Cons curr next
 240  =   Error_Expr_Curr curr
 241  |   Error_Expr_Next next
 242  deriving (Eq, Show)
 243
 244 -- ** Class 'Error_Expr_LiftN'
 245 -- | Construct the sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'
 246 -- lifting a given error type to the top of a given error type stack.
 247 class Error_Expr_LiftN (n::Peano) err errs where
 248         error_expr_liftN :: Proxy n -> err -> errs
 249 instance Error_Expr_LiftN 'Zero curr curr where
 250         error_expr_liftN _ = id
 251 instance Error_Expr_LiftN 'Zero curr (Error_Expr_Cons curr next) where
 252         error_expr_liftN _ = Error_Expr_Curr
 253 instance
 254  Error_Expr_LiftN n other next =>
 255  Error_Expr_LiftN ('Succ n) other (Error_Expr_Cons curr next) where
 256         error_expr_liftN _ = Error_Expr_Next . error_expr_liftN (Proxy::Proxy n)
 257
 258 -- | Lift an error type within a type stack to its top,
 259 -- using a 'Peano' number calculated by 'Peano_of_Error_Expr'
 260 -- to avoid the overlapping of the 'Error_Expr_LiftN' instances.
 261 error_expr_lift
 262  :: forall err errs.
 263  Error_Expr_Lift err errs =>
 264  err -> errs
 265 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
 266
 267 type Error_Expr_Lift err errs
 268  =   Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
 269 -- | Return a 'Peano' number derived from the location
 270 -- of a given error type within a given error type stack.
 271 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: Peano where
 272         Peano_of_Error_Expr err err                           = 'Zero
 273         Peano_of_Error_Expr err (Error_Expr_Cons err next)    = 'Zero
 274         Peano_of_Error_Expr other (Error_Expr_Cons curr next) = 'Succ (Peano_of_Error_Expr other next)
 275
 276 -- ** Type 'Error_Expr_Read'
 277 data Error_Expr_Read ast
 278  =   Error_Expr_Read Error_Read ast
 279  deriving (Eq, Show)
 280