author  wenzelm 
Sat, 25 May 2013 16:55:27 +0200  
changeset 52144  9065615d0360 
parent 52143  36ffe23b25f8 
child 52163  72e83c82c1d4 
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 

52143  22 
val mk_binder_tr: string * string > string * (Proof.context > term list > term) 
42284  23 
val antiquote_tr: string > term > term 
24 
val quote_tr: string > term > term 

52143  25 
val quote_antiquote_tr: string > string > string > 
26 
string * (Proof.context > term list > term) 

27 
val non_typed_tr': (Proof.context > term list > term) > 

28 
Proof.context > typ > term list > term 

42284  29 
val tappl_ast_tr': Ast.ast * Ast.ast list > Ast.ast 
30 
val appl_ast_tr': Ast.ast * Ast.ast list > Ast.ast 

31 
val applC_ast_tr': Ast.ast * Ast.ast list > Ast.ast 

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 
52143  39 
val mk_binder_tr': string * string > string * (Proof.context > term list > term) 
40 
val preserve_binder_abs_tr': string > string > string * (Proof.context > term list > term) 

41 
val preserve_binder_abs2_tr': string > string > string * (Proof.context > 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 

52143  48 
val quote_antiquote_tr': string > string > string > 
49 
string * (Proof.context > term list > term) 

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

50 
val update_name_tr': term > term 
52143  51 
val pure_parse_ast_translation: (string * (Proof.context > Ast.ast list > Ast.ast)) list 
52 
val pure_parse_translation: (string * (Proof.context > term list > term)) list 

53 
val pure_print_ast_translation: (string * (Proof.context > Ast.ast list > Ast.ast)) list 

52144  54 
val struct_tr: string list > string * (Proof.context > term list > term) 
55 
val struct_ast_tr': string list > string * (Proof.context > Ast.ast list > Ast.ast) 

2698  56 
end; 
548  57 

42284  58 
structure Syntax_Trans: SYNTAX_TRANS = 
548  59 
struct 
2698  60 

42476  61 
structure Syntax = Lexicon.Syntax; 
62 

63 

42262  64 
(* print mode *) 
65 

66 
val bracketsN = "brackets"; 

67 
val no_bracketsN = "no_brackets"; 

68 

69 
fun no_brackets () = 

70 
find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) 

71 
(print_mode_value ()) = SOME no_bracketsN; 

72 

73 
val type_bracketsN = "type_brackets"; 

74 
val no_type_bracketsN = "no_type_brackets"; 

75 

76 
fun no_type_brackets () = 

77 
find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) 

78 
(print_mode_value ()) <> SOME type_bracketsN; 

79 

80 

2698  81 

548  82 
(** parse (ast) translations **) 
83 

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

84 
(* 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

85 

42264  86 
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

87 
 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

88 

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 

11491  90 
(* constify *) 
91 

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

92 
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

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

94 
 constify_ast_tr [Ast.Variable c] = Ast.Constant c 
11491  95 
 constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts); 
96 

97 

42262  98 
(* type syntax *) 
99 

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

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

102 

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

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

105 

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

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

108 

109 

548  110 
(* application *) 
111 

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

114 

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

548  117 

118 

119 
(* abstraction *) 

120 

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

548  123 

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

126 

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

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

548  129 

44241  130 
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

131 
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

132 
then error ("Illegal internal variable in abstraction: " ^ quote x) 
44241  133 
else absfree (x, T) t; 
21773  134 

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

42284  137 
 abs_tr [Const ("_constrain", _) $ x $ tT, t] = 
42476  138 
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

139 
 abs_tr ts = raise TERM ("abs_tr", ts); 
548  140 

141 

142 
(* binder *) 

143 

21535  144 
fun mk_binder_tr (syn, name) = 
548  145 
let 
42055  146 
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

147 
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

148 
 binder_tr [x, t] = 
42055  149 
let val abs = abs_tr [x, t] handle TERM _ => err [x, t] 
42476  150 
in Syntax.const name $ abs end 
42055  151 
 binder_tr ts = err ts; 
52143  152 
in (syn, fn _ => binder_tr) end; 
548  153 

154 

28628  155 
(* type propositions *) 
156 

35255  157 
fun mk_type ty = 
42476  158 
Syntax.const "_constrain" $ 
159 
Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty); 

28628  160 

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

28628  163 

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

167 

548  168 
(* meta propositions *) 
169 

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

173 

174 
(* meta implication *) 

175 

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

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

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

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

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

183 

548  184 

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

185 
(* type/term reflection *) 
4148  186 

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

4148  189 

548  190 

6761  191 
(* dddot *) 
192 

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

195 

5084  196 
(* quote / antiquote *) 
197 

8577  198 
fun antiquote_tr name = 
199 
let 

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

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

