18
|
1 |
(* Title: Pure/Syntax/sextension.ML
|
0
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
|
|
4 |
|
18
|
5 |
Syntax extensions (external interface): mixfix declarations, syntax rules,
|
|
6 |
infixes, binders and the Pure syntax.
|
0
|
7 |
|
|
8 |
TODO:
|
18
|
9 |
move ast_to_term (?)
|
0
|
10 |
*)
|
|
11 |
|
|
12 |
infix |-> <-| <->;
|
|
13 |
|
|
14 |
signature SEXTENSION0 =
|
|
15 |
sig
|
|
16 |
structure Ast: AST
|
|
17 |
local open Ast in
|
|
18 |
datatype mixfix =
|
|
19 |
Mixfix of string * string * string * int list * int |
|
|
20 |
Delimfix of string * string * string |
|
|
21 |
Infixl of string * string * int |
|
|
22 |
Infixr of string * string * int |
|
|
23 |
Binder of string * string * string * int * int |
|
|
24 |
TInfixl of string * string * int |
|
|
25 |
TInfixr of string * string * int
|
|
26 |
datatype xrule =
|
|
27 |
op |-> of (string * string) * (string * string) |
|
|
28 |
op <-| of (string * string) * (string * string) |
|
|
29 |
op <-> of (string * string) * (string * string)
|
|
30 |
datatype sext =
|
|
31 |
Sext of {
|
|
32 |
mixfix: mixfix list,
|
|
33 |
parse_translation: (string * (term list -> term)) list,
|
|
34 |
print_translation: (string * (term list -> term)) list} |
|
|
35 |
NewSext of {
|
|
36 |
mixfix: mixfix list,
|
|
37 |
xrules: xrule list,
|
|
38 |
parse_ast_translation: (string * (ast list -> ast)) list,
|
|
39 |
parse_translation: (string * (term list -> term)) list,
|
|
40 |
print_translation: (string * (term list -> term)) list,
|
|
41 |
print_ast_translation: (string * (ast list -> ast)) list}
|
|
42 |
val eta_contract: bool ref
|
|
43 |
val mk_binder_tr: string * string -> string * (term list -> term)
|
|
44 |
val mk_binder_tr': string * string -> string * (term list -> term)
|
|
45 |
val dependent_tr': string * string -> term list -> term
|
|
46 |
val max_pri: int
|
|
47 |
end
|
|
48 |
end;
|
|
49 |
|
|
50 |
signature SEXTENSION1 =
|
|
51 |
sig
|
|
52 |
include SEXTENSION0
|
|
53 |
val empty_sext: sext
|
|
54 |
val simple_sext: mixfix list -> sext
|
|
55 |
val constants: sext -> (string list * string) list
|
|
56 |
val pure_sext: sext
|
|
57 |
val syntax_types: string list
|
|
58 |
val constrainAbsC: string
|
|
59 |
end;
|
|
60 |
|
|
61 |
signature SEXTENSION =
|
|
62 |
sig
|
|
63 |
include SEXTENSION1
|
|
64 |
structure Extension: EXTENSION
|
|
65 |
sharing Extension.XGram.Ast = Ast
|
|
66 |
local open Extension Ast in
|
|
67 |
val xrules_of: sext -> xrule list
|
|
68 |
val abs_tr': term -> term
|
|
69 |
val appl_ast_tr': ast * ast list -> ast
|
|
70 |
val ext_of_sext: string list -> string list -> (string -> typ) -> sext -> ext
|
|
71 |
val ast_to_term: (string -> (term list -> term) option) -> ast -> term
|
|
72 |
val constrainIdtC: string
|
|
73 |
val apropC: string
|
|
74 |
end
|
|
75 |
end;
|
|
76 |
|
18
|
77 |
functor SExtensionFun(structure TypeExt: TYPE_EXT and Lexicon: LEXICON): SEXTENSION =
|
0
|
78 |
struct
|
|
79 |
|
|
80 |
structure Extension = TypeExt.Extension;
|
|
81 |
structure Ast = Extension.XGram.Ast;
|
18
|
82 |
open Lexicon Extension Extension.XGram Ast;
|
0
|
83 |
|
|
84 |
|
|
85 |
(** datatype sext **)
|
|
86 |
|
|
87 |
datatype mixfix =
|
|
88 |
Mixfix of string * string * string * int list * int |
|
|
89 |
Delimfix of string * string * string |
|
|
90 |
Infixl of string * string * int |
|
|
91 |
Infixr of string * string * int |
|
|
92 |
Binder of string * string * string * int * int |
|
|
93 |
TInfixl of string * string * int |
|
|
94 |
TInfixr of string * string * int;
|
|
95 |
|
|
96 |
datatype xrule =
|
|
97 |
op |-> of (string * string) * (string * string) |
|
|
98 |
op <-| of (string * string) * (string * string) |
|
|
99 |
op <-> of (string * string) * (string * string);
|
|
100 |
|
|
101 |
datatype sext =
|
|
102 |
Sext of {
|
|
103 |
mixfix: mixfix list,
|
|
104 |
parse_translation: (string * (term list -> term)) list,
|
|
105 |
print_translation: (string * (term list -> term)) list} |
|
|
106 |
NewSext of {
|
|
107 |
mixfix: mixfix list,
|
|
108 |
xrules: xrule list,
|
|
109 |
parse_ast_translation: (string * (ast list -> ast)) list,
|
|
110 |
parse_translation: (string * (term list -> term)) list,
|
|
111 |
print_translation: (string * (term list -> term)) list,
|
|
112 |
print_ast_translation: (string * (ast list -> ast)) list};
|
|
113 |
|
|
114 |
|
|
115 |
(* simple_sext *)
|
|
116 |
|
|
117 |
fun simple_sext mixfix =
|
|
118 |
Sext {mixfix = mixfix, parse_translation = [], print_translation = []};
|
|
119 |
|
|
120 |
|
|
121 |
(* empty_sext *)
|
|
122 |
|
|
123 |
val empty_sext = simple_sext [];
|
|
124 |
|
|
125 |
|
|
126 |
(* sext_components *)
|
|
127 |
|
|
128 |
fun sext_components (Sext {mixfix, parse_translation, print_translation}) =
|
|
129 |
{mixfix = mixfix,
|
|
130 |
xrules = [],
|
|
131 |
parse_ast_translation = [],
|
|
132 |
parse_translation = parse_translation,
|
|
133 |
print_translation = print_translation,
|
|
134 |
print_ast_translation = []}
|
|
135 |
| sext_components (NewSext cmps) = cmps;
|
|
136 |
|
|
137 |
|
|
138 |
(* mixfix_of *)
|
|
139 |
|
|
140 |
fun mixfix_of (Sext {mixfix, ...}) = mixfix
|
|
141 |
| mixfix_of (NewSext {mixfix, ...}) = mixfix;
|
|
142 |
|
|
143 |
|
|
144 |
(* xrules_of *)
|
|
145 |
|
|
146 |
fun xrules_of (Sext _) = []
|
|
147 |
| xrules_of (NewSext {xrules, ...}) = xrules;
|
|
148 |
|
|
149 |
|
|
150 |
|
18
|
151 |
(** parse (ast) translations **)
|
0
|
152 |
|
|
153 |
(* application *)
|
|
154 |
|
|
155 |
fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args)
|
|
156 |
| appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts;
|
|
157 |
|
|
158 |
|
|
159 |
(* abstraction *)
|
|
160 |
|
|
161 |
fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty]
|
|
162 |
| idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts;
|
|
163 |
|
|
164 |
fun lambda_ast_tr (*"_lambda"*) [idts, body] =
|
18
|
165 |
fold_ast_p "_abs" (unfold_ast "_idts" idts, body)
|
0
|
166 |
| lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts;
|
|
167 |
|
18
|
168 |
fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body)
|
|
169 |
| abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =
|
0
|
170 |
if c = constrainC then
|
|
171 |
Const ("_constrainAbs", dummyT) $ absfree (x, T, body) $ tT
|
18
|
172 |
else raise_term "abs_tr" ts
|
|
173 |
| abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts;
|
0
|
174 |
|
|
175 |
|
18
|
176 |
(* nondependent abstraction *)
|
|
177 |
|
|
178 |
fun k_tr (*"_K"*) [t] = Abs ("x", dummyT, incr_boundvars 1 t)
|
|
179 |
| k_tr (*"_K"*) ts = raise_term "k_tr" ts;
|
|
180 |
|
|
181 |
|
|
182 |
(* binder *)
|
0
|
183 |
|
|
184 |
fun mk_binder_tr (sy, name) =
|
|
185 |
let
|
|
186 |
val const = Const (name, dummyT);
|
|
187 |
|
|
188 |
fun tr (Free (x, T), t) = const $ absfree (x, T, t)
|
|
189 |
| tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
|
18
|
190 |
| tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) =
|
0
|
191 |
if c = constrainC then
|
|
192 |
const $ (Const ("_constrainAbs", dummyT) $ absfree (x, T, t) $ tT)
|
18
|
193 |
else raise_term "binder_tr" [t1, t]
|
|
194 |
| tr (t1, t2) = raise_term "binder_tr" [t1, t2];
|
0
|
195 |
|
|
196 |
fun binder_tr (*sy*) [idts, body] = tr (idts, body)
|
18
|
197 |
| binder_tr (*sy*) ts = raise_term "binder_tr" ts;
|
0
|
198 |
in
|
|
199 |
(sy, binder_tr)
|
|
200 |
end;
|
|
201 |
|
|
202 |
|
|
203 |
(* atomic props *)
|
|
204 |
|
18
|
205 |
fun aprop_tr (*"_aprop"*) [t] =
|
|
206 |
Const (constrainC, dummyT) $ t $ Free ("prop", dummyT)
|
|
207 |
| aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts;
|
0
|
208 |
|
|
209 |
|
|
210 |
(* meta implication *)
|
|
211 |
|
|
212 |
fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
|
|
213 |
fold_ast_p "==>" (unfold_ast "_asms" asms, concl)
|
|
214 |
| bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
|
|
215 |
|
|
216 |
|
|
217 |
|
18
|
218 |
(** print (ast) translations **)
|
0
|
219 |
|
|
220 |
(* application *)
|
|
221 |
|
|
222 |
fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f]
|
|
223 |
| appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
|
|
224 |
|
|
225 |
|
18
|
226 |
(* abstraction *)
|
0
|
227 |
|
|
228 |
fun strip_abss vars_of body_of tm =
|
|
229 |
let
|
18
|
230 |
fun free (x, _) = Free (x, dummyT);
|
|
231 |
|
0
|
232 |
val vars = vars_of tm;
|
|
233 |
val body = body_of tm;
|
|
234 |
val rev_new_vars = rename_wrt_term body vars;
|
|
235 |
in
|
18
|
236 |
(map Free (rev rev_new_vars), subst_bounds (map free rev_new_vars, body))
|
0
|
237 |
end;
|
|
238 |
|
|
239 |
(*do (partial) eta-contraction before printing*)
|
|
240 |
|
|
241 |
val eta_contract = ref false;
|
|
242 |
|
|
243 |
fun eta_contr tm =
|
|
244 |
let
|
|
245 |
fun eta_abs (Abs (a, T, t)) =
|
|
246 |
(case eta_abs t of
|
18
|
247 |
t' as f $ u =>
|
0
|
248 |
(case eta_abs u of
|
|
249 |
Bound 0 =>
|
|
250 |
if not (0 mem loose_bnos f) then incr_boundvars ~1 f
|
|
251 |
else Abs (a, T, t')
|
|
252 |
| _ => Abs (a, T, t'))
|
|
253 |
| t' => Abs (a, T, t'))
|
|
254 |
| eta_abs t = t;
|
|
255 |
in
|
|
256 |
if ! eta_contract then eta_abs tm else tm
|
|
257 |
end;
|
|
258 |
|
|
259 |
|
|
260 |
fun abs_tr' tm =
|
18
|
261 |
foldr (fn (x, t) => Const ("_abs", dummyT) $ x $ t)
|
0
|
262 |
(strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
|
|
263 |
|
|
264 |
|
18
|
265 |
fun abs_ast_tr' (*"_abs"*) asts =
|
|
266 |
(case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of
|
|
267 |
([], _) => raise_ast "abs_ast_tr'" asts
|
0
|
268 |
| (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]);
|
|
269 |
|
|
270 |
|
18
|
271 |
(* binder *)
|
0
|
272 |
|
|
273 |
fun mk_binder_tr' (name, sy) =
|
|
274 |
let
|
|
275 |
fun mk_idts [] = raise Match (*abort translation*)
|
|
276 |
| mk_idts [idt] = idt
|
|
277 |
| mk_idts (idt :: idts) = Const ("_idts", dummyT) $ idt $ mk_idts idts;
|
|
278 |
|
|
279 |
fun tr' t =
|
|
280 |
let
|
|
281 |
val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
|
|
282 |
in
|
|
283 |
Const (sy, dummyT) $ mk_idts xs $ bd
|
|
284 |
end;
|
|
285 |
|
|
286 |
fun binder_tr' (*name*) (t :: ts) =
|
|
287 |
list_comb (tr' (Const (name, dummyT) $ t), ts)
|
|
288 |
| binder_tr' (*name*) [] = raise Match;
|
|
289 |
in
|
|
290 |
(name, binder_tr')
|
|
291 |
end;
|
|
292 |
|
|
293 |
|
|
294 |
(* idts *)
|
|
295 |
|
|
296 |
fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] =
|
|
297 |
if c = constrainC then
|
|
298 |
Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs]
|
|
299 |
else raise Match
|
|
300 |
| idts_ast_tr' (*"_idts"*) _ = raise Match;
|
|
301 |
|
|
302 |
|
|
303 |
(* meta implication *)
|
|
304 |
|
|
305 |
fun impl_ast_tr' (*"==>"*) asts =
|
|
306 |
(case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of
|
18
|
307 |
(asms as _ :: _ :: _, concl)
|
0
|
308 |
=> Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl]
|
|
309 |
| _ => raise Match);
|
|
310 |
|
|
311 |
|
18
|
312 |
(* dependent / nondependent quantifiers *)
|
0
|
313 |
|
18
|
314 |
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
|
0
|
315 |
if 0 mem (loose_bnos B) then
|
|
316 |
let val (x', B') = variant_abs (x, dummyT, B);
|
18
|
317 |
in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts) end
|
|
318 |
else list_comb (Const (r, dummyT) $ A $ B, ts)
|
0
|
319 |
| dependent_tr' _ _ = raise Match;
|
|
320 |
|
|
321 |
|
|
322 |
|
18
|
323 |
(** ext_of_sext **)
|
0
|
324 |
|
18
|
325 |
fun strip_esc str =
|
0
|
326 |
let
|
18
|
327 |
fun strip ("'" :: c :: cs) = c :: strip cs
|
|
328 |
| strip ["'"] = []
|
|
329 |
| strip (c :: cs) = c :: strip cs
|
|
330 |
| strip [] = [];
|
0
|
331 |
in
|
18
|
332 |
implode (strip (explode str))
|
0
|
333 |
end;
|
|
334 |
|
18
|
335 |
fun infix_name sy = "op " ^ strip_esc sy;
|
0
|
336 |
|
|
337 |
|
|
338 |
fun ext_of_sext roots xconsts read_typ sext =
|
|
339 |
let
|
18
|
340 |
val {mixfix, parse_ast_translation, parse_translation, print_translation,
|
|
341 |
print_ast_translation, ...} = sext_components sext;
|
0
|
342 |
|
18
|
343 |
val tinfixT = [typeT, typeT] ---> typeT;
|
0
|
344 |
|
|
345 |
fun binder (Binder (sy, _, name, _, _)) = Some (sy, name)
|
|
346 |
| binder _ = None;
|
|
347 |
|
|
348 |
fun binder_typ ty =
|
|
349 |
(case read_typ ty of
|
|
350 |
Type ("fun", [Type ("fun", [_, T2]), T3]) =>
|
|
351 |
[Type ("idts", []), T2] ---> T3
|
18
|
352 |
| _ => error ("Illegal binder type " ^ quote ty));
|
0
|
353 |
|
18
|
354 |
fun mk_infix sy T c p1 p2 p3 =
|
|
355 |
[Mfix ("op " ^ sy, T, c, [], max_pri),
|
|
356 |
Mfix ("(_ " ^ sy ^ "/ _)", T, c, [p1, p2], p3)];
|
|
357 |
|
|
358 |
fun mfix_of (Mixfix (sy, ty, c, ps, p)) = [Mfix (sy, read_typ ty, c, ps, p)]
|
0
|
359 |
| mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)]
|
|
360 |
| mfix_of (Infixl (sy, ty, p)) =
|
18
|
361 |
mk_infix sy (read_typ ty) (infix_name sy) p (p + 1) p
|
0
|
362 |
| mfix_of (Infixr (sy, ty, p)) =
|
18
|
363 |
mk_infix sy (read_typ ty) (infix_name sy) (p + 1) p p
|
0
|
364 |
| mfix_of (Binder (sy, ty, _, p, q)) =
|
|
365 |
[Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)]
|
|
366 |
| mfix_of (TInfixl (s, c, p)) =
|
18
|
367 |
[Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p, p + 1], p)]
|
0
|
368 |
| mfix_of (TInfixr (s, c, p)) =
|
18
|
369 |
[Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p + 1, p], p)];
|
0
|
370 |
|
|
371 |
val mfix = flat (map mfix_of mixfix);
|
18
|
372 |
val binders = mapfilter binder mixfix;
|
|
373 |
val bparses = map mk_binder_tr binders;
|
|
374 |
val bprints = map (mk_binder_tr' o (fn (x, y) => (y, x))) binders;
|
0
|
375 |
in
|
|
376 |
Ext {
|
|
377 |
roots = roots, mfix = mfix,
|
18
|
378 |
extra_consts = distinct (filter is_xid xconsts),
|
0
|
379 |
parse_ast_translation = parse_ast_translation,
|
|
380 |
parse_translation = bparses @ parse_translation,
|
|
381 |
print_translation = bprints @ print_translation,
|
|
382 |
print_ast_translation = print_ast_translation}
|
|
383 |
end;
|
|
384 |
|
|
385 |
|
|
386 |
|
18
|
387 |
(** constants **)
|
|
388 |
|
|
389 |
fun constants sext =
|
|
390 |
let
|
|
391 |
fun consts (Delimfix (_, ty, c)) = ([c], ty)
|
|
392 |
| consts (Mixfix (_, ty, c, _, _)) = ([c], ty)
|
|
393 |
| consts (Infixl (c, ty, _)) = ([infix_name c], ty)
|
|
394 |
| consts (Infixr (c, ty, _)) = ([infix_name c], ty)
|
|
395 |
| consts (Binder (_, ty, c, _, _)) = ([c], ty)
|
|
396 |
| consts _ = ([""], ""); (*is filtered out below*)
|
|
397 |
in
|
|
398 |
distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext)))
|
|
399 |
end;
|
|
400 |
|
|
401 |
|
|
402 |
|
0
|
403 |
(** ast_to_term **)
|
|
404 |
|
|
405 |
fun ast_to_term trf ast =
|
|
406 |
let
|
|
407 |
fun trans a args =
|
|
408 |
(case trf a of
|
|
409 |
None => list_comb (Const (a, dummyT), args)
|
18
|
410 |
| Some f => f args handle exn
|
|
411 |
=> (writeln ("Error in parse translation for " ^ quote a); raise exn));
|
0
|
412 |
|
18
|
413 |
fun term_of (Constant a) = trans a []
|
|
414 |
| term_of (Variable x) = scan_var x
|
|
415 |
| term_of (Appl (Constant a :: (asts as _ :: _))) =
|
|
416 |
trans a (map term_of asts)
|
|
417 |
| term_of (Appl (ast :: (asts as _ :: _))) =
|
|
418 |
list_comb (term_of ast, map term_of asts)
|
|
419 |
| term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast];
|
0
|
420 |
in
|
18
|
421 |
term_of ast
|
0
|
422 |
end;
|
|
423 |
|
|
424 |
|
|
425 |
|
|
426 |
(** the Pure syntax **)
|
|
427 |
|
|
428 |
val pure_sext =
|
|
429 |
NewSext {
|
|
430 |
mixfix = [
|
|
431 |
Mixfix ("(3%_./ _)", "[idts, 'a] => ('b => 'a)", "_lambda", [0], 0),
|
|
432 |
Delimfix ("_", "'a => " ^ args, ""),
|
|
433 |
Delimfix ("_,/ _", "['a, " ^ args ^ "] => " ^ args, "_args"),
|
|
434 |
Delimfix ("_", "id => idt", ""),
|
|
435 |
Mixfix ("_::_", "[id, type] => idt", "_idtyp", [0, 0], 0),
|
|
436 |
Delimfix ("'(_')", "idt => idt", ""),
|
|
437 |
Delimfix ("_", "idt => idts", ""),
|
|
438 |
Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0),
|
|
439 |
Delimfix ("_", "id => aprop", ""),
|
|
440 |
Delimfix ("_", "var => aprop", ""),
|
42
|
441 |
Mixfix ("_/(1'(_'))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0),
|
0
|
442 |
Delimfix ("PROP _", "aprop => prop", "_aprop"),
|
|
443 |
Delimfix ("_", "prop => asms", ""),
|
|
444 |
Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"),
|
|
445 |
Mixfix ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1),
|
|
446 |
Mixfix ("(_ ==/ _)", "['a::{}, 'a] => prop", "==", [3, 2], 2),
|
|
447 |
Mixfix ("(_ =?=/ _)", "['a::{}, 'a] => prop", "=?=", [3, 2], 2),
|
|
448 |
Mixfix ("(_ ==>/ _)", "[prop, prop] => prop", "==>", [2, 1], 1),
|
|
449 |
Binder ("!!", "('a::logic => prop) => prop", "all", 0, 0)],
|
|
450 |
xrules = [],
|
|
451 |
parse_ast_translation =
|
|
452 |
[(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
|
18
|
453 |
("_bigimpl", bigimpl_ast_tr)],
|
|
454 |
parse_translation = [("_abs", abs_tr), ("_K", k_tr), ("_aprop", aprop_tr)],
|
0
|
455 |
print_translation = [],
|
18
|
456 |
print_ast_translation = [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'),
|
0
|
457 |
("==>", impl_ast_tr')]};
|
|
458 |
|
18
|
459 |
val syntax_types = [id, var, tfree, tvar, logic, "type", "types", "sort",
|
|
460 |
"classes", args, "idt", "idts", "aprop", "asms"];
|
0
|
461 |
|
|
462 |
val constrainIdtC = "_idtyp";
|
|
463 |
val constrainAbsC = "_constrainAbs";
|
|
464 |
val apropC = "_aprop";
|
|
465 |
|
|
466 |
|
|
467 |
end;
|
|
468 |
|