author | wenzelm |
Fri, 23 Sep 2011 14:13:15 +0200 | |
changeset 45057 | 86c9b73158a8 |
parent 44433 | 9fbee4aab115 |
child 45389 | bc0d50f8ae19 |
permissions | -rw-r--r-- |
42284 | 1 |
(* Title: Pure/Syntax/syntax_trans.ML |
548 | 2 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
3 |
||
4 |
Syntax translation functions. |
|
5 |
*) |
|
6 |
||
42284 | 7 |
signature BASIC_SYNTAX_TRANS = |
8 |
sig |
|
9 |
val eta_contract: bool Config.T |
|
10 |
end |
|
11 |
||
12 |
signature SYNTAX_TRANS = |
|
2698 | 13 |
sig |
42284 | 14 |
include BASIC_SYNTAX_TRANS |
45057
86c9b73158a8
default print mode for Isabelle/Scala, not just Isabelle/jEdit;
wenzelm
parents:
44433
diff
changeset
|
15 |
val bracketsN: string |
86c9b73158a8
default print mode for Isabelle/Scala, not just Isabelle/jEdit;
wenzelm
parents:
44433
diff
changeset
|
16 |
val no_bracketsN: string |
42284 | 17 |
val no_brackets: unit -> bool |
45057
86c9b73158a8
default print mode for Isabelle/Scala, not just Isabelle/jEdit;
wenzelm
parents:
44433
diff
changeset
|
18 |
val type_bracketsN: string |
86c9b73158a8
default print mode for Isabelle/Scala, not just Isabelle/jEdit;
wenzelm
parents:
44433
diff
changeset
|
19 |
val no_type_bracketsN: string |
42284 | 20 |
val no_type_brackets: unit -> bool |
21 |
val abs_tr: term list -> term |
|
22 |
val mk_binder_tr: string * string -> string * (term list -> term) |
|
23 |
val antiquote_tr: string -> term -> term |
|
24 |
val quote_tr: string -> term -> term |
|
25 |
val quote_antiquote_tr: string -> string -> string -> string * (term list -> term) |
|
26 |
val non_typed_tr': (term list -> term) -> typ -> term list -> term |
|
27 |
val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term |
|
28 |
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
|
29 |
val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
|
30 |
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
|
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
37216
diff
changeset
|
31 |
val eta_contract_default: bool Unsynchronized.ref |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39128
diff
changeset
|
32 |
val eta_contract_raw: Config.raw |
42284 | 33 |
val mark_bound: string -> term |
34 |
val mark_boundT: string * typ -> term |
|
35 |
val bound_vars: (string * typ) list -> term -> term |
|
36 |
val abs_tr': Proof.context -> term -> term |
|
13762 | 37 |
val atomic_abs_tr': string * typ * term -> term * term |
42086
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset
|
38 |
val const_abs_tr': term -> term |
42085 | 39 |
val mk_binder_tr': string * string -> string * (term list -> term) |
32120
53a21a5e6889
attempt for more concise setup of non-etacontracting binders
haftmann
parents:
31542
diff
changeset
|
40 |
val preserve_binder_abs_tr': string -> string -> string * (term list -> term) |
53a21a5e6889
attempt for more concise setup of non-etacontracting binders
haftmann
parents:
31542
diff
changeset
|
41 |
val preserve_binder_abs2_tr': string -> string -> string * (term list -> term) |
42284 | 42 |
val prop_tr': term -> term |
43 |
val variant_abs: string * typ * term -> string * term |
|
44 |
val variant_abs': string * typ * term -> string * term |
|
548 | 45 |
val dependent_tr': string * string -> term list -> term |
8577 | 46 |
val antiquote_tr': string -> term -> term |
47 |
val quote_tr': string -> term -> term |
|
5084 | 48 |
val quote_antiquote_tr': string -> string -> string -> string * (term list -> term) |
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
49 |
val update_name_tr': term -> term |
1511 | 50 |
val pure_trfuns: |
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
51 |
(string * (Ast.ast list -> Ast.ast)) list * |
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
52 |
(string * (term list -> term)) list * |
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
53 |
(string * (term list -> term)) list * |
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
54 |
(string * (Ast.ast list -> Ast.ast)) list |
14697 | 55 |
val struct_trfuns: string list -> |
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
56 |
(string * (Ast.ast list -> Ast.ast)) list * |
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
57 |
(string * (term list -> term)) list * |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
58 |
(string * (typ -> term list -> term)) list * |
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
59 |
(string * (Ast.ast list -> Ast.ast)) list |
2698 | 60 |
end; |
548 | 61 |
|
42284 | 62 |
structure Syntax_Trans: SYNTAX_TRANS = |
548 | 63 |
struct |
2698 | 64 |
|
42476 | 65 |
structure Syntax = Lexicon.Syntax; |
66 |
||
67 |
||
42262 | 68 |
(* print mode *) |
69 |
||
70 |
val bracketsN = "brackets"; |
|
71 |
val no_bracketsN = "no_brackets"; |
|
72 |
||
73 |
fun no_brackets () = |
|
74 |
find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) |
|
75 |
(print_mode_value ()) = SOME no_bracketsN; |
|
76 |
||
77 |
val type_bracketsN = "type_brackets"; |
|
78 |
val no_type_bracketsN = "no_type_brackets"; |
|
79 |
||
80 |
fun no_type_brackets () = |
|
81 |
find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) |
|
82 |
(print_mode_value ()) <> SOME type_bracketsN; |
|
83 |
||
84 |
||
2698 | 85 |
|
548 | 86 |
(** parse (ast) translations **) |
87 |
||
42057
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42055
diff
changeset
|
88 |
(* strip_positions *) |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42055
diff
changeset
|
89 |
|
42264 | 90 |
fun strip_positions_ast_tr [ast] = Ast.strip_positions ast |
42057
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42055
diff
changeset
|
91 |
| strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts); |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42055
diff
changeset
|
92 |
|
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42055
diff
changeset
|
93 |
|
11491 | 94 |
(* constify *) |
95 |
||
96 |
fun constify_ast_tr [Ast.Variable c] = Ast.Constant c |
|
97 |
| constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts); |
|
98 |
||
99 |
||
42262 | 100 |
(* type syntax *) |
101 |
||
102 |
fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] |
|
103 |
| tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); |
|
104 |
||
105 |
fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) |
|
106 |
| tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); |
|
107 |
||
108 |
fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) |
|
109 |
| bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); |
|
110 |
||
111 |
||
548 | 112 |
(* application *) |
113 |
||
5690 | 114 |
fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args) |
115 |
| appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts); |
|
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
639
diff
changeset
|
116 |
|
5690 | 117 |
fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args) |
118 |
| applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts); |
|
548 | 119 |
|
120 |
||
121 |
(* abstraction *) |
|
122 |
||
42278 | 123 |
fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty] |
124 |
| idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts); |
|
548 | 125 |
|
42278 | 126 |
fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty] |
127 |
| idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts); |
|
128 |
||
129 |
fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body) |
|
130 |
| lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts); |
|
548 | 131 |
|
44241 | 132 |
fun absfree_proper (x, T) t = |
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42045
diff
changeset
|
133 |
if can Name.dest_internal x |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42045
diff
changeset
|
134 |
then error ("Illegal internal variable in abstraction: " ^ quote x) |
44241 | 135 |
else absfree (x, T) t; |
21773 | 136 |
|
44241 | 137 |
fun abs_tr [Free x, t] = absfree_proper x t |
138 |
| abs_tr [Const ("_idtdummy", T), t] = absdummy T t |
|
42284 | 139 |
| abs_tr [Const ("_constrain", _) $ x $ tT, t] = |
42476 | 140 |
Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT |
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42045
diff
changeset
|
141 |
| abs_tr ts = raise TERM ("abs_tr", ts); |
548 | 142 |
|
143 |
||
144 |
(* binder *) |
|
145 |
||
21535 | 146 |
fun mk_binder_tr (syn, name) = |
548 | 147 |
let |
42055 | 148 |
fun err ts = raise TERM ("binder_tr: " ^ syn, ts) |
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42045
diff
changeset
|
149 |
fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]] |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42045
diff
changeset
|
150 |
| binder_tr [x, t] = |
42055 | 151 |
let val abs = abs_tr [x, t] handle TERM _ => err [x, t] |
42476 | 152 |
in Syntax.const name $ abs end |
42055 | 153 |
| binder_tr ts = err ts; |
21535 | 154 |
in (syn, binder_tr) end; |
548 | 155 |
|
156 |
||
28628 | 157 |
(* type propositions *) |
158 |
||
35255 | 159 |
fun mk_type ty = |
42476 | 160 |
Syntax.const "_constrain" $ |
161 |
Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty); |
|
28628 | 162 |
|
42278 | 163 |
fun ofclass_tr [ty, cls] = cls $ mk_type ty |
164 |
| ofclass_tr ts = raise TERM ("ofclass_tr", ts); |
|
28628 | 165 |
|
42476 | 166 |
fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty |
42278 | 167 |
| sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts); |
28628 | 168 |
|
169 |
||
548 | 170 |
(* meta propositions *) |
171 |
||
42476 | 172 |
fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop" |
42278 | 173 |
| aprop_tr ts = raise TERM ("aprop_tr", ts); |
548 | 174 |
|
175 |
||
176 |
(* meta implication *) |
|
177 |
||
42278 | 178 |
fun bigimpl_ast_tr (asts as [asms, concl]) = |
16612
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
179 |
let val prems = |
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
180 |
(case Ast.unfold_ast_p "_asms" asms of |
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
181 |
(asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm'] |
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
182 |
| _ => raise Ast.AST ("bigimpl_ast_tr", asts)) |
35255 | 183 |
in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end |
42278 | 184 |
| bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts); |
15421
fcf747c0b6b8
Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
schirmer
parents:
14981
diff
changeset
|
185 |
|
548 | 186 |
|
23824
8ad7131dbfcf
moved print_translations from Pure.thy to Syntax/syn_trans.ML;
wenzelm
parents:
21773
diff
changeset
|
187 |
(* type/term reflection *) |
4148 | 188 |
|
42278 | 189 |
fun type_tr [ty] = mk_type ty |
190 |
| type_tr ts = raise TERM ("type_tr", ts); |
|
4148 | 191 |
|
548 | 192 |
|
6761 | 193 |
(* dddot *) |
194 |
||
42476 | 195 |
fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts); |
6761 | 196 |
|
197 |
||
5084 | 198 |
(* quote / antiquote *) |
199 |
||
8577 | 200 |
fun antiquote_tr name = |
201 |
let |
|
202 |
fun tr i ((t as Const (c, _)) $ u) = |
|
203 |
if c = name then tr i u $ Bound i |
|
204 |
else tr i t $ tr i u |
|
205 |
| tr i (t $ u) = tr i t $ tr i u |
|
206 |
| tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t) |
|
207 |
| tr _ a = a; |
|
208 |
in tr 0 end; |
|
209 |
||
210 |
fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t)); |
|
211 |
||
5084 | 212 |
fun quote_antiquote_tr quoteN antiquoteN name = |
213 |
let |
|
42476 | 214 |
fun tr [t] = Syntax.const name $ quote_tr antiquoteN t |
8577 | 215 |
| tr ts = raise TERM ("quote_tr", ts); |
216 |
in (quoteN, tr) end; |
|
5084 | 217 |
|
218 |
||
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
219 |
(* corresponding updates *) |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
220 |
|
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
221 |
fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts) |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
222 |
| update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts) |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
223 |
| update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = |
42264 | 224 |
if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts) |
42053
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42048
diff
changeset
|
225 |
else |
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42048
diff
changeset
|
226 |
list_comb (c $ update_name_tr [t] $ |
42080
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
227 |
(Lexicon.fun_type $ |
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
228 |
(Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts) |
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
229 |
| update_name_tr ts = raise TERM ("update_name_tr", ts); |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
230 |
|
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
231 |
|
14697 | 232 |
(* indexed syntax *) |
233 |
||
42278 | 234 |
fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast |
235 |
| struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts; |
|
14697 | 236 |
|
237 |
fun index_ast_tr ast = |
|
238 |
Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]]; |
|
239 |
||
42278 | 240 |
fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault") |
241 |
| indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts); |
|
242 |
||
243 |
fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast]) |
|
244 |
| indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts); |
|
14697 | 245 |
|
42278 | 246 |
fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"] |
247 |
| indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts); |
|
12122 | 248 |
|
42278 | 249 |
fun index_tr [t] = t |
250 |
| index_tr ts = raise TERM ("index_tr", ts); |
|
14697 | 251 |
|
252 |
||
253 |
(* implicit structures *) |
|
254 |
||
255 |
fun the_struct structs i = |
|
30146 | 256 |
if 1 <= i andalso i <= length structs then nth structs (i - 1) |
31542
3371a3c19bb1
reraise exceptions to preserve position information;
wenzelm
parents:
30146
diff
changeset
|
257 |
else error ("Illegal reference to implicit structure #" ^ string_of_int i); |
14697 | 258 |
|
44433
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
259 |
fun legacy_struct structs i = |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
260 |
let |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
261 |
val x = the_struct structs i; |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
262 |
val _ = |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
263 |
legacy_feature |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
264 |
("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^ |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
265 |
Position.str_of (Position.thread_data ()) ^ |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
266 |
" -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^ |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
267 |
(if i = 1 then " (may be omitted)" else "")) |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
268 |
in x end; |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
269 |
|
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
270 |
fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1) |
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
271 |
| struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1) |
42278 | 272 |
| struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] = |
44380
1b1afb1380ee
old-style numbered structure index is legacy feature (hardly ever used now);
wenzelm
parents:
44241
diff
changeset
|
273 |
(case Lexicon.read_nat s of |
44433
9fbee4aab115
special treatment of structure index 1 in Pure, including legacy warning;
wenzelm
parents:
44381
diff
changeset
|
274 |
SOME i => Syntax.free (legacy_struct structs i) |
44380
1b1afb1380ee
old-style numbered structure index is legacy feature (hardly ever used now);
wenzelm
parents:
44241
diff
changeset
|
275 |
| NONE => raise TERM ("struct_tr", [t])) |
42278 | 276 |
| struct_tr _ ts = raise TERM ("struct_tr", ts); |
12122 | 277 |
|
278 |
||
5084 | 279 |
|
548 | 280 |
(** print (ast) translations **) |
281 |
||
14647 | 282 |
(* types *) |
283 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
284 |
fun non_typed_tr' f _ ts = f ts; |
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
285 |
fun non_typed_tr'' f x _ ts = f x ts; |
14647 | 286 |
|
287 |
||
42262 | 288 |
(* type syntax *) |
289 |
||
290 |
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) |
|
291 |
| tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] |
|
292 |
| tappl_ast_tr' (f, ty :: tys) = |
|
293 |
Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; |
|
294 |
||
295 |
fun fun_ast_tr' asts = |
|
296 |
if no_brackets () orelse no_type_brackets () then raise Match |
|
297 |
else |
|
298 |
(case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of |
|
299 |
(dom as _ :: _ :: _, cod) |
|
300 |
=> Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod] |
|
301 |
| _ => raise Match); |
|
302 |
||
303 |
||
548 | 304 |
(* application *) |
305 |
||
5690 | 306 |
fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) |
307 |
| appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args]; |
|
548 | 308 |
|
5690 | 309 |
fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f]) |
310 |
| applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args]; |
|
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
639
diff
changeset
|
311 |
|
548 | 312 |
|
42085 | 313 |
(* partial eta-contraction before printing *) |
314 |
||
315 |
fun eta_abs (Abs (a, T, t)) = |
|
316 |
(case eta_abs t of |
|
317 |
t' as Const ("_aprop", _) $ _ => Abs (a, T, t') |
|
318 |
| t' as f $ u => |
|
319 |
(case eta_abs u of |
|
320 |
Bound 0 => |
|
321 |
if Term.is_dependent f then Abs (a, T, t') |
|
322 |
else incr_boundvars ~1 f |
|
323 |
| _ => Abs (a, T, t')) |
|
324 |
| t' => Abs (a, T, t')) |
|
325 |
| eta_abs t = t; |
|
326 |
||
327 |
val eta_contract_default = Unsynchronized.ref true; |
|
328 |
val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default)); |
|
329 |
val eta_contract = Config.bool eta_contract_raw; |
|
330 |
||
331 |
fun eta_contr ctxt tm = |
|
332 |
if Config.get ctxt eta_contract then eta_abs tm else tm; |
|
333 |
||
334 |
||
548 | 335 |
(* abstraction *) |
336 |
||
19311 | 337 |
fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T); |
2698 | 338 |
fun mark_bound x = mark_boundT (x, dummyT); |
339 |
||
18958 | 340 |
fun bound_vars vars body = |
341 |
subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body); |
|
342 |
||
548 | 343 |
fun strip_abss vars_of body_of tm = |
344 |
let |
|
345 |
val vars = vars_of tm; |
|
346 |
val body = body_of tm; |
|
29276 | 347 |
val rev_new_vars = Term.rename_wrt_term body vars; |
21750 | 348 |
fun subst (x, T) b = |
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
42080
diff
changeset
|
349 |
if can Name.dest_internal x andalso not (Term.is_dependent b) |
21750 | 350 |
then (Const ("_idtdummy", T), incr_boundvars ~1 b) |
351 |
else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b)); |
|
352 |
val (rev_vars', body') = fold_map subst rev_new_vars body; |
|
353 |
in (rev rev_vars', body') end; |
|
548 | 354 |
|
3928
787d2659ce4a
no longer tries bogus eta-contract involving aprops;
wenzelm
parents:
3777
diff
changeset
|
355 |
|
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
37216
diff
changeset
|
356 |
fun abs_tr' ctxt tm = |
42476 | 357 |
uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t)) |
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
37216
diff
changeset
|
358 |
(strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); |
548 | 359 |
|
14697 | 360 |
fun atomic_abs_tr' (x, T, t) = |
29276 | 361 |
let val [xT] = Term.rename_wrt_term t [(x, T)] |
14697 | 362 |
in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end; |
13762 | 363 |
|
42085 | 364 |
fun abs_ast_tr' asts = |
5690 | 365 |
(case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of |
366 |
([], _) => raise Ast.AST ("abs_ast_tr'", asts) |
|
367 |
| (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]); |
|
548 | 368 |
|
42086
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset
|
369 |
fun const_abs_tr' t = |
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset
|
370 |
(case eta_abs t of |
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset
|
371 |
Abs (_, _, t') => |
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset
|
372 |
if Term.is_dependent t' then raise Match |
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset
|
373 |
else incr_boundvars ~1 t' |
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset
|
374 |
| _ => raise Match); |
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset
|
375 |
|
32120
53a21a5e6889
attempt for more concise setup of non-etacontracting binders
haftmann
parents:
31542
diff
changeset
|
376 |
|
42085 | 377 |
(* binders *) |
548 | 378 |
|
21535 | 379 |
fun mk_binder_tr' (name, syn) = |
548 | 380 |
let |
381 |
fun mk_idts [] = raise Match (*abort translation*) |
|
382 |
| mk_idts [idt] = idt |
|
42476 | 383 |
| mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts; |
548 | 384 |
|
385 |
fun tr' t = |
|
386 |
let |
|
387 |
val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; |
|
42476 | 388 |
in Syntax.const syn $ mk_idts xs $ bd end; |
548 | 389 |
|
42476 | 390 |
fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts) |
21535 | 391 |
| binder_tr' [] = raise Match; |
392 |
in (name, binder_tr') end; |
|
548 | 393 |
|
42085 | 394 |
fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts => |
395 |
let val (x, t) = atomic_abs_tr' abs |
|
42476 | 396 |
in list_comb (Syntax.const syn $ x $ t, ts) end); |
42085 | 397 |
|
398 |
fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts => |
|
399 |
let val (x, t) = atomic_abs_tr' abs |
|
42476 | 400 |
in list_comb (Syntax.const syn $ x $ A $ t, ts) end); |
42085 | 401 |
|
548 | 402 |
|
3691
f0396ac63e12
tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts
wenzelm
parents:
2698
diff
changeset
|
403 |
(* idtyp constraints *) |
548 | 404 |
|
42045 | 405 |
fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] = |
406 |
Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs] |
|
3691
f0396ac63e12
tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts
wenzelm
parents:
2698
diff
changeset
|
407 |
| idtyp_ast_tr' _ _ = raise Match; |
548 | 408 |
|
409 |
||
410 |
(* meta propositions *) |
|
411 |
||
4148 | 412 |
fun prop_tr' tm = |
548 | 413 |
let |
42476 | 414 |
fun aprop t = Syntax.const "_aprop" $ t; |
548 | 415 |
|
2698 | 416 |
fun is_prop Ts t = |
417 |
fastype_of1 (Ts, t) = propT handle TERM _ => false; |
|
548 | 418 |
|
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
419 |
fun is_term (Const ("Pure.term", _) $ _) = true |
19848 | 420 |
| is_term _ = false; |
421 |
||
548 | 422 |
fun tr' _ (t as Const _) = t |
18478
29a5070b517c
prop_tr': proper handling of aprop marked as bound;
wenzelm
parents:
18342
diff
changeset
|
423 |
| tr' Ts (t as Const ("_bound", _) $ u) = |
29a5070b517c
prop_tr': proper handling of aprop marked as bound;
wenzelm
parents:
18342
diff
changeset
|
424 |
if is_prop Ts u then aprop t else t |
2698 | 425 |
| tr' _ (t as Free (x, T)) = |
42476 | 426 |
if T = propT then aprop (Syntax.free x) else t |
2698 | 427 |
| tr' _ (t as Var (xi, T)) = |
42476 | 428 |
if T = propT then aprop (Syntax.var xi) else t |
2698 | 429 |
| tr' Ts (t as Bound _) = |
430 |
if is_prop Ts t then aprop t else t |
|
431 |
| tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t) |
|
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset
|
432 |
| tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = |
28628 | 433 |
if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1 |
2698 | 434 |
else tr' Ts t1 $ tr' Ts t2 |
435 |
| tr' Ts (t as t1 $ t2) = |
|
5690 | 436 |
(if is_Const (Term.head_of t) orelse not (is_prop Ts t) |
2698 | 437 |
then I else aprop) (tr' Ts t1 $ tr' Ts t2); |
16612
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
438 |
in tr' [] tm end; |
548 | 439 |
|
2698 | 440 |
|
548 | 441 |
(* meta implication *) |
442 |
||
42278 | 443 |
fun impl_ast_tr' asts = |
42262 | 444 |
if no_brackets () then raise Match |
10572 | 445 |
else |
35255 | 446 |
(case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of |
16612
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
447 |
(prems as _ :: _ :: _, concl) => |
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
448 |
let |
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
449 |
val (asms, asm) = split_last prems; |
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
450 |
val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]); |
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset
|
451 |
in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end |
15421
fcf747c0b6b8
Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
schirmer
parents:
14981
diff
changeset
|
452 |
| _ => raise Match); |
fcf747c0b6b8
Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
schirmer
parents:
14981
diff
changeset
|
453 |
|
548 | 454 |
|
455 |
(* dependent / nondependent quantifiers *) |
|
456 |
||
20202 | 457 |
fun var_abs mark (x, T, b) = |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
42476
diff
changeset
|
458 |
let val (x', _) = Name.variant x (Term.declare_term_names b Name.context) |
20202 | 459 |
in (x', subst_bound (mark (x', T), b)) end; |
460 |
||
461 |
val variant_abs = var_abs Free; |
|
462 |
val variant_abs' = var_abs mark_boundT; |
|
2698 | 463 |
|
548 | 464 |
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = |
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
42080
diff
changeset
|
465 |
if Term.is_dependent B then |
2698 | 466 |
let val (x', B') = variant_abs' (x, dummyT, B); |
42476 | 467 |
in Term.list_comb (Syntax.const q $ mark_boundT (x', T) $ A $ B', ts) end |
468 |
else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts) |
|
548 | 469 |
| dependent_tr' _ _ = raise Match; |
470 |
||
471 |
||
5084 | 472 |
(* quote / antiquote *) |
473 |
||
8577 | 474 |
fun antiquote_tr' name = |
475 |
let |
|
476 |
fun tr' i (t $ u) = |
|
42476 | 477 |
if u aconv Bound i then Syntax.const name $ tr' i t |
42084
532b3a76103f
dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
wenzelm
parents:
42083
diff
changeset
|
478 |
else tr' i t $ tr' i u |
8577 | 479 |
| tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t) |
18139 | 480 |
| tr' i a = if a aconv Bound i then raise Match else a; |
8577 | 481 |
in tr' 0 end; |
482 |
||
483 |
fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t) |
|
484 |
| quote_tr' _ _ = raise Match; |
|
485 |
||
5084 | 486 |
fun quote_antiquote_tr' quoteN antiquoteN name = |
487 |
let |
|
42476 | 488 |
fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts) |
8577 | 489 |
| tr' _ = raise Match; |
490 |
in (name, tr') end; |
|
5084 | 491 |
|
492 |
||
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
493 |
(* corresponding updates *) |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
494 |
|
42080
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
495 |
local |
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
496 |
|
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
497 |
fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T |
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
498 |
| upd_type _ = dummyT; |
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
499 |
|
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
500 |
fun upd_tr' (x_upd, T) = |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
501 |
(case try (unsuffix "_update") x_upd of |
42080
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
502 |
SOME x => (x, upd_type T) |
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
503 |
| NONE => raise Match); |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
504 |
|
42080
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
505 |
in |
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
506 |
|
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
507 |
fun update_name_tr' (Free x) = Free (upd_tr' x) |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
508 |
| update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x) |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
509 |
| update_name_tr' (Const x) = Const (upd_tr' x) |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
510 |
| update_name_tr' _ = raise Match; |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
511 |
|
42080
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
512 |
end; |
58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset
|
513 |
|
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
514 |
|
14697 | 515 |
(* indexed syntax *) |
548 | 516 |
|
42278 | 517 |
fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast |
14697 | 518 |
| index_ast_tr' _ = raise Match; |
519 |
||
520 |
||
521 |
(* implicit structures *) |
|
522 |
||
523 |
fun the_struct' structs s = |
|
524 |
[(case Lexicon.read_nat s of |
|
18678 | 525 |
SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match) |
15531 | 526 |
| NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free"); |
14697 | 527 |
|
42278 | 528 |
fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1" |
529 |
| struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] = |
|
14697 | 530 |
the_struct' structs s |
531 |
| struct_ast_tr' _ _ = raise Match; |
|
532 |
||
533 |
||
534 |
||
535 |
(** Pure translations **) |
|
548 | 536 |
|
537 |
val pure_trfuns = |
|
42057
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42055
diff
changeset
|
538 |
([("_strip_positions", strip_positions_ast_tr), |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42055
diff
changeset
|
539 |
("_constify", constify_ast_tr), |
42262 | 540 |
("_tapp", tapp_ast_tr), |
541 |
("_tappl", tappl_ast_tr), |
|
542 |
("_bracket", bracket_ast_tr), |
|
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
543 |
("_appl", appl_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
544 |
("_applC", applC_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
545 |
("_lambda", lambda_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
546 |
("_idtyp", idtyp_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
547 |
("_idtypdummy", idtypdummy_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
548 |
("_bigimpl", bigimpl_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
549 |
("_indexdefault", indexdefault_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
550 |
("_indexnum", indexnum_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
551 |
("_indexvar", indexvar_ast_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
552 |
("_struct", struct_ast_tr)], |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
553 |
[("_abs", abs_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
554 |
("_aprop", aprop_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
555 |
("_ofclass", ofclass_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
556 |
("_sort_constraint", sort_constraint_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
557 |
("_TYPE", type_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
558 |
("_DDDOT", dddot_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
559 |
("_update_name", update_name_tr), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
560 |
("_index", index_tr)], |
35198 | 561 |
([]: (string * (term list -> term)) list), |
42262 | 562 |
[("\\<^type>fun", fun_ast_tr'), |
563 |
("_abs", abs_ast_tr'), |
|
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
564 |
("_idts", idtyp_ast_tr' "_idts"), |
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
565 |
("_pttrns", idtyp_ast_tr' "_pttrns"), |
35255 | 566 |
("\\<^const>==>", impl_ast_tr'), |
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset
|
567 |
("_index", index_ast_tr')]); |
548 | 568 |
|
14697 | 569 |
fun struct_trfuns structs = |
570 |
([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]); |
|
571 |
||
548 | 572 |
end; |
42284 | 573 |
|
574 |
structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans; |
|
575 |
open Basic_Syntax_Trans; |