--- a/NEWS Sat May 25 15:00:53 2013 +0200
+++ b/NEWS Sat May 25 15:37:53 2013 +0200
@@ -40,6 +40,10 @@
*** Pure ***
+* Syntax translation functions (print_translation etc.) always depend
+on Proof.context. Discontinued former "(advanced)" option -- this is
+now the default. Minor INCOMPATIBILITY.
+
* Target-sensitive commands 'interpretation' and 'sublocale'.
Particulary, 'interpretation' now allows for non-persistent
interpretation within "context ... begin ... end" blocks.
--- a/etc/isar-keywords-ZF.el Sat May 25 15:00:53 2013 +0200
+++ b/etc/isar-keywords-ZF.el Sat May 25 15:37:53 2013 +0200
@@ -209,8 +209,7 @@
"}"))
(defconst isar-keywords-minor
- '("advanced"
- "and"
+ '("and"
"assumes"
"attach"
"begin"
--- a/etc/isar-keywords.el Sat May 25 15:00:53 2013 +0200
+++ b/etc/isar-keywords.el Sat May 25 15:37:53 2013 +0200
@@ -303,8 +303,7 @@
"}"))
(defconst isar-keywords-minor
- '("advanced"
- "and"
+ '("and"
"assumes"
"attach"
"avoids"
--- a/src/CCL/Term.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/CCL/Term.thy Sat May 25 15:37:53 2013 +0200
@@ -95,17 +95,17 @@
*}
parse_translation {*
- [(@{syntax_const "_let"}, let_tr),
- (@{syntax_const "_letrec"}, letrec_tr),
- (@{syntax_const "_letrec2"}, letrec2_tr),
- (@{syntax_const "_letrec3"}, letrec3_tr)]
+ [(@{syntax_const "_let"}, K let_tr),
+ (@{syntax_const "_letrec"}, K letrec_tr),
+ (@{syntax_const "_letrec2"}, K letrec2_tr),
+ (@{syntax_const "_letrec3"}, K letrec3_tr)]
*}
print_translation {*
- [(@{const_syntax let}, let_tr'),
- (@{const_syntax letrec}, letrec_tr'),
- (@{const_syntax letrec2}, letrec2_tr'),
- (@{const_syntax letrec3}, letrec3_tr')]
+ [(@{const_syntax let}, K let_tr'),
+ (@{const_syntax letrec}, K letrec_tr'),
+ (@{const_syntax letrec2}, K letrec2_tr'),
+ (@{const_syntax letrec3}, K letrec3_tr')]
*}
consts
--- a/src/CCL/Type.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/CCL/Type.thy Sat May 25 15:37:53 2013 +0200
@@ -47,9 +47,9 @@
print_translation {*
[(@{const_syntax Pi},
- Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
+ fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
(@{const_syntax Sigma},
- Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
+ fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
*}
defs
--- a/src/Cube/Cube.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Cube/Cube.thy Sat May 25 15:37:53 2013 +0200
@@ -63,7 +63,7 @@
print_translation {*
[(@{const_syntax Prod},
- Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
+ fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
*}
axiomatization where
--- a/src/Doc/Classes/Setup.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Doc/Classes/Setup.thy Sat May 25 15:37:53 2013 +0200
@@ -30,10 +30,10 @@
Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
| beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
in
- [(@{syntax_const "_alpha"}, alpha_ast_tr),
- (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
- (@{syntax_const "_beta"}, beta_ast_tr),
- (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
+ [(@{syntax_const "_alpha"}, K alpha_ast_tr),
+ (@{syntax_const "_alpha_ofsort"}, K alpha_ofsort_ast_tr),
+ (@{syntax_const "_beta"}, K beta_ast_tr),
+ (@{syntax_const "_beta_ofsort"}, K beta_ofsort_ast_tr)]
end
*}
--- a/src/Doc/IsarRef/Inner_Syntax.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy Sat May 25 15:37:53 2013 +0200
@@ -1469,7 +1469,7 @@
@{rail "
( @@{command parse_ast_translation} | @@{command parse_translation} |
@@{command print_translation} | @@{command typed_print_translation} |
- @@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text}
+ @@{command print_ast_translation}) @{syntax text}
;
(@@{ML_antiquotation class_syntax} |
@@{ML_antiquotation type_syntax} |
@@ -1486,31 +1486,31 @@
\medskip
{\footnotesize
- \begin{tabular}{ll}
- @{command parse_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
- @{command parse_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
- @{command print_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
- @{command typed_print_translation} & : @{ML_type "(string * (typ -> term list -> term)) list"} \\
- @{command print_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
+ \begin{tabular}{l}
+ @{command parse_ast_translation} : \\
+ \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
+ @{command parse_translation} : \\
+ \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
+ @{command print_translation} : \\
+ \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
+ @{command typed_print_translation} : \\
+ \quad @{ML_type "(string * (Proof.context -> typ -> term list -> term)) list"} \\
+ @{command print_ast_translation} : \\
+ \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
\end{tabular}}
\medskip
The argument list consists of @{text "(c, tr)"} pairs, where @{text
"c"} is the syntax name of the formal entity involved, and @{text
"tr"} a function that translates a syntax form @{text "c args"} into
- @{text "tr args"}. The ML naming convention for parse translations
- is @{text "c_tr"} and for print translations @{text "c_tr'"}.
+ @{text "tr ctxt args"} (depending on the context). The ML naming
+ convention for parse translations is @{text "c_tr"} and for print
+ translations @{text "c_tr'"}.
The @{command_ref print_syntax} command displays the sets of names
associated with the translation functions of a theory under @{text
"parse_ast_translation"} etc.
- If the @{verbatim "("}@{keyword "advanced"}@{verbatim ")"} option is
- given, the corresponding translation functions depend on the current
- theory or proof context as additional argument. This allows to
- implement advanced syntax mechanisms, as translations functions may
- refer to specific theory declarations or auxiliary proof data.
-
\item @{text "@{class_syntax c}"}, @{text "@{type_syntax c}"},
@{text "@{const_syntax c}"} inline the authentic syntax name of the
given formal entities into the ML source. This is the
--- a/src/FOLP/IFOLP.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/FOLP/IFOLP.thy Sat May 25 15:37:53 2013 +0200
@@ -66,13 +66,13 @@
parse_translation {*
let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p
- in [(@{syntax_const "_Proof"}, proof_tr)] end
+ in [(@{syntax_const "_Proof"}, K proof_tr)] end
*}
(*show_proofs = true displays the proof terms -- they are ENORMOUS*)
ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *}
-print_translation (advanced) {*
+print_translation {*
let
fun proof_tr' ctxt [P, p] =
if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
--- a/src/HOL/Big_Operators.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Big_Operators.thy Sat May 25 15:37:53 2013 +0200
@@ -370,7 +370,7 @@
Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
end
| setsum_tr' _ = raise Match;
-in [(@{const_syntax setsum}, setsum_tr')] end
+in [(@{const_syntax setsum}, K setsum_tr')] end
*}
text {* TODO These are candidates for generalization *}
--- a/src/HOL/Code_Evaluation.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Code_Evaluation.thy Sat May 25 15:37:53 2013 +0200
@@ -144,15 +144,15 @@
subsubsection {* Obfuscation *}
print_translation {*
-let
- val term = Const ("<TERM>", dummyT);
- fun tr1' [_, _] = term;
- fun tr2' [] = term;
-in
- [(@{const_syntax Const}, tr1'),
+ let
+ val term = Const ("<TERM>", dummyT);
+ fun tr1' _ [_, _] = term;
+ fun tr2' _ [] = term;
+ in
+ [(@{const_syntax Const}, tr1'),
(@{const_syntax App}, tr1'),
(@{const_syntax dummy_term}, tr2')]
-end
+ end
*}
--- a/src/HOL/Groups.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Groups.thy Sat May 25 15:37:53 2013 +0200
@@ -121,7 +121,7 @@
simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
-typed_print_translation (advanced) {*
+typed_print_translation {*
let
fun tr' c = (c, fn ctxt => fn T => fn ts =>
if not (null ts) orelse T = dummyT orelse
--- a/src/HOL/HOL.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/HOL.thy Sat May 25 15:37:53 2013 +0200
@@ -116,7 +116,7 @@
syntax "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10)
translations "THE x. P" == "CONST The (%x. P)"
print_translation {*
- [(@{const_syntax The}, fn [Abs abs] =>
+ [(@{const_syntax The}, fn _ => fn [Abs abs] =>
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
in Syntax.const @{syntax_const "_The"} $ x $ t end)]
*} -- {* To avoid eta-contraction of body *}
--- a/src/HOL/HOLCF/Cfun.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Sat May 25 15:37:53 2013 +0200
@@ -40,7 +40,7 @@
*}
print_translation {*
- [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
+ [(@{const_syntax Abs_cfun}, fn _ => fn [Abs abs] =>
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
*} -- {* To avoid eta-contraction of body *}
@@ -61,7 +61,7 @@
Ast.fold_ast_p @{syntax_const "_cabs"}
(Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
| Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
- in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
+ in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end;
*}
print_ast_translation {*
@@ -75,7 +75,7 @@
| (xs, body) => Ast.Appl
[Ast.Constant @{syntax_const "_Lambda"},
Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
- in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
+ in [(@{syntax_const "_cabs"}, K cabs_ast_tr')] end
*}
text {* Dummy patterns for continuous abstraction *}
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sat May 25 15:37:53 2013 +0200
@@ -131,7 +131,7 @@
parse_translation {*
(* rewrite (_pat x) => (succeed) *)
(* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
- [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
+ [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
*}
@@ -164,7 +164,7 @@
(Syntax.const @{syntax_const "_match"} $ p $ v) $ t
end;
- in [(@{const_syntax Rep_cfun}, Case1_tr')] end;
+ in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
*}
translations
--- a/src/HOL/Hilbert_Choice.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hilbert_Choice.thy Sat May 25 15:37:53 2013 +0200
@@ -25,7 +25,7 @@
"SOME x. P" == "CONST Eps (%x. P)"
print_translation {*
- [(@{const_syntax Eps}, fn [Abs abs] =>
+ [(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
*} -- {* to avoid eta-contraction of body *}
--- a/src/HOL/Hoare/Hoare_Logic.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Sat May 25 15:37:53 2013 +0200
@@ -54,8 +54,8 @@
("{_} // _ // {_}" [0,55,0] 50)
ML_file "hoare_syntax.ML"
-parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
-print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
+parse_translation {* [(@{syntax_const "_hoare_vars"}, K Hoare_Syntax.hoare_vars_tr)] *}
+print_translation {* [(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare"}))] *}
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat May 25 15:37:53 2013 +0200
@@ -56,9 +56,9 @@
("{_} // _ // {_}" [0,55,0] 50)
ML_file "hoare_syntax.ML"
-parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, K Hoare_Syntax.hoare_vars_tr)] *}
print_translation
- {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
+ {* [(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"}))] *}
(*** The proof rules ***)
--- a/src/HOL/Hoare/Separation.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hoare/Separation.thy Sat May 25 15:37:53 2013 +0200
@@ -77,10 +77,10 @@
*}
parse_translation {*
- [(@{syntax_const "_emp"}, emp_tr),
- (@{syntax_const "_singl"}, singl_tr),
- (@{syntax_const "_star"}, star_tr),
- (@{syntax_const "_wand"}, wand_tr)]
+ [(@{syntax_const "_emp"}, K emp_tr),
+ (@{syntax_const "_singl"}, K singl_tr),
+ (@{syntax_const "_star"}, K star_tr),
+ (@{syntax_const "_wand"}, K wand_tr)]
*}
text{* Now it looks much better: *}
@@ -128,10 +128,10 @@
*}
print_translation {*
- [(@{const_syntax is_empty}, is_empty_tr'),
- (@{const_syntax singl}, singl_tr'),
- (@{const_syntax star}, star_tr'),
- (@{const_syntax wand}, wand_tr')]
+ [(@{const_syntax is_empty}, K is_empty_tr'),
+ (@{const_syntax singl}, K singl_tr'),
+ (@{const_syntax star}, K star_tr'),
+ (@{const_syntax wand}, K wand_tr')]
*}
text{* Now the intermediate proof states are also readable: *}
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat May 25 15:37:53 2013 +0200
@@ -113,15 +113,15 @@
fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts;
in
- [(@{const_syntax Collect}, assert_tr'),
- (@{const_syntax Basic}, assign_tr'),
- (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
- (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"}),
- (@{const_syntax AnnBasic}, annassign_tr'),
- (@{const_syntax AnnWhile}, annbexp_tr' @{syntax_const "_AnnWhile"}),
- (@{const_syntax AnnAwait}, annbexp_tr' @{syntax_const "_AnnAwait"}),
- (@{const_syntax AnnCond1}, annbexp_tr' @{syntax_const "_AnnCond1"}),
- (@{const_syntax AnnCond2}, annbexp_tr' @{syntax_const "_AnnCond2"})]
+ [(@{const_syntax Collect}, K assert_tr'),
+ (@{const_syntax Basic}, K assign_tr'),
+ (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
+ (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"})),
+ (@{const_syntax AnnBasic}, K annassign_tr'),
+ (@{const_syntax AnnWhile}, K (annbexp_tr' @{syntax_const "_AnnWhile"})),
+ (@{const_syntax AnnAwait}, K (annbexp_tr' @{syntax_const "_AnnAwait"})),
+ (@{const_syntax AnnCond1}, K (annbexp_tr' @{syntax_const "_AnnCond1"})),
+ (@{const_syntax AnnCond2}, K (annbexp_tr' @{syntax_const "_AnnCond2"}))]
end;
*}
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Sat May 25 15:37:53 2013 +0200
@@ -18,7 +18,7 @@
let
fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
| quote_tr ts = raise TERM ("quote_tr", ts);
- in [(@{syntax_const "_quote"}, quote_tr)] end
+ in [(@{syntax_const "_quote"}, K quote_tr)] end
*}
end
\ No newline at end of file
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat May 25 15:37:53 2013 +0200
@@ -72,10 +72,10 @@
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
- [(@{const_syntax Collect}, assert_tr'),
- (@{const_syntax Basic}, assign_tr'),
- (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
- (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
+ [(@{const_syntax Collect}, K assert_tr'),
+ (@{const_syntax Basic}, K assign_tr'),
+ (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
+ (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While"}))]
end
*}
--- a/src/HOL/Inductive.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Inductive.thy Sat May 25 15:37:53 2013 +0200
@@ -299,14 +299,14 @@
syntax (xsymbols)
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10)
-parse_translation (advanced) {*
-let
- fun fun_tr ctxt [cs] =
- let
- val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
- val ft = Case_Translation.case_tr true ctxt [x, cs];
- in lambda x ft end
-in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
+parse_translation {*
+ let
+ fun fun_tr ctxt [cs] =
+ let
+ val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
+ val ft = Case_Translation.case_tr true ctxt [x, cs];
+ in lambda x ft end
+ in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
*}
end
--- a/src/HOL/Isar_Examples/Hoare.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Sat May 25 15:37:53 2013 +0200
@@ -216,7 +216,7 @@
let
fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
| quote_tr ts = raise TERM ("quote_tr", ts);
- in [(@{syntax_const "_quote"}, quote_tr)] end
+ in [(@{syntax_const "_quote"}, K quote_tr)] end
*}
text {* As usual in Isabelle syntax translations, the part for
@@ -241,10 +241,10 @@
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
- [(@{const_syntax Collect}, assert_tr'),
- (@{const_syntax Basic}, assign_tr'),
- (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
- (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})]
+ [(@{const_syntax Collect}, K assert_tr'),
+ (@{const_syntax Basic}, K assign_tr'),
+ (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
+ (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))]
end
*}
--- a/src/HOL/Library/Cardinality.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Library/Cardinality.thy Sat May 25 15:37:53 2013 +0200
@@ -43,7 +43,7 @@
translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
-typed_print_translation (advanced) {*
+typed_print_translation {*
let
fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
--- a/src/HOL/Library/Numeral_Type.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Sat May 25 15:37:53 2013 +0200
@@ -324,7 +324,7 @@
code_datatype Num0
instantiation num0 :: equal begin
-definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
+definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
where "equal_num0 = op ="
instance by intro_classes (simp add: equal_num0_def)
end
@@ -351,7 +351,7 @@
definition "enum_class.enum_ex P = P (1 :: num1)"
instance
by intro_classes
- (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
+ (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
(metis (full_types) num1_eq_iff)+)
end
@@ -477,47 +477,49 @@
(type) "0" == (type) "num0"
parse_translation {*
-let
- fun mk_bintype n =
- let
- fun mk_bit 0 = Syntax.const @{type_syntax bit0}
- | mk_bit 1 = Syntax.const @{type_syntax bit1};
- fun bin_of n =
- if n = 1 then Syntax.const @{type_syntax num1}
- else if n = 0 then Syntax.const @{type_syntax num0}
- else if n = ~1 then raise TERM ("negative type numeral", [])
- else
- let val (q, r) = Integer.div_mod n 2;
- in mk_bit r $ bin_of q end;
- in bin_of n end;
+ let
+ fun mk_bintype n =
+ let
+ fun mk_bit 0 = Syntax.const @{type_syntax bit0}
+ | mk_bit 1 = Syntax.const @{type_syntax bit1};
+ fun bin_of n =
+ if n = 1 then Syntax.const @{type_syntax num1}
+ else if n = 0 then Syntax.const @{type_syntax num0}
+ else if n = ~1 then raise TERM ("negative type numeral", [])
+ else
+ let val (q, r) = Integer.div_mod n 2;
+ in mk_bit r $ bin_of q end;
+ in bin_of n end;
- fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
- | numeral_tr ts = raise TERM ("numeral_tr", ts);
+ fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
+ | numeral_tr ts = raise TERM ("numeral_tr", ts);
-in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
+ in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
*}
print_translation {*
-let
- fun int_of [] = 0
- | int_of (b :: bs) = b + 2 * int_of bs;
+ let
+ fun int_of [] = 0
+ | int_of (b :: bs) = b + 2 * int_of bs;
- fun bin_of (Const (@{type_syntax num0}, _)) = []
- | bin_of (Const (@{type_syntax num1}, _)) = [1]
- | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
- | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
- | bin_of t = raise TERM ("bin_of", [t]);
+ fun bin_of (Const (@{type_syntax num0}, _)) = []
+ | bin_of (Const (@{type_syntax num1}, _)) = [1]
+ | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
+ | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
+ | bin_of t = raise TERM ("bin_of", [t]);
- fun bit_tr' b [t] =
- let
- val rev_digs = b :: bin_of t handle TERM _ => raise Match
- val i = int_of rev_digs;
- val num = string_of_int (abs i);
- in
- Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
- end
- | bit_tr' b _ = raise Match;
-in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
+ fun bit_tr' b [t] =
+ let
+ val rev_digs = b :: bin_of t handle TERM _ => raise Match
+ val i = int_of rev_digs;
+ val num = string_of_int (abs i);
+ in
+ Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
+ end
+ | bit_tr' b _ = raise Match;
+ in
+ [(@{type_syntax bit0}, K (bit_tr' 0)),
+ (@{type_syntax bit1}, K (bit_tr' 1))] end;
*}
subsection {* Examples *}
--- a/src/HOL/Library/Phantom_Type.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Library/Phantom_Type.thy Sat May 25 15:37:53 2013 +0200
@@ -27,13 +27,13 @@
translations
"Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
-typed_print_translation (advanced) {*
-let
- fun phantom_tr' ctxt
- (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
- Term.list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
- | phantom_tr' _ _ _ = raise Match;
-in [(@{const_syntax phantom}, phantom_tr')] end
+typed_print_translation {*
+ let
+ fun phantom_tr' ctxt
+ (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
+ list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
+ | phantom_tr' _ _ _ = raise Match;
+ in [(@{const_syntax phantom}, phantom_tr')] end
*}
end
--- a/src/HOL/List.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/List.thy Sat May 25 15:37:53 2013 +0200
@@ -386,7 +386,7 @@
syntax (HTML output)
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
-parse_translation (advanced) {*
+parse_translation {*
let
val NilC = Syntax.const @{const_syntax Nil};
val ConsC = Syntax.const @{const_syntax Cons};
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat May 25 15:37:53 2013 +0200
@@ -28,18 +28,19 @@
syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
parse_translation {*
-let
- fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
- fun finite_vec_tr [t, u] =
- (case Term_Position.strip_positions u of
- v as Free (x, _) =>
- if Lexicon.is_tid x then
- vec t (Syntax.const @{syntax_const "_ofsort"} $ v $ Syntax.const @{class_syntax finite})
- else vec t u
- | _ => vec t u)
-in
- [(@{syntax_const "_finite_vec"}, finite_vec_tr)]
-end
+ let
+ fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
+ fun finite_vec_tr [t, u] =
+ (case Term_Position.strip_positions u of
+ v as Free (x, _) =>
+ if Lexicon.is_tid x then
+ vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
+ Syntax.const @{class_syntax finite})
+ else vec t u
+ | _ => vec t u)
+ in
+ [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
+ end
*}
lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
--- a/src/HOL/Num.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Num.thy Sat May 25 15:37:53 2013 +0200
@@ -291,50 +291,54 @@
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
parse_translation {*
-let
- fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
- of (0, 1) => Syntax.const @{const_name One}
- | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
- | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n
- else raise Match;
- val pos = Syntax.const @{const_name numeral}
- val neg = Syntax.const @{const_name neg_numeral}
- val one = Syntax.const @{const_name Groups.one}
- val zero = Syntax.const @{const_name Groups.zero}
- fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
- c $ numeral_tr [t] $ u
- | numeral_tr [Const (num, _)] =
- let
- val {value, ...} = Lexicon.read_xnum num;
- in
- if value = 0 then zero else
- if value > 0
- then pos $ num_of_int value
- else neg $ num_of_int (~value)
- end
- | numeral_tr ts = raise TERM ("numeral_tr", ts);
-in [("_Numeral", numeral_tr)] end
+ let
+ fun num_of_int n =
+ if n > 0 then
+ (case IntInf.quotRem (n, 2) of
+ (0, 1) => Syntax.const @{const_name One}
+ | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
+ | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
+ else raise Match
+ val pos = Syntax.const @{const_name numeral}
+ val neg = Syntax.const @{const_name neg_numeral}
+ val one = Syntax.const @{const_name Groups.one}
+ val zero = Syntax.const @{const_name Groups.zero}
+ fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
+ c $ numeral_tr [t] $ u
+ | numeral_tr [Const (num, _)] =
+ let
+ val {value, ...} = Lexicon.read_xnum num;
+ in
+ if value = 0 then zero else
+ if value > 0
+ then pos $ num_of_int value
+ else neg $ num_of_int (~value)
+ end
+ | numeral_tr ts = raise TERM ("numeral_tr", ts);
+ in [("_Numeral", K numeral_tr)] end
*}
-typed_print_translation (advanced) {*
-let
- fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
- | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
- | dest_num (Const (@{const_syntax One}, _)) = 1;
- fun num_tr' sign ctxt T [n] =
- let
- val k = dest_num n;
- val t' = Syntax.const @{syntax_const "_Numeral"} $
- Syntax.free (sign ^ string_of_int k);
- in
- case T of
- Type (@{type_name fun}, [_, T']) =>
- if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
- else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
- | T' => if T' = dummyT then t' else raise Match
- end;
-in [(@{const_syntax numeral}, num_tr' ""),
- (@{const_syntax neg_numeral}, num_tr' "-")] end
+typed_print_translation {*
+ let
+ fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
+ | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
+ | dest_num (Const (@{const_syntax One}, _)) = 1;
+ fun num_tr' sign ctxt T [n] =
+ let
+ val k = dest_num n;
+ val t' = Syntax.const @{syntax_const "_Numeral"} $
+ Syntax.free (sign ^ string_of_int k);
+ in
+ (case T of
+ Type (@{type_name fun}, [_, T']) =>
+ if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
+ else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
+ | T' => if T' = dummyT then t' else raise Match)
+ end;
+ in
+ [(@{const_syntax numeral}, num_tr' ""),
+ (@{const_syntax neg_numeral}, num_tr' "-")]
+ end
*}
ML_file "Tools/numeral.ML"
--- a/src/HOL/Orderings.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Orderings.thy Sat May 25 15:37:53 2013 +0200
@@ -727,8 +727,8 @@
fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P;
- fun tr' q = (q,
- fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
+ fun tr' q = (q, fn _ =>
+ (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
(case AList.lookup (op =) trans (q, c, d) of
NONE => raise Match
@@ -736,7 +736,7 @@
if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
else raise Match)
- | _ => raise Match);
+ | _ => raise Match));
in [tr' All_binder, tr' Ex_binder] end
*}
--- a/src/HOL/Product_Type.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Product_Type.thy Sat May 25 15:37:53 2013 +0200
@@ -196,71 +196,71 @@
(*reconstruct pattern from (nested) splits, avoiding eta-contraction of body;
works best with enclosing "let", if "let" does not avoid eta-contraction*)
print_translation {*
-let
- fun split_tr' [Abs (x, T, t as (Abs abs))] =
- (* split (%x y. t) => %(x,y) t *)
- let
- val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
- val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
- in
- Syntax.const @{syntax_const "_abs"} $
- (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
- end
- | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
- (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
- let
- val Const (@{syntax_const "_abs"}, _) $
- (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
- val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
- in
- Syntax.const @{syntax_const "_abs"} $
- (Syntax.const @{syntax_const "_pattern"} $ x' $
- (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
- end
- | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
- (* split (split (%x y z. t)) => %((x, y), z). t *)
- split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
- | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
- (* split (%pttrn z. t) => %(pttrn,z). t *)
- let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
- Syntax.const @{syntax_const "_abs"} $
- (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
- end
- | split_tr' _ = raise Match;
-in [(@{const_syntax prod_case}, split_tr')] end
+ let
+ fun split_tr' [Abs (x, T, t as (Abs abs))] =
+ (* split (%x y. t) => %(x,y) t *)
+ let
+ val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+ end
+ | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
+ (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
+ let
+ val Const (@{syntax_const "_abs"}, _) $
+ (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $
+ (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
+ end
+ | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
+ (* split (split (%x y z. t)) => %((x, y), z). t *)
+ split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
+ | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
+ (* split (%pttrn z. t) => %(pttrn,z). t *)
+ let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
+ end
+ | split_tr' _ = raise Match;
+ in [(@{const_syntax prod_case}, K split_tr')] end
*}
(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
typed_print_translation {*
-let
- fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
- | split_guess_names_tr' T [Abs (x, xT, t)] =
- (case (head_of t) of
- Const (@{const_syntax prod_case}, _) => raise Match
- | _ =>
- let
- val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
- val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
- val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
- in
- Syntax.const @{syntax_const "_abs"} $
- (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
- end)
- | split_guess_names_tr' T [t] =
- (case head_of t of
- Const (@{const_syntax prod_case}, _) => raise Match
- | _ =>
- let
- val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
- val (y, t') =
- Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
- val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
- in
- Syntax.const @{syntax_const "_abs"} $
- (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
- end)
- | split_guess_names_tr' _ _ = raise Match;
-in [(@{const_syntax prod_case}, split_guess_names_tr')] end
+ let
+ fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
+ | split_guess_names_tr' T [Abs (x, xT, t)] =
+ (case (head_of t) of
+ Const (@{const_syntax prod_case}, _) => raise Match
+ | _ =>
+ let
+ val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+ val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+ end)
+ | split_guess_names_tr' T [t] =
+ (case head_of t of
+ Const (@{const_syntax prod_case}, _) => raise Match
+ | _ =>
+ let
+ val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+ val (y, t') =
+ Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+ end)
+ | split_guess_names_tr' _ _ = raise Match;
+ in [(@{const_syntax prod_case}, K split_guess_names_tr')] end
*}
(* Force eta-contraction for terms of the form "Q A (%p. prod_case P p)"
@@ -270,19 +270,20 @@
Otherwise prevent eta-contraction.
*)
print_translation {*
-let
- fun contract Q f ts =
- case ts of
- [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
- => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s
- | _ => f ts;
- fun contract2 (Q,f) = (Q, contract Q f);
- val pairs =
+ let
+ fun contract Q tr ctxt ts =
+ (case ts of
+ [A, Abs (_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)] =>
+ if Term.is_dependent t then tr ctxt ts
+ else Syntax.const Q $ A $ s
+ | _ => tr ctxt ts);
+ in
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
-in map contract2 pairs end
+ |> map (fn (Q, tr) => (Q, contract Q tr))
+ end
*}
subsubsection {* Code generator setup *}
--- a/src/HOL/Set.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Set.thy Sat May 25 15:37:53 2013 +0200
@@ -256,35 +256,36 @@
"\<exists>!A\<subseteq>B. P" => "EX! A. A \<subseteq> B & P"
print_translation {*
-let
- val All_binder = Mixfix.binder_name @{const_syntax All};
- val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
- val impl = @{const_syntax HOL.implies};
- val conj = @{const_syntax HOL.conj};
- val sbset = @{const_syntax subset};
- val sbset_eq = @{const_syntax subset_eq};
-
- val trans =
- [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
- ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
- ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
- ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
-
- fun mk v (v', T) c n P =
- if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
- then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P else raise Match;
-
- fun tr' q = (q,
- fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
- Const (c, _) $
- (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
- (case AList.lookup (op =) trans (q, c, d) of
- NONE => raise Match
- | SOME l => mk v (v', T) l n P)
- | _ => raise Match);
-in
- [tr' All_binder, tr' Ex_binder]
-end
+ let
+ val All_binder = Mixfix.binder_name @{const_syntax All};
+ val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
+ val impl = @{const_syntax HOL.implies};
+ val conj = @{const_syntax HOL.conj};
+ val sbset = @{const_syntax subset};
+ val sbset_eq = @{const_syntax subset_eq};
+
+ val trans =
+ [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
+ ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
+ ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
+ ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
+
+ fun mk v (v', T) c n P =
+ if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
+ then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P
+ else raise Match;
+
+ fun tr' q = (q, fn _ =>
+ (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
+ Const (c, _) $
+ (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
+ (case AList.lookup (op =) trans (q, c, d) of
+ NONE => raise Match
+ | SOME l => mk v (v', T) l n P)
+ | _ => raise Match));
+ in
+ [tr' All_binder, tr' Ex_binder]
+ end
*}
@@ -304,11 +305,11 @@
fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
| nvars _ = 1;
- fun setcompr_tr [e, idts, b] =
+ fun setcompr_tr ctxt [e, idts, b] =
let
val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
- val exP = ex_tr [idts, P];
+ val exP = ex_tr ctxt [idts, P];
in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
@@ -323,7 +324,7 @@
let
val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
- fun setcompr_tr' [Abs (abs as (_, _, P))] =
+ fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =
let
fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
| check (Const (@{const_syntax HOL.conj}, _) $
@@ -333,7 +334,7 @@
| check _ = false;
fun tr' (_ $ abs) =
- let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
+ let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' ctxt [abs]
in Syntax.const @{syntax_const "_Setcompr"} $ e $ idts $ Q end;
in
if check (P, 0) then tr' P
@@ -1004,7 +1005,7 @@
lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
by (unfold less_le) blast
-lemma psubsetE [elim!,no_atp]:
+lemma psubsetE [elim!,no_atp]:
"[|A \<subset> B; [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
by (unfold less_le) blast
@@ -1758,10 +1759,10 @@
lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
by auto
-lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) =
+lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) =
(if c \<in> A then (if d \<in> A then UNIV else B)
- else if d \<in> A then -B else {})"
- by (auto simp add: vimage_def)
+ else if d \<in> A then -B else {})"
+ by (auto simp add: vimage_def)
lemma vimage_inter_cong:
"(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
--- a/src/HOL/Statespace/StateSpaceSyntax.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy Sat May 25 15:37:53 2013 +0200
@@ -21,14 +21,14 @@
"s<x:=y>" == "_statespace_update s x y"
-parse_translation (advanced)
+parse_translation
{*
[(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
(@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
*}
-print_translation (advanced)
+print_translation
{*
[(@{const_syntax lookup}, StateSpace.lookup_tr'),
(@{const_syntax update}, StateSpace.update_tr')]
--- a/src/HOL/Tools/case_translation.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML Sat May 25 15:37:53 2013 +0200
@@ -148,10 +148,7 @@
end
| case_tr _ _ _ = case_error "case_tr";
-val trfun_setup =
- Sign.add_advanced_trfuns ([],
- [(@{syntax_const "_case_syntax"}, case_tr true)],
- [], []);
+val trfun_setup = Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)];
(* print translation *)
@@ -176,8 +173,7 @@
(mk_clauses t), ts)
end;
-val trfun_setup' = Sign.add_trfuns
- ([], [], [(@{const_syntax "case_guard"}, case_tr')], []);
+val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
(* declarations *)
--- a/src/HOL/Tools/float_syntax.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Tools/float_syntax.ML Sat May 25 15:37:53 2013 +0200
@@ -47,7 +47,6 @@
(* theory setup *)
-val setup =
- Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
+val setup = Sign.parse_translation [(@{syntax_const "_Float"}, K float_tr)];
end;
--- a/src/HOL/Tools/record.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Tools/record.ML Sat May 25 15:37:53 2013 +0200
@@ -735,10 +735,8 @@
in
val parse_translation =
- [(@{syntax_const "_record_update"}, record_update_tr)];
-
-val advanced_parse_translation =
- [(@{syntax_const "_record"}, record_tr),
+ [(@{syntax_const "_record_update"}, K record_update_tr),
+ (@{syntax_const "_record"}, record_tr),
(@{syntax_const "_record_scheme"}, record_scheme_tr),
(@{syntax_const "_record_type"}, record_type_tr),
(@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
@@ -1896,7 +1894,7 @@
val trnames = if parent_len > 0 then [extension_name] else [];
in map record_ext_type_tr' trnames end;
- val advanced_print_translation =
+ val print_translation =
map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
record_ext_type_tr's @ record_ext_type_abbr_tr's;
@@ -1995,7 +1993,7 @@
timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
(fn () =>
ext_thy
- |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
+ |> Sign.print_translation print_translation
|> Sign.restore_naming thy
|> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
|> Typedecl.abbrev_global
@@ -2316,8 +2314,7 @@
(* setup theory *)
val setup =
- Sign.add_trfuns ([], parse_translation, [], []) #>
- Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
+ Sign.parse_translation parse_translation #>
map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]);
--- a/src/HOL/Tools/string_syntax.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Tools/string_syntax.ML Sat May 25 15:37:53 2013 +0200
@@ -87,8 +87,11 @@
(* theory setup *)
val setup =
- Sign.add_trfuns
- ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
- [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
+ Sign.parse_ast_translation
+ [(@{syntax_const "_Char"}, K char_ast_tr),
+ (@{syntax_const "_String"}, K string_ast_tr)] #>
+ Sign.print_ast_translation
+ [(@{const_syntax Char}, K char_ast_tr'),
+ (@{syntax_const "_list"}, K list_ast_tr')];
end;
--- a/src/HOL/Typerep.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Typerep.thy Sat May 25 15:37:53 2013 +0200
@@ -21,24 +21,24 @@
"_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))")
parse_translation {*
-let
- fun typerep_tr (*"_TYPEREP"*) [ty] =
- Syntax.const @{const_syntax typerep} $
- (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
- (Syntax.const @{type_syntax itself} $ ty))
- | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
-in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
+ let
+ fun typerep_tr (*"_TYPEREP"*) [ty] =
+ Syntax.const @{const_syntax typerep} $
+ (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
+ (Syntax.const @{type_syntax itself} $ ty))
+ | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
+ in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end
*}
-typed_print_translation (advanced) {*
-let
- fun typerep_tr' ctxt (*"typerep"*)
- (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
- (Const (@{const_syntax TYPE}, _) :: ts) =
- Term.list_comb
- (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
- | typerep_tr' _ T ts = raise Match;
-in [(@{const_syntax typerep}, typerep_tr')] end
+typed_print_translation {*
+ let
+ fun typerep_tr' ctxt (*"typerep"*)
+ (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
+ (Const (@{const_syntax TYPE}, _) :: ts) =
+ Term.list_comb
+ (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
+ | typerep_tr' _ T ts = raise Match;
+ in [(@{const_syntax typerep}, typerep_tr')] end
*}
setup {*
--- a/src/HOL/ex/Binary.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/ex/Binary.thy Sat May 25 15:37:53 2013 +0200
@@ -85,7 +85,7 @@
shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True"
and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False"
by simp_all
-
+
lemma binary_less:
fixes n :: nat
shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False"
@@ -191,19 +191,19 @@
"_Binary" :: "num_const \<Rightarrow> 'a" ("$_")
parse_translation {*
-let
- val syntax_consts =
- map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
+ let
+ val syntax_consts =
+ map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
- fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
- | binary_tr [Const (num, _)] =
- let
- val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
- val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
- in syntax_consts (mk_binary n) end
- | binary_tr ts = raise TERM ("binary_tr", ts);
+ fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
+ | binary_tr [Const (num, _)] =
+ let
+ val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
+ val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
+ in syntax_consts (mk_binary n) end
+ | binary_tr ts = raise TERM ("binary_tr", ts);
-in [(@{syntax_const "_Binary"}, binary_tr)] end
+ in [(@{syntax_const "_Binary"}, K binary_tr)] end
*}
--- a/src/HOL/ex/Multiquote.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/ex/Multiquote.thy Sat May 25 15:37:53 2013 +0200
@@ -32,7 +32,7 @@
fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
| quote_tr ts = raise TERM ("quote_tr", ts);
- in [(@{syntax_const "_quote"}, quote_tr)] end
+ in [(@{syntax_const "_quote"}, K quote_tr)] end
*}
text {* basic examples *}
--- a/src/HOL/ex/Numeral_Representation.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/ex/Numeral_Representation.thy Sat May 25 15:37:53 2013 +0200
@@ -277,42 +277,42 @@
"_Numerals" :: "xnum_token \<Rightarrow> 'a" ("_")
parse_translation {*
-let
- fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
- of (0, 1) => Const (@{const_name One}, dummyT)
- | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
- | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
- else raise Match;
- fun numeral_tr [Free (num, _)] =
- let
- val {leading_zeros, value, ...} = Lexicon.read_xnum num;
- val _ = leading_zeros = 0 andalso value > 0
- orelse error ("Bad numeral: " ^ num);
- in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
- | numeral_tr ts = raise TERM ("numeral_tr", ts);
-in [(@{syntax_const "_Numerals"}, numeral_tr)] end
+ let
+ fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
+ of (0, 1) => Const (@{const_name One}, dummyT)
+ | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
+ | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
+ else raise Match;
+ fun numeral_tr [Free (num, _)] =
+ let
+ val {leading_zeros, value, ...} = Lexicon.read_xnum num;
+ val _ = leading_zeros = 0 andalso value > 0
+ orelse error ("Bad numeral: " ^ num);
+ in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
+ | numeral_tr ts = raise TERM ("numeral_tr", ts);
+ in [(@{syntax_const "_Numerals"}, K numeral_tr)] end
*}
-typed_print_translation (advanced) {*
-let
- fun dig b n = b + 2 * n;
- fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
- dig 0 (int_of_num' n)
- | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
- dig 1 (int_of_num' n)
- | int_of_num' (Const (@{const_syntax One}, _)) = 1;
- fun num_tr' ctxt T [n] =
- let
- val k = int_of_num' n;
- val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
- in
- case T of
- Type (@{type_name fun}, [_, T']) =>
- if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
- else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
- | T' => if T' = dummyT then t' else raise Match
- end;
-in [(@{const_syntax of_num}, num_tr')] end
+typed_print_translation {*
+ let
+ fun dig b n = b + 2 * n;
+ fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
+ dig 0 (int_of_num' n)
+ | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
+ dig 1 (int_of_num' n)
+ | int_of_num' (Const (@{const_syntax One}, _)) = 1;
+ fun num_tr' ctxt T [n] =
+ let
+ val k = int_of_num' n;
+ val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
+ in
+ case T of
+ Type (@{type_name fun}, [_, T']) =>
+ if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
+ else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
+ | T' => if T' = dummyT then t' else raise Match
+ end;
+ in [(@{const_syntax of_num}, num_tr')] end
*}
--- a/src/Pure/Isar/expression.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Isar/expression.ML Sat May 25 15:37:53 2013 +0200
@@ -622,7 +622,7 @@
fun aprop_tr' n c =
let
val c' = Lexicon.mark_const c;
- fun tr' T args =
+ fun tr' (_: Proof.context) T args =
if T <> dummyT andalso length args = n
then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args)
else raise Match;
@@ -656,7 +656,7 @@
val ([pred_def], defs_thy) =
thy
- |> bodyT = propT ? Sign.add_trfunsT [aprop_tr' (length args) name]
+ |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
|> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
|> Global_Theory.add_defs false
[((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
--- a/src/Pure/Isar/isar_cmd.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sat May 25 15:37:53 2013 +0200
@@ -8,11 +8,11 @@
sig
val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
- val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
- val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
- val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
- val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
- val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+ val parse_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
+ val parse_translation: Symbol_Pos.text * Position.T -> theory -> theory
+ val print_translation: Symbol_Pos.text * Position.T -> theory -> theory
+ val typed_print_translation: Symbol_Pos.text * Position.T -> theory -> theory
+ val print_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
val translations: (xstring * string) Syntax.trrule list -> theory -> theory
val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
@@ -85,57 +85,41 @@
(* translation functions *)
-local
-
-fun advancedT false = ""
- | advancedT true = "Proof.context -> ";
-
-fun advancedN false = ""
- | advancedN true = "advanced_";
-
-in
-
-fun parse_ast_translation (a, (txt, pos)) =
+fun parse_ast_translation (txt, pos) =
ML_Lex.read pos txt
|> ML_Context.expression pos
- ("val parse_ast_translation: (string * (" ^ advancedT a ^
- "Ast.ast list -> Ast.ast)) list")
- ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
+ "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
+ "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
|> Context.theory_map;
-fun parse_translation (a, (txt, pos)) =
+fun parse_translation (txt, pos) =
+ ML_Lex.read pos txt
+ |> ML_Context.expression pos
+ "val parse_translation: (string * (Proof.context -> term list -> term)) list"
+ "Context.map_theory (Sign.parse_translation parse_translation)"
+ |> Context.theory_map;
+
+fun print_translation (txt, pos) =
ML_Lex.read pos txt
|> ML_Context.expression pos
- ("val parse_translation: (string * (" ^ advancedT a ^
- "term list -> term)) list")
- ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
- |> Context.theory_map;
-
-fun print_translation (a, (txt, pos)) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos
- ("val print_translation: (string * (" ^ advancedT a ^
- "term list -> term)) list")
- ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
+ "val print_translation: (string * (Proof.context -> term list -> term)) list"
+ "Context.map_theory (Sign.print_translation print_translation)"
|> Context.theory_map;
-fun print_ast_translation (a, (txt, pos)) =
+fun typed_print_translation (txt, pos) =
ML_Lex.read pos txt
|> ML_Context.expression pos
- ("val print_ast_translation: (string * (" ^ advancedT a ^
- "Ast.ast list -> Ast.ast)) list")
- ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
+ "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
+ "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
|> Context.theory_map;
-fun typed_print_translation (a, (txt, pos)) =
+fun print_ast_translation (txt, pos) =
ML_Lex.read pos txt
|> ML_Context.expression pos
- ("val typed_print_translation: (string * (" ^ advancedT a ^ "typ -> term list -> term)) list")
- ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
+ "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
+ "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
|> Context.theory_map;
-end;
-
(* translation rules *)
--- a/src/Pure/Isar/isar_syn.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sat May 25 15:37:53 2013 +0200
@@ -323,32 +323,30 @@
(* translation functions *)
-val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
-
val _ =
Outer_Syntax.command @{command_spec "parse_ast_translation"}
"install parse ast translation functions"
- (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
+ (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
val _ =
Outer_Syntax.command @{command_spec "parse_translation"}
"install parse translation functions"
- (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
+ (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
val _ =
Outer_Syntax.command @{command_spec "print_translation"}
"install print translation functions"
- (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
+ (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
val _ =
Outer_Syntax.command @{command_spec "typed_print_translation"}
"install typed print translation functions"
- (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
+ (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
val _ =
Outer_Syntax.command @{command_spec "print_ast_translation"}
"install print ast translation functions"
- (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
+ (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
(* oracles *)
--- a/src/Pure/Pure.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Pure.thy Sat May 25 15:37:53 2013 +0200
@@ -8,7 +8,7 @@
keywords
"!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="
"=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>"
- "\<rightleftharpoons>" "\<subseteq>" "]" "advanced" "and" "assumes"
+ "\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes"
"attach" "begin" "binder" "constrains" "defines" "fixes" "for"
"identifier" "if" "imports" "in" "includes" "infix" "infixl"
"infixr" "is" "keywords" "notes" "obtains" "open" "output"
--- a/src/Pure/Syntax/local_syntax.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Syntax/local_syntax.ML Sat May 25 15:37:53 2013 +0200
@@ -59,11 +59,10 @@
| update_gram ((false, add, m), decls) =
Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
- val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs;
val local_syntax = thy_syntax
|> Syntax.update_trfuns
- (map Syntax_Ext.mk_trfun atrs, map Syntax_Ext.mk_trfun trs,
- map Syntax_Ext.mk_trfun trs', map Syntax_Ext.mk_trfun atrs')
+ ([], map Syntax_Ext.mk_trfun (Syntax_Trans.struct_parse_translation structs),
+ [], map Syntax_Ext.mk_trfun (Syntax_Trans.struct_print_ast_translation structs))
|> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
--- a/src/Pure/Syntax/mixfix.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Syntax/mixfix.ML Sat May 25 15:37:53 2013 +0200
@@ -145,10 +145,10 @@
val mfix = maps mfix_of const_decls;
val binders = map_filter binder const_decls;
val binder_trs = binders
- |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
+ |> map (Syntax_Ext.stamp_trfun binder_stamp o Syntax_Trans.mk_binder_tr);
val binder_trs' = binders
|> map (Syntax_Ext.stamp_trfun binder_stamp o
- apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
+ apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap);
val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
in
--- a/src/Pure/Syntax/syntax.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Syntax/syntax.ML Sat May 25 15:37:53 2013 +0200
@@ -103,11 +103,6 @@
Parse_Print_Rule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
val update_trfuns:
- (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
- (string * ((term list -> term) * stamp)) list *
- (string * ((typ -> term list -> term) * stamp)) list *
- (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
- val update_advanced_trfuns:
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((Proof.context -> term list -> term) * stamp)) list *
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
@@ -651,10 +646,7 @@
(** modify syntax **)
-fun ext_syntax f decls = update_syntax mode_default (f decls);
-
-val update_trfuns = ext_syntax Syntax_Ext.syn_ext_trfuns;
-val update_advanced_trfuns = ext_syntax Syntax_Ext.syn_ext_advanced_trfuns;
+val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns;
fun update_type_gram add prmode decls =
(if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
@@ -662,7 +654,7 @@
fun update_const_gram add is_logtype prmode decls =
(if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
-val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
+val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
--- a/src/Pure/Syntax/syntax_ext.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Sat May 25 15:37:53 2013 +0200
@@ -45,11 +45,6 @@
(Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
val syn_ext_trfuns:
- (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
- (string * ((term list -> term) * stamp)) list *
- (string * ((typ -> term list -> term) * stamp)) list *
- (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
- val syn_ext_advanced_trfuns:
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((Proof.context -> term list -> term) * stamp)) list *
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
@@ -319,12 +314,7 @@
val syn_ext = syn_ext' (K false);
fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
-fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
-
-fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
- let fun simple (name, (f, s)) = (name, (K f, s)) in
- syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
- end;
+fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []);
fun stamp_trfun s (c, f) = (c, (f, s));
fun mk_trfun tr = stamp_trfun (stamp ()) tr;
--- a/src/Pure/Syntax/syntax_phases.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Sat May 25 15:37:53 2013 +0200
@@ -751,10 +751,10 @@
(* setup translations *)
val _ = Context.>> (Context.map_theory
- (Sign.add_advanced_trfuns
- ([("_context_const", const_ast_tr true),
- ("_context_xconst", const_ast_tr false)], [], [], []) #>
- Sign.add_advanced_trfunsT
+ (Sign.parse_ast_translation
+ [("_context_const", const_ast_tr true),
+ ("_context_xconst", const_ast_tr false)] #>
+ Sign.typed_print_translation
[("_type_prop", type_prop_tr'),
("\\<^const>TYPE", type_tr'),
("_type_constraint_", type_constraint_tr')]));
--- a/src/Pure/Syntax/syntax_trans.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Sat May 25 15:37:53 2013 +0200
@@ -19,12 +19,13 @@
val no_type_bracketsN: string
val no_type_brackets: unit -> bool
val abs_tr: term list -> term
- val mk_binder_tr: string * string -> string * (term list -> term)
+ val mk_binder_tr: string * string -> string * (Proof.context -> term list -> term)
val antiquote_tr: string -> term -> term
val quote_tr: string -> term -> term
- val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
- val non_typed_tr': (term list -> term) -> typ -> term list -> term
- val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
+ val quote_antiquote_tr: string -> string -> string ->
+ string * (Proof.context -> term list -> term)
+ val non_typed_tr': (Proof.context -> term list -> term) ->
+ Proof.context -> typ -> term list -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
@@ -35,27 +36,25 @@
val abs_tr': Proof.context -> term -> term
val atomic_abs_tr': string * typ * term -> term * term
val const_abs_tr': term -> term
- val mk_binder_tr': string * string -> string * (term list -> term)
- val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
- val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
+ val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
+ val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
+ val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
val prop_tr': term -> term
val variant_abs: string * typ * term -> string * term
val variant_abs': string * typ * term -> string * term
val dependent_tr': string * string -> term list -> term
val antiquote_tr': string -> term -> term
val quote_tr': string -> term -> term
- val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
+ val quote_antiquote_tr': string -> string -> string ->
+ string * (Proof.context -> term list -> term)
val update_name_tr': term -> term
- val pure_trfuns:
- (string * (Ast.ast list -> Ast.ast)) list *
- (string * (term list -> term)) list *
- (string * (term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list
- val struct_trfuns: string list ->
- (string * (Ast.ast list -> Ast.ast)) list *
- (string * (term list -> term)) list *
- (string * (typ -> term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list
+ val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
+ val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
+ val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
+ val struct_parse_translation: string list ->
+ (string * (Proof.context -> term list -> term)) list
+ val struct_print_ast_translation: string list ->
+ (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
end;
structure Syntax_Trans: SYNTAX_TRANS =
@@ -152,7 +151,7 @@
let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
in Syntax.const name $ abs end
| binder_tr ts = err ts;
- in (syn, binder_tr) end;
+ in (syn, fn _ => binder_tr) end;
(* type propositions *)
@@ -214,7 +213,7 @@
let
fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
| tr ts = raise TERM ("quote_tr", ts);
- in (quoteN, tr) end;
+ in (quoteN, fn _ => tr) end;
(* corresponding updates *)
@@ -259,8 +258,7 @@
(* types *)
-fun non_typed_tr' f _ ts = f ts;
-fun non_typed_tr'' f x _ ts = f x ts;
+fun non_typed_tr' f ctxt _ ts = f ctxt ts;
(* type syntax *)
@@ -366,13 +364,13 @@
fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
| binder_tr' [] = raise Match;
- in (name, binder_tr') end;
+ in (name, fn _ => binder_tr') end;
-fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
+fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts =>
let val (x, t) = atomic_abs_tr' abs
in list_comb (Syntax.const syn $ x $ t, ts) end);
-fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
+fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
let val (x, t) = atomic_abs_tr' abs
in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
@@ -464,7 +462,7 @@
let
fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
| tr' _ = raise Match;
- in (name, tr') end;
+ in (name, fn _ => tr') end;
(* corresponding updates *)
@@ -503,39 +501,42 @@
(** Pure translations **)
-val pure_trfuns =
- ([("_strip_positions", strip_positions_ast_tr),
- ("_constify", constify_ast_tr),
- ("_tapp", tapp_ast_tr),
- ("_tappl", tappl_ast_tr),
- ("_bracket", bracket_ast_tr),
- ("_appl", appl_ast_tr),
- ("_applC", applC_ast_tr),
- ("_lambda", lambda_ast_tr),
- ("_idtyp", idtyp_ast_tr),
- ("_idtypdummy", idtypdummy_ast_tr),
- ("_bigimpl", bigimpl_ast_tr),
- ("_indexdefault", indexdefault_ast_tr),
- ("_indexvar", indexvar_ast_tr),
- ("_struct", struct_ast_tr)],
- [("_abs", abs_tr),
- ("_aprop", aprop_tr),
- ("_ofclass", ofclass_tr),
- ("_sort_constraint", sort_constraint_tr),
- ("_TYPE", type_tr),
- ("_DDDOT", dddot_tr),
- ("_update_name", update_name_tr),
- ("_index", index_tr)],
- ([]: (string * (term list -> term)) list),
- [("\\<^type>fun", fun_ast_tr'),
- ("_abs", abs_ast_tr'),
- ("_idts", idtyp_ast_tr' "_idts"),
- ("_pttrns", idtyp_ast_tr' "_pttrns"),
- ("\\<^const>==>", impl_ast_tr'),
- ("_index", index_ast_tr')]);
+val pure_parse_ast_translation =
+ [("_strip_positions", fn _ => strip_positions_ast_tr),
+ ("_constify", fn _ => constify_ast_tr),
+ ("_tapp", fn _ => tapp_ast_tr),
+ ("_tappl", fn _ => tappl_ast_tr),
+ ("_bracket", fn _ => bracket_ast_tr),
+ ("_appl", fn _ => appl_ast_tr),
+ ("_applC", fn _ => applC_ast_tr),
+ ("_lambda", fn _ => lambda_ast_tr),
+ ("_idtyp", fn _ => idtyp_ast_tr),
+ ("_idtypdummy", fn _ => idtypdummy_ast_tr),
+ ("_bigimpl", fn _ => bigimpl_ast_tr),
+ ("_indexdefault", fn _ => indexdefault_ast_tr),
+ ("_indexvar", fn _ => indexvar_ast_tr),
+ ("_struct", fn _ => struct_ast_tr)];
-fun struct_trfuns structs =
- ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
+val pure_parse_translation =
+ [("_abs", fn _ => abs_tr),
+ ("_aprop", fn _ => aprop_tr),
+ ("_ofclass", fn _ => ofclass_tr),
+ ("_sort_constraint", fn _ => sort_constraint_tr),
+ ("_TYPE", fn _ => type_tr),
+ ("_DDDOT", fn _ => dddot_tr),
+ ("_update_name", fn _ => update_name_tr),
+ ("_index", fn _ => index_tr)];
+
+val pure_print_ast_translation =
+ [("\\<^type>fun", fn _ => fun_ast_tr'),
+ ("_abs", fn _ => abs_ast_tr'),
+ ("_idts", fn _ => idtyp_ast_tr' "_idts"),
+ ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
+ ("\\<^const>==>", fn _ => impl_ast_tr'),
+ ("_index", fn _ => index_ast_tr')];
+
+fun struct_parse_translation structs = [("_struct", fn _ => struct_tr structs)];
+fun struct_print_ast_translation structs = [("_struct", fn _ => struct_ast_tr' structs)];
end;
--- a/src/Pure/pure_thy.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/pure_thy.ML Sat May 25 15:37:53 2013 +0200
@@ -189,7 +189,9 @@
#> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
#> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
#> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
- #> Sign.add_trfuns Syntax_Trans.pure_trfuns
+ #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
+ #> Sign.parse_translation Syntax_Trans.pure_parse_translation
+ #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
#> Sign.local_path
#> Sign.add_consts_i
[(Binding.name "term", typ "'a => prop", NoSyn),
--- a/src/Pure/sign.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/sign.ML Sat May 25 15:37:53 2013 +0200
@@ -87,19 +87,16 @@
val primitive_class: binding * class list -> theory -> theory
val primitive_classrel: class * class -> theory -> theory
val primitive_arity: arity -> theory -> theory
- val add_trfuns:
- (string * (Ast.ast list -> Ast.ast)) list *
- (string * (term list -> term)) list *
- (string * (term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
- val add_trfunsT: (string * (typ -> term list -> term)) list -> theory -> theory
- val add_advanced_trfuns:
- (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
- (string * (Proof.context -> term list -> term)) list *
- (string * (Proof.context -> term list -> term)) list *
+ val parse_ast_translation:
(string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
- val add_advanced_trfunsT:
+ val parse_translation:
+ (string * (Proof.context -> term list -> term)) list -> theory -> theory
+ val print_translation:
+ (string * (Proof.context -> term list -> term)) list -> theory -> theory
+ val typed_print_translation:
(string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
+ val print_ast_translation:
+ (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
val new_group: theory -> theory
@@ -466,17 +463,14 @@
fun mk trs = map Syntax_Ext.mk_trfun trs;
-fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) =
- map_syn (ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's));
-
-fun gen_add_trfunsT ext tr's = map_syn (ext ([], [], mk tr's, []));
-
in
-val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax_Trans.non_typed_tr';
-val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
-val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax_Trans.non_typed_tr'';
-val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
+fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], []));
+fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], []));
+fun print_translation tr's =
+ map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), []));
+fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, []));
+fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's));
end;
--- a/src/Sequents/ILL.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/ILL.thy Sat May 25 15:37:53 2013 +0200
@@ -36,15 +36,15 @@
"_PromAux" :: "three_seqe" ("promaux {_||_||_}")
parse_translation {*
- [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
- (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
- (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
+ [(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})),
+ (@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})),
+ (@{syntax_const "_PromAux"}, K (three_seq_tr @{const_syntax PromAux}))]
*}
print_translation {*
- [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
- (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
- (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
+ [(@{const_syntax Trueprop}, K (single_tr' @{syntax_const "_Trueprop"})),
+ (@{const_syntax Context}, K (two_seq_tr' @{syntax_const "_Context"})),
+ (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
*}
defs
--- a/src/Sequents/LK0.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/LK0.thy Sat May 25 15:37:53 2013 +0200
@@ -34,8 +34,8 @@
syntax
"_Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
-parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
-print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
+parse_translation {* [(@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))] *}
+print_translation {* [(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))] *}
abbreviation
not_equal (infixl "~=" 50) where
--- a/src/Sequents/Modal0.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/Modal0.thy Sat May 25 15:37:53 2013 +0200
@@ -27,13 +27,13 @@
*}
parse_translation {*
- [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
- (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
+ [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
+ (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
*}
print_translation {*
- [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
- (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
+ [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
+ (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
*}
defs
--- a/src/Sequents/S43.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/S43.thy Sat May 25 15:37:53 2013 +0200
@@ -21,7 +21,7 @@
val tr = seq_tr;
fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
- in [(@{syntax_const "_S43pi"}, s43pi_tr)] end
+ in [(@{syntax_const "_S43pi"}, K s43pi_tr)] end
*}
print_translation {*
@@ -29,7 +29,7 @@
val tr' = seq_tr';
fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
-in [(@{const_syntax S43pi}, s43pi_tr')] end
+in [(@{const_syntax S43pi}, K s43pi_tr')] end
*}
axiomatization where
--- a/src/Sequents/Sequents.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/Sequents.thy Sat May 25 15:37:53 2013 +0200
@@ -139,7 +139,7 @@
fun side_tr [s1] = seq_tr s1;
*}
-parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
+parse_translation {* [(@{syntax_const "_Side"}, K side_tr)] *}
ML_file "prover.ML"
--- a/src/ZF/Tools/numeral_syntax.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML Sat May 25 15:37:53 2013 +0200
@@ -79,6 +79,7 @@
val setup =
- Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [(@{const_syntax integ_of}, int_tr')], []);
+ Sign.parse_translation [(@{syntax_const "_Int"}, K int_tr)] #>
+ Sign.print_translation [(@{const_syntax integ_of}, K int_tr')];
end;