]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/From.hs
explore parsing of partially applied functions
[haskell/symantic.git] / Language / Symantic / Expr / From.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE DefaultSignatures #-}
4 {-# LANGUAGE FlexibleContexts #-}
5 {-# LANGUAGE FlexibleInstances #-}
6 {-# LANGUAGE GADTs #-}
7 {-# LANGUAGE KindSignatures #-}
8 {-# LANGUAGE MultiParamTypeClasses #-}
9 {-# LANGUAGE OverloadedStrings #-}
10 {-# LANGUAGE Rank2Types #-}
11 {-# LANGUAGE ScopedTypeVariables #-}
12 {-# LANGUAGE TypeFamilies #-}
13 {-# LANGUAGE TypeOperators #-}
14 {-# LANGUAGE UndecidableInstances #-}
15 module Language.Symantic.Expr.From where
16
17 import Data.Maybe (fromMaybe)
18 import Data.Monoid
19 import Data.Proxy (Proxy(..))
20 import Data.Text (Text)
21 import qualified Data.Text as Text
22 import Data.Type.Equality ((:~:)(Refl))
23 import GHC.Prim (Constraint)
24
25 import Language.Symantic.Type
26 import Language.Symantic.Expr.Root
27 import Language.Symantic.Expr.Alt
28 import Language.Symantic.Expr.Error
29 import Language.Symantic.Trans.Common
30 import Language.Symantic.Repr
31
32 -- * Class 'Expr_From'
33 -- | Parse given @ast@ into
34 -- a 'Type_Root_of_Expr' and
35 -- a 'Forall_Repr_with_Context',
36 -- or return an 'Error_of_Expr'.
37 class Expr_From ast (ex:: *) where
38 expr_from :: ExprFrom ast ex hs ret
39 instance -- Expr_From
40 ( Expr_From ast (ex (Expr_Root ex))
41 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
42 ) => Expr_From ast (Expr_Root ex) where
43 expr_from _ex ctx ast k =
44 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
45 ctx ast $ \ty (Forall_Repr_with_Context repr) ->
46 k ty (Forall_Repr_with_Context repr)
47 instance -- Expr_From
48 ( Expr_From ast (curr root)
49 , Expr_From ast (next root)
50 , Root_of_Expr (curr root) ~ root
51 , Root_of_Expr (next root) ~ root
52 , Error_Expr_Unlift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
53 (Type_Root_of_Expr root) ast)
54 (Error_of_Expr ast root)
55 ) => Expr_From ast (Expr_Alt curr next root) where
56 expr_from _ex ctx ast k =
57 case expr_from (Proxy::Proxy (curr root)) ctx ast $
58 \ty (Forall_Repr_with_Context repr) ->
59 Right $ k ty (Forall_Repr_with_Context repr) of
60 Right ret -> ret
61 Left err ->
62 case error_expr_unlift err of
63 Just (Error_Expr_Unsupported_here _
64 :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
65 (Type_Root_of_Expr root) ast) ->
66 expr_from (Proxy::Proxy (next root)) ctx ast $
67 \ty (Forall_Repr_with_Context repr) ->
68 k ty (Forall_Repr_with_Context repr)
69 _ -> Left err
70
71 -- ** Type 'ExprFrom'
72 -- | Convenient type synonym defining a parser.
73 type ExprFrom ast ex hs ret
74 = Proxy ex
75 -- ^ Select the 'Expr_From' instance.
76 -> ast
77 -- ^ The input data to parse.
78 -> Lambda_Context (Lambda_Var (Type_Root_of_Expr ex)) hs
79 -- ^ The bound variables in scope and their types:
80 -- held in the heterogeneous list @hs@,
81 -- from the closest including lambda abstraction to the farest.
82 -> ( forall h
83 . Type_Root_of_Expr ex h
84 -> Forall_Repr_with_Context ex hs h
85 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
86 -- ^ The accumulating continuation.
87 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
88
89 -- ** Type 'Lambda_Context'
90 -- | GADT for a typing context,
91 -- accumulating an @item@ at each lambda;
92 -- used to accumulate object-types (in 'Expr_From')
93 -- or host-terms (in 'Repr_Host')
94 -- associated with the 'Lambda_Var's in scope.
95 data Lambda_Context :: (* -> *) -> [*] -> * where
96 Lambda_Context_Empty :: Lambda_Context item '[]
97 Lambda_Context_Next :: item h
98 -> Lambda_Context item hs
99 -> Lambda_Context item (h ': hs)
100 infixr 5 `Lambda_Context_Next`
101
102 -- ** Type 'Lambda_Var'
103 -- | Join a name and a type.
104 --
105 -- This data type is used to handle lambda variables by name
106 -- (instead of DeBruijn indices for instance).
107 data Lambda_Var ty h
108 = Lambda_Var Lambda_Var_Name (ty h)
109 type Lambda_Var_Name = Text
110
111 -- ** Type 'Forall_Repr_with_Context'
112 -- | A data type embedding a universal quantification
113 -- over an interpreter @repr@
114 -- and qualified by the symantics of an expression.
115 --
116 -- Moreover the expression is abstracted by a 'Lambda_Context'
117 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
118 -- for lambda abstractions.
119 --
120 -- This data type is used to keep a parsed expression polymorphic enough
121 -- to stay interpretable by different interpreters.
122 --
123 -- NOTE: 'Sym_of_Expr'@ ex repr@
124 -- is needed to be able to use symantic methods of the parsed expression
125 -- into a 'Forall_Repr_with_Context'@ ex@.
126 --
127 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
128 -- is needed to be able to use an expression
129 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
130 -- into a 'Forall_Repr_with_Context'@ ex@,
131 -- which happens when a symantic method includes a polymorphic type
132 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
133 --
134 -- NOTE: 'Sym_Lambda_Lam repr@
135 -- is needed to be able to parse partially applied functions
136 -- (when their type is knowable).
137 data Forall_Repr_with_Context ex hs h
138 = Forall_Repr_with_Context
139 ( forall repr. ( Sym_of_Expr ex repr
140 , Sym_of_Expr (Root_of_Expr ex) repr
141 , Sym_Lambda_Lam repr
142 ) => Lambda_Context repr hs -> repr h )
143
144 -- ** Type 'Forall_Repr'
145 -- | 'Forall_Repr_with_Context' applied on a 'Lambda_Context'.
146 data Forall_Repr ex h
147 = Forall_Repr
148 { unForall_Repr :: forall repr
149 . ( Sym_of_Expr ex repr
150 , Sym_of_Expr (Root_of_Expr ex) repr
151 , Sym_Lambda_Lam repr )
152 => repr h }
153
154 -- * Class 'Sym_Lambda_Lam'
155 class Sym_Lambda_Lam repr where
156 -- | /Lambda abstraction/.
157 lam :: (repr arg -> repr res) -> repr ((->) arg res)
158 default lam :: Trans t repr
159 => (t repr arg -> t repr res) -> t repr ((->) arg res)
160 lam f = trans_lift $ lam $ trans_apply . f . trans_lift
161 instance Sym_Lambda_Lam Repr_Host where
162 lam f = Repr_Host (unRepr_Host . f . Repr_Host)
163 instance Sym_Lambda_Lam Repr_Text where
164 lam f =
165 Repr_Text $ \p v ->
166 let p' = Precedence 1 in
167 let x = "x" <> Text.pack (show v) in
168 paren p p' $ "\\" <> x <> " -> "
169 <> unRepr_Text (f (Repr_Text $ \_p _v -> x)) p' (succ v)
170 instance (Sym_Lambda_Lam r1, Sym_Lambda_Lam r2) => Sym_Lambda_Lam (Repr_Dup r1 r2) where
171 lam f = repr_dup_1 (lam f) `Repr_Dup` repr_dup_2 (lam f)
172
173 -- ** Type family 'Sym_of_Expr'
174 -- | The symantic of an expression.
175 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
176 type instance Sym_of_Expr (Expr_Root ex) repr
177 = Sym_of_Expr (ex (Expr_Root ex)) repr
178 type instance Sym_of_Expr (Expr_Alt curr next root) repr
179 = ( Sym_of_Expr (curr root) repr
180 , Sym_of_Expr (next root) repr
181 )
182
183 -- * Checks
184
185 -- | Parsing utility to check that two types are equal,
186 -- or raise 'Error_Expr_Type_mismatch'.
187 check_type0_family
188 :: forall ast ex ta root ty h ret.
189 ( root ~ Root_of_Expr ex
190 , ty ~ Type_Root_of_Expr ex
191 , Type0_Family ta ty
192 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
193 (Error_of_Expr ast root)
194 ) => Proxy ta -> Proxy ex -> ast -> ty h
195 -> (ty (Host_of_Type0_Family ta h) -> Either (Error_of_Expr ast root) ret)
196 -> Either (Error_of_Expr ast root) ret
197 check_type0_family ta ex ast ty k =
198 case type0_family ta ty of
199 Just t -> k t
200 Nothing -> Left $ error_expr ex $
201 Error_Expr_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
202
203 -- | Parsing utility to check that two types are equal,
204 -- or raise 'Error_Expr_Type_mismatch'.
205 check_type0_eq
206 :: forall ast ex root ty x y ret.
207 ( root ~ Root_of_Expr ex
208 , ty ~ Type_Root_of_Expr ex
209 , Type0_Eq ty
210 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
211 (Error_of_Expr ast root)
212 ) => Proxy ex -> ast -> ty x -> ty y
213 -> (x :~: y -> Either (Error_of_Expr ast root) ret)
214 -> Either (Error_of_Expr ast root) ret
215 check_type0_eq ex ast x y k =
216 case x `type0_eq` y of
217 Just Refl -> k Refl
218 Nothing -> Left $ error_expr ex $
219 Error_Expr_Type_mismatch ast
220 (Exists_Type0 x)
221 (Exists_Type0 y)
222
223 -- | Parsing utility to check that two 'Type1' are equal,
224 -- or raise 'Error_Expr_Type_mismatch'.
225 check_type1_eq
226 :: forall ast ex root ty h1 h2 a1 a2 ret.
227 ( root ~ Root_of_Expr ex
228 , ty ~ Type_Root_of_Expr ex
229 , Type1_Eq ty
230 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
231 (Error_of_Expr ast root)
232 )
233 => Proxy ex -> ast -> ty (h1 a1) -> ty (h2 a2)
234 -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
235 -> Either (Error_of_Expr ast root) ret
236 check_type1_eq ex ast h1 h2 k =
237 case h1 `type1_eq` h2 of
238 Just Refl -> k Refl
239 Nothing -> Left $ error_expr ex $
240 Error_Expr_Type_mismatch ast
241 (Exists_Type0 h1)
242 (Exists_Type0 h2)
243
244 -- | Parsing utility to check that a 'Type0' or higher
245 -- is an instance of a given 'Constraint',
246 -- or raise 'Error_Expr_Constraint_missing'.
247 check_type0_constraint
248 :: forall ast ex c root ty h ret.
249 ( root ~ Root_of_Expr ex
250 , ty ~ Type_Root_of_Expr ex
251 , Type0_Constraint c ty
252 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
253 (Error_of_Expr ast root)
254 )
255 => Proxy ex -> Proxy c -> ast -> ty h
256 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
257 -> Either (Error_of_Expr ast root) ret
258 check_type0_constraint ex c ast ty k =
259 case type0_constraint c ty of
260 Just Dict -> k Dict
261 Nothing -> Left $ error_expr ex $
262 Error_Expr_Constraint_missing ast
263 {-(Exists_Dict c)-}
264 -- FIXME: not easy to report the constraint
265 -- and still support 'Eq' and 'Show' deriving.
266 (Exists_Type0 ty)
267
268 -- | Parsing utility to check that a 'Type1' or higher
269 -- is an instance of a given 'Constraint',
270 -- or raise 'Error_Expr_Constraint_missing'.
271 check_type1_constraint
272 :: forall ast ex c root ty h a ret.
273 ( root ~ Root_of_Expr ex
274 , ty ~ Type_Root_of_Expr ex
275 , Type1_Constraint c ty
276 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
277 (Error_of_Expr ast root)
278 ) => Proxy ex -> Proxy c -> ast -> ty (h a)
279 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
280 -> Either (Error_of_Expr ast root) ret
281 check_type1_constraint ex c ast ty k =
282 case type1_constraint c ty of
283 Just Dict -> k Dict
284 Nothing -> Left $ error_expr ex $
285 Error_Expr_Constraint_missing ast
286 (Exists_Type0 ty)
287
288 -- | Parsing utility to check that the given type is at least a 'Type1'
289 -- or raise 'Error_Expr_Type_mismatch'.
290 check_type1
291 :: forall ast ex root ty h ret.
292 ( root ~ Root_of_Expr ex
293 , ty ~ Type_Root_of_Expr ex
294 , Type1_Unlift (Type_of_Expr root)
295 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
296 (Error_of_Expr ast root)
297 ) => Proxy ex -> ast -> ty h
298 -> (forall (t1:: *).
299 ( Type1 t1 ty h
300 , Type1_Lift t1 ty (Type_Var0 :|: Type_Var1 :|: Type_of_Expr root)
301 ) -> Either (Error_of_Expr ast root) ret)
302 -> Either (Error_of_Expr ast root) ret
303 check_type1 ex ast ty k =
304 (`fromMaybe` type1_unlift (unType_Root ty) (Just . k)) $
305 Left $
306 error_expr ex $
307 Error_Expr_Type_mismatch ast
308 (Exists_Type0 (type_var1 SZero (type_var0 SZero)
309 :: ty (Var1 Var0)))
310 (Exists_Type0 ty)
311
312 -- * Parsers
313
314 -- | Like 'expr_from' but for a root expression.
315 root_expr_from
316 :: forall ast root.
317 ( Expr_From ast root
318 , Root_of_Expr root ~ root
319 ) => Proxy root -> ast
320 -> Either (Error_of_Expr ast root)
321 (Exists_Type0_and_Repr (Type_Root_of_Expr root)
322 (Forall_Repr root))
323 root_expr_from _ex ast =
324 expr_from (Proxy::Proxy root) ast
325 Lambda_Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
326 Right $ Exists_Type0_and_Repr ty $
327 Forall_Repr $ repr Lambda_Context_Empty
328
329 -- | Parse a literal.
330 lit_from
331 :: forall ty lit ex ast hs ret.
332 ( ty ~ Type_Root_of_Expr ex
333 , Read lit
334 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
335 (Error_of_Expr ast (Root_of_Expr ex))
336 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
337 -> ty lit -> Text
338 -> ExprFrom ast ex hs ret
339 lit_from lit ty_lit toread ex ast _ctx k =
340 case read_safe toread of
341 Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
342 Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
343
344 -- | Parse a unary class operator.
345 class_op1_from
346 :: forall root ty cl ex ast hs ret.
347 ( ty ~ Type_Root_of_Expr ex
348 , root ~ Root_of_Expr ex
349 , Type0_Eq ty
350 , Expr_From ast root
351 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
352 (Error_of_Expr ast root)
353 , Root_of_Expr root ~ root
354 , Type0_Constraint cl ty
355 ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit)
356 -> Proxy cl -> ast
357 -> ExprFrom ast ex hs ret
358 class_op1_from op cl ast_x ex _ast ctx k =
359 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
360 check_type0_constraint ex cl ast_x ty_x $ \Dict ->
361 k ty_x $ Forall_Repr_with_Context (op . x)
362
363 -- | Parse a binary class operator.
364 class_op2_from
365 :: forall root ty cl ex ast hs ret.
366 ( ty ~ Type_Root_of_Expr ex
367 , root ~ Root_of_Expr ex
368 , Type0_Eq ty
369 , Expr_From ast root
370 , Type0_Constraint cl ty
371 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
372 (Error_of_Expr ast root)
373 , Root_of_Expr root ~ root
374 ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit -> repr lit)
375 -> Proxy cl -> ast -> ast
376 -> ExprFrom ast ex hs ret
377 class_op2_from op cl ast_x ast_y ex ast ctx k =
378 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
379 expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
380 check_type0_constraint ex cl ast_x ty_x $ \Dict ->
381 check_type0_constraint ex cl ast_y ty_y $ \Dict ->
382 check_type0_eq ex ast ty_x ty_y $ \Refl ->
383 k ty_x $ Forall_Repr_with_Context $
384 \c -> x c `op` y c
385
386 -- | Parse a binary class operator, partially applied.
387 class_op2_from1
388 :: forall root ty cl ex ast hs ret.
389 ( ty ~ Type_Root_of_Expr ex
390 , root ~ Root_of_Expr ex
391 , Type0_Eq ty
392 , Type0_Constraint cl ty
393 , Type0_Lift Type_Fun (Type_of_Expr root)
394 , Expr_From ast root
395 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
396 (Error_of_Expr ast root)
397 , Root_of_Expr root ~ root
398 ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit -> repr lit)
399 -> Proxy cl -> ast
400 -> ExprFrom ast ex hs ret
401 class_op2_from1 op cl ast_x ex _ast ctx k =
402 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
403 check_type0_constraint ex cl ast_x ty_x $ \Dict ->
404 k (type_fun ty_x ty_x) $ Forall_Repr_with_Context $
405 \c -> lam $ \y -> x c `op` y
406
407 -- | Parse a unary operator.
408 op1_from
409 :: forall root ty lit ex ast hs ret.
410 ( ty ~ Type_Root_of_Expr ex
411 , root ~ Root_of_Expr ex
412 , Type0_Eq ty
413 , Expr_From ast root
414 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
415 (Error_of_Expr ast root)
416 , Root_of_Expr root ~ root
417 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
418 -> ty lit -> ast
419 -> ExprFrom ast ex hs ret
420 op1_from op ty_lit ast_x ex ast ctx k =
421 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
422 check_type0_eq ex ast ty_lit ty_x $ \Refl ->
423 k ty_x $ Forall_Repr_with_Context (op . x)
424
425 -- | Parse a unary operator, partially applied.
426 op1_from0
427 :: forall root ty lit ex ast hs ret.
428 ( ty ~ Type_Root_of_Expr ex
429 , root ~ Root_of_Expr ex
430 , Type0_Eq ty
431 , Type0_Lift Type_Fun (Type_of_Expr root)
432 , Expr_From ast root
433 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
434 (Error_of_Expr ast root)
435 , Root_of_Expr root ~ root
436 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
437 -> ty lit
438 -> ExprFrom ast ex hs ret
439 op1_from0 op ty_lit _ex _ast _ctx k =
440 k (type_fun ty_lit ty_lit) $ Forall_Repr_with_Context $
441 \_c -> lam op
442
443 -- | Parse a binary operator.
444 op2_from
445 :: forall root ty lit ex ast hs ret.
446 ( ty ~ Type_Root_of_Expr ex
447 , root ~ Root_of_Expr ex
448 , Type0_Eq ty
449 , Expr_From ast root
450 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
451 (Error_of_Expr ast root)
452 , Root_of_Expr root ~ root
453 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
454 -> ty lit -> ast -> ast
455 -> ExprFrom ast ex hs ret
456 op2_from op ty_lit ast_x ast_y ex ast ctx k =
457 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
458 expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
459 check_type0_eq ex ast ty_lit ty_x $ \Refl ->
460 check_type0_eq ex ast ty_lit ty_y $ \Refl ->
461 k ty_x $ Forall_Repr_with_Context $
462 \c -> x c `op` y c
463
464 -- | Parse a binary operator, partially applied.
465 op2_from1
466 :: forall root ty lit ex ast hs ret.
467 ( ty ~ Type_Root_of_Expr ex
468 , root ~ Root_of_Expr ex
469 , Type0_Eq ty
470 , Type0_Lift Type_Fun (Type_of_Expr root)
471 , Expr_From ast root
472 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
473 (Error_of_Expr ast root)
474 , Root_of_Expr root ~ root
475 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
476 -> ty lit -> ast
477 -> ExprFrom ast ex hs ret
478 op2_from1 op ty_lit ast_x ex ast ctx k =
479 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
480 check_type0_eq ex ast ty_lit ty_x $ \Refl ->
481 k (type_fun ty_x ty_x) $ Forall_Repr_with_Context $
482 \c -> lam $ \y -> x c `op` y
483
484 -- | Parse a binary operator, partially applied.
485 op2_from0
486 :: forall root ty lit ex ast hs ret.
487 ( ty ~ Type_Root_of_Expr ex
488 , root ~ Root_of_Expr ex
489 , Type0_Eq ty
490 , Type0_Lift Type_Fun (Type_of_Expr root)
491 , Expr_From ast root
492 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
493 (Error_of_Expr ast root)
494 , Root_of_Expr root ~ root
495 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
496 -> ty lit
497 -> ExprFrom ast ex hs ret
498 op2_from0 op ty_lit _ex _ast _ctx k =
499 k (type_fun ty_lit $ type_fun ty_lit ty_lit) $ Forall_Repr_with_Context $
500 \_c -> lam $ \x -> lam $ \y -> x `op` y