author  wenzelm 
Sun, 26 May 2013 22:47:00 +0200  
changeset 52163  72e83c82c1d4 
parent 52144  9065615d0360 
child 52177  15fcad6eb956 
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 lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body) 
125 
 lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts); 

548  126 

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

128 
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

129 
then error ("Illegal internal variable in abstraction: " ^ quote x) 
44241  130 
else absfree (x, T) t; 
21773  131 

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

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

136 
 abs_tr ts = raise TERM ("abs_tr", ts); 
548  137 

138 

139 
(* binder *) 

140 

21535  141 
fun mk_binder_tr (syn, name) = 
548  142 
let 
42055  143 
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

144 
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

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

151 

28628  152 
(* type propositions *) 
153 

35255  154 
fun mk_type ty = 
42476  155 
Syntax.const "_constrain" $ 
156 
Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty); 

28628  157 

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

28628  160 

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

164 

548  165 
(* meta propositions *) 
166 

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

170 

171 
(* meta implication *) 

172 

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

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

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

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

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

180 

548  181 

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

182 
(* type/term reflection *) 
4148  183 

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

4148  186 

548  187 

6761  188 
(* dddot *) 
189 

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

192 

5084  193 
(* quote / antiquote *) 
194 

8577  195 
fun antiquote_tr name = 
196 
let 

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

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

199 
else tr i t $ tr i u 

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

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

202 
 tr _ a = a; 

203 
in tr 0 end; 

204 

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

206 

5084  207 
fun quote_antiquote_tr quoteN antiquoteN name = 
208 
let 

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

213 

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

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

215 

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

216 
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

217 
 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

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

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

221 
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

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

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

224 
 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

225 

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

226 

14697  227 
(* indexed syntax *) 
228 

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

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

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

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

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

233 

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

234 
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

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

236 

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

14697  239 

42278  240 
fun index_tr [t] = t 
241 
 index_tr ts = raise TERM ("index_tr", ts); 

14697  242 

52144  243 
fun struct_tr structs = 
244 
("_struct", fn _ => 

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

246 
(case structs of 

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

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

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

12122  250 

251 

5084  252 

548  253 
(** print (ast) translations **) 
254 

14647  255 
(* types *) 
256 

52143  257 
fun non_typed_tr' f ctxt _ ts = f ctxt ts; 
14647  258 

259 

42262  260 
(* type syntax *) 
261 

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

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

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

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

266 

267 
fun fun_ast_tr' asts = 

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

269 
else 

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

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

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

273 
 _ => raise Match); 

274 

275 

548  276 
(* application *) 
277 

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

548  280 

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

283 

548  284 

42085  285 
(* partial etacontraction before printing *) 
286 

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

288 
(case eta_abs t of 

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

290 
 t' as f $ u => 

291 
(case eta_abs u of 

292 
Bound 0 => 

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

294 
else incr_boundvars ~1 f 

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

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

297 
 eta_abs t = t; 

298 

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

299 
val eta_contract_raw = Config.declare_option "eta_contract"; 
42085  300 
val eta_contract = Config.bool eta_contract_raw; 
301 

302 
fun eta_contr ctxt tm = 

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

304 

305 

548  306 
(* abstraction *) 
307 

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

308 
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

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

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

312 
subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body); 
18958  313 

548  314 
fun strip_abss vars_of body_of tm = 
315 
let 

316 
val vars = vars_of tm; 

317 
val body = body_of tm; 

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

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

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

548  325 

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

326 

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

327 
fun abs_tr' ctxt tm = 
42476  328 
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

329 
(strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); 
548  330 

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

333 
in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end; 
13762  334 

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

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

548  339 

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

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

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

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

343 
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

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

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

346 

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

347 

42085  348 
(* binders *) 
548  349 

21535  350 
fun mk_binder_tr' (name, syn) = 
548  351 
let 
352 
fun mk_idts [] = raise Match (*abort translation*) 

353 
 mk_idts [idt] = idt 

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

356 
fun tr' t = 

357 
let 

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

42476  359 
in Syntax.const syn $ mk_idts xs $ bd end; 
548  360 

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

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

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

548  373 

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

374 
(* idtyp constraints *) 
548  375 

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

378 
 idtyp_ast_tr' _ _ = raise Match; 
548  379 

380 

381 
(* meta propositions *) 

382 

4148  383 
fun prop_tr' tm = 
548  384 
let 
42476  385 
fun aprop t = Syntax.const "_aprop" $ t; 
548  386 

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

548  389 

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

390 
fun is_term (Const ("Pure.term", _) $ _) = true 
19848  391 
 is_term _ = false; 
392 

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

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

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

402 
 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

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

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

409 
in tr' [] tm end; 
548  410 

2698  411 

548  412 
(* meta implication *) 
413 

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

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

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

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

421 
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

422 
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

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

424 

548  425 

426 
(* dependent / nondependent quantifiers *) 

427 

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

429 
let val (x', _) = Name.variant x (Term.declare_term_names b Name.context) 
20202  430 
in (x', subst_bound (mark (x', T), b)) end; 
431 

432 
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

433 
val variant_abs' = var_abs mark_bound_abs; 
2698  434 

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

436 
if Term.is_dependent B then 
2698  437 
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

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

442 

5084  443 
(* quote / antiquote *) 
444 

8577  445 
fun antiquote_tr' name = 
446 
let 

447 
fun tr' i (t $ u) = 

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

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

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

455 
 quote_tr' _ _ = raise Match; 

456 

5084  457 
fun quote_antiquote_tr' quoteN antiquoteN name = 
458 
let 

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

463 

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

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

465 

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

466 
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

467 

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

468 
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

469 
 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

470 

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

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

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

473 
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

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

475 

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

477 

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

478 
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

479 
 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

480 
 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

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

482 

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

483 
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

484 

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

485 

14697  486 
(* indexed syntax *) 
548  487 

42278  488 
fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast 
14697  489 
 index_ast_tr' _ = raise Match; 
490 

52144  491 
fun struct_ast_tr' structs = 
492 
("_struct", fn _ => 

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

494 
(case structs of 

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

496 
 _ => raise Match) 

497 
 _ => raise Match)); 

14697  498 

499 

500 

501 
(** Pure translations **) 

548  502 

52143  503 
val pure_parse_ast_translation = 
504 
[("_strip_positions", fn _ => strip_positions_ast_tr), 

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

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

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

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

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

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

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

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

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

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

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

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

548  517 

52143  518 
val pure_parse_translation = 
519 
[("_abs", fn _ => abs_tr), 

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

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

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

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

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

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

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

527 

528 
val pure_print_ast_translation = 

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

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

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

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

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

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

535 

548  536 
end; 
42284  537 

538 
structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans; 

539 
open Basic_Syntax_Trans; 