author  wenzelm 
Tue, 09 Apr 2013 13:24:00 +0200  
changeset 51656  4ce2f7607d3d 
parent 49660  de49d9b4d7bc 
child 52043  286629271d65 
permissions  rwrr 
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 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

33 
val mark_bound_abs: string * typ > term 
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

34 
val mark_bound_body: string * typ > term 
42284  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 nonetacontracting 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 nonetacontracting 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 

46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
45389
diff
changeset

96 
fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] = 
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
45389
diff
changeset

97 
Ast.Appl [c, constify_ast_tr [ast1], ast2] 
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
45389
diff
changeset

98 
 constify_ast_tr [Ast.Variable c] = Ast.Constant c 
11491  99 
 constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts); 
100 

101 

42262  102 
(* type syntax *) 
103 

104 
fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] 

105 
 tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); 

106 

107 
fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) 

108 
 tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); 

109 

110 
fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) 

111 
 bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); 

112 

113 

548  114 
(* application *) 
115 

5690  116 
fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args) 
117 
 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

118 

5690  119 
fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args) 
120 
 applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts); 

548  121 

122 

123 
(* abstraction *) 

124 

42278  125 
fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty] 
126 
 idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts); 

548  127 

42278  128 
fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty] 
129 
 idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts); 

130 

131 
fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body) 

132 
 lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts); 

548  133 

44241  134 
fun absfree_proper (x, T) t = 
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo typeconstraints  still inactive;
wenzelm
parents:
42045
diff
changeset

135 
if can Name.dest_internal x 
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo typeconstraints  still inactive;
wenzelm
parents:
42045
diff
changeset

136 
then error ("Illegal internal variable in abstraction: " ^ quote x) 
44241  137 
else absfree (x, T) t; 
21773  138 

44241  139 
fun abs_tr [Free x, t] = absfree_proper x t 
140 
 abs_tr [Const ("_idtdummy", T), t] = absdummy T t 

42284  141 
 abs_tr [Const ("_constrain", _) $ x $ tT, t] = 
42476  142 
Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT 
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo typeconstraints  still inactive;
wenzelm
parents:
42045
diff
changeset

143 
 abs_tr ts = raise TERM ("abs_tr", ts); 
548  144 

145 

146 
(* binder *) 

147 

21535  148 
fun mk_binder_tr (syn, name) = 
548  149 
let 
42055  150 
fun err ts = raise TERM ("binder_tr: " ^ syn, ts) 
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo typeconstraints  still inactive;
wenzelm
parents:
42045
diff
changeset

151 
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 typeconstraints  still inactive;
wenzelm
parents:
42045
diff
changeset

152 
 binder_tr [x, t] = 
42055  153 
let val abs = abs_tr [x, t] handle TERM _ => err [x, t] 
42476  154 
in Syntax.const name $ abs end 
42055  155 
 binder_tr ts = err ts; 
21535  156 
in (syn, binder_tr) end; 
548  157 

158 

28628  159 
(* type propositions *) 
160 

35255  161 
fun mk_type ty = 
42476  162 
Syntax.const "_constrain" $ 
163 
Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty); 

28628  164 

42278  165 
fun ofclass_tr [ty, cls] = cls $ mk_type ty 
166 
 ofclass_tr ts = raise TERM ("ofclass_tr", ts); 

28628  167 

42476  168 
fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty 
42278  169 
 sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts); 
28628  170 

171 

548  172 
(* meta propositions *) 
173 

42476  174 
fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop" 
42278  175 
 aprop_tr ts = raise TERM ("aprop_tr", ts); 
548  176 

177 

178 
(* meta implication *) 

179 

42278  180 
fun bigimpl_ast_tr (asts as [asms, concl]) = 
16612
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset

181 
let val prems = 
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset

182 
(case Ast.unfold_ast_p "_asms" asms of 
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset

183 
(asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm'] 
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset

184 
 _ => raise Ast.AST ("bigimpl_ast_tr", asts)) 
35255  185 
in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end 
42278  186 
 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

187 

548  188 

23824
8ad7131dbfcf
moved print_translations from Pure.thy to Syntax/syn_trans.ML;
wenzelm
parents:
21773
diff
changeset

189 
(* type/term reflection *) 
4148  190 

42278  191 
fun type_tr [ty] = mk_type ty 
192 
 type_tr ts = raise TERM ("type_tr", ts); 

4148  193 

548  194 

6761  195 
(* dddot *) 
196 

42476  197 
fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts); 
6761  198 

199 

5084  200 
(* quote / antiquote *) 
201 

8577  202 
fun antiquote_tr name = 
203 
let 

204 
fun tr i ((t as Const (c, _)) $ u) = 

