# HG changeset patch # User wenzelm # Date 1369499438 -7200 # Node ID 893b15200ec1ee0e167186c90ed82a873c5485bd # Parent eff000cab70f21ddca804bd95c90f1460b94f39b# Parent 9943f8067f11d5a168d656535e35954bb9ecd962 merged diff -r eff000cab70f -r 893b15200ec1 NEWS --- a/NEWS Sat May 25 15:44:29 2013 +0200 +++ b/NEWS Sat May 25 18:30:38 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. diff -r eff000cab70f -r 893b15200ec1 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Sat May 25 15:44:29 2013 +0200 +++ b/etc/isar-keywords-ZF.el Sat May 25 18:30:38 2013 +0200 @@ -209,8 +209,7 @@ "}")) (defconst isar-keywords-minor - '("advanced" - "and" + '("and" "assumes" "attach" "begin" diff -r eff000cab70f -r 893b15200ec1 etc/isar-keywords.el --- a/etc/isar-keywords.el Sat May 25 15:44:29 2013 +0200 +++ b/etc/isar-keywords.el Sat May 25 18:30:38 2013 +0200 @@ -52,11 +52,13 @@ "code_const" "code_datatype" "code_deps" + "code_identifier" "code_include" "code_instance" "code_modulename" "code_monad" "code_pred" + "code_printing" "code_reflect" "code_reserved" "code_thms" @@ -301,15 +303,18 @@ "}")) (defconst isar-keywords-minor - '("advanced" - "and" + '("and" "assumes" "attach" "avoids" "begin" "binder" "checking" + "class_instance" + "class_relation" + "code_module" "congs" + "constant" "constrains" "datatypes" "defaults" @@ -345,6 +350,8 @@ "rep_compat" "shows" "structure" + "type_class" + "type_constructor" "unchecked" "unsafe" "where")) @@ -487,10 +494,12 @@ "code_class" "code_const" "code_datatype" + "code_identifier" "code_include" "code_instance" "code_modulename" "code_monad" + "code_printing" "code_reflect" "code_reserved" "code_type" diff -r eff000cab70f -r 893b15200ec1 src/CCL/Term.thy --- a/src/CCL/Term.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/CCL/Term.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/CCL/Type.thy --- a/src/CCL/Type.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/CCL/Type.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/Cube/Cube.thy --- a/src/Cube/Cube.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Cube/Cube.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/Doc/Classes/Setup.thy --- a/src/Doc/Classes/Setup.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Doc/Classes/Setup.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/Doc/IsarRef/Inner_Syntax.thy --- a/src/Doc/IsarRef/Inner_Syntax.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Doc/IsarRef/Inner_Syntax.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/FOLP/IFOLP.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Big_Operators.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Code_Evaluation.thy Sat May 25 18:30:38 2013 +0200 @@ -144,15 +144,15 @@ subsubsection {* Obfuscation *} print_translation {* -let - val term = Const ("", dummyT); - fun tr1' [_, _] = term; - fun tr2' [] = term; -in - [(@{const_syntax Const}, tr1'), + let + val term = Const ("", dummyT); + fun tr1' _ [_, _] = term; + fun tr2' _ [] = term; + in + [(@{const_syntax Const}, tr1'), (@{const_syntax App}, tr1'), (@{const_syntax dummy_term}, tr2')] -end + end *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Groups.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/HOL.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/HOLCF/Cfun.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Hilbert_Choice.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Hoare/Hoare_Logic.thy Sat May 25 18:30:38 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 \ q \ Valid p (Basic id) q" diff -r eff000cab70f -r 893b15200ec1 src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat May 25 18:30:38 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 ***) diff -r eff000cab70f -r 893b15200ec1 src/HOL/Hoare/Separation.thy --- a/src/HOL/Hoare/Separation.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Hoare/Separation.thy Sat May 25 18:30:38 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: *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Hoare_Parallel/OG_Syntax.thy --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat May 25 18:30:38 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; *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Hoare_Parallel/Quote_Antiquote.thy --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/HOL/Hoare_Parallel/RG_Syntax.thy --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Inductive.thy Sat May 25 18:30:38 2013 +0200 @@ -299,14 +299,14 @@ syntax (xsymbols) "_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\_)" 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 diff -r eff000cab70f -r 893b15200ec1 src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Isar_Examples/Hoare.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Library/Cardinality.thy Sat May 25 18:30:38 2013 +0200 @@ -43,9 +43,9 @@ translations "CARD('t)" => "CONST card (CONST UNIV \ 't set)" -typed_print_translation (advanced) {* +print_translation {* let - fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] = + fun card_univ_tr' ctxt [Const (@{const_syntax UNIV}, Type (_, [T]))] = Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T in [(@{const_syntax card}, card_univ_tr')] end *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Library/Numeral_Type.thy Sat May 25 18:30:38 2013 +0200 @@ -324,7 +324,7 @@ code_datatype Num0 instantiation num0 :: equal begin -definition equal_num0 :: "num0 \ num0 \ bool" +definition equal_num0 :: "num0 \ num0 \ 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,50 @@ (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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Library/Phantom_Type.thy --- a/src/HOL/Library/Phantom_Type.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Library/Phantom_Type.thy Sat May 25 18:30:38 2013 +0200 @@ -27,13 +27,13 @@ translations "Phantom('t)" => "CONST phantom :: _ \ ('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 diff -r eff000cab70f -r 893b15200ec1 src/HOL/List.thy --- a/src/HOL/List.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/List.thy Sat May 25 18:30:38 2013 +0200 @@ -386,7 +386,7 @@ syntax (HTML output) "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _") -parse_translation (advanced) {* +parse_translation {* let val NilC = Syntax.const @{const_syntax Nil}; val ConsC = Syntax.const @{const_syntax Cons}; diff -r eff000cab70f -r 893b15200ec1 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat May 25 18:30:38 2013 +0200 @@ -28,18 +28,19 @@ syntax "_finite_vec" :: "type \ type \ 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) \ (\i. x$i = y$i)" diff -r eff000cab70f -r 893b15200ec1 src/HOL/Num.thy --- a/src/HOL/Num.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Num.thy Sat May 25 18:30:38 2013 +0200 @@ -291,50 +291,54 @@ "_Numeral" :: "num_const \ '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" diff -r eff000cab70f -r 893b15200ec1 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Orderings.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Product_Type.thy Sat May 25 18:30:38 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 "\(x,y). f x y" and "split (\x. f x)" as "\(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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Rat.thy Sat May 25 18:30:38 2013 +0200 @@ -341,7 +341,7 @@ proof - have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract) by (rule sym) (auto intro: normalize_eq) - moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) + moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) by (cases "normalize (a, b)") (rule normalize_denom_pos, simp) moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime) by (rule normalize_coprime) simp @@ -1106,16 +1106,42 @@ ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat -subsection{* Float syntax *} + +subsection {* Float syntax *} syntax "_Float" :: "float_const \ 'a" ("_") -ML_file "Tools/float_syntax.ML" -setup Float_Syntax.setup +parse_translation {* + let + fun mk_number i = + let + fun mk 1 = Syntax.const @{const_syntax Num.One} + | mk i = + let val (q, r) = Integer.div_mod i 2 + in HOLogic.mk_bit r $ (mk q) end; + in + if i = 0 then Syntax.const @{const_syntax Groups.zero} + else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i + else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i) + end; + + fun mk_frac str = + let + val {mant = i, exp = n} = Lexicon.read_float str; + val exp = Syntax.const @{const_syntax Power.power}; + val ten = mk_number 10; + val exp10 = if n = 1 then ten else exp $ ten $ mk_number n; + in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end; + + fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u + | float_tr [t as Const (str, _)] = mk_frac str + | float_tr ts = raise TERM ("float_tr", ts); + in [(@{syntax_const "_Float"}, K float_tr)] end +*} text{* Test: *} lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)" -by simp + by simp hide_const (open) normalize positive diff -r eff000cab70f -r 893b15200ec1 src/HOL/Set.thy --- a/src/HOL/Set.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Set.thy Sat May 25 18:30:38 2013 +0200 @@ -256,35 +256,36 @@ "\!A\B. P" => "EX! A. A \ 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 \ B ==> A \ B ==> A \ B" by (unfold less_le) blast -lemma psubsetE [elim!,no_atp]: +lemma psubsetE [elim!,no_atp]: "[|A \ B; [|A \ B; ~ (B\A)|] ==> R|] ==> R" by (unfold less_le) blast @@ -1758,10 +1759,10 @@ lemma vimage_const [simp]: "((\x. c) -` A) = (if c \ A then UNIV else {})" by auto -lemma vimage_if [simp]: "((\x. if x \ B then c else d) -` A) = +lemma vimage_if [simp]: "((\x. if x \ B then c else d) -` A) = (if c \ A then (if d \ A then UNIV else B) - else if d \ A then -B else {})" - by (auto simp add: vimage_def) + else if d \ A then -B else {})" + by (auto simp add: vimage_def) lemma vimage_inter_cong: "(\ w. w \ S \ f w = g w) \ f -` y \ S = g -` y \ S" diff -r eff000cab70f -r 893b15200ec1 src/HOL/Statespace/StateSpaceSyntax.thy --- a/src/HOL/Statespace/StateSpaceSyntax.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy Sat May 25 18:30:38 2013 +0200 @@ -21,14 +21,14 @@ "s" == "_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')] diff -r eff000cab70f -r 893b15200ec1 src/HOL/Tools/case_translation.ML --- a/src/HOL/Tools/case_translation.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Tools/case_translation.ML Sat May 25 18:30:38 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 *) diff -r eff000cab70f -r 893b15200ec1 src/HOL/Tools/float_syntax.ML --- a/src/HOL/Tools/float_syntax.ML Sat May 25 15:44:29 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -(* Title: HOL/Tools/float_syntax.ML - Author: Tobias Nipkow, TU Muenchen - -Concrete syntax for floats. -*) - -signature FLOAT_SYNTAX = -sig - val setup: theory -> theory -end; - -structure Float_Syntax: FLOAT_SYNTAX = -struct - -(* parse translation *) - -local - -fun mk_number i = - let - fun mk 1 = Syntax.const @{const_syntax Num.One} - | mk i = - let val (q, r) = Integer.div_mod i 2 - in HOLogic.mk_bit r $ (mk q) end; - in - if i = 0 then Syntax.const @{const_syntax Groups.zero} - else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i - else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i) - end; - -fun mk_frac str = - let - val {mant = i, exp = n} = Lexicon.read_float str; - val exp = Syntax.const @{const_syntax Power.power}; - val ten = mk_number 10; - val exp10 = if n = 1 then ten else exp $ ten $ mk_number n; - in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end; - -in - -fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u - | float_tr [t as Const (str, _)] = mk_frac str - | float_tr ts = raise TERM ("float_tr", ts); - -end; - - -(* theory setup *) - -val setup = - Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []); - -end; diff -r eff000cab70f -r 893b15200ec1 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Tools/record.ML Sat May 25 18:30:38 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]); diff -r eff000cab70f -r 893b15200ec1 src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Tools/string_syntax.ML Sat May 25 18:30:38 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; diff -r eff000cab70f -r 893b15200ec1 src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/Typerep.thy Sat May 25 18:30:38 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 {* diff -r eff000cab70f -r 893b15200ec1 src/HOL/ex/Binary.thy --- a/src/HOL/ex/Binary.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/ex/Binary.thy Sat May 25 18:30:38 2013 +0200 @@ -85,7 +85,7 @@ shows "n \ m + k \ (m \ n) \ True" and "m \ n + k + 1 \ (m \ n) \ False" by simp_all - + lemma binary_less: fixes n :: nat shows "m \ n + k \ (m < n) \ False" @@ -191,19 +191,19 @@ "_Binary" :: "num_const \ '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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/ex/Multiquote.thy --- a/src/HOL/ex/Multiquote.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/ex/Multiquote.thy Sat May 25 18:30:38 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 *} diff -r eff000cab70f -r 893b15200ec1 src/HOL/ex/Numeral_Representation.thy --- a/src/HOL/ex/Numeral_Representation.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/ex/Numeral_Representation.thy Sat May 25 18:30:38 2013 +0200 @@ -277,42 +277,42 @@ "_Numerals" :: "xnum_token \ '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 *} diff -r eff000cab70f -r 893b15200ec1 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Isar/expression.ML Sat May 25 18:30:38 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)), [])]; diff -r eff000cab70f -r 893b15200ec1 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat May 25 18:30:38 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 *) diff -r eff000cab70f -r 893b15200ec1 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sat May 25 18:30:38 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 *) diff -r eff000cab70f -r 893b15200ec1 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Pure.thy Sat May 25 18:30:38 2013 +0200 @@ -8,7 +8,7 @@ keywords "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "==" "=>" "?" "[" "\" "\" "\" - "\" "\" "]" "advanced" "and" "assumes" + "\" "\" "]" "and" "assumes" "attach" "begin" "binder" "constrains" "defines" "fixes" "for" "identifier" "if" "imports" "in" "includes" "infix" "infixl" "infixr" "is" "keywords" "notes" "obtains" "open" "output" diff -r eff000cab70f -r 893b15200ec1 src/Pure/Syntax/local_syntax.ML --- a/src/Pure/Syntax/local_syntax.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Syntax/local_syntax.ML Sat May 25 18:30:38 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') + ([], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_tr structs)], + [], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_ast_tr' structs)]) |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; diff -r eff000cab70f -r 893b15200ec1 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Syntax/mixfix.ML Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Syntax/syntax.ML Sat May 25 18:30:38 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; diff -r eff000cab70f -r 893b15200ec1 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Sat May 25 18:30:38 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; diff -r eff000cab70f -r 893b15200ec1 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Sat May 25 18:30:38 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')])); diff -r eff000cab70f -r 893b15200ec1 src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/Syntax/syntax_trans.ML Sat May 25 18:30:38 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,23 @@ 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_tr: string list -> string * (Proof.context -> term list -> term) + val struct_ast_tr': string list -> string * (Proof.context -> Ast.ast list -> Ast.ast) end; structure Syntax_Trans: SYNTAX_TRANS = @@ -152,7 +149,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 +211,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 *) @@ -246,12 +243,13 @@ fun index_tr [t] = t | index_tr ts = raise TERM ("index_tr", ts); -fun the_struct [] = error "Illegal reference to implicit structure" - | the_struct (x :: _) = x; - -fun struct_tr structs [Const ("_indexdefault", _)] = - Syntax.const (Lexicon.mark_fixed (the_struct structs)) - | struct_tr _ ts = raise TERM ("struct_tr", ts); +fun struct_tr structs = + ("_struct", fn _ => + (fn [Const ("_indexdefault", _)] => + (case structs of + x :: _ => Syntax.const (Lexicon.mark_fixed x) + | _ => error "Illegal reference to implicit structure") + | ts => raise TERM ("struct_tr", ts))); @@ -259,8 +257,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 +363,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 +461,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 *) @@ -494,48 +491,51 @@ fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast | index_ast_tr' _ = raise Match; -fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = - Ast.Appl [Ast.Constant "_free", - Ast.Variable (the_struct structs handle ERROR _ => raise Match)] - | struct_ast_tr' _ _ = raise Match; +fun struct_ast_tr' structs = + ("_struct", fn _ => + (fn [Ast.Constant "_indexdefault"] => + (case structs of + x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x] + | _ => raise Match) + | _ => raise Match)); (** 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')]; end; diff -r eff000cab70f -r 893b15200ec1 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/pure_thy.ML Sat May 25 18:30:38 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), diff -r eff000cab70f -r 893b15200ec1 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/Pure/sign.ML Sat May 25 18:30:38 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; diff -r eff000cab70f -r 893b15200ec1 src/Sequents/ILL.thy --- a/src/Sequents/ILL.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Sequents/ILL.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Sequents/LK0.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/Sequents/Modal0.thy --- a/src/Sequents/Modal0.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Sequents/Modal0.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/Sequents/S43.thy --- a/src/Sequents/S43.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Sequents/S43.thy Sat May 25 18:30:38 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 diff -r eff000cab70f -r 893b15200ec1 src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/Sequents/Sequents.thy Sat May 25 18:30:38 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" diff -r eff000cab70f -r 893b15200ec1 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/ZF/Tools/inductive_package.ML Sat May 25 18:30:38 2013 +0200 @@ -260,8 +260,8 @@ THEN (PRIMITIVE (fold_rule part_rec_defs)); (*Elimination*) - val elim = rule_by_tactic (Proof_Context.init_global thy1) (basic_elim_tac ctxt1) - (unfold RS Ind_Syntax.equals_CollectD) + val elim = + rule_by_tactic ctxt1 (basic_elim_tac ctxt1) (unfold RS Ind_Syntax.equals_CollectD) (*Applies freeness of the given constructors, which *must* be unfolded by the given defs. Cannot simply use the local con_defs because diff -r eff000cab70f -r 893b15200ec1 src/ZF/Tools/numeral_syntax.ML --- a/src/ZF/Tools/numeral_syntax.ML Sat May 25 15:44:29 2013 +0200 +++ b/src/ZF/Tools/numeral_syntax.ML Sat May 25 18:30:38 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;