1.1 --- a/NEWS Sat May 25 15:00:53 2013 +0200
1.2 +++ b/NEWS Sat May 25 15:37:53 2013 +0200
1.3 @@ -40,6 +40,10 @@
1.4
1.5 *** Pure ***
1.6
1.7 +* Syntax translation functions (print_translation etc.) always depend
1.8 +on Proof.context. Discontinued former "(advanced)" option -- this is
1.9 +now the default. Minor INCOMPATIBILITY.
1.10 +
1.11 * Target-sensitive commands 'interpretation' and 'sublocale'.
1.12 Particulary, 'interpretation' now allows for non-persistent
1.13 interpretation within "context ... begin ... end" blocks.
2.1 --- a/etc/isar-keywords-ZF.el Sat May 25 15:00:53 2013 +0200
2.2 +++ b/etc/isar-keywords-ZF.el Sat May 25 15:37:53 2013 +0200
2.3 @@ -209,8 +209,7 @@
2.4 "}"))
2.5
2.6 (defconst isar-keywords-minor
2.7 - '("advanced"
2.8 - "and"
2.9 + '("and"
2.10 "assumes"
2.11 "attach"
2.12 "begin"
3.1 --- a/etc/isar-keywords.el Sat May 25 15:00:53 2013 +0200
3.2 +++ b/etc/isar-keywords.el Sat May 25 15:37:53 2013 +0200
3.3 @@ -303,8 +303,7 @@
3.4 "}"))
3.5
3.6 (defconst isar-keywords-minor
3.7 - '("advanced"
3.8 - "and"
3.9 + '("and"
3.10 "assumes"
3.11 "attach"
3.12 "avoids"
4.1 --- a/src/CCL/Term.thy Sat May 25 15:00:53 2013 +0200
4.2 +++ b/src/CCL/Term.thy Sat May 25 15:37:53 2013 +0200
4.3 @@ -95,17 +95,17 @@
4.4 *}
4.5
4.6 parse_translation {*
4.7 - [(@{syntax_const "_let"}, let_tr),
4.8 - (@{syntax_const "_letrec"}, letrec_tr),
4.9 - (@{syntax_const "_letrec2"}, letrec2_tr),
4.10 - (@{syntax_const "_letrec3"}, letrec3_tr)]
4.11 + [(@{syntax_const "_let"}, K let_tr),
4.12 + (@{syntax_const "_letrec"}, K letrec_tr),
4.13 + (@{syntax_const "_letrec2"}, K letrec2_tr),
4.14 + (@{syntax_const "_letrec3"}, K letrec3_tr)]
4.15 *}
4.16
4.17 print_translation {*
4.18 - [(@{const_syntax let}, let_tr'),
4.19 - (@{const_syntax letrec}, letrec_tr'),
4.20 - (@{const_syntax letrec2}, letrec2_tr'),
4.21 - (@{const_syntax letrec3}, letrec3_tr')]
4.22 + [(@{const_syntax let}, K let_tr'),
4.23 + (@{const_syntax letrec}, K letrec_tr'),
4.24 + (@{const_syntax letrec2}, K letrec2_tr'),
4.25 + (@{const_syntax letrec3}, K letrec3_tr')]
4.26 *}
4.27
4.28 consts
5.1 --- a/src/CCL/Type.thy Sat May 25 15:00:53 2013 +0200
5.2 +++ b/src/CCL/Type.thy Sat May 25 15:37:53 2013 +0200
5.3 @@ -47,9 +47,9 @@
5.4
5.5 print_translation {*
5.6 [(@{const_syntax Pi},
5.7 - Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
5.8 + fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
5.9 (@{const_syntax Sigma},
5.10 - Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
5.11 + fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
5.12 *}
5.13
5.14 defs
6.1 --- a/src/Cube/Cube.thy Sat May 25 15:00:53 2013 +0200
6.2 +++ b/src/Cube/Cube.thy Sat May 25 15:37:53 2013 +0200
6.3 @@ -63,7 +63,7 @@
6.4
6.5 print_translation {*
6.6 [(@{const_syntax Prod},
6.7 - Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
6.8 + fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
6.9 *}
6.10
6.11 axiomatization where
7.1 --- a/src/Doc/Classes/Setup.thy Sat May 25 15:00:53 2013 +0200
7.2 +++ b/src/Doc/Classes/Setup.thy Sat May 25 15:37:53 2013 +0200
7.3 @@ -30,10 +30,10 @@
7.4 Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
7.5 | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
7.6 in
7.7 - [(@{syntax_const "_alpha"}, alpha_ast_tr),
7.8 - (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
7.9 - (@{syntax_const "_beta"}, beta_ast_tr),
7.10 - (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
7.11 + [(@{syntax_const "_alpha"}, K alpha_ast_tr),
7.12 + (@{syntax_const "_alpha_ofsort"}, K alpha_ofsort_ast_tr),
7.13 + (@{syntax_const "_beta"}, K beta_ast_tr),
7.14 + (@{syntax_const "_beta_ofsort"}, K beta_ofsort_ast_tr)]
7.15 end
7.16 *}
7.17
8.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy Sat May 25 15:00:53 2013 +0200
8.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy Sat May 25 15:37:53 2013 +0200
8.3 @@ -1469,7 +1469,7 @@
8.4 @{rail "
8.5 ( @@{command parse_ast_translation} | @@{command parse_translation} |
8.6 @@{command print_translation} | @@{command typed_print_translation} |
8.7 - @@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text}
8.8 + @@{command print_ast_translation}) @{syntax text}
8.9 ;
8.10 (@@{ML_antiquotation class_syntax} |
8.11 @@{ML_antiquotation type_syntax} |
8.12 @@ -1486,31 +1486,31 @@
8.13
8.14 \medskip
8.15 {\footnotesize
8.16 - \begin{tabular}{ll}
8.17 - @{command parse_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
8.18 - @{command parse_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
8.19 - @{command print_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
8.20 - @{command typed_print_translation} & : @{ML_type "(string * (typ -> term list -> term)) list"} \\
8.21 - @{command print_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
8.22 + \begin{tabular}{l}
8.23 + @{command parse_ast_translation} : \\
8.24 + \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
8.25 + @{command parse_translation} : \\
8.26 + \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
8.27 + @{command print_translation} : \\
8.28 + \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
8.29 + @{command typed_print_translation} : \\
8.30 + \quad @{ML_type "(string * (Proof.context -> typ -> term list -> term)) list"} \\
8.31 + @{command print_ast_translation} : \\
8.32 + \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
8.33 \end{tabular}}
8.34 \medskip
8.35
8.36 The argument list consists of @{text "(c, tr)"} pairs, where @{text
8.37 "c"} is the syntax name of the formal entity involved, and @{text
8.38 "tr"} a function that translates a syntax form @{text "c args"} into
8.39 - @{text "tr args"}. The ML naming convention for parse translations
8.40 - is @{text "c_tr"} and for print translations @{text "c_tr'"}.
8.41 + @{text "tr ctxt args"} (depending on the context). The ML naming
8.42 + convention for parse translations is @{text "c_tr"} and for print
8.43 + translations @{text "c_tr'"}.
8.44
8.45 The @{command_ref print_syntax} command displays the sets of names
8.46 associated with the translation functions of a theory under @{text
8.47 "parse_ast_translation"} etc.
8.48
8.49 - If the @{verbatim "("}@{keyword "advanced"}@{verbatim ")"} option is
8.50 - given, the corresponding translation functions depend on the current
8.51 - theory or proof context as additional argument. This allows to
8.52 - implement advanced syntax mechanisms, as translations functions may
8.53 - refer to specific theory declarations or auxiliary proof data.
8.54 -
8.55 \item @{text "@{class_syntax c}"}, @{text "@{type_syntax c}"},
8.56 @{text "@{const_syntax c}"} inline the authentic syntax name of the
8.57 given formal entities into the ML source. This is the
9.1 --- a/src/FOLP/IFOLP.thy Sat May 25 15:00:53 2013 +0200
9.2 +++ b/src/FOLP/IFOLP.thy Sat May 25 15:37:53 2013 +0200
9.3 @@ -66,13 +66,13 @@
9.4
9.5 parse_translation {*
9.6 let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p
9.7 - in [(@{syntax_const "_Proof"}, proof_tr)] end
9.8 + in [(@{syntax_const "_Proof"}, K proof_tr)] end
9.9 *}
9.10
9.11 (*show_proofs = true displays the proof terms -- they are ENORMOUS*)
9.12 ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *}
9.13
9.14 -print_translation (advanced) {*
9.15 +print_translation {*
9.16 let
9.17 fun proof_tr' ctxt [P, p] =
9.18 if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
10.1 --- a/src/HOL/Big_Operators.thy Sat May 25 15:00:53 2013 +0200
10.2 +++ b/src/HOL/Big_Operators.thy Sat May 25 15:37:53 2013 +0200
10.3 @@ -370,7 +370,7 @@
10.4 Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
10.5 end
10.6 | setsum_tr' _ = raise Match;
10.7 -in [(@{const_syntax setsum}, setsum_tr')] end
10.8 +in [(@{const_syntax setsum}, K setsum_tr')] end
10.9 *}
10.10
10.11 text {* TODO These are candidates for generalization *}
11.1 --- a/src/HOL/Code_Evaluation.thy Sat May 25 15:00:53 2013 +0200
11.2 +++ b/src/HOL/Code_Evaluation.thy Sat May 25 15:37:53 2013 +0200
11.3 @@ -144,15 +144,15 @@
11.4 subsubsection {* Obfuscation *}
11.5
11.6 print_translation {*
11.7 -let
11.8 - val term = Const ("<TERM>", dummyT);
11.9 - fun tr1' [_, _] = term;
11.10 - fun tr2' [] = term;
11.11 -in
11.12 - [(@{const_syntax Const}, tr1'),
11.13 + let
11.14 + val term = Const ("<TERM>", dummyT);
11.15 + fun tr1' _ [_, _] = term;
11.16 + fun tr2' _ [] = term;
11.17 + in
11.18 + [(@{const_syntax Const}, tr1'),
11.19 (@{const_syntax App}, tr1'),
11.20 (@{const_syntax dummy_term}, tr2')]
11.21 -end
11.22 + end
11.23 *}
11.24
11.25
12.1 --- a/src/HOL/Groups.thy Sat May 25 15:00:53 2013 +0200
12.2 +++ b/src/HOL/Groups.thy Sat May 25 15:37:53 2013 +0200
12.3 @@ -121,7 +121,7 @@
12.4 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
12.5 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
12.6
12.7 -typed_print_translation (advanced) {*
12.8 +typed_print_translation {*
12.9 let
12.10 fun tr' c = (c, fn ctxt => fn T => fn ts =>
12.11 if not (null ts) orelse T = dummyT orelse
13.1 --- a/src/HOL/HOL.thy Sat May 25 15:00:53 2013 +0200
13.2 +++ b/src/HOL/HOL.thy Sat May 25 15:37:53 2013 +0200
13.3 @@ -116,7 +116,7 @@
13.4 syntax "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10)
13.5 translations "THE x. P" == "CONST The (%x. P)"
13.6 print_translation {*
13.7 - [(@{const_syntax The}, fn [Abs abs] =>
13.8 + [(@{const_syntax The}, fn _ => fn [Abs abs] =>
13.9 let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
13.10 in Syntax.const @{syntax_const "_The"} $ x $ t end)]
13.11 *} -- {* To avoid eta-contraction of body *}
14.1 --- a/src/HOL/HOLCF/Cfun.thy Sat May 25 15:00:53 2013 +0200
14.2 +++ b/src/HOL/HOLCF/Cfun.thy Sat May 25 15:37:53 2013 +0200
14.3 @@ -40,7 +40,7 @@
14.4 *}
14.5
14.6 print_translation {*
14.7 - [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
14.8 + [(@{const_syntax Abs_cfun}, fn _ => fn [Abs abs] =>
14.9 let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
14.10 in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
14.11 *} -- {* To avoid eta-contraction of body *}
14.12 @@ -61,7 +61,7 @@
14.13 Ast.fold_ast_p @{syntax_const "_cabs"}
14.14 (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
14.15 | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
14.16 - in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
14.17 + in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end;
14.18 *}
14.19
14.20 print_ast_translation {*
14.21 @@ -75,7 +75,7 @@
14.22 | (xs, body) => Ast.Appl
14.23 [Ast.Constant @{syntax_const "_Lambda"},
14.24 Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
14.25 - in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
14.26 + in [(@{syntax_const "_cabs"}, K cabs_ast_tr')] end
14.27 *}
14.28
14.29 text {* Dummy patterns for continuous abstraction *}
15.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sat May 25 15:00:53 2013 +0200
15.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sat May 25 15:37:53 2013 +0200
15.3 @@ -131,7 +131,7 @@
15.4 parse_translation {*
15.5 (* rewrite (_pat x) => (succeed) *)
15.6 (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
15.7 - [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
15.8 + [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
15.9 Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
15.10 *}
15.11
15.12 @@ -164,7 +164,7 @@
15.13 (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
15.14 end;
15.15
15.16 - in [(@{const_syntax Rep_cfun}, Case1_tr')] end;
15.17 + in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
15.18 *}
15.19
15.20 translations
16.1 --- a/src/HOL/Hilbert_Choice.thy Sat May 25 15:00:53 2013 +0200
16.2 +++ b/src/HOL/Hilbert_Choice.thy Sat May 25 15:37:53 2013 +0200
16.3 @@ -25,7 +25,7 @@
16.4 "SOME x. P" == "CONST Eps (%x. P)"
16.5
16.6 print_translation {*
16.7 - [(@{const_syntax Eps}, fn [Abs abs] =>
16.8 + [(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
16.9 let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
16.10 in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
16.11 *} -- {* to avoid eta-contraction of body *}
17.1 --- a/src/HOL/Hoare/Hoare_Logic.thy Sat May 25 15:00:53 2013 +0200
17.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy Sat May 25 15:37:53 2013 +0200
17.3 @@ -54,8 +54,8 @@
17.4 ("{_} // _ // {_}" [0,55,0] 50)
17.5
17.6 ML_file "hoare_syntax.ML"
17.7 -parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
17.8 -print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
17.9 +parse_translation {* [(@{syntax_const "_hoare_vars"}, K Hoare_Syntax.hoare_vars_tr)] *}
17.10 +print_translation {* [(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare"}))] *}
17.11
17.12
17.13 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
18.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat May 25 15:00:53 2013 +0200
18.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat May 25 15:37:53 2013 +0200
18.3 @@ -56,9 +56,9 @@
18.4 ("{_} // _ // {_}" [0,55,0] 50)
18.5
18.6 ML_file "hoare_syntax.ML"
18.7 -parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
18.8 +parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, K Hoare_Syntax.hoare_vars_tr)] *}
18.9 print_translation
18.10 - {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
18.11 + {* [(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"}))] *}
18.12
18.13
18.14 (*** The proof rules ***)
19.1 --- a/src/HOL/Hoare/Separation.thy Sat May 25 15:00:53 2013 +0200
19.2 +++ b/src/HOL/Hoare/Separation.thy Sat May 25 15:37:53 2013 +0200
19.3 @@ -77,10 +77,10 @@
19.4 *}
19.5
19.6 parse_translation {*
19.7 - [(@{syntax_const "_emp"}, emp_tr),
19.8 - (@{syntax_const "_singl"}, singl_tr),
19.9 - (@{syntax_const "_star"}, star_tr),
19.10 - (@{syntax_const "_wand"}, wand_tr)]
19.11 + [(@{syntax_const "_emp"}, K emp_tr),
19.12 + (@{syntax_const "_singl"}, K singl_tr),
19.13 + (@{syntax_const "_star"}, K star_tr),
19.14 + (@{syntax_const "_wand"}, K wand_tr)]
19.15 *}
19.16
19.17 text{* Now it looks much better: *}
19.18 @@ -128,10 +128,10 @@
19.19 *}
19.20
19.21 print_translation {*
19.22 - [(@{const_syntax is_empty}, is_empty_tr'),
19.23 - (@{const_syntax singl}, singl_tr'),
19.24 - (@{const_syntax star}, star_tr'),
19.25 - (@{const_syntax wand}, wand_tr')]
19.26 + [(@{const_syntax is_empty}, K is_empty_tr'),
19.27 + (@{const_syntax singl}, K singl_tr'),
19.28 + (@{const_syntax star}, K star_tr'),
19.29 + (@{const_syntax wand}, K wand_tr')]
19.30 *}
19.31
19.32 text{* Now the intermediate proof states are also readable: *}
20.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat May 25 15:00:53 2013 +0200
20.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat May 25 15:37:53 2013 +0200
20.3 @@ -113,15 +113,15 @@
20.4
20.5 fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts;
20.6 in
20.7 - [(@{const_syntax Collect}, assert_tr'),
20.8 - (@{const_syntax Basic}, assign_tr'),
20.9 - (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
20.10 - (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"}),
20.11 - (@{const_syntax AnnBasic}, annassign_tr'),
20.12 - (@{const_syntax AnnWhile}, annbexp_tr' @{syntax_const "_AnnWhile"}),
20.13 - (@{const_syntax AnnAwait}, annbexp_tr' @{syntax_const "_AnnAwait"}),
20.14 - (@{const_syntax AnnCond1}, annbexp_tr' @{syntax_const "_AnnCond1"}),
20.15 - (@{const_syntax AnnCond2}, annbexp_tr' @{syntax_const "_AnnCond2"})]
20.16 + [(@{const_syntax Collect}, K assert_tr'),
20.17 + (@{const_syntax Basic}, K assign_tr'),
20.18 + (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
20.19 + (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"})),
20.20 + (@{const_syntax AnnBasic}, K annassign_tr'),
20.21 + (@{const_syntax AnnWhile}, K (annbexp_tr' @{syntax_const "_AnnWhile"})),
20.22 + (@{const_syntax AnnAwait}, K (annbexp_tr' @{syntax_const "_AnnAwait"})),
20.23 + (@{const_syntax AnnCond1}, K (annbexp_tr' @{syntax_const "_AnnCond1"})),
20.24 + (@{const_syntax AnnCond2}, K (annbexp_tr' @{syntax_const "_AnnCond2"}))]
20.25 end;
20.26 *}
20.27
21.1 --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Sat May 25 15:00:53 2013 +0200
21.2 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Sat May 25 15:37:53 2013 +0200
21.3 @@ -18,7 +18,7 @@
21.4 let
21.5 fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
21.6 | quote_tr ts = raise TERM ("quote_tr", ts);
21.7 - in [(@{syntax_const "_quote"}, quote_tr)] end
21.8 + in [(@{syntax_const "_quote"}, K quote_tr)] end
21.9 *}
21.10
21.11 end
21.12 \ No newline at end of file
22.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat May 25 15:00:53 2013 +0200
22.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat May 25 15:37:53 2013 +0200
22.3 @@ -72,10 +72,10 @@
22.4 (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
22.5 | assign_tr' _ = raise Match;
22.6 in
22.7 - [(@{const_syntax Collect}, assert_tr'),
22.8 - (@{const_syntax Basic}, assign_tr'),
22.9 - (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
22.10 - (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
22.11 + [(@{const_syntax Collect}, K assert_tr'),
22.12 + (@{const_syntax Basic}, K assign_tr'),
22.13 + (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
22.14 + (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While"}))]
22.15 end
22.16 *}
22.17
23.1 --- a/src/HOL/Inductive.thy Sat May 25 15:00:53 2013 +0200
23.2 +++ b/src/HOL/Inductive.thy Sat May 25 15:37:53 2013 +0200
23.3 @@ -299,14 +299,14 @@
23.4 syntax (xsymbols)
23.5 "_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10)
23.6
23.7 -parse_translation (advanced) {*
23.8 -let
23.9 - fun fun_tr ctxt [cs] =
23.10 - let
23.11 - val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
23.12 - val ft = Case_Translation.case_tr true ctxt [x, cs];
23.13 - in lambda x ft end
23.14 -in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
23.15 +parse_translation {*
23.16 + let
23.17 + fun fun_tr ctxt [cs] =
23.18 + let
23.19 + val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
23.20 + val ft = Case_Translation.case_tr true ctxt [x, cs];
23.21 + in lambda x ft end
23.22 + in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
23.23 *}
23.24
23.25 end
24.1 --- a/src/HOL/Isar_Examples/Hoare.thy Sat May 25 15:00:53 2013 +0200
24.2 +++ b/src/HOL/Isar_Examples/Hoare.thy Sat May 25 15:37:53 2013 +0200
24.3 @@ -216,7 +216,7 @@
24.4 let
24.5 fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
24.6 | quote_tr ts = raise TERM ("quote_tr", ts);
24.7 - in [(@{syntax_const "_quote"}, quote_tr)] end
24.8 + in [(@{syntax_const "_quote"}, K quote_tr)] end
24.9 *}
24.10
24.11 text {* As usual in Isabelle syntax translations, the part for
24.12 @@ -241,10 +241,10 @@
24.13 (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
24.14 | assign_tr' _ = raise Match;
24.15 in
24.16 - [(@{const_syntax Collect}, assert_tr'),
24.17 - (@{const_syntax Basic}, assign_tr'),
24.18 - (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
24.19 - (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})]
24.20 + [(@{const_syntax Collect}, K assert_tr'),
24.21 + (@{const_syntax Basic}, K assign_tr'),
24.22 + (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
24.23 + (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))]
24.24 end
24.25 *}
24.26
25.1 --- a/src/HOL/Library/Cardinality.thy Sat May 25 15:00:53 2013 +0200
25.2 +++ b/src/HOL/Library/Cardinality.thy Sat May 25 15:37:53 2013 +0200
25.3 @@ -43,7 +43,7 @@
25.4
25.5 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
25.6
25.7 -typed_print_translation (advanced) {*
25.8 +typed_print_translation {*
25.9 let
25.10 fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
25.11 Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
26.1 --- a/src/HOL/Library/Numeral_Type.thy Sat May 25 15:00:53 2013 +0200
26.2 +++ b/src/HOL/Library/Numeral_Type.thy Sat May 25 15:37:53 2013 +0200
26.3 @@ -324,7 +324,7 @@
26.4 code_datatype Num0
26.5
26.6 instantiation num0 :: equal begin
26.7 -definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
26.8 +definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
26.9 where "equal_num0 = op ="
26.10 instance by intro_classes (simp add: equal_num0_def)
26.11 end
26.12 @@ -351,7 +351,7 @@
26.13 definition "enum_class.enum_ex P = P (1 :: num1)"
26.14 instance
26.15 by intro_classes
26.16 - (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
26.17 + (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
26.18 (metis (full_types) num1_eq_iff)+)
26.19 end
26.20
26.21 @@ -477,47 +477,49 @@
26.22 (type) "0" == (type) "num0"
26.23
26.24 parse_translation {*
26.25 -let
26.26 - fun mk_bintype n =
26.27 - let
26.28 - fun mk_bit 0 = Syntax.const @{type_syntax bit0}
26.29 - | mk_bit 1 = Syntax.const @{type_syntax bit1};
26.30 - fun bin_of n =
26.31 - if n = 1 then Syntax.const @{type_syntax num1}
26.32 - else if n = 0 then Syntax.const @{type_syntax num0}
26.33 - else if n = ~1 then raise TERM ("negative type numeral", [])
26.34 - else
26.35 - let val (q, r) = Integer.div_mod n 2;
26.36 - in mk_bit r $ bin_of q end;
26.37 - in bin_of n end;
26.38 + let
26.39 + fun mk_bintype n =
26.40 + let
26.41 + fun mk_bit 0 = Syntax.const @{type_syntax bit0}
26.42 + | mk_bit 1 = Syntax.const @{type_syntax bit1};
26.43 + fun bin_of n =
26.44 + if n = 1 then Syntax.const @{type_syntax num1}
26.45 + else if n = 0 then Syntax.const @{type_syntax num0}
26.46 + else if n = ~1 then raise TERM ("negative type numeral", [])
26.47 + else
26.48 + let val (q, r) = Integer.div_mod n 2;
26.49 + in mk_bit r $ bin_of q end;
26.50 + in bin_of n end;
26.51
26.52 - fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
26.53 - | numeral_tr ts = raise TERM ("numeral_tr", ts);
26.54 + fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
26.55 + | numeral_tr ts = raise TERM ("numeral_tr", ts);
26.56
26.57 -in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
26.58 + in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
26.59 *}
26.60
26.61 print_translation {*
26.62 -let
26.63 - fun int_of [] = 0
26.64 - | int_of (b :: bs) = b + 2 * int_of bs;
26.65 + let
26.66 + fun int_of [] = 0
26.67 + | int_of (b :: bs) = b + 2 * int_of bs;
26.68
26.69 - fun bin_of (Const (@{type_syntax num0}, _)) = []
26.70 - | bin_of (Const (@{type_syntax num1}, _)) = [1]
26.71 - | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
26.72 - | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
26.73 - | bin_of t = raise TERM ("bin_of", [t]);
26.74 + fun bin_of (Const (@{type_syntax num0}, _)) = []
26.75 + | bin_of (Const (@{type_syntax num1}, _)) = [1]
26.76 + | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
26.77 + | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
26.78 + | bin_of t = raise TERM ("bin_of", [t]);
26.79
26.80 - fun bit_tr' b [t] =
26.81 - let
26.82 - val rev_digs = b :: bin_of t handle TERM _ => raise Match
26.83 - val i = int_of rev_digs;
26.84 - val num = string_of_int (abs i);
26.85 - in
26.86 - Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
26.87 - end
26.88 - | bit_tr' b _ = raise Match;
26.89 -in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
26.90 + fun bit_tr' b [t] =
26.91 + let
26.92 + val rev_digs = b :: bin_of t handle TERM _ => raise Match
26.93 + val i = int_of rev_digs;
26.94 + val num = string_of_int (abs i);
26.95 + in
26.96 + Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
26.97 + end
26.98 + | bit_tr' b _ = raise Match;
26.99 + in
26.100 + [(@{type_syntax bit0}, K (bit_tr' 0)),
26.101 + (@{type_syntax bit1}, K (bit_tr' 1))] end;
26.102 *}
26.103
26.104 subsection {* Examples *}
27.1 --- a/src/HOL/Library/Phantom_Type.thy Sat May 25 15:00:53 2013 +0200
27.2 +++ b/src/HOL/Library/Phantom_Type.thy Sat May 25 15:37:53 2013 +0200
27.3 @@ -27,13 +27,13 @@
27.4 translations
27.5 "Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
27.6
27.7 -typed_print_translation (advanced) {*
27.8 -let
27.9 - fun phantom_tr' ctxt
27.10 - (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
27.11 - Term.list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
27.12 - | phantom_tr' _ _ _ = raise Match;
27.13 -in [(@{const_syntax phantom}, phantom_tr')] end
27.14 +typed_print_translation {*
27.15 + let
27.16 + fun phantom_tr' ctxt
27.17 + (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
27.18 + list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
27.19 + | phantom_tr' _ _ _ = raise Match;
27.20 + in [(@{const_syntax phantom}, phantom_tr')] end
27.21 *}
27.22
27.23 end
28.1 --- a/src/HOL/List.thy Sat May 25 15:00:53 2013 +0200
28.2 +++ b/src/HOL/List.thy Sat May 25 15:37:53 2013 +0200
28.3 @@ -386,7 +386,7 @@
28.4 syntax (HTML output)
28.5 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
28.6
28.7 -parse_translation (advanced) {*
28.8 +parse_translation {*
28.9 let
28.10 val NilC = Syntax.const @{const_syntax Nil};
28.11 val ConsC = Syntax.const @{const_syntax Cons};
29.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat May 25 15:00:53 2013 +0200
29.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat May 25 15:37:53 2013 +0200
29.3 @@ -28,18 +28,19 @@
29.4 syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
29.5
29.6 parse_translation {*
29.7 -let
29.8 - fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
29.9 - fun finite_vec_tr [t, u] =
29.10 - (case Term_Position.strip_positions u of
29.11 - v as Free (x, _) =>
29.12 - if Lexicon.is_tid x then
29.13 - vec t (Syntax.const @{syntax_const "_ofsort"} $ v $ Syntax.const @{class_syntax finite})
29.14 - else vec t u
29.15 - | _ => vec t u)
29.16 -in
29.17 - [(@{syntax_const "_finite_vec"}, finite_vec_tr)]
29.18 -end
29.19 + let
29.20 + fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
29.21 + fun finite_vec_tr [t, u] =
29.22 + (case Term_Position.strip_positions u of
29.23 + v as Free (x, _) =>
29.24 + if Lexicon.is_tid x then
29.25 + vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
29.26 + Syntax.const @{class_syntax finite})
29.27 + else vec t u
29.28 + | _ => vec t u)
29.29 + in
29.30 + [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
29.31 + end
29.32 *}
29.33
29.34 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
30.1 --- a/src/HOL/Num.thy Sat May 25 15:00:53 2013 +0200
30.2 +++ b/src/HOL/Num.thy Sat May 25 15:37:53 2013 +0200
30.3 @@ -291,50 +291,54 @@
30.4 "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
30.5
30.6 parse_translation {*
30.7 -let
30.8 - fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
30.9 - of (0, 1) => Syntax.const @{const_name One}
30.10 - | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
30.11 - | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n
30.12 - else raise Match;
30.13 - val pos = Syntax.const @{const_name numeral}
30.14 - val neg = Syntax.const @{const_name neg_numeral}
30.15 - val one = Syntax.const @{const_name Groups.one}
30.16 - val zero = Syntax.const @{const_name Groups.zero}
30.17 - fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
30.18 - c $ numeral_tr [t] $ u
30.19 - | numeral_tr [Const (num, _)] =
30.20 - let
30.21 - val {value, ...} = Lexicon.read_xnum num;
30.22 - in
30.23 - if value = 0 then zero else
30.24 - if value > 0
30.25 - then pos $ num_of_int value
30.26 - else neg $ num_of_int (~value)
30.27 - end
30.28 - | numeral_tr ts = raise TERM ("numeral_tr", ts);
30.29 -in [("_Numeral", numeral_tr)] end
30.30 + let
30.31 + fun num_of_int n =
30.32 + if n > 0 then
30.33 + (case IntInf.quotRem (n, 2) of
30.34 + (0, 1) => Syntax.const @{const_name One}
30.35 + | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
30.36 + | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
30.37 + else raise Match
30.38 + val pos = Syntax.const @{const_name numeral}
30.39 + val neg = Syntax.const @{const_name neg_numeral}
30.40 + val one = Syntax.const @{const_name Groups.one}
30.41 + val zero = Syntax.const @{const_name Groups.zero}
30.42 + fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
30.43 + c $ numeral_tr [t] $ u
30.44 + | numeral_tr [Const (num, _)] =
30.45 + let
30.46 + val {value, ...} = Lexicon.read_xnum num;
30.47 + in
30.48 + if value = 0 then zero else
30.49 + if value > 0
30.50 + then pos $ num_of_int value
30.51 + else neg $ num_of_int (~value)
30.52 + end
30.53 + | numeral_tr ts = raise TERM ("numeral_tr", ts);
30.54 + in [("_Numeral", K numeral_tr)] end
30.55 *}
30.56
30.57 -typed_print_translation (advanced) {*
30.58 -let
30.59 - fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
30.60 - | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
30.61 - | dest_num (Const (@{const_syntax One}, _)) = 1;
30.62 - fun num_tr' sign ctxt T [n] =
30.63 - let
30.64 - val k = dest_num n;
30.65 - val t' = Syntax.const @{syntax_const "_Numeral"} $
30.66 - Syntax.free (sign ^ string_of_int k);
30.67 - in
30.68 - case T of
30.69 - Type (@{type_name fun}, [_, T']) =>
30.70 - if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
30.71 - else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
30.72 - | T' => if T' = dummyT then t' else raise Match
30.73 - end;
30.74 -in [(@{const_syntax numeral}, num_tr' ""),
30.75 - (@{const_syntax neg_numeral}, num_tr' "-")] end
30.76 +typed_print_translation {*
30.77 + let
30.78 + fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
30.79 + | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
30.80 + | dest_num (Const (@{const_syntax One}, _)) = 1;
30.81 + fun num_tr' sign ctxt T [n] =
30.82 + let
30.83 + val k = dest_num n;
30.84 + val t' = Syntax.const @{syntax_const "_Numeral"} $
30.85 + Syntax.free (sign ^ string_of_int k);
30.86 + in
30.87 + (case T of
30.88 + Type (@{type_name fun}, [_, T']) =>
30.89 + if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
30.90 + else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
30.91 + | T' => if T' = dummyT then t' else raise Match)
30.92 + end;
30.93 + in
30.94 + [(@{const_syntax numeral}, num_tr' ""),
30.95 + (@{const_syntax neg_numeral}, num_tr' "-")]
30.96 + end
30.97 *}
30.98
30.99 ML_file "Tools/numeral.ML"
31.1 --- a/src/HOL/Orderings.thy Sat May 25 15:00:53 2013 +0200
31.2 +++ b/src/HOL/Orderings.thy Sat May 25 15:37:53 2013 +0200
31.3 @@ -727,8 +727,8 @@
31.4 fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
31.5 fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P;
31.6
31.7 - fun tr' q = (q,
31.8 - fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
31.9 + fun tr' q = (q, fn _ =>
31.10 + (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
31.11 Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
31.12 (case AList.lookup (op =) trans (q, c, d) of
31.13 NONE => raise Match
31.14 @@ -736,7 +736,7 @@
31.15 if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
31.16 else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
31.17 else raise Match)
31.18 - | _ => raise Match);
31.19 + | _ => raise Match));
31.20 in [tr' All_binder, tr' Ex_binder] end
31.21 *}
31.22
32.1 --- a/src/HOL/Product_Type.thy Sat May 25 15:00:53 2013 +0200
32.2 +++ b/src/HOL/Product_Type.thy Sat May 25 15:37:53 2013 +0200
32.3 @@ -196,71 +196,71 @@
32.4 (*reconstruct pattern from (nested) splits, avoiding eta-contraction of body;
32.5 works best with enclosing "let", if "let" does not avoid eta-contraction*)
32.6 print_translation {*
32.7 -let
32.8 - fun split_tr' [Abs (x, T, t as (Abs abs))] =
32.9 - (* split (%x y. t) => %(x,y) t *)
32.10 - let
32.11 - val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
32.12 - val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
32.13 - in
32.14 - Syntax.const @{syntax_const "_abs"} $
32.15 - (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
32.16 - end
32.17 - | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
32.18 - (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
32.19 - let
32.20 - val Const (@{syntax_const "_abs"}, _) $
32.21 - (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
32.22 - val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
32.23 - in
32.24 - Syntax.const @{syntax_const "_abs"} $
32.25 - (Syntax.const @{syntax_const "_pattern"} $ x' $
32.26 - (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
32.27 - end
32.28 - | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
32.29 - (* split (split (%x y z. t)) => %((x, y), z). t *)
32.30 - split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
32.31 - | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
32.32 - (* split (%pttrn z. t) => %(pttrn,z). t *)
32.33 - let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
32.34 - Syntax.const @{syntax_const "_abs"} $
32.35 - (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
32.36 - end
32.37 - | split_tr' _ = raise Match;
32.38 -in [(@{const_syntax prod_case}, split_tr')] end
32.39 + let
32.40 + fun split_tr' [Abs (x, T, t as (Abs abs))] =
32.41 + (* split (%x y. t) => %(x,y) t *)
32.42 + let
32.43 + val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
32.44 + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
32.45 + in
32.46 + Syntax.const @{syntax_const "_abs"} $
32.47 + (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
32.48 + end
32.49 + | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
32.50 + (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
32.51 + let
32.52 + val Const (@{syntax_const "_abs"}, _) $
32.53 + (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
32.54 + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
32.55 + in
32.56 + Syntax.const @{syntax_const "_abs"} $
32.57 + (Syntax.const @{syntax_const "_pattern"} $ x' $
32.58 + (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
32.59 + end
32.60 + | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
32.61 + (* split (split (%x y z. t)) => %((x, y), z). t *)
32.62 + split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
32.63 + | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
32.64 + (* split (%pttrn z. t) => %(pttrn,z). t *)
32.65 + let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
32.66 + Syntax.const @{syntax_const "_abs"} $
32.67 + (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
32.68 + end
32.69 + | split_tr' _ = raise Match;
32.70 + in [(@{const_syntax prod_case}, K split_tr')] end
32.71 *}
32.72
32.73 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
32.74 typed_print_translation {*
32.75 -let
32.76 - fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
32.77 - | split_guess_names_tr' T [Abs (x, xT, t)] =
32.78 - (case (head_of t) of
32.79 - Const (@{const_syntax prod_case}, _) => raise Match
32.80 - | _ =>
32.81 - let
32.82 - val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
32.83 - val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
32.84 - val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
32.85 - in
32.86 - Syntax.const @{syntax_const "_abs"} $
32.87 - (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
32.88 - end)
32.89 - | split_guess_names_tr' T [t] =
32.90 - (case head_of t of
32.91 - Const (@{const_syntax prod_case}, _) => raise Match
32.92 - | _ =>
32.93 - let
32.94 - val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
32.95 - val (y, t') =
32.96 - Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
32.97 - val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
32.98 - in
32.99 - Syntax.const @{syntax_const "_abs"} $
32.100 - (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
32.101 - end)
32.102 - | split_guess_names_tr' _ _ = raise Match;
32.103 -in [(@{const_syntax prod_case}, split_guess_names_tr')] end
32.104 + let
32.105 + fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
32.106 + | split_guess_names_tr' T [Abs (x, xT, t)] =
32.107 + (case (head_of t) of
32.108 + Const (@{const_syntax prod_case}, _) => raise Match
32.109 + | _ =>
32.110 + let
32.111 + val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
32.112 + val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
32.113 + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
32.114 + in
32.115 + Syntax.const @{syntax_const "_abs"} $
32.116 + (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
32.117 + end)
32.118 + | split_guess_names_tr' T [t] =
32.119 + (case head_of t of
32.120 + Const (@{const_syntax prod_case}, _) => raise Match
32.121 + | _ =>
32.122 + let
32.123 + val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
32.124 + val (y, t') =
32.125 + Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
32.126 + val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
32.127 + in
32.128 + Syntax.const @{syntax_const "_abs"} $
32.129 + (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
32.130 + end)
32.131 + | split_guess_names_tr' _ _ = raise Match;
32.132 + in [(@{const_syntax prod_case}, K split_guess_names_tr')] end
32.133 *}
32.134
32.135 (* Force eta-contraction for terms of the form "Q A (%p. prod_case P p)"
32.136 @@ -270,19 +270,20 @@
32.137 Otherwise prevent eta-contraction.
32.138 *)
32.139 print_translation {*
32.140 -let
32.141 - fun contract Q f ts =
32.142 - case ts of
32.143 - [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
32.144 - => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s
32.145 - | _ => f ts;
32.146 - fun contract2 (Q,f) = (Q, contract Q f);
32.147 - val pairs =
32.148 + let
32.149 + fun contract Q tr ctxt ts =
32.150 + (case ts of
32.151 + [A, Abs (_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)] =>
32.152 + if Term.is_dependent t then tr ctxt ts
32.153 + else Syntax.const Q $ A $ s
32.154 + | _ => tr ctxt ts);
32.155 + in
32.156 [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
32.157 Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
32.158 Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
32.159 Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
32.160 -in map contract2 pairs end
32.161 + |> map (fn (Q, tr) => (Q, contract Q tr))
32.162 + end
32.163 *}
32.164
32.165 subsubsection {* Code generator setup *}
33.1 --- a/src/HOL/Set.thy Sat May 25 15:00:53 2013 +0200
33.2 +++ b/src/HOL/Set.thy Sat May 25 15:37:53 2013 +0200
33.3 @@ -256,35 +256,36 @@
33.4 "\<exists>!A\<subseteq>B. P" => "EX! A. A \<subseteq> B & P"
33.5
33.6 print_translation {*
33.7 -let
33.8 - val All_binder = Mixfix.binder_name @{const_syntax All};
33.9 - val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
33.10 - val impl = @{const_syntax HOL.implies};
33.11 - val conj = @{const_syntax HOL.conj};
33.12 - val sbset = @{const_syntax subset};
33.13 - val sbset_eq = @{const_syntax subset_eq};
33.14 -
33.15 - val trans =
33.16 - [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
33.17 - ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
33.18 - ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
33.19 - ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
33.20 -
33.21 - fun mk v (v', T) c n P =
33.22 - if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
33.23 - then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P else raise Match;
33.24 -
33.25 - fun tr' q = (q,
33.26 - fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
33.27 - Const (c, _) $
33.28 - (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
33.29 - (case AList.lookup (op =) trans (q, c, d) of
33.30 - NONE => raise Match
33.31 - | SOME l => mk v (v', T) l n P)
33.32 - | _ => raise Match);
33.33 -in
33.34 - [tr' All_binder, tr' Ex_binder]
33.35 -end
33.36 + let
33.37 + val All_binder = Mixfix.binder_name @{const_syntax All};
33.38 + val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
33.39 + val impl = @{const_syntax HOL.implies};
33.40 + val conj = @{const_syntax HOL.conj};
33.41 + val sbset = @{const_syntax subset};
33.42 + val sbset_eq = @{const_syntax subset_eq};
33.43 +
33.44 + val trans =
33.45 + [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
33.46 + ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
33.47 + ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
33.48 + ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
33.49 +
33.50 + fun mk v (v', T) c n P =
33.51 + if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
33.52 + then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P
33.53 + else raise Match;
33.54 +
33.55 + fun tr' q = (q, fn _ =>
33.56 + (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
33.57 + Const (c, _) $
33.58 + (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
33.59 + (case AList.lookup (op =) trans (q, c, d) of
33.60 + NONE => raise Match
33.61 + | SOME l => mk v (v', T) l n P)
33.62 + | _ => raise Match));
33.63 + in
33.64 + [tr' All_binder, tr' Ex_binder]
33.65 + end
33.66 *}
33.67
33.68
33.69 @@ -304,11 +305,11 @@
33.70 fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
33.71 | nvars _ = 1;
33.72
33.73 - fun setcompr_tr [e, idts, b] =
33.74 + fun setcompr_tr ctxt [e, idts, b] =
33.75 let
33.76 val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
33.77 val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
33.78 - val exP = ex_tr [idts, P];
33.79 + val exP = ex_tr ctxt [idts, P];
33.80 in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
33.81
33.82 in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
33.83 @@ -323,7 +324,7 @@
33.84 let
33.85 val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
33.86
33.87 - fun setcompr_tr' [Abs (abs as (_, _, P))] =
33.88 + fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =
33.89 let
33.90 fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
33.91 | check (Const (@{const_syntax HOL.conj}, _) $
33.92 @@ -333,7 +334,7 @@
33.93 | check _ = false;
33.94
33.95 fun tr' (_ $ abs) =
33.96 - let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
33.97 + let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' ctxt [abs]
33.98 in Syntax.const @{syntax_const "_Setcompr"} $ e $ idts $ Q end;
33.99 in
33.100 if check (P, 0) then tr' P
33.101 @@ -1004,7 +1005,7 @@
33.102 lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
33.103 by (unfold less_le) blast
33.104
33.105 -lemma psubsetE [elim!,no_atp]:
33.106 +lemma psubsetE [elim!,no_atp]:
33.107 "[|A \<subset> B; [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
33.108 by (unfold less_le) blast
33.109
33.110 @@ -1758,10 +1759,10 @@
33.111 lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
33.112 by auto
33.113
33.114 -lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) =
33.115 +lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) =
33.116 (if c \<in> A then (if d \<in> A then UNIV else B)
33.117 - else if d \<in> A then -B else {})"
33.118 - by (auto simp add: vimage_def)
33.119 + else if d \<in> A then -B else {})"
33.120 + by (auto simp add: vimage_def)
33.121
33.122 lemma vimage_inter_cong:
33.123 "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
34.1 --- a/src/HOL/Statespace/StateSpaceSyntax.thy Sat May 25 15:00:53 2013 +0200
34.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy Sat May 25 15:37:53 2013 +0200
34.3 @@ -21,14 +21,14 @@
34.4 "s<x:=y>" == "_statespace_update s x y"
34.5
34.6
34.7 -parse_translation (advanced)
34.8 +parse_translation
34.9 {*
34.10 [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
34.11 (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
34.12 *}
34.13
34.14
34.15 -print_translation (advanced)
34.16 +print_translation
34.17 {*
34.18 [(@{const_syntax lookup}, StateSpace.lookup_tr'),
34.19 (@{const_syntax update}, StateSpace.update_tr')]
35.1 --- a/src/HOL/Tools/case_translation.ML Sat May 25 15:00:53 2013 +0200
35.2 +++ b/src/HOL/Tools/case_translation.ML Sat May 25 15:37:53 2013 +0200
35.3 @@ -148,10 +148,7 @@
35.4 end
35.5 | case_tr _ _ _ = case_error "case_tr";
35.6
35.7 -val trfun_setup =
35.8 - Sign.add_advanced_trfuns ([],
35.9 - [(@{syntax_const "_case_syntax"}, case_tr true)],
35.10 - [], []);
35.11 +val trfun_setup = Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)];
35.12
35.13
35.14 (* print translation *)
35.15 @@ -176,8 +173,7 @@
35.16 (mk_clauses t), ts)
35.17 end;
35.18
35.19 -val trfun_setup' = Sign.add_trfuns
35.20 - ([], [], [(@{const_syntax "case_guard"}, case_tr')], []);
35.21 +val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
35.22
35.23
35.24 (* declarations *)
36.1 --- a/src/HOL/Tools/float_syntax.ML Sat May 25 15:00:53 2013 +0200
36.2 +++ b/src/HOL/Tools/float_syntax.ML Sat May 25 15:37:53 2013 +0200
36.3 @@ -47,7 +47,6 @@
36.4
36.5 (* theory setup *)
36.6
36.7 -val setup =
36.8 - Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
36.9 +val setup = Sign.parse_translation [(@{syntax_const "_Float"}, K float_tr)];
36.10
36.11 end;
37.1 --- a/src/HOL/Tools/record.ML Sat May 25 15:00:53 2013 +0200
37.2 +++ b/src/HOL/Tools/record.ML Sat May 25 15:37:53 2013 +0200
37.3 @@ -735,10 +735,8 @@
37.4 in
37.5
37.6 val parse_translation =
37.7 - [(@{syntax_const "_record_update"}, record_update_tr)];
37.8 -
37.9 -val advanced_parse_translation =
37.10 - [(@{syntax_const "_record"}, record_tr),
37.11 + [(@{syntax_const "_record_update"}, K record_update_tr),
37.12 + (@{syntax_const "_record"}, record_tr),
37.13 (@{syntax_const "_record_scheme"}, record_scheme_tr),
37.14 (@{syntax_const "_record_type"}, record_type_tr),
37.15 (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
37.16 @@ -1896,7 +1894,7 @@
37.17 val trnames = if parent_len > 0 then [extension_name] else [];
37.18 in map record_ext_type_tr' trnames end;
37.19
37.20 - val advanced_print_translation =
37.21 + val print_translation =
37.22 map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
37.23 record_ext_type_tr's @ record_ext_type_abbr_tr's;
37.24
37.25 @@ -1995,7 +1993,7 @@
37.26 timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
37.27 (fn () =>
37.28 ext_thy
37.29 - |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
37.30 + |> Sign.print_translation print_translation
37.31 |> Sign.restore_naming thy
37.32 |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
37.33 |> Typedecl.abbrev_global
37.34 @@ -2316,8 +2314,7 @@
37.35 (* setup theory *)
37.36
37.37 val setup =
37.38 - Sign.add_trfuns ([], parse_translation, [], []) #>
37.39 - Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
37.40 + Sign.parse_translation parse_translation #>
37.41 map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]);
37.42
37.43
38.1 --- a/src/HOL/Tools/string_syntax.ML Sat May 25 15:00:53 2013 +0200
38.2 +++ b/src/HOL/Tools/string_syntax.ML Sat May 25 15:37:53 2013 +0200
38.3 @@ -87,8 +87,11 @@
38.4 (* theory setup *)
38.5
38.6 val setup =
38.7 - Sign.add_trfuns
38.8 - ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
38.9 - [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
38.10 + Sign.parse_ast_translation
38.11 + [(@{syntax_const "_Char"}, K char_ast_tr),
38.12 + (@{syntax_const "_String"}, K string_ast_tr)] #>
38.13 + Sign.print_ast_translation
38.14 + [(@{const_syntax Char}, K char_ast_tr'),
38.15 + (@{syntax_const "_list"}, K list_ast_tr')];
38.16
38.17 end;
39.1 --- a/src/HOL/Typerep.thy Sat May 25 15:00:53 2013 +0200
39.2 +++ b/src/HOL/Typerep.thy Sat May 25 15:37:53 2013 +0200
39.3 @@ -21,24 +21,24 @@
39.4 "_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))")
39.5
39.6 parse_translation {*
39.7 -let
39.8 - fun typerep_tr (*"_TYPEREP"*) [ty] =
39.9 - Syntax.const @{const_syntax typerep} $
39.10 - (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
39.11 - (Syntax.const @{type_syntax itself} $ ty))
39.12 - | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
39.13 -in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
39.14 + let
39.15 + fun typerep_tr (*"_TYPEREP"*) [ty] =
39.16 + Syntax.const @{const_syntax typerep} $
39.17 + (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
39.18 + (Syntax.const @{type_syntax itself} $ ty))
39.19 + | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
39.20 + in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end
39.21 *}
39.22
39.23 -typed_print_translation (advanced) {*
39.24 -let
39.25 - fun typerep_tr' ctxt (*"typerep"*)
39.26 - (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
39.27 - (Const (@{const_syntax TYPE}, _) :: ts) =
39.28 - Term.list_comb
39.29 - (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
39.30 - | typerep_tr' _ T ts = raise Match;
39.31 -in [(@{const_syntax typerep}, typerep_tr')] end
39.32 +typed_print_translation {*
39.33 + let
39.34 + fun typerep_tr' ctxt (*"typerep"*)
39.35 + (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
39.36 + (Const (@{const_syntax TYPE}, _) :: ts) =
39.37 + Term.list_comb
39.38 + (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
39.39 + | typerep_tr' _ T ts = raise Match;
39.40 + in [(@{const_syntax typerep}, typerep_tr')] end
39.41 *}
39.42
39.43 setup {*
40.1 --- a/src/HOL/ex/Binary.thy Sat May 25 15:00:53 2013 +0200
40.2 +++ b/src/HOL/ex/Binary.thy Sat May 25 15:37:53 2013 +0200
40.3 @@ -85,7 +85,7 @@
40.4 shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True"
40.5 and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False"
40.6 by simp_all
40.7 -
40.8 +
40.9 lemma binary_less:
40.10 fixes n :: nat
40.11 shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False"
40.12 @@ -191,19 +191,19 @@
40.13 "_Binary" :: "num_const \<Rightarrow> 'a" ("$_")
40.14
40.15 parse_translation {*
40.16 -let
40.17 - val syntax_consts =
40.18 - map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
40.19 + let
40.20 + val syntax_consts =
40.21 + map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
40.22
40.23 - fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
40.24 - | binary_tr [Const (num, _)] =
40.25 - let
40.26 - val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
40.27 - val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
40.28 - in syntax_consts (mk_binary n) end
40.29 - | binary_tr ts = raise TERM ("binary_tr", ts);
40.30 + fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
40.31 + | binary_tr [Const (num, _)] =
40.32 + let
40.33 + val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
40.34 + val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
40.35 + in syntax_consts (mk_binary n) end
40.36 + | binary_tr ts = raise TERM ("binary_tr", ts);
40.37
40.38 -in [(@{syntax_const "_Binary"}, binary_tr)] end
40.39 + in [(@{syntax_const "_Binary"}, K binary_tr)] end
40.40 *}
40.41
40.42
41.1 --- a/src/HOL/ex/Multiquote.thy Sat May 25 15:00:53 2013 +0200
41.2 +++ b/src/HOL/ex/Multiquote.thy Sat May 25 15:37:53 2013 +0200
41.3 @@ -32,7 +32,7 @@
41.4
41.5 fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
41.6 | quote_tr ts = raise TERM ("quote_tr", ts);
41.7 - in [(@{syntax_const "_quote"}, quote_tr)] end
41.8 + in [(@{syntax_const "_quote"}, K quote_tr)] end
41.9 *}
41.10
41.11 text {* basic examples *}
42.1 --- a/src/HOL/ex/Numeral_Representation.thy Sat May 25 15:00:53 2013 +0200
42.2 +++ b/src/HOL/ex/Numeral_Representation.thy Sat May 25 15:37:53 2013 +0200
42.3 @@ -277,42 +277,42 @@
42.4 "_Numerals" :: "xnum_token \<Rightarrow> 'a" ("_")
42.5
42.6 parse_translation {*
42.7 -let
42.8 - fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
42.9 - of (0, 1) => Const (@{const_name One}, dummyT)
42.10 - | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
42.11 - | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
42.12 - else raise Match;
42.13 - fun numeral_tr [Free (num, _)] =
42.14 - let
42.15 - val {leading_zeros, value, ...} = Lexicon.read_xnum num;
42.16 - val _ = leading_zeros = 0 andalso value > 0
42.17 - orelse error ("Bad numeral: " ^ num);
42.18 - in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
42.19 - | numeral_tr ts = raise TERM ("numeral_tr", ts);
42.20 -in [(@{syntax_const "_Numerals"}, numeral_tr)] end
42.21 + let
42.22 + fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
42.23 + of (0, 1) => Const (@{const_name One}, dummyT)
42.24 + | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
42.25 + | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
42.26 + else raise Match;
42.27 + fun numeral_tr [Free (num, _)] =
42.28 + let
42.29 + val {leading_zeros, value, ...} = Lexicon.read_xnum num;
42.30 + val _ = leading_zeros = 0 andalso value > 0
42.31 + orelse error ("Bad numeral: " ^ num);
42.32 + in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
42.33 + | numeral_tr ts = raise TERM ("numeral_tr", ts);
42.34 + in [(@{syntax_const "_Numerals"}, K numeral_tr)] end
42.35 *}
42.36
42.37 -typed_print_translation (advanced) {*
42.38 -let
42.39 - fun dig b n = b + 2 * n;
42.40 - fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
42.41 - dig 0 (int_of_num' n)
42.42 - | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
42.43 - dig 1 (int_of_num' n)
42.44 - | int_of_num' (Const (@{const_syntax One}, _)) = 1;
42.45 - fun num_tr' ctxt T [n] =
42.46 - let
42.47 - val k = int_of_num' n;
42.48 - val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
42.49 - in
42.50 - case T of
42.51 - Type (@{type_name fun}, [_, T']) =>
42.52 - if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
42.53 - else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
42.54 - | T' => if T' = dummyT then t' else raise Match
42.55 - end;
42.56 -in [(@{const_syntax of_num}, num_tr')] end
42.57 +typed_print_translation {*
42.58 + let
42.59 + fun dig b n = b + 2 * n;
42.60 + fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
42.61 + dig 0 (int_of_num' n)
42.62 + | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
42.63 + dig 1 (int_of_num' n)
42.64 + | int_of_num' (Const (@{const_syntax One}, _)) = 1;
42.65 + fun num_tr' ctxt T [n] =
42.66 + let
42.67 + val k = int_of_num' n;
42.68 + val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
42.69 + in
42.70 + case T of
42.71 + Type (@{type_name fun}, [_, T']) =>
42.72 + if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
42.73 + else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
42.74 + | T' => if T' = dummyT then t' else raise Match
42.75 + end;
42.76 + in [(@{const_syntax of_num}, num_tr')] end
42.77 *}
42.78
42.79
43.1 --- a/src/Pure/Isar/expression.ML Sat May 25 15:00:53 2013 +0200
43.2 +++ b/src/Pure/Isar/expression.ML Sat May 25 15:37:53 2013 +0200
43.3 @@ -622,7 +622,7 @@
43.4 fun aprop_tr' n c =
43.5 let
43.6 val c' = Lexicon.mark_const c;
43.7 - fun tr' T args =
43.8 + fun tr' (_: Proof.context) T args =
43.9 if T <> dummyT andalso length args = n
43.10 then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args)
43.11 else raise Match;
43.12 @@ -656,7 +656,7 @@
43.13
43.14 val ([pred_def], defs_thy) =
43.15 thy
43.16 - |> bodyT = propT ? Sign.add_trfunsT [aprop_tr' (length args) name]
43.17 + |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
43.18 |> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
43.19 |> Global_Theory.add_defs false
43.20 [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
44.1 --- a/src/Pure/Isar/isar_cmd.ML Sat May 25 15:00:53 2013 +0200
44.2 +++ b/src/Pure/Isar/isar_cmd.ML Sat May 25 15:37:53 2013 +0200
44.3 @@ -8,11 +8,11 @@
44.4 sig
44.5 val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
44.6 val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
44.7 - val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
44.8 - val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
44.9 - val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
44.10 - val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
44.11 - val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
44.12 + val parse_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
44.13 + val parse_translation: Symbol_Pos.text * Position.T -> theory -> theory
44.14 + val print_translation: Symbol_Pos.text * Position.T -> theory -> theory
44.15 + val typed_print_translation: Symbol_Pos.text * Position.T -> theory -> theory
44.16 + val print_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
44.17 val translations: (xstring * string) Syntax.trrule list -> theory -> theory
44.18 val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
44.19 val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
44.20 @@ -85,57 +85,41 @@
44.21
44.22 (* translation functions *)
44.23
44.24 -local
44.25 -
44.26 -fun advancedT false = ""
44.27 - | advancedT true = "Proof.context -> ";
44.28 -
44.29 -fun advancedN false = ""
44.30 - | advancedN true = "advanced_";
44.31 -
44.32 -in
44.33 -
44.34 -fun parse_ast_translation (a, (txt, pos)) =
44.35 +fun parse_ast_translation (txt, pos) =
44.36 ML_Lex.read pos txt
44.37 |> ML_Context.expression pos
44.38 - ("val parse_ast_translation: (string * (" ^ advancedT a ^
44.39 - "Ast.ast list -> Ast.ast)) list")
44.40 - ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
44.41 + "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
44.42 + "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
44.43 |> Context.theory_map;
44.44
44.45 -fun parse_translation (a, (txt, pos)) =
44.46 +fun parse_translation (txt, pos) =
44.47 ML_Lex.read pos txt
44.48 |> ML_Context.expression pos
44.49 - ("val parse_translation: (string * (" ^ advancedT a ^
44.50 - "term list -> term)) list")
44.51 - ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
44.52 + "val parse_translation: (string * (Proof.context -> term list -> term)) list"
44.53 + "Context.map_theory (Sign.parse_translation parse_translation)"
44.54 |> Context.theory_map;
44.55
44.56 -fun print_translation (a, (txt, pos)) =
44.57 +fun print_translation (txt, pos) =
44.58 ML_Lex.read pos txt
44.59 |> ML_Context.expression pos
44.60 - ("val print_translation: (string * (" ^ advancedT a ^
44.61 - "term list -> term)) list")
44.62 - ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
44.63 + "val print_translation: (string * (Proof.context -> term list -> term)) list"
44.64 + "Context.map_theory (Sign.print_translation print_translation)"
44.65 |> Context.theory_map;
44.66
44.67 -fun print_ast_translation (a, (txt, pos)) =
44.68 +fun typed_print_translation (txt, pos) =
44.69 ML_Lex.read pos txt
44.70 |> ML_Context.expression pos
44.71 - ("val print_ast_translation: (string * (" ^ advancedT a ^
44.72 - "Ast.ast list -> Ast.ast)) list")
44.73 - ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
44.74 + "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
44.75 + "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
44.76 |> Context.theory_map;
44.77
44.78 -fun typed_print_translation (a, (txt, pos)) =
44.79 +fun print_ast_translation (txt, pos) =
44.80 ML_Lex.read pos txt
44.81 |> ML_Context.expression pos
44.82 - ("val typed_print_translation: (string * (" ^ advancedT a ^ "typ -> term list -> term)) list")
44.83 - ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
44.84 + "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
44.85 + "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
44.86 |> Context.theory_map;
44.87
44.88 -end;
44.89 -
44.90
44.91 (* translation rules *)
44.92
45.1 --- a/src/Pure/Isar/isar_syn.ML Sat May 25 15:00:53 2013 +0200
45.2 +++ b/src/Pure/Isar/isar_syn.ML Sat May 25 15:37:53 2013 +0200
45.3 @@ -323,32 +323,30 @@
45.4
45.5 (* translation functions *)
45.6
45.7 -val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
45.8 -
45.9 val _ =
45.10 Outer_Syntax.command @{command_spec "parse_ast_translation"}
45.11 "install parse ast translation functions"
45.12 - (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
45.13 + (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
45.14
45.15 val _ =
45.16 Outer_Syntax.command @{command_spec "parse_translation"}
45.17 "install parse translation functions"
45.18 - (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
45.19 + (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
45.20
45.21 val _ =
45.22 Outer_Syntax.command @{command_spec "print_translation"}
45.23 "install print translation functions"
45.24 - (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
45.25 + (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
45.26
45.27 val _ =
45.28 Outer_Syntax.command @{command_spec "typed_print_translation"}
45.29 "install typed print translation functions"
45.30 - (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
45.31 + (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
45.32
45.33 val _ =
45.34 Outer_Syntax.command @{command_spec "print_ast_translation"}
45.35 "install print ast translation functions"
45.36 - (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
45.37 + (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
45.38
45.39
45.40 (* oracles *)
46.1 --- a/src/Pure/Pure.thy Sat May 25 15:00:53 2013 +0200
46.2 +++ b/src/Pure/Pure.thy Sat May 25 15:37:53 2013 +0200
46.3 @@ -8,7 +8,7 @@
46.4 keywords
46.5 "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="
46.6 "=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>"
46.7 - "\<rightleftharpoons>" "\<subseteq>" "]" "advanced" "and" "assumes"
46.8 + "\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes"
46.9 "attach" "begin" "binder" "constrains" "defines" "fixes" "for"
46.10 "identifier" "if" "imports" "in" "includes" "infix" "infixl"
46.11 "infixr" "is" "keywords" "notes" "obtains" "open" "output"
47.1 --- a/src/Pure/Syntax/local_syntax.ML Sat May 25 15:00:53 2013 +0200
47.2 +++ b/src/Pure/Syntax/local_syntax.ML Sat May 25 15:37:53 2013 +0200
47.3 @@ -59,11 +59,10 @@
47.4 | update_gram ((false, add, m), decls) =
47.5 Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
47.6
47.7 - val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs;
47.8 val local_syntax = thy_syntax
47.9 |> Syntax.update_trfuns
47.10 - (map Syntax_Ext.mk_trfun atrs, map Syntax_Ext.mk_trfun trs,
47.11 - map Syntax_Ext.mk_trfun trs', map Syntax_Ext.mk_trfun atrs')
47.12 + ([], map Syntax_Ext.mk_trfun (Syntax_Trans.struct_parse_translation structs),
47.13 + [], map Syntax_Ext.mk_trfun (Syntax_Trans.struct_print_ast_translation structs))
47.14 |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
47.15 in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
47.16
48.1 --- a/src/Pure/Syntax/mixfix.ML Sat May 25 15:00:53 2013 +0200
48.2 +++ b/src/Pure/Syntax/mixfix.ML Sat May 25 15:37:53 2013 +0200
48.3 @@ -145,10 +145,10 @@
48.4 val mfix = maps mfix_of const_decls;
48.5 val binders = map_filter binder const_decls;
48.6 val binder_trs = binders
48.7 - |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
48.8 + |> map (Syntax_Ext.stamp_trfun binder_stamp o Syntax_Trans.mk_binder_tr);
48.9 val binder_trs' = binders
48.10 |> map (Syntax_Ext.stamp_trfun binder_stamp o
48.11 - apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
48.12 + apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap);
48.13
48.14 val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
48.15 in
49.1 --- a/src/Pure/Syntax/syntax.ML Sat May 25 15:00:53 2013 +0200
49.2 +++ b/src/Pure/Syntax/syntax.ML Sat May 25 15:37:53 2013 +0200
49.3 @@ -103,11 +103,6 @@
49.4 Parse_Print_Rule of 'a * 'a
49.5 val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
49.6 val update_trfuns:
49.7 - (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
49.8 - (string * ((term list -> term) * stamp)) list *
49.9 - (string * ((typ -> term list -> term) * stamp)) list *
49.10 - (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
49.11 - val update_advanced_trfuns:
49.12 (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
49.13 (string * ((Proof.context -> term list -> term) * stamp)) list *
49.14 (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
49.15 @@ -651,10 +646,7 @@
49.16
49.17 (** modify syntax **)
49.18
49.19 -fun ext_syntax f decls = update_syntax mode_default (f decls);
49.20 -
49.21 -val update_trfuns = ext_syntax Syntax_Ext.syn_ext_trfuns;
49.22 -val update_advanced_trfuns = ext_syntax Syntax_Ext.syn_ext_advanced_trfuns;
49.23 +val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns;
49.24
49.25 fun update_type_gram add prmode decls =
49.26 (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
49.27 @@ -662,7 +654,7 @@
49.28 fun update_const_gram add is_logtype prmode decls =
49.29 (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
49.30
49.31 -val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
49.32 +val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
49.33 val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
49.34
49.35
50.1 --- a/src/Pure/Syntax/syntax_ext.ML Sat May 25 15:00:53 2013 +0200
50.2 +++ b/src/Pure/Syntax/syntax_ext.ML Sat May 25 15:37:53 2013 +0200
50.3 @@ -45,11 +45,6 @@
50.4 (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
50.5 val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
50.6 val syn_ext_trfuns:
50.7 - (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
50.8 - (string * ((term list -> term) * stamp)) list *
50.9 - (string * ((typ -> term list -> term) * stamp)) list *
50.10 - (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
50.11 - val syn_ext_advanced_trfuns:
50.12 (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
50.13 (string * ((Proof.context -> term list -> term) * stamp)) list *
50.14 (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
50.15 @@ -319,12 +314,7 @@
50.16 val syn_ext = syn_ext' (K false);
50.17
50.18 fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
50.19 -fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
50.20 -
50.21 -fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
50.22 - let fun simple (name, (f, s)) = (name, (K f, s)) in
50.23 - syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
50.24 - end;
50.25 +fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []);
50.26
50.27 fun stamp_trfun s (c, f) = (c, (f, s));
50.28 fun mk_trfun tr = stamp_trfun (stamp ()) tr;
51.1 --- a/src/Pure/Syntax/syntax_phases.ML Sat May 25 15:00:53 2013 +0200
51.2 +++ b/src/Pure/Syntax/syntax_phases.ML Sat May 25 15:37:53 2013 +0200
51.3 @@ -751,10 +751,10 @@
51.4 (* setup translations *)
51.5
51.6 val _ = Context.>> (Context.map_theory
51.7 - (Sign.add_advanced_trfuns
51.8 - ([("_context_const", const_ast_tr true),
51.9 - ("_context_xconst", const_ast_tr false)], [], [], []) #>
51.10 - Sign.add_advanced_trfunsT
51.11 + (Sign.parse_ast_translation
51.12 + [("_context_const", const_ast_tr true),
51.13 + ("_context_xconst", const_ast_tr false)] #>
51.14 + Sign.typed_print_translation
51.15 [("_type_prop", type_prop_tr'),
51.16 ("\\<^const>TYPE", type_tr'),
51.17 ("_type_constraint_", type_constraint_tr')]));
52.1 --- a/src/Pure/Syntax/syntax_trans.ML Sat May 25 15:00:53 2013 +0200
52.2 +++ b/src/Pure/Syntax/syntax_trans.ML Sat May 25 15:37:53 2013 +0200
52.3 @@ -19,12 +19,13 @@
52.4 val no_type_bracketsN: string
52.5 val no_type_brackets: unit -> bool
52.6 val abs_tr: term list -> term
52.7 - val mk_binder_tr: string * string -> string * (term list -> term)
52.8 + val mk_binder_tr: string * string -> string * (Proof.context -> term list -> term)
52.9 val antiquote_tr: string -> term -> term
52.10 val quote_tr: string -> term -> term
52.11 - val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
52.12 - val non_typed_tr': (term list -> term) -> typ -> term list -> term
52.13 - val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
52.14 + val quote_antiquote_tr: string -> string -> string ->
52.15 + string * (Proof.context -> term list -> term)
52.16 + val non_typed_tr': (Proof.context -> term list -> term) ->
52.17 + Proof.context -> typ -> term list -> term
52.18 val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
52.19 val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
52.20 val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
52.21 @@ -35,27 +36,25 @@
52.22 val abs_tr': Proof.context -> term -> term
52.23 val atomic_abs_tr': string * typ * term -> term * term
52.24 val const_abs_tr': term -> term
52.25 - val mk_binder_tr': string * string -> string * (term list -> term)
52.26 - val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
52.27 - val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
52.28 + val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
52.29 + val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
52.30 + val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
52.31 val prop_tr': term -> term
52.32 val variant_abs: string * typ * term -> string * term
52.33 val variant_abs': string * typ * term -> string * term
52.34 val dependent_tr': string * string -> term list -> term
52.35 val antiquote_tr': string -> term -> term
52.36 val quote_tr': string -> term -> term
52.37 - val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
52.38 + val quote_antiquote_tr': string -> string -> string ->
52.39 + string * (Proof.context -> term list -> term)
52.40 val update_name_tr': term -> term
52.41 - val pure_trfuns:
52.42 - (string * (Ast.ast list -> Ast.ast)) list *
52.43 - (string * (term list -> term)) list *
52.44 - (string * (term list -> term)) list *
52.45 - (string * (Ast.ast list -> Ast.ast)) list
52.46 - val struct_trfuns: string list ->
52.47 - (string * (Ast.ast list -> Ast.ast)) list *
52.48 - (string * (term list -> term)) list *
52.49 - (string * (typ -> term list -> term)) list *
52.50 - (string * (Ast.ast list -> Ast.ast)) list
52.51 + val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
52.52 + val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
52.53 + val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
52.54 + val struct_parse_translation: string list ->
52.55 + (string * (Proof.context -> term list -> term)) list
52.56 + val struct_print_ast_translation: string list ->
52.57 + (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
52.58 end;
52.59
52.60 structure Syntax_Trans: SYNTAX_TRANS =
52.61 @@ -152,7 +151,7 @@
52.62 let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
52.63 in Syntax.const name $ abs end
52.64 | binder_tr ts = err ts;
52.65 - in (syn, binder_tr) end;
52.66 + in (syn, fn _ => binder_tr) end;
52.67
52.68
52.69 (* type propositions *)
52.70 @@ -214,7 +213,7 @@
52.71 let
52.72 fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
52.73 | tr ts = raise TERM ("quote_tr", ts);
52.74 - in (quoteN, tr) end;
52.75 + in (quoteN, fn _ => tr) end;
52.76
52.77
52.78 (* corresponding updates *)
52.79 @@ -259,8 +258,7 @@
52.80
52.81 (* types *)
52.82
52.83 -fun non_typed_tr' f _ ts = f ts;
52.84 -fun non_typed_tr'' f x _ ts = f x ts;
52.85 +fun non_typed_tr' f ctxt _ ts = f ctxt ts;
52.86
52.87
52.88 (* type syntax *)
52.89 @@ -366,13 +364,13 @@
52.90
52.91 fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
52.92 | binder_tr' [] = raise Match;
52.93 - in (name, binder_tr') end;
52.94 + in (name, fn _ => binder_tr') end;
52.95
52.96 -fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
52.97 +fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts =>
52.98 let val (x, t) = atomic_abs_tr' abs
52.99 in list_comb (Syntax.const syn $ x $ t, ts) end);
52.100
52.101 -fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
52.102 +fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
52.103 let val (x, t) = atomic_abs_tr' abs
52.104 in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
52.105
52.106 @@ -464,7 +462,7 @@
52.107 let
52.108 fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
52.109 | tr' _ = raise Match;
52.110 - in (name, tr') end;
52.111 + in (name, fn _ => tr') end;
52.112
52.113
52.114 (* corresponding updates *)
52.115 @@ -503,39 +501,42 @@
52.116
52.117 (** Pure translations **)
52.118
52.119 -val pure_trfuns =
52.120 - ([("_strip_positions", strip_positions_ast_tr),
52.121 - ("_constify", constify_ast_tr),
52.122 - ("_tapp", tapp_ast_tr),
52.123 - ("_tappl", tappl_ast_tr),
52.124 - ("_bracket", bracket_ast_tr),
52.125 - ("_appl", appl_ast_tr),
52.126 - ("_applC", applC_ast_tr),
52.127 - ("_lambda", lambda_ast_tr),
52.128 - ("_idtyp", idtyp_ast_tr),
52.129 - ("_idtypdummy", idtypdummy_ast_tr),
52.130 - ("_bigimpl", bigimpl_ast_tr),
52.131 - ("_indexdefault", indexdefault_ast_tr),
52.132 - ("_indexvar", indexvar_ast_tr),
52.133 - ("_struct", struct_ast_tr)],
52.134 - [("_abs", abs_tr),
52.135 - ("_aprop", aprop_tr),
52.136 - ("_ofclass", ofclass_tr),
52.137 - ("_sort_constraint", sort_constraint_tr),
52.138 - ("_TYPE", type_tr),
52.139 - ("_DDDOT", dddot_tr),
52.140 - ("_update_name", update_name_tr),
52.141 - ("_index", index_tr)],
52.142 - ([]: (string * (term list -> term)) list),
52.143 - [("\\<^type>fun", fun_ast_tr'),
52.144 - ("_abs", abs_ast_tr'),
52.145 - ("_idts", idtyp_ast_tr' "_idts"),
52.146 - ("_pttrns", idtyp_ast_tr' "_pttrns"),
52.147 - ("\\<^const>==>", impl_ast_tr'),
52.148 - ("_index", index_ast_tr')]);
52.149 +val pure_parse_ast_translation =
52.150 + [("_strip_positions", fn _ => strip_positions_ast_tr),
52.151 + ("_constify", fn _ => constify_ast_tr),
52.152 + ("_tapp", fn _ => tapp_ast_tr),
52.153 + ("_tappl", fn _ => tappl_ast_tr),
52.154 + ("_bracket", fn _ => bracket_ast_tr),
52.155 + ("_appl", fn _ => appl_ast_tr),
52.156 + ("_applC", fn _ => applC_ast_tr),
52.157 + ("_lambda", fn _ => lambda_ast_tr),
52.158 + ("_idtyp", fn _ => idtyp_ast_tr),
52.159 + ("_idtypdummy", fn _ => idtypdummy_ast_tr),
52.160 + ("_bigimpl", fn _ => bigimpl_ast_tr),
52.161 + ("_indexdefault", fn _ => indexdefault_ast_tr),
52.162 + ("_indexvar", fn _ => indexvar_ast_tr),
52.163 + ("_struct", fn _ => struct_ast_tr)];
52.164
52.165 -fun struct_trfuns structs =
52.166 - ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
52.167 +val pure_parse_translation =
52.168 + [("_abs", fn _ => abs_tr),
52.169 + ("_aprop", fn _ => aprop_tr),
52.170 + ("_ofclass", fn _ => ofclass_tr),
52.171 + ("_sort_constraint", fn _ => sort_constraint_tr),
52.172 + ("_TYPE", fn _ => type_tr),
52.173 + ("_DDDOT", fn _ => dddot_tr),
52.174 + ("_update_name", fn _ => update_name_tr),
52.175 + ("_index", fn _ => index_tr)];
52.176 +
52.177 +val pure_print_ast_translation =
52.178 + [("\\<^type>fun", fn _ => fun_ast_tr'),
52.179 + ("_abs", fn _ => abs_ast_tr'),
52.180 + ("_idts", fn _ => idtyp_ast_tr' "_idts"),
52.181 + ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
52.182 + ("\\<^const>==>", fn _ => impl_ast_tr'),
52.183 + ("_index", fn _ => index_ast_tr')];
52.184 +
52.185 +fun struct_parse_translation structs = [("_struct", fn _ => struct_tr structs)];
52.186 +fun struct_print_ast_translation structs = [("_struct", fn _ => struct_ast_tr' structs)];
52.187
52.188 end;
52.189
53.1 --- a/src/Pure/pure_thy.ML Sat May 25 15:00:53 2013 +0200
53.2 +++ b/src/Pure/pure_thy.ML Sat May 25 15:37:53 2013 +0200
53.3 @@ -189,7 +189,9 @@
53.4 #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
53.5 #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
53.6 #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
53.7 - #> Sign.add_trfuns Syntax_Trans.pure_trfuns
53.8 + #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
53.9 + #> Sign.parse_translation Syntax_Trans.pure_parse_translation
53.10 + #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
53.11 #> Sign.local_path
53.12 #> Sign.add_consts_i
53.13 [(Binding.name "term", typ "'a => prop", NoSyn),
54.1 --- a/src/Pure/sign.ML Sat May 25 15:00:53 2013 +0200
54.2 +++ b/src/Pure/sign.ML Sat May 25 15:37:53 2013 +0200
54.3 @@ -87,19 +87,16 @@
54.4 val primitive_class: binding * class list -> theory -> theory
54.5 val primitive_classrel: class * class -> theory -> theory
54.6 val primitive_arity: arity -> theory -> theory
54.7 - val add_trfuns:
54.8 - (string * (Ast.ast list -> Ast.ast)) list *
54.9 - (string * (term list -> term)) list *
54.10 - (string * (term list -> term)) list *
54.11 - (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
54.12 - val add_trfunsT: (string * (typ -> term list -> term)) list -> theory -> theory
54.13 - val add_advanced_trfuns:
54.14 - (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
54.15 - (string * (Proof.context -> term list -> term)) list *
54.16 - (string * (Proof.context -> term list -> term)) list *
54.17 + val parse_ast_translation:
54.18 (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
54.19 - val add_advanced_trfunsT:
54.20 + val parse_translation:
54.21 + (string * (Proof.context -> term list -> term)) list -> theory -> theory
54.22 + val print_translation:
54.23 + (string * (Proof.context -> term list -> term)) list -> theory -> theory
54.24 + val typed_print_translation:
54.25 (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
54.26 + val print_ast_translation:
54.27 + (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
54.28 val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
54.29 val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
54.30 val new_group: theory -> theory
54.31 @@ -466,17 +463,14 @@
54.32
54.33 fun mk trs = map Syntax_Ext.mk_trfun trs;
54.34
54.35 -fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) =
54.36 - map_syn (ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's));
54.37 -
54.38 -fun gen_add_trfunsT ext tr's = map_syn (ext ([], [], mk tr's, []));
54.39 -
54.40 in
54.41
54.42 -val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax_Trans.non_typed_tr';
54.43 -val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
54.44 -val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax_Trans.non_typed_tr'';
54.45 -val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
54.46 +fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], []));
54.47 +fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], []));
54.48 +fun print_translation tr's =
54.49 + map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), []));
54.50 +fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, []));
54.51 +fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's));
54.52
54.53 end;
54.54
55.1 --- a/src/Sequents/ILL.thy Sat May 25 15:00:53 2013 +0200
55.2 +++ b/src/Sequents/ILL.thy Sat May 25 15:37:53 2013 +0200
55.3 @@ -36,15 +36,15 @@
55.4 "_PromAux" :: "three_seqe" ("promaux {_||_||_}")
55.5
55.6 parse_translation {*
55.7 - [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
55.8 - (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
55.9 - (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
55.10 + [(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})),
55.11 + (@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})),
55.12 + (@{syntax_const "_PromAux"}, K (three_seq_tr @{const_syntax PromAux}))]
55.13 *}
55.14
55.15 print_translation {*
55.16 - [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
55.17 - (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
55.18 - (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
55.19 + [(@{const_syntax Trueprop}, K (single_tr' @{syntax_const "_Trueprop"})),
55.20 + (@{const_syntax Context}, K (two_seq_tr' @{syntax_const "_Context"})),
55.21 + (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
55.22 *}
55.23
55.24 defs
56.1 --- a/src/Sequents/LK0.thy Sat May 25 15:00:53 2013 +0200
56.2 +++ b/src/Sequents/LK0.thy Sat May 25 15:37:53 2013 +0200
56.3 @@ -34,8 +34,8 @@
56.4 syntax
56.5 "_Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
56.6
56.7 -parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
56.8 -print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
56.9 +parse_translation {* [(@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))] *}
56.10 +print_translation {* [(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))] *}
56.11
56.12 abbreviation
56.13 not_equal (infixl "~=" 50) where
57.1 --- a/src/Sequents/Modal0.thy Sat May 25 15:00:53 2013 +0200
57.2 +++ b/src/Sequents/Modal0.thy Sat May 25 15:37:53 2013 +0200
57.3 @@ -27,13 +27,13 @@
57.4 *}
57.5
57.6 parse_translation {*
57.7 - [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
57.8 - (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
57.9 + [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
57.10 + (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
57.11 *}
57.12
57.13 print_translation {*
57.14 - [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
57.15 - (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
57.16 + [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
57.17 + (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
57.18 *}
57.19
57.20 defs
58.1 --- a/src/Sequents/S43.thy Sat May 25 15:00:53 2013 +0200
58.2 +++ b/src/Sequents/S43.thy Sat May 25 15:37:53 2013 +0200
58.3 @@ -21,7 +21,7 @@
58.4 val tr = seq_tr;
58.5 fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
58.6 Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
58.7 - in [(@{syntax_const "_S43pi"}, s43pi_tr)] end
58.8 + in [(@{syntax_const "_S43pi"}, K s43pi_tr)] end
58.9 *}
58.10
58.11 print_translation {*
58.12 @@ -29,7 +29,7 @@
58.13 val tr' = seq_tr';
58.14 fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
58.15 Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
58.16 -in [(@{const_syntax S43pi}, s43pi_tr')] end
58.17 +in [(@{const_syntax S43pi}, K s43pi_tr')] end
58.18 *}
58.19
58.20 axiomatization where
59.1 --- a/src/Sequents/Sequents.thy Sat May 25 15:00:53 2013 +0200
59.2 +++ b/src/Sequents/Sequents.thy Sat May 25 15:37:53 2013 +0200
59.3 @@ -139,7 +139,7 @@
59.4 fun side_tr [s1] = seq_tr s1;
59.5 *}
59.6
59.7 -parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
59.8 +parse_translation {* [(@{syntax_const "_Side"}, K side_tr)] *}
59.9
59.10 ML_file "prover.ML"
59.11
60.1 --- a/src/ZF/Tools/numeral_syntax.ML Sat May 25 15:00:53 2013 +0200
60.2 +++ b/src/ZF/Tools/numeral_syntax.ML Sat May 25 15:37:53 2013 +0200
60.3 @@ -79,6 +79,7 @@
60.4
60.5
60.6 val setup =
60.7 - Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [(@{const_syntax integ_of}, int_tr')], []);
60.8 + Sign.parse_translation [(@{syntax_const "_Int"}, K int_tr)] #>
60.9 + Sign.print_translation [(@{const_syntax integ_of}, K int_tr')];
60.10
60.11 end;