205 
if c = name then tr i u $ Bound i 

206 
else tr i t $ tr i u 

207 
 tr i (t $ u) = tr i t $ tr i u 

208 
 tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t) 

209 
 tr _ a = a; 

210 
in tr 0 end; 

211 

212 
fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t)); 

213 

5084  214 
fun quote_antiquote_tr quoteN antiquoteN name = 
215 
let 

42476  216 
fun tr [t] = Syntax.const name $ quote_tr antiquoteN t 
8577  217 
 tr ts = raise TERM ("quote_tr", ts); 
218 
in (quoteN, tr) end; 

5084  219 

220 

35145
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

221 
(* corresponding updates *) 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

222 

f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

223 
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

224 
 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

225 
 update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = 
42264  226 
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

227 
else 
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42048
diff
changeset

228 
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

229 
(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

230 
(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

231 
 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

232 

f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

233 

14697  234 
(* indexed syntax *) 
235 

45389
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

236 
fun indexdefault_ast_tr [] = 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

237 
Ast.Appl [Ast.Constant "_index", 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

238 
Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]] 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

239 
 indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts); 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

240 

bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

241 
fun indexvar_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Variable "some_index"] 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

242 
 indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts); 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

243 

42278  244 
fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast 
245 
 struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts; 

14697  246 

42278  247 
fun index_tr [t] = t 
248 
 index_tr ts = raise TERM ("index_tr", ts); 

14697  249 

45389
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

250 
fun the_struct [] = error "Illegal reference to implicit structure" 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

251 
 the_struct (x :: _) = x; 
14697  252 

51656
4ce2f7607d3d
more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;
wenzelm
parents:
49660
diff
changeset

253 
fun struct_tr structs [Const ("_indexdefault", _)] = 
4ce2f7607d3d
more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;
wenzelm
parents:
49660
diff
changeset

254 
Syntax.const (Lexicon.mark_fixed (the_struct structs)) 
42278  255 
 struct_tr _ ts = raise TERM ("struct_tr", ts); 
12122  256 

257 

5084  258 

548  259 
(** print (ast) translations **) 
260 

14647  261 
(* types *) 
262 

42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

263 
fun non_typed_tr' f _ ts = f ts; 
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

264 
fun non_typed_tr'' f x _ ts = f x ts; 
14647  265 

266 

42262  267 
(* type syntax *) 
268 

269 
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) 

270 
 tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] 

271 
 tappl_ast_tr' (f, ty :: tys) = 

272 
Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; 

273 

274 
fun fun_ast_tr' asts = 

275 
if no_brackets () orelse no_type_brackets () then raise Match 

276 
else 

277 
(case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of 

278 
(dom as _ :: _ :: _, cod) 

279 
=> Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod] 

280 
 _ => raise Match); 

281 

282 

548  283 
(* application *) 
284 

5690  285 
fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) 
286 
 appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args]; 

548  287 

5690  288 
fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f]) 
289 
 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

290 

548  291 

42085  292 
(* partial etacontraction before printing *) 
293 

294 
fun eta_abs (Abs (a, T, t)) = 

295 
(case eta_abs t of 

296 
t' as Const ("_aprop", _) $ _ => Abs (a, T, t') 

297 
 t' as f $ u => 

298 
(case eta_abs u of 

299 
Bound 0 => 

300 
if Term.is_dependent f then Abs (a, T, t') 

301 
else incr_boundvars ~1 f 

302 
 _ => Abs (a, T, t')) 

303 
 t' => Abs (a, T, t')) 

304 
 eta_abs t = t; 

305 

306 
val eta_contract_default = Unsynchronized.ref true; 

307 
val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default)); 

308 
val eta_contract = Config.bool eta_contract_raw; 

309 

310 
fun eta_contr ctxt tm = 

311 
if Config.get ctxt eta_contract then eta_abs tm else tm; 

312 

313 

548  314 
(* abstraction *) 
315 

49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

316 
fun mark_bound_abs (x, T) = Const ("_bound", T > T) $ Free (x, T); 
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

317 
fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T); 
2698  318 

18958  319 
fun bound_vars vars body = 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

320 
subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body); 
18958  321 

548  322 
fun strip_abss vars_of body_of tm = 
323 
let 

324 
val vars = vars_of tm; 

325 
val body = body_of tm; 

29276  326 
val rev_new_vars = Term.rename_wrt_term body vars; 
21750  327 
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

328 
if can Name.dest_internal x andalso not (Term.is_dependent b) 
21750  329 
then (Const ("_idtdummy", T), incr_boundvars ~1 b) 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

