# HG changeset patch # User wenzelm # Date 1291320260 -3600 # Node ID 74877f1f3c6888b0a8526a2733d58a849b502726 # Parent 29a45797e269952ff778e1cd950651df6e782246# Parent be44a567ed28391eb519329f155b1d2e4c5cd618 merged; diff -r 29a45797e269 -r 74877f1f3c68 NEWS --- a/NEWS Thu Dec 02 11:18:44 2010 -0800 +++ b/NEWS Thu Dec 02 21:04:20 2010 +0100 @@ -34,8 +34,8 @@ * Various options that affect pretty printing etc. are now properly handled within the context via configuration options, instead of -unsynchronized references. There are both ML Config.T entities and -Isar declaration attributes to access these. +unsynchronized references or print modes. There are both ML Config.T +entities and Isar declaration attributes to access these. ML (Config.T) Isar (attribute) @@ -45,6 +45,7 @@ show_types show_types show_question_marks show_question_marks show_consts show_consts + show_abbrevs show_abbrevs Syntax.ambiguity_level syntax_ambiguity_level @@ -59,6 +60,14 @@ Note that corresponding "..._default" references in ML may be only changed globally at the ROOT session setup, but *not* within a theory. +The option "show_abbrevs" supersedes the former print mode +"no_abbrevs" with inverted meaning. + +* More systematic naming of some configuration options. + INCOMPATIBILTY. + + trace_simp ~> simp_trace + debug_simp ~> simp_debug *** Pure *** diff -r 29a45797e269 -r 74877f1f3c68 doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Dec 02 11:18:44 2010 -0800 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Dec 02 21:04:20 2010 +0100 @@ -339,6 +339,9 @@ \item @{antiquotation_option_def show_structs}~@{text "= bool"} controls printing of implicit structures. + \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"} + controls folding of abbreviations. + \item @{antiquotation_option_def long_names}~@{text "= bool"} forces names of types and constants etc.\ to be printed in their fully qualified internal form. diff -r 29a45797e269 -r 74877f1f3c68 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Dec 02 11:18:44 2010 -0800 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Dec 02 21:04:20 2010 +0100 @@ -99,6 +99,7 @@ @{index_ML show_types: "bool Config.T"} & default @{ML false} \\ @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\ @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\ + @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\ @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\ @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\ @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\ @@ -141,6 +142,8 @@ Note that the output can be enormous, because polymorphic constants often occur at several different type instances. + \item @{ML show_abbrevs} controls folding of constant abbreviations. + \item @{ML long_names}, @{ML short_names}, and @{ML unique_names} control the way of printing fully qualified internal names in external form. See also \secref{sec:antiq} for the document diff -r 29a45797e269 -r 74877f1f3c68 doc-src/IsarRef/Thy/document/Document_Preparation.tex --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Dec 02 11:18:44 2010 -0800 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Dec 02 21:04:20 2010 +0100 @@ -357,6 +357,9 @@ \item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}structs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} controls printing of implicit structures. + \item \indexdef{}{antiquotation option}{show\_abbrevs}\hypertarget{antiquotation option.show-abbrevs}{\hyperlink{antiquotation option.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} + controls folding of abbreviations. + \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces names of types and constants etc.\ to be printed in their fully qualified internal form. diff -r 29a45797e269 -r 74877f1f3c68 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Dec 02 11:18:44 2010 -0800 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Dec 02 21:04:20 2010 +0100 @@ -121,6 +121,7 @@ \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\ \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\ \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\ + \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\ \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\ \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\ \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\ @@ -162,6 +163,8 @@ Note that the output can be enormous, because polymorphic constants often occur at several different type instances. + \item \verb|show_abbrevs| controls folding of constant abbreviations. + \item \verb|long_names|, \verb|short_names|, and \verb|unique_names| control the way of printing fully qualified internal names in external form. See also \secref{sec:antiq} for the document diff -r 29a45797e269 -r 74877f1f3c68 doc-src/TutorialI/Misc/simp.thy --- a/doc-src/TutorialI/Misc/simp.thy Thu Dec 02 11:18:44 2010 -0800 +++ b/doc-src/TutorialI/Misc/simp.thy Thu Dec 02 21:04:20 2010 +0100 @@ -422,7 +422,7 @@ (*<*)lemma "x=x" (*>*) -using [[trace_simp=true]] +using [[simp_trace=true]] apply simp (*<*)oops(*>*) diff -r 29a45797e269 -r 74877f1f3c68 doc-src/TutorialI/Recdef/Nested2.thy --- a/doc-src/TutorialI/Recdef/Nested2.thy Thu Dec 02 11:18:44 2010 -0800 +++ b/doc-src/TutorialI/Recdef/Nested2.thy Thu Dec 02 21:04:20 2010 +0100 @@ -30,7 +30,7 @@ text{*\noindent If the proof of the induction step mystifies you, we recommend that you go through the chain of simplification steps in detail; you will probably need the help of -@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below. +@{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below. %\begin{quote} %{term[display]"trev(trev(App f ts))"}\\ %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\ diff -r 29a45797e269 -r 74877f1f3c68 src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Thu Dec 02 11:18:44 2010 -0800 +++ b/src/HOL/Isar_Examples/Hoare.thy Thu Dec 02 21:04:20 2010 +0100 @@ -16,8 +16,7 @@ text {* The following abstract syntax and semantics of Hoare Logic over \texttt{WHILE} programs closely follows the existing tradition in Isabelle/HOL of formalizing the presentation given in - \cite[\S6]{Winskel:1993}. See also - \url{http://isabelle.in.tum.de/library/Hoare/} and + \cite[\S6]{Winskel:1993}. See also @{file "~~/src/HOL/Hoare"} and \cite{Nipkow:1998:Winskel}. *} types @@ -364,7 +363,7 @@ text {* We now load the \emph{original} ML file for proof scripts and tactic definition for the Hoare Verification Condition Generator - (see \url{http://isabelle.in.tum.de/library/Hoare/}). As far as we + (see @{file "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a proof method \name{hoare}, which may be applied to a Hoare Logic assertion to extract purely logical verification conditions. It is important to note that the method diff -r 29a45797e269 -r 74877f1f3c68 src/HOL/Isar_Examples/Mutilated_Checkerboard.thy --- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Dec 02 11:18:44 2010 -0800 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Dec 02 21:04:20 2010 +0100 @@ -10,9 +10,7 @@ begin text {* The Mutilated Checker Board Problem, formalized inductively. - See \cite{paulson-mutilated-board} and - \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for - the original tactic script version. *} + See \cite{paulson-mutilated-board} for the original tactic script version. *} subsection {* Tilings *} diff -r 29a45797e269 -r 74877f1f3c68 src/HOL/Isar_Examples/Summation.thy --- a/src/HOL/Isar_Examples/Summation.thy Thu Dec 02 11:18:44 2010 -0800 +++ b/src/HOL/Isar_Examples/Summation.thy Thu Dec 02 21:04:20 2010 +0100 @@ -8,11 +8,6 @@ imports Main begin -text_raw {* \footnote{This example is somewhat reminiscent of the - \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is - discussed in \cite{isabelle-ref} in the context of permutative - rewrite rules and ordered rewriting.} *} - text {* Subsequently, we prove some summation laws of natural numbers (including odds, squares, and cubes). These examples demonstrate how plain natural deduction (including induction) may be combined @@ -126,8 +121,8 @@ qed text {* Comparing these examples with the tactic script version - \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note - an important difference of how induction vs.\ simplification is + @{file "~~/src/HOL/ex/NatSum.thy"}, we note an important difference + of how induction vs.\ simplification is applied. While \cite[\S10]{isabelle-ref} advises for these examples that ``induction should not be applied until the goal is in the simplest form'' this would be a very bad idea in our setting. diff -r 29a45797e269 -r 74877f1f3c68 src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Thu Dec 02 21:04:20 2010 +0100 @@ -446,7 +446,7 @@ (*examples: print_depth 22; set timing; -set trace_simp; +set simp_trace; fun test s = (Goal s; by (Simp_tac 1)); (*cancel_numerals*) diff -r 29a45797e269 -r 74877f1f3c68 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/HOL/Tools/numeral_simprocs.ML Thu Dec 02 21:04:20 2010 +0100 @@ -764,7 +764,7 @@ (*examples: print_depth 22; set timing; -set trace_simp; +set simp_trace; fun test s = (Goal s, by (Simp_tac 1)); test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; @@ -803,7 +803,7 @@ (*examples: print_depth 22; set timing; -set trace_simp; +set simp_trace; fun test s = (Goal s; by (Simp_tac 1)); test "9*x = 12 * (y::int)"; @@ -873,7 +873,7 @@ (*examples: print_depth 22; set timing; -set trace_simp; +set simp_trace; fun test s = (Goal s; by (Asm_simp_tac 1)); test "x*k = k*(y::int)"; @@ -890,7 +890,7 @@ (*And the same examples for fields such as rat or real: print_depth 22; set timing; -set trace_simp; +set simp_trace; fun test s = (Goal s; by (Asm_simp_tac 1)); test "x*k = k*(y::rat)"; diff -r 29a45797e269 -r 74877f1f3c68 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/Pure/Isar/attrib.ML Thu Dec 02 21:04:20 2010 +0100 @@ -405,6 +405,7 @@ register_config Syntax.show_question_marks_raw #> register_config Syntax.ambiguity_level_raw #> register_config Syntax.eta_contract_raw #> + register_config ProofContext.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> register_config Goal_Display.show_main_goal_raw #> register_config Goal_Display.show_consts_raw #> @@ -415,7 +416,7 @@ register_config Unify.trace_simp_raw #> register_config Unify.trace_types_raw #> register_config MetaSimplifier.simp_depth_limit_raw #> - register_config MetaSimplifier.debug_simp_raw #> - register_config MetaSimplifier.trace_simp_raw)); + register_config MetaSimplifier.simp_debug_raw #> + register_config MetaSimplifier.simp_trace_raw)); end; diff -r 29a45797e269 -r 74877f1f3c68 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/Pure/Isar/proof_context.ML Thu Dec 02 21:04:20 2010 +0100 @@ -70,6 +70,8 @@ val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term + val show_abbrevs_raw: Config.raw + val show_abbrevs: bool Config.T val expand_abbrevs: Proof.context -> term -> term val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term @@ -554,6 +556,8 @@ end; +val show_abbrevs_raw = Config.declare "show_abbrevs" (fn _ => Config.Bool true); +val show_abbrevs = Config.bool show_abbrevs_raw; fun contract_abbrevs ctxt t = let @@ -563,7 +567,7 @@ val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]); fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u)); in - if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t + if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t else Pattern.rewrite_term_top thy [] [match_abbrev] t end; @@ -1480,3 +1484,5 @@ end; +val show_abbrevs = ProofContext.show_abbrevs; + diff -r 29a45797e269 -r 74877f1f3c68 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/Pure/ProofGeneral/preferences.ML Thu Dec 02 21:04:20 2010 +0100 @@ -147,10 +147,10 @@ "Show leading question mark of variable name"]; val tracing_preferences = - [bool_pref trace_simp_default + [bool_pref simp_trace_default "trace-simplifier" "Trace simplification rules.", - nat_pref trace_simp_depth_limit + nat_pref simp_trace_depth_limit "trace-simplifier-depth" "Trace simplifier depth limit.", bool_pref trace_rules diff -r 29a45797e269 -r 74877f1f3c68 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/Pure/Thy/thy_output.ML Thu Dec 02 21:04:20 2010 +0100 @@ -449,6 +449,7 @@ val _ = add_option "show_sorts" (Config.put show_sorts o boolean); val _ = add_option "show_structs" (Config.put show_structs o boolean); val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean); +val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean); val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean); val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean); val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean); diff -r 29a45797e269 -r 74877f1f3c68 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/Pure/meta_simplifier.ML Thu Dec 02 21:04:20 2010 +0100 @@ -11,12 +11,12 @@ signature BASIC_META_SIMPLIFIER = sig - val debug_simp: bool Config.T - val debug_simp_raw: Config.raw - val trace_simp: bool Config.T - val trace_simp_raw: Config.raw - val trace_simp_default: bool Unsynchronized.ref - val trace_simp_depth_limit: int Unsynchronized.ref + val simp_debug: bool Config.T + val simp_debug_raw: Config.raw + val simp_trace: bool Config.T + val simp_trace_raw: Config.raw + val simp_trace_default: bool Unsynchronized.ref + val simp_trace_depth_limit: int Unsynchronized.ref type rrule val eq_rrule: rrule * rrule -> bool type simpset @@ -253,18 +253,18 @@ val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100)); val simp_depth_limit = Config.int simp_depth_limit_raw; -val trace_simp_depth_limit = Unsynchronized.ref 1; +val simp_trace_depth_limit = Unsynchronized.ref 1; fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg = - if depth > ! trace_simp_depth_limit then - if ! exceeded then () else (tracing "trace_simp_depth_limit exceeded!"; exceeded := true) + if depth > ! simp_trace_depth_limit then + if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true) else (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false); val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) => (rules, prems, bounds, (depth + 1, - if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context)); + if depth = ! simp_trace_depth_limit then Unsynchronized.ref false else exceeded), context)); fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth; @@ -273,12 +273,12 @@ exception SIMPLIFIER of string * thm; -val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false)); -val debug_simp = Config.bool debug_simp_raw; +val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false)); +val simp_debug = Config.bool simp_debug_raw; -val trace_simp_default = Unsynchronized.ref false; -val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default)); -val trace_simp = Config.bool trace_simp_raw; +val simp_trace_default = Unsynchronized.ref false; +val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default)); +val simp_trace = Config.bool simp_trace_raw; fun if_enabled (Simpset ({context, ...}, _)) flag f = (case context of @@ -303,27 +303,27 @@ fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^ Syntax.string_of_term ctxt - (if Config.get ctxt debug_simp then t else show_bounds ss t)); + (if Config.get ctxt simp_debug then t else show_bounds ss t)); in fun print_term_global ss warn a thy t = print_term ss warn (K a) t (ProofContext.init_global thy); -fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ())); -fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ())); +fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ())); +fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ())); -fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t); -fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t); +fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t); +fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t); fun trace_cterm warn a ss ct = - if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct)); + if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct)); fun trace_thm a ss th = - if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th)); + if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th)); fun trace_named_thm a ss (th, name) = - if_enabled ss trace_simp (print_term ss false + if_enabled ss simp_trace (print_term ss false (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":") (Thm.full_prop_of th)); diff -r 29a45797e269 -r 74877f1f3c68 src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/ZF/arith_data.ML Thu Dec 02 21:04:20 2010 +0100 @@ -223,7 +223,7 @@ (*examples: print_depth 22; set timing; -set trace_simp; +set simp_trace; fun test s = (Goal s; by (Asm_simp_tac 1)); test "x #+ y = x #+ z"; diff -r 29a45797e269 -r 74877f1f3c68 src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Thu Dec 02 11:18:44 2010 -0800 +++ b/src/ZF/int_arith.ML Thu Dec 02 21:04:20 2010 +0100 @@ -312,7 +312,7 @@ (* print_depth 22; set timing; -set trace_simp; +set simp_trace; fun test s = (Goal s; by (Asm_simp_tac 1)); val sg = #sign (rep_thm (topthm())); val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));