202 
else tr i t $ tr i u 

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

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

205 
 tr _ a = a; 

206 
in tr 0 end; 

207 

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

209 

5084  210 
fun quote_antiquote_tr quoteN antiquoteN name = 
211 
let 

42476  212 
fun tr [t] = Syntax.const name $ quote_tr antiquoteN t 
8577  213 
 tr ts = raise TERM ("quote_tr", ts); 
52143  214 
in (quoteN, fn _ => tr) end; 
5084  215 

216 

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

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

218 

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

219 
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

220 
 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

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

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

224 
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

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

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

227 
 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

228 

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

229 

14697  230 
(* indexed syntax *) 
231 

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

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

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

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

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

236 

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

237 
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

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

239 

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

14697  242 

42278  243 
fun index_tr [t] = t 
244 
 index_tr ts = raise TERM ("index_tr", ts); 

14697  245 

52144  246 
fun struct_tr structs = 
247 
("_struct", fn _ => 

248 
(fn [Const ("_indexdefault", _)] => 

249 
(case structs of 

250 
x :: _ => Syntax.const (Lexicon.mark_fixed x) 

251 
 _ => error "Illegal reference to implicit structure") 

252 
 ts => raise TERM ("struct_tr", ts))); 

12122  253 

254 

5084  255 

548  256 
(** print (ast) translations **) 
257 

14647  258 
(* types *) 
259 

52143  260 
fun non_typed_tr' f ctxt _ ts = f ctxt ts; 
14647  261 

262 

42262  263 
(* type syntax *) 
264 

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

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

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

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

269 

270 
fun fun_ast_tr' asts = 

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

272 
else 

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

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

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

276 
 _ => raise Match); 

277 

278 

548  279 
(* application *) 
280 

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

548  283 

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

286 

548  287 

42085  288 
(* partial etacontraction before printing *) 
289 

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

291 
(case eta_abs t of 

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

293 
 t' as f $ u => 

294 
(case eta_abs u of 

295 
Bound 0 => 

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

297 
else incr_boundvars ~1 f 

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

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

300 
 eta_abs t = t; 

301 

52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
51656
diff
changeset

302 
val eta_contract_raw = Config.declare_option "eta_contract"; 
42085  303 
val eta_contract = Config.bool eta_contract_raw; 
304 

305 
fun eta_contr ctxt tm = 

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

307 

308 

548  309 
(* abstraction *) 
310 

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

311 
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

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

18958  314 
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

315 
subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body); 
18958  316 

548  317 
fun strip_abss vars_of body_of tm = 
318 
let 

319 
val vars = vars_of tm; 

320 
val body = body_of tm; 

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

323 
if can Name.dest_internal x andalso not (Term.is_dependent b) 
21750  324 
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

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

548  328 

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

329 

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

330 
fun abs_tr' ctxt tm = 
42476  331 
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

332 
(strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); 
548  333 

14697  334 
fun atomic_abs_tr' (x, T, t) = 
29276  335 
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

336 
in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end; 
13762  337 

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

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

548  342 

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

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

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

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

346 
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

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

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

349 

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

350 

42085  351 
(* binders *) 
548  352 

21535  353 
fun mk_binder_tr' (name, syn) = 
548  354 
let 
355 
fun mk_idts [] = raise Match (*abort translation*) 

356 
 mk_idts [idt] = idt 

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

359 
fun tr' t = 

360 
let 

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

42476  362 
in Syntax.const syn $ mk_idts xs $ bd end; 
548  363 

42476  364 
fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts) 
21535  365 
 binder_tr' [] = raise Match; 
52143  366 
in (name, fn _ => binder_tr') end; 
548  367 

52143  368 
fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts => 
42085  369 
let val (x, t) = atomic_abs_tr' abs 
42476  370 
in list_comb (Syntax.const syn $ x $ t, ts) end); 
42085  371 

52143  372 
fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts => 
42085  373 
let val (x, t) = atomic_abs_tr' abs 
42476  374 
in list_comb (Syntax.const syn $ x $ A $ t, ts) end); 
42085  375 

548  376 

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

377 
(* idtyp constraints *) 
548  378 

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

381 
 idtyp_ast_tr' _ _ = raise Match; 
548  382 

383 

384 
(* meta propositions *) 

385 

4148  386 
fun prop_tr' tm = 
548  387 
let 
42476  388 
fun aprop t = Syntax.const "_aprop" $ t; 
548  389 

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

548  392 

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

393 
fun is_term (Const ("Pure.term", _) $ _) = true 
19848  394 
 is_term _ = false; 
395 

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

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

398 
if is_prop Ts u then aprop t else t 
2698  399 
 tr' _ (t as Free (x, T)) = 
42476  400 
if T = propT then aprop (Syntax.free x) else t 
2698  401 
 tr' _ (t as Var (xi, T)) = 
