1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
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
15 import Data.Proxy (Proxy(..))
16 import GHC.Prim (Constraint)
17 import Data.Text (Text)
20 import Language.LOL.Symantic.AST
21 import Language.LOL.Symantic.Type
23 -- * Class 'Expr_from'
25 class Expr_from ast (ex:: *) where
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.
35 -- ^ The input data to parse.
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
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_Next :: item h -> Context item hs -> Context item (h ': hs)
52 infixr 5 `Context_Next`
55 -- | Join a name and a type.
57 -- This data type is used to handle lambda variables by name
58 -- (instead of DeBruijn indices for instance).
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.
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.
72 -- This data type is used to keep a parsed expression polymorphic enough
73 -- to stay interpretable by different interpreters.
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@.
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 )
91 -- ** Type 'Forall_Repr'
94 { unForall_Repr :: forall repr
98 -- ** Type family 'Root_of_Expr'
99 -- | The root expression, closing an expression with itself.
100 type family Root_of_Expr (ex:: *) :: *
102 -- ** Type family 'Sym_of_Expr'
103 -- | The symantic of an expression.
104 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
106 -- ** Type family 'Error_of_Expr'
107 -- | The error(s) of an expression.
108 type family Error_of_Expr (ast:: *) (ex:: *) :: *
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-}* -> *
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))
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)
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
149 Expr_Root_Lift ex (Expr_Root root) where
150 expr_root_lift = Expr_Root . expr_lift
152 -- * Type 'Expr_Cons'
153 -- | Combine two expressions into one.
154 data Expr_Cons curr next (root:: *)
155 = Expr_Curr (curr root)
156 | Expr_Next (next root)
157 type instance Root_of_Expr (Expr_Cons curr next root) = root
158 type instance Type_of_Expr (Expr_Cons curr next root)
159 = Type_Cons (Type_of_Expr (curr root))
160 (Type_of_Expr (next root))
161 type instance Error_of_Expr ast (Expr_Cons curr next root)
162 = Error_Expr_Cons (Error_of_Expr ast (curr root))
163 (Error_of_Expr ast (next root))
164 type instance Sym_of_Expr (Expr_Cons curr next root) repr
165 = ( Sym_of_Expr (curr root) repr
166 , Sym_of_Expr (next root) repr
168 instance -- Expr_from
169 ( Expr_from ast (curr root)
170 , Expr_from ast (next root)
171 , Root_of_Expr (curr root) ~ root
172 , Root_of_Expr (next root) ~ root
173 , Error_Expr_Unlift (Error_Expr ast) (Error_of_Expr ast root)
174 ) => Expr_from ast (Expr_Cons curr next root) where
175 expr_from _px_ex ctx ast k =
176 case expr_from (Proxy::Proxy (curr root)) ctx ast $
177 \ty (Forall_Repr_with_Context repr) ->
178 Right $ k ty (Forall_Repr_with_Context repr) of
181 case error_expr_unlift err of
182 Just (Error_Expr_Unsupported_here (_::ast)) ->
183 expr_from (Proxy::Proxy (next root)) ctx ast $
184 \ty (Forall_Repr_with_Context repr) ->
185 k ty (Forall_Repr_with_Context repr)
188 -- ** Type 'Expr_Lift'
189 -- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
190 type Expr_Lift ex exs
191 = Expr_LiftN (Peano_of_Expr ex exs) ex exs
193 -- | Convenient wrapper around 'expr_liftN',
194 -- passing it the 'Peano' number from 'Peano_of_Expr',
195 -- used to avoid @OverlappingInstances@.
197 :: forall ex exs (root:: *).
200 expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
202 -- *** Type family 'Peano_of_Expr'
203 -- | Return a 'Peano' number derived from the location
204 -- of a given expression within a given expression stack.
205 type family Peano_of_Expr
207 (exs:: * -> *) :: Peano where
208 Peano_of_Expr ex ex = 'Zero
209 Peano_of_Expr ex (Expr_Cons ex next) = 'Zero
210 Peano_of_Expr other (Expr_Cons curr next) = 'Succ (Peano_of_Expr other next)
212 -- *** Class 'Expr_LiftN'
213 -- | Lift a given expression to the top of a given expression stack including it,
214 -- by constructing the appropriate sequence of 'Expr_Curr' and 'Expr_Next'.
215 class Expr_LiftN (n::Peano) ex exs where
216 expr_liftN :: forall (root:: *). Proxy n -> ex root -> exs root
217 instance Expr_LiftN 'Zero curr curr where
219 instance Expr_LiftN 'Zero curr (Expr_Cons curr next) where
220 expr_liftN _ = Expr_Curr
222 Expr_LiftN n other next =>
223 Expr_LiftN ('Succ n) other (Expr_Cons curr next) where
224 expr_liftN _ = Expr_Next . expr_liftN (Proxy::Proxy n)
226 {- NOTE: unused code so far
227 -- ** Type 'Expr_Unlift'
228 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
229 type Expr_Unlift ex exs
230 = Expr_UnliftN (Peano_of_Expr ex exs) ex exs
232 -- | Convenient wrapper around 'expr_unliftN',
233 -- passing it the 'Peano' number from 'Peano_of_Expr',
234 -- used to avoid @OverlappingInstances@.
236 :: forall ex exs (root:: *).
237 Expr_Unlift ex exs =>
238 exs root -> Maybe (ex root)
239 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
241 -- *** Class 'Expr_UnliftN'
242 -- | Try to unlift a given expression out of a given expression stack including it,
243 -- by deconstructing the appropriate sequence of 'Expr_Curr' and 'Expr_Next'.
244 class Expr_UnliftN (n::Peano) ex exs where
245 expr_unliftN :: forall (root:: *). Proxy n -> exs root -> Maybe (ex root)
246 instance Expr_UnliftN 'Zero curr curr where
247 expr_unliftN _ = Just
248 instance Expr_UnliftN 'Zero curr (Expr_Cons curr next) where
249 expr_unliftN _ (Expr_Curr x) = Just x
250 expr_unliftN _ (Expr_Next _) = Nothing
252 Expr_UnliftN n other next =>
253 Expr_UnliftN ('Succ n) other (Expr_Cons curr next) where
254 expr_unliftN _ (Expr_Next x) = expr_unliftN (Proxy::Proxy n) x
255 expr_unliftN _ (Expr_Curr _) = Nothing
258 -- * Type 'Error_Expr_Cons'
259 -- | Combine two expression errors into one.
260 data Error_Expr_Cons curr next
261 = Error_Expr_Curr curr
262 | Error_Expr_Next next
265 -- ** Type 'Error_Expr_Lift'
266 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftN'.
267 type Error_Expr_Lift err errs
268 = Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
270 -- | Convenient wrapper around 'error_expr_liftN',
271 -- passing it the 'Peano' number from 'Peano_of_Error_Expr',
272 -- used to avoid @OverlappingInstances@.
275 Error_Expr_Lift err errs =>
277 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
279 -- * Type family 'Is_Last_Expr'
280 type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
281 Is_Last_Expr ex ex = 'True
282 Is_Last_Expr ex (Expr_Root exs) = Is_Last_Expr ex (exs (Expr_Root exs))
283 Is_Last_Expr (ex root) (Expr_Cons ex next root) = 'False
284 Is_Last_Expr other (Expr_Cons curr next root) = Is_Last_Expr other (next root)
286 -- *** Type family 'Peano_of_Error_Expr'
287 -- | Return a 'Peano' number derived from the location
288 -- of a given error type within a given error type stack.
289 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: Peano where
290 Peano_of_Error_Expr err err = 'Zero
291 Peano_of_Error_Expr err (Error_Expr_Cons err next) = 'Zero
292 Peano_of_Error_Expr other (Error_Expr_Cons curr next) = 'Succ (Peano_of_Error_Expr other next)
294 -- *** Class 'Error_Expr_LiftN'
295 -- | Lift a given expression to the top of a given expression stack including it,
296 -- by constructing the appropriate sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'.
297 class Error_Expr_LiftN (n::Peano) err errs where
298 error_expr_liftN :: Proxy n -> err -> errs
299 instance Error_Expr_LiftN 'Zero curr curr where
300 error_expr_liftN _ = id
301 instance Error_Expr_LiftN 'Zero curr (Error_Expr_Cons curr next) where
302 error_expr_liftN _ = Error_Expr_Curr
304 Error_Expr_LiftN n other next =>
305 Error_Expr_LiftN ('Succ n) other (Error_Expr_Cons curr next) where
306 error_expr_liftN _ = Error_Expr_Next . error_expr_liftN (Proxy::Proxy n)
308 -- ** Type 'Error_Expr_Unlift'
309 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftN'.
310 type Error_Expr_Unlift ex exs
311 = Error_Expr_UnliftN (Peano_of_Error_Expr ex exs) ex exs
313 -- | Convenient wrapper around 'error_expr_unliftN',
314 -- passing it the 'Peano' number from 'Peano_of_Error_Expr',
315 -- used to avoid @OverlappingInstances@.
318 Error_Expr_Unlift ex exs =>
320 error_expr_unlift = error_expr_unliftN (Proxy::Proxy (Peano_of_Error_Expr ex exs))
322 -- *** Class 'Error_Expr_UnliftN'
323 -- | Try to unlift a given expression error out of a given expression error stack including it,
324 -- by deconstructing the appropriate sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'.
325 class Error_Expr_UnliftN (n::Peano) ex exs where
326 error_expr_unliftN :: Proxy n -> exs -> Maybe ex
327 instance Error_Expr_UnliftN 'Zero curr curr where
328 error_expr_unliftN _ = Just
329 instance Error_Expr_UnliftN 'Zero curr (Error_Expr_Cons curr next) where
330 error_expr_unliftN _ (Error_Expr_Curr x) = Just x
331 error_expr_unliftN _ (Error_Expr_Next _) = Nothing
333 Error_Expr_UnliftN n other next =>
334 Error_Expr_UnliftN ('Succ n) other (Error_Expr_Cons curr next) where
335 error_expr_unliftN _ (Error_Expr_Next x) = error_expr_unliftN (Proxy::Proxy n) x
336 error_expr_unliftN _ (Error_Expr_Curr _) = Nothing
338 -- ** Type 'Error_Expr_Read'
339 -- | Common expression errors.
341 = Error_Expr_Read Error_Read ast
342 | Error_Expr_Unsupported ast
343 -- ^ Given syntax is supported by none
344 -- of the expression parser components
345 -- of the expression stack.
346 | Error_Expr_Unsupported_here ast
347 -- ^ Given syntax not supported by the current expression parser component.