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.Symantic.Expr.From where
15 import Data.Maybe (fromMaybe)
16 import Data.Proxy (Proxy(..))
17 import Data.Text (Text)
18 import Data.Type.Equality ((:~:)(Refl))
19 import GHC.Prim (Constraint)
21 import Language.Symantic.Type
22 import Language.Symantic.Expr.Root
23 import Language.Symantic.Expr.Alt
24 import Language.Symantic.Expr.Error
26 -- * Class 'Expr_From'
27 -- | Parse given @ast@ into
28 -- a 'Type_Root_of_Expr' and
29 -- a 'Forall_Repr_with_Context',
30 -- or return an 'Error_of_Expr'.
31 class Expr_From ast (ex:: *) where
32 expr_from :: ExprFrom ast ex hs ret
34 ( Expr_From ast (ex (Expr_Root ex))
35 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
36 ) => Expr_From ast (Expr_Root ex) where
37 expr_from _ex ctx ast k =
38 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
39 ctx ast $ \ty (Forall_Repr_with_Context repr) ->
40 k ty (Forall_Repr_with_Context repr)
42 ( Expr_From ast (curr root)
43 , Expr_From ast (next root)
44 , Root_of_Expr (curr root) ~ root
45 , Root_of_Expr (next root) ~ root
46 , Error_Expr_Unlift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
47 (Type_Root_of_Expr root) ast)
48 (Error_of_Expr ast root)
49 ) => Expr_From ast (Expr_Alt curr next root) where
50 expr_from _ex ctx ast k =
51 case expr_from (Proxy::Proxy (curr root)) ctx ast $
52 \ty (Forall_Repr_with_Context repr) ->
53 Right $ k ty (Forall_Repr_with_Context repr) of
56 case error_expr_unlift err of
57 Just (Error_Expr_Unsupported_here _
58 :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
59 (Type_Root_of_Expr root) ast) ->
60 expr_from (Proxy::Proxy (next root)) ctx ast $
61 \ty (Forall_Repr_with_Context repr) ->
62 k ty (Forall_Repr_with_Context repr)
66 type ExprFrom ast ex hs ret
68 -- ^ Select the 'Expr_From' instance.
70 -- ^ The input data to parse.
71 -> Lambda_Context (Lambda_Var (Type_Root_of_Expr ex)) hs
72 -- ^ The bound variables in scope and their types:
73 -- held in the heterogeneous list @hs@,
74 -- from the closest including lambda abstraction to the farest.
76 . Type_Root_of_Expr ex h
77 -> Forall_Repr_with_Context ex hs h
78 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
79 -- ^ The accumulating continuation.
80 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
82 -- ** Type 'Lambda_Context'
83 -- | GADT for a typing context,
84 -- accumulating an @item@ at each lambda;
85 -- used to accumulate object-types (in 'Expr_From')
86 -- or host-terms (in 'Repr_Host')
87 -- associated with the 'Lambda_Var's in scope.
88 data Lambda_Context :: (* -> *) -> [*] -> * where
89 Lambda_Context_Empty :: Lambda_Context item '[]
90 Lambda_Context_Next :: item h -> Lambda_Context item hs -> Lambda_Context item (h ': hs)
91 infixr 5 `Lambda_Context_Next`
93 -- ** Type 'Lambda_Var'
94 -- | Join a name and a type.
96 -- This data type is used to handle lambda variables by name
97 -- (instead of DeBruijn indices for instance).
99 = Lambda_Var Lambda_Var_Name (ty h)
100 type Lambda_Var_Name = Text
102 -- ** Type 'Forall_Repr_with_Context'
103 -- | A data type embedding a universal quantification
104 -- over an interpreter @repr@
105 -- and qualified by the symantics of an expression.
107 -- Moreover the expression is abstracted by a 'Lambda_Context'
108 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
109 -- for lambda abstractions.
111 -- This data type is used to keep a parsed expression polymorphic enough
112 -- to stay interpretable by different interpreters.
114 -- NOTE: 'Sym_of_Expr'@ ex repr@
115 -- is needed to be able to use symantic methods of the parsed expression
116 -- into a 'Forall_Repr_with_Context'@ ex@.
118 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
119 -- is needed to be able to use an expression
120 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
121 -- into a 'Forall_Repr_with_Context'@ ex@,
122 -- which happens when a symantic method includes a polymorphic type
123 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
124 data Forall_Repr_with_Context ex hs h
125 = Forall_Repr_with_Context
126 ( forall repr. ( Sym_of_Expr ex repr
127 , Sym_of_Expr (Root_of_Expr ex) repr
128 ) => Lambda_Context repr hs -> repr h )
130 -- ** Type 'Forall_Repr'
131 data Forall_Repr ex h
133 { unForall_Repr :: forall repr
134 . ( Sym_of_Expr ex repr
135 , Sym_of_Expr (Root_of_Expr ex) repr )
138 -- ** Type family 'Sym_of_Expr'
139 -- | The symantic of an expression.
140 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
141 type instance Sym_of_Expr (Expr_Root ex) repr
142 = Sym_of_Expr (ex (Expr_Root ex)) repr
143 type instance Sym_of_Expr (Expr_Alt curr next root) repr
144 = ( Sym_of_Expr (curr root) repr
145 , Sym_of_Expr (next root) repr
150 -- | Parsing utility to check that two types are equal,
151 -- or raise 'Error_Expr_Type_mismatch'.
153 :: forall ast ex ta root ty h ret.
154 ( root ~ Root_of_Expr ex
155 , ty ~ Type_Root_of_Expr ex
157 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
158 (Error_of_Expr ast root)
159 ) => Proxy ta -> Proxy ex -> ast -> ty h
160 -> (ty (Host_of_Type0_Family ta h) -> Either (Error_of_Expr ast root) ret)
161 -> Either (Error_of_Expr ast root) ret
162 check_type0_family ta ex ast ty k =
163 case type0_family ta ty of
165 Nothing -> Left $ error_expr ex $
166 Error_Expr_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
168 -- | Parsing utility to check that two types are equal,
169 -- or raise 'Error_Expr_Type_mismatch'.
171 :: forall ast ex root ty x y ret.
172 ( root ~ Root_of_Expr ex
173 , ty ~ Type_Root_of_Expr ex
175 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
176 (Error_of_Expr ast root)
177 ) => Proxy ex -> ast -> ty x -> ty y
178 -> (x :~: y -> Either (Error_of_Expr ast root) ret)
179 -> Either (Error_of_Expr ast root) ret
180 check_type0_eq ex ast x y k =
181 case x `type0_eq` y of
183 Nothing -> Left $ error_expr ex $
184 Error_Expr_Type_mismatch ast
188 -- | Parsing utility to check that two 'Type1' are equal,
189 -- or raise 'Error_Expr_Type_mismatch'.
191 :: forall ast ex root ty h1 h2 a1 a2 ret.
192 ( root ~ Root_of_Expr ex
193 , ty ~ Type_Root_of_Expr ex
195 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
196 (Error_of_Expr ast root)
198 => Proxy ex -> ast -> ty (h1 a1) -> ty (h2 a2)
199 -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
200 -> Either (Error_of_Expr ast root) ret
201 check_type1_eq ex ast h1 h2 k =
202 case h1 `type1_eq` h2 of
204 Nothing -> Left $ error_expr ex $
205 Error_Expr_Type_mismatch ast
209 -- | Parsing utility to check that a 'Type0' or higher
210 -- is an instance of a given 'Constraint',
211 -- or raise 'Error_Expr_Constraint_missing'.
212 check_type0_constraint
213 :: forall ast ex c root ty h ret.
214 ( root ~ Root_of_Expr ex
215 , ty ~ Type_Root_of_Expr ex
216 , Type0_Constraint c ty
217 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
218 (Error_of_Expr ast root)
220 => Proxy ex -> Proxy c -> ast -> ty h
221 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
222 -> Either (Error_of_Expr ast root) ret
223 check_type0_constraint ex c ast ty k =
224 case type0_constraint c ty of
226 Nothing -> Left $ error_expr ex $
227 Error_Expr_Constraint_missing ast
229 -- FIXME: not easy to report the constraint
230 -- and still support 'Eq' and 'Show' deriving.
233 -- | Parsing utility to check that a 'Type1' or higher
234 -- is an instance of a given 'Constraint',
235 -- or raise 'Error_Expr_Constraint_missing'.
236 check_type1_constraint
237 :: forall ast ex c root ty h a ret.
238 ( root ~ Root_of_Expr ex
239 , ty ~ Type_Root_of_Expr ex
240 , Type1_Constraint c ty
241 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
242 (Error_of_Expr ast root)
243 ) => Proxy ex -> Proxy c -> ast -> ty (h a)
244 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
245 -> Either (Error_of_Expr ast root) ret
246 check_type1_constraint ex c ast ty k =
247 case type1_constraint c ty of
249 Nothing -> Left $ error_expr ex $
250 Error_Expr_Constraint_missing ast
253 -- | Parsing utility to check that the given type is at least a 'Type1'
254 -- or raise 'Error_Expr_Type_mismatch'.
256 :: forall ast ex root ty h ret.
257 ( root ~ Root_of_Expr ex
258 , ty ~ Type_Root_of_Expr ex
259 , Type1_Unlift (Type_of_Expr root)
260 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
261 (Error_of_Expr ast root)
262 ) => Proxy ex -> ast -> ty h
265 , Type1_Lift t1 ty (Type_Var0 :|: Type_Var1 :|: Type_of_Expr root)
266 ) -> Either (Error_of_Expr ast root) ret)
267 -> Either (Error_of_Expr ast root) ret
268 check_type1 ex ast ty k =
269 (`fromMaybe` type1_unlift (unType_Root ty) (Just . k)) $
272 Error_Expr_Type_mismatch ast
273 (Exists_Type0 (type_var1 SZero (type_var0 SZero)
279 -- | Like 'expr_from' but for a root expression.
283 , Root_of_Expr root ~ root
284 ) => Proxy root -> ast
285 -> Either (Error_of_Expr ast root)
286 (Exists_Type0_and_Repr (Type_Root_of_Expr root)
288 root_expr_from _ex ast =
289 expr_from (Proxy::Proxy root) ast
290 Lambda_Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
291 Right $ Exists_Type0_and_Repr ty $
292 Forall_Repr $ repr Lambda_Context_Empty
294 -- | Parse a literal.
296 :: forall ty lit ex ast hs ret.
297 ( ty ~ Type_Root_of_Expr ex
299 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
300 (Error_of_Expr ast (Root_of_Expr ex))
301 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
302 -> ty lit -> Lambda_Var_Name
303 -> ExprFrom ast ex hs ret
304 lit_from lit ty_lit toread ex ast _ctx k =
305 case read_safe toread of
306 Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
307 Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
309 -- | Parse a unary class operator.
311 :: forall root ty cl ex ast hs ret.
312 ( ty ~ Type_Root_of_Expr ex
313 , root ~ Root_of_Expr ex
316 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
317 (Error_of_Expr ast root)
318 , Root_of_Expr root ~ root
319 , Type0_Constraint cl ty
320 ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit)
322 -> ExprFrom ast ex hs ret
323 class_op1_from op cl ast_x ex _ast ctx k =
324 expr_from (Proxy::Proxy root) ast_x ctx $
325 \ty_x (Forall_Repr_with_Context x) ->
326 check_type0_constraint ex cl ast_x ty_x $ \Dict ->
327 k ty_x $ Forall_Repr_with_Context (op . x)
329 -- | Parse a binary class operator.
331 :: forall root ty cl ex ast hs ret.
332 ( ty ~ Type_Root_of_Expr ex
333 , root ~ Root_of_Expr ex
336 , Type0_Constraint cl ty
337 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
338 (Error_of_Expr ast root)
339 , Root_of_Expr root ~ root
340 ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit -> repr lit)
341 -> Proxy cl -> ast -> ast
342 -> ExprFrom ast ex hs ret
343 class_op2_from op cl ast_x ast_y ex ast ctx k =
344 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
345 expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
346 check_type0_constraint ex cl ast_x ty_x $ \Dict ->
347 check_type0_constraint ex cl ast_y ty_y $ \Dict ->
348 check_type0_eq ex ast ty_x ty_y $ \Refl ->
349 k ty_x $ Forall_Repr_with_Context $
352 -- | Parse a unary operator.
354 :: forall root ty lit ex ast hs ret.
355 ( ty ~ Type_Root_of_Expr ex
356 , root ~ Root_of_Expr ex
359 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
360 (Error_of_Expr ast root)
361 , Root_of_Expr root ~ root
362 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
364 -> ExprFrom ast ex hs ret
365 op1_from op ty_lit ast_x ex ast ctx k =
366 expr_from (Proxy::Proxy root) ast_x ctx $
367 \ty_x (Forall_Repr_with_Context x) ->
368 check_type0_eq ex ast ty_lit ty_x $ \Refl ->
369 k ty_x $ Forall_Repr_with_Context (op . x)
371 -- | Parse a binary operator.
373 :: forall root ty lit ex ast hs ret.
374 ( ty ~ Type_Root_of_Expr ex
375 , root ~ Root_of_Expr ex
378 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
379 (Error_of_Expr ast root)
380 , Root_of_Expr root ~ root
381 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
382 -> ty lit -> ast -> ast
383 -> ExprFrom ast ex hs ret
384 op2_from op ty_lit ast_x ast_y ex ast ctx k =
385 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
386 expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
387 check_type0_eq ex ast ty_lit ty_x $ \Refl ->
388 check_type0_eq ex ast ty_lit ty_y $ \Refl ->
389 k ty_x $ Forall_Repr_with_Context $