42476  402 
if T = propT then aprop (Syntax.var xi) else t 
2698  403 
 tr' Ts (t as Bound _) = 
404 
if is_prop Ts t then aprop t else t 

405 
 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

406 
 tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = 
28628  407 
if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1 
2698  408 
else tr' Ts t1 $ tr' Ts t2 
409 
 tr' Ts (t as t1 $ t2) = 

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

412 
in tr' [] tm end; 
548  413 

2698  414 

548  415 
(* meta implication *) 
416 

42278  417 
fun impl_ast_tr' asts = 
42262  418 
if no_brackets () then raise Match 
10572  419 
else 
35255  420 
(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

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

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

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

424 
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

425 
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

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

427 

548  428 

429 
(* dependent / nondependent quantifiers *) 

430 

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

432 
let val (x', _) = Name.variant x (Term.declare_term_names b Name.context) 
20202  433 
in (x', subst_bound (mark (x', T), b)) end; 
434 

435 
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

436 
val variant_abs' = var_abs mark_bound_abs; 
2698  437 

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

439 
if Term.is_dependent B then 
2698  440 
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

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

445 

5084  446 
(* quote / antiquote *) 
447 

8577  448 
fun antiquote_tr' name = 
449 
let 

450 
fun tr' i (t $ u) = 

42476  451 
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

452 
else tr' i t $ tr' i u 
8577  453 
 tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t) 
18139  454 
 tr' i a = if a aconv Bound i then raise Match else a; 
8577  455 
in tr' 0 end; 
456 

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

458 
 quote_tr' _ _ = raise Match; 

459 

5084  460 
fun quote_antiquote_tr' quoteN antiquoteN name = 
461 
let 

42476  462 
fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts) 
8577  463 
 tr' _ = raise Match; 
52143  464 
in (name, fn _ => tr') end; 
5084  465 

466 

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

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

468 

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

469 
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

470 

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

471 
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

472 
 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

473 

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

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

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

476 
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

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

478 

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

479 
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

480 

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

481 
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

482 
 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

483 
 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

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

485 

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

486 
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

487 

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

488 

14697  489 
(* indexed syntax *) 
548  490 

42278  491 
fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast 
14697  492 
 index_ast_tr' _ = raise Match; 
493 

52144  494 
fun struct_ast_tr' structs = 
495 
("_struct", fn _ => 

496 
(fn [Ast.Constant "_indexdefault"] => 

497 
(case structs of 

498 
x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x] 

499 
 _ => raise Match) 

500 
 _ => raise Match)); 

14697  501 

502 

503 

504 
(** Pure translations **) 

548  505 

52143  506 
val pure_parse_ast_translation = 
507 
[("_strip_positions", fn _ => strip_positions_ast_tr), 

508 
("_constify", fn _ => constify_ast_tr), 

509 
("_tapp", fn _ => tapp_ast_tr), 

510 
("_tappl", fn _ => tappl_ast_tr), 

511 
("_bracket", fn _ => bracket_ast_tr), 

512 
("_appl", fn _ => appl_ast_tr), 

513 
("_applC", fn _ => applC_ast_tr), 

514 
("_lambda", fn _ => lambda_ast_tr), 

515 
("_idtyp", fn _ => idtyp_ast_tr), 

516 
("_idtypdummy", fn _ => idtypdummy_ast_tr), 

517 
("_bigimpl", fn _ => bigimpl_ast_tr), 

518 
("_indexdefault", fn _ => indexdefault_ast_tr), 

519 
("_indexvar", fn _ => indexvar_ast_tr), 

520 
("_struct", fn _ => struct_ast_tr)]; 

548  521 

52143  522 
val pure_parse_translation = 
523 
[("_abs", fn _ => abs_tr), 

524 
("_aprop", fn _ => aprop_tr), 

525 
("_ofclass", fn _ => ofclass_tr), 

526 
("_sort_constraint", fn _ => sort_constraint_tr), 

527 
("_TYPE", fn _ => type_tr), 

528 
("_DDDOT", fn _ => dddot_tr), 

529 
("_update_name", fn _ => update_name_tr), 

530 
("_index", fn _ => index_tr)]; 

531 

532 
val pure_print_ast_translation = 

533 
[("\\<^type>fun", fn _ => fun_ast_tr'), 

534 
("_abs", fn _ => abs_ast_tr'), 

535 
("_idts", fn _ => idtyp_ast_tr' "_idts"), 

536 
("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"), 

537 
("\\<^const>==>", fn _ => impl_ast_tr'), 

538 
("_index", fn _ => index_ast_tr')]; 

539 

548  540 
end; 
42284  541 

542 
structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans; 

543 
open Basic_Syntax_Trans; 