330 
else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b)); 
21750  331 
val (rev_vars', body') = fold_map subst rev_new_vars body; 
332 
in (rev rev_vars', body') end; 

548  333 

3928
787d2659ce4a
no longer tries bogus etacontract involving aprops;
wenzelm
parents:
3777
diff
changeset

334 

39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
37216
diff
changeset

335 
fun abs_tr' ctxt tm = 
42476  336 
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

337 
(strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); 
548  338 

14697  339 
fun atomic_abs_tr' (x, T, t) = 
29276  340 
let val [xT] = Term.rename_wrt_term t [(x, T)] 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

341 
in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end; 
13762  342 

42085  343 
fun abs_ast_tr' asts = 
5690  344 
(case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of 
345 
([], _) => raise Ast.AST ("abs_ast_tr'", asts) 

346 
 (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]); 

548  347 

42086
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset

348 
fun const_abs_tr' t = 
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset

349 
(case eta_abs t of 
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset

350 
Abs (_, _, t') => 
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset

351 
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

352 
else incr_boundvars ~1 t' 
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset

353 
 _ => raise Match); 
74bf78db0d87
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents:
42085
diff
changeset

354 

32120
53a21a5e6889
attempt for more concise setup of nonetacontracting binders
haftmann
parents:
31542
diff
changeset

355 

42085  356 
(* binders *) 
548  357 

21535  358 
fun mk_binder_tr' (name, syn) = 
548  359 
let 
360 
fun mk_idts [] = raise Match (*abort translation*) 

361 
 mk_idts [idt] = idt 

42476  362 
 mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts; 
548  363 

364 
fun tr' t = 

365 
let 

366 
val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; 

42476  367 
in Syntax.const syn $ mk_idts xs $ bd end; 
548  368 

42476  369 
fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts) 
21535  370 
 binder_tr' [] = raise Match; 
371 
in (name, binder_tr') end; 

548  372 

42085  373 
fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts => 
374 
let val (x, t) = atomic_abs_tr' abs 

42476  375 
in list_comb (Syntax.const syn $ x $ t, ts) end); 
42085  376 

377 
fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts => 

378 
let val (x, t) = atomic_abs_tr' abs 

42476  379 
in list_comb (Syntax.const syn $ x $ A $ t, ts) end); 
42085  380 

548  381 

3691
f0396ac63e12
tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts
wenzelm
parents:
2698
diff
changeset

382 
(* idtyp constraints *) 
548  383 

42045  384 
fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] = 
385 
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

386 
 idtyp_ast_tr' _ _ = raise Match; 
548  387 

388 

389 
(* meta propositions *) 

390 

4148  391 
fun prop_tr' tm = 
548  392 
let 
42476  393 
fun aprop t = Syntax.const "_aprop" $ t; 
548  394 

2698  395 
fun is_prop Ts t = 
396 
fastype_of1 (Ts, t) = propT handle TERM _ => false; 

548  397 

35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35255
diff
changeset

398 
fun is_term (Const ("Pure.term", _) $ _) = true 
19848  399 
 is_term _ = false; 
400 

548  401 
fun tr' _ (t as Const _) = t 
18478
29a5070b517c
prop_tr': proper handling of aprop marked as bound;
wenzelm
parents:
18342
diff
changeset

402 
 tr' Ts (t as Const ("_bound", _) $ u) = 
29a5070b517c
prop_tr': proper handling of aprop marked as bound;
wenzelm
parents:
18342
diff
changeset

403 
if is_prop Ts u then aprop t else t 
2698  404 
 tr' _ (t as Free (x, T)) = 
42476  405 
if T = propT then aprop (Syntax.free x) else t 
2698  406 
 tr' _ (t as Var (xi, T)) = 
42476  407 
if T = propT then aprop (Syntax.var xi) else t 
2698  408 
 tr' Ts (t as Bound _) = 
409 
if is_prop Ts t then aprop t else t 

410 
 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

411 
 tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = 
28628  412 
if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1 
2698  413 
else tr' Ts t1 $ tr' Ts t2 
414 
 tr' Ts (t as t1 $ t2) = 

5690  415 
(if is_Const (Term.head_of t) orelse not (is_prop Ts t) 
2698  416 
then I else aprop) (tr' Ts t1 $ tr' Ts t2); 
16612
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset

417 
in tr' [] tm end; 
548  418 

2698  419 

548  420 
(* meta implication *) 
421 

42278  422 
fun impl_ast_tr' asts = 
42262  423 
if no_brackets () then raise Match 
10572  424 
else 
35255  425 
(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

426 
(prems as _ :: _ :: _, concl) => 
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset

427 
let 
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset

428 
val (asms, asm) = split_last prems; 
48be8ef738df
transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents:
15570
diff
changeset

429 
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

430 
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

431 
 _ => raise Match); 
fcf747c0b6b8
Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
schirmer
parents:
14981
diff
changeset

432 

548  433 

434 
(* dependent / nondependent quantifiers *) 

435 

20202  436 
fun var_abs mark (x, T, b) = 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42476
diff
changeset

437 
let val (x', _) = Name.variant x (Term.declare_term_names b Name.context) 
20202  438 
in (x', subst_bound (mark (x', T), b)) end; 
439 

440 
val variant_abs = var_abs Free; 

49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

441 
val variant_abs' = var_abs mark_bound_abs; 
2698  442 

548  443 
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

444 
if Term.is_dependent B then 
2698  445 
let val (x', B') = variant_abs' (x, dummyT, B); 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
46236
diff
changeset

446 
in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end 
42476  447 
else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts) 
548  448 
 dependent_tr' _ _ = raise Match; 
449 

450 

5084  451 
(* quote / antiquote *) 
452 

8577  453 
fun antiquote_tr' name = 
454 
let 

455 
fun tr' i (t $ u) = 

42476  456 
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 topdown;
wenzelm
parents:
42083
diff
changeset

457 
else tr' i t $ tr' i u 
8577  458 
 tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t) 
18139  459 
 tr' i a = if a aconv Bound i then raise Match else a; 
8577  460 
in tr' 0 end; 
461 

462 
fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t) 

463 
 quote_tr' _ _ = raise Match; 

464 

5084  465 
fun quote_antiquote_tr' quoteN antiquoteN name = 
466 
let 

42476  467 
fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts) 
8577  468 
 tr' _ = raise Match; 
469 
in (name, tr') end; 

5084  470 

471 

35145
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

472 
(* corresponding updates *) 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

473 

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

474 
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

475 

58b465952287
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents:
42057
diff
changeset

476 
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

477 
 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

478 

35145
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

479 
fun upd_tr' (x_upd, T) = 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

480 
(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

481 
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

482 
 NONE => raise Match); 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

483 

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

484 
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

485 

35145
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

486 
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

487 
 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

488 
 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

489 
 update_name_tr' _ = raise Match; 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

490 

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

491 
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

492 

35145
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

493 

14697  494 
(* indexed syntax *) 
548  495 

42278  496 
fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast 
14697  497 
 index_ast_tr' _ = raise Match; 
498 

45389
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

499 
fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

500 
Ast.Appl [Ast.Constant "_free", 
bc0d50f8ae19
discontinued numbered structure indexes (legacy feature);
wenzelm
parents:
45057
diff
changeset

501 
Ast.Variable (the_struct structs handle ERROR _ => raise Match)] 
14697  502 
 struct_ast_tr' _ _ = raise Match; 
503 

504 

505 

506 
(** Pure translations **) 

548  507 

508 
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

509 
([("_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

510 
("_constify", constify_ast_tr), 
42262  511 
("_tapp", tapp_ast_tr), 
512 
("_tappl", tappl_ast_tr), 

513 
("_bracket", bracket_ast_tr), 

35145
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

514 
("_appl", appl_ast_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

515 
("_applC", applC_ast_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

516 
("_lambda", lambda_ast_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

517 
("_idtyp", idtyp_ast_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

518 
("_idtypdummy", idtypdummy_ast_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

519 
("_bigimpl", bigimpl_ast_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

520 
("_indexdefault", indexdefault_ast_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

521 
("_indexvar", indexvar_ast_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

522 
("_struct", struct_ast_tr)], 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

523 
[("_abs", abs_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

524 
("_aprop", aprop_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

525 
("_ofclass", ofclass_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

526 
("_sort_constraint", sort_constraint_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

527 
("_TYPE", type_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

528 
("_DDDOT", dddot_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

529 
("_update_name", update_name_tr), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

530 
("_index", index_tr)], 
35198  531 
([]: (string * (term list > term)) list), 
42262  532 
[("\\<^type>fun", fun_ast_tr'), 
533 
("_abs", abs_ast_tr'), 

35145
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

534 
("_idts", idtyp_ast_tr' "_idts"), 
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

535 
("_pttrns", idtyp_ast_tr' "_pttrns"), 
35255  536 
("\\<^const>==>", impl_ast_tr'), 
35145
f132a4fd8679
moved generic update_name to Pure syntax  not specific to HOL/record;
wenzelm
parents:
32786
diff
changeset

537 
("_index", index_ast_tr')]); 
548  538 

14697  539 
fun struct_trfuns structs = 
540 
([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]); 

541 

548  542 
end; 
42284  543 

544 
structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans; 

545 
open Basic_Syntax_Trans; 