merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
--- a/NEWS Fri Aug 27 10:57:32 2010 +0200
+++ b/NEWS Fri Aug 27 12:57:55 2010 +0200
@@ -23,6 +23,22 @@
at the cost of clarity of file dependencies. Recall that Isabelle/ML
files exclusively use the .ML extension. Minor INCOMPATIBILTY.
+* Various options that affect document antiquotations 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.
+
+ ML: Isar:
+
+ Thy_Output.display thy_output_display
+ Thy_Output.quotes thy_output_quotes
+ Thy_Output.indent thy_output_indent
+ Thy_Output.source thy_output_source
+ Thy_Output.break thy_output_break
+
+Note that the corresponding "..._default" references may be only
+changed globally at the ROOT session setup, but *not* within a theory.
+
*** Pure ***
--- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Fri Aug 27 12:57:55 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set Thy_Output.source;
+Thy_Output.source_default := true;
use "../../antiquote_setup.ML";
use_thy "HOLCF_Specific";
--- a/doc-src/IsarRef/Thy/ROOT-ZF.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML Fri Aug 27 12:57:55 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set Thy_Output.source;
+Thy_Output.source_default := true;
use "../../antiquote_setup.ML";
use_thy "ZF_Specific";
--- a/doc-src/IsarRef/Thy/ROOT.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Fri Aug 27 12:57:55 2010 +0200
@@ -1,5 +1,5 @@
-Unsynchronized.set quick_and_dirty;
-Unsynchronized.set Thy_Output.source;
+quick_and_dirty := true;
+Thy_Output.source_default := true;
use "../../antiquote_setup.ML";
use_thys [
--- a/doc-src/Main/Docs/Main_Doc.thy Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy Fri Aug 27 12:57:55 2010 +0200
@@ -10,9 +10,9 @@
Syntax.pretty_typ ctxt T)
val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
- (fn {source, context, ...} => fn arg =>
- Thy_Output.output
- (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg]));
+ (fn {source, context = ctxt, ...} => fn arg =>
+ Thy_Output.output ctxt
+ (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]));
*}
(*>*)
text{*
--- a/doc-src/System/Thy/ROOT.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/System/Thy/ROOT.ML Fri Aug 27 12:57:55 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set Thy_Output.source;
+Thy_Output.source_default := true;
use "../../antiquote_setup.ML";
use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
--- a/doc-src/TutorialI/Documents/Documents.thy Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy Fri Aug 27 12:57:55 2010 +0200
@@ -144,7 +144,7 @@
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
(*<*)
-local
+setup {* Sign.local_path *}
(*>*)
text {*
@@ -169,7 +169,7 @@
notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
(*<*)
-local
+setup {* Sign.local_path *}
(*>*)
text {*\noindent
--- a/doc-src/TutorialI/Documents/document/Documents.tex Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Fri Aug 27 12:57:55 2010 +0200
@@ -168,6 +168,19 @@
\isacommand{definition}\isamarkupfalse%
\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
\isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
\begin{isamarkuptext}%
\noindent The X-Symbol package within Proof~General provides several
input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may
@@ -200,6 +213,19 @@
\isanewline
\isacommand{notation}\isamarkupfalse%
\ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
\begin{isamarkuptext}%
\noindent
The \commdx{notation} command associates a mixfix
--- a/doc-src/TutorialI/Rules/Primes.thy Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy Fri Aug 27 12:57:55 2010 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
(* EXTRACT from HOL/ex/Primes.thy*)
(*Euclid's algorithm
@@ -10,7 +9,7 @@
ML "Pretty.margin_default := 64"
-ML "Thy_Output.indent := 5" (*that is, Doc/TutorialI/settings.ML*)
+declare [[thy_output_indent = 5]] (*that is, Doc/TutorialI/settings.ML*)
text {*Now in Basic.thy!
--- a/doc-src/TutorialI/Types/Numbers.thy Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy Fri Aug 27 12:57:55 2010 +0200
@@ -3,7 +3,7 @@
begin
ML "Pretty.margin_default := 64"
-ML "Thy_Output.indent := 0" (*we don't want 5 for listing theorems*)
+declare [[thy_output_indent = 0]] (*we don't want 5 for listing theorems*)
text{*
--- a/doc-src/TutorialI/Types/document/Numbers.tex Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Fri Aug 27 12:57:55 2010 +0200
@@ -26,16 +26,16 @@
%
\isatagML
\isacommand{ML}\isamarkupfalse%
-\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}%
\endisatagML
{\isafoldML}%
%
\isadelimML
+\isanewline
%
\endisadelimML
-%
+\isacommand{declare}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}thy{\isacharunderscore}output{\isacharunderscore}indent\ {\isacharequal}\ {\isadigit{0}}{\isacharbrackright}{\isacharbrackright}%
\begin{isamarkuptext}%
numeric literals; default simprules; can re-orient%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/settings.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/TutorialI/settings.ML Fri Aug 27 12:57:55 2010 +0200
@@ -1,3 +1,1 @@
-(* $Id$ *)
-
-Thy_Output.indent := 5;
+Thy_Output.indent_default := 5;
--- a/doc-src/antiquote_setup.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/antiquote_setup.ML Fri Aug 27 12:57:55 2010 +0200
@@ -71,8 +71,8 @@
in
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
(txt'
- |> (if ! Thy_Output.quotes then quote else I)
- |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+ |> (if Config.get ctxt Thy_Output.quotes then quote else I)
+ |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
end);
@@ -93,18 +93,18 @@
(Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
(fn {context = ctxt, ...} =>
map (apfst (Thy_Output.pretty_thm ctxt))
- #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
- #> (if ! Thy_Output.display
+ #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
+ #> (if Config.get ctxt Thy_Output.display
then
map (fn (p, name) =>
- Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
- "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
+ Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
+ "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
#> space_implode "\\par\\smallskip%\n"
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else
map (fn (p, name) =>
Output.output (Pretty.str_of p) ^
- "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
+ "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
#> space_implode "\\par\\smallskip%\n"
#> enclose "\\isa{" "}"));
@@ -112,7 +112,8 @@
(* theory file *)
val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
- (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
+ (fn {context = ctxt, ...} =>
+ fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
(* Isabelle/Isar entities (with index) *)
@@ -152,8 +153,9 @@
idx ^
(Output.output name
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> (if ! Thy_Output.quotes then quote else I)
- |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ |> (if Config.get ctxt Thy_Output.quotes then quote else I)
+ |> (if Config.get ctxt Thy_Output.display
+ then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else hyper o enclose "\\mbox{\\isa{" "}}"))
else error ("Bad " ^ kind ^ " " ^ quote name)
end);
--- a/doc-src/more_antiquote.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/more_antiquote.ML Fri Aug 27 12:57:55 2010 +0200
@@ -95,7 +95,7 @@
|> snd
|> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
|> map (holize o no_vars ctxt o AxClass.overload thy);
- in Thy_Output.output (Thy_Output.maybe_pretty_source (pretty_thm ctxt) src thms) end;
+ in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
in
--- a/doc-src/rail.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/doc-src/rail.ML Fri Aug 27 12:57:55 2010 +0200
@@ -97,8 +97,9 @@
(idx ^
(Output.output name
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> (if ! Thy_Output.quotes then quote else I)
- |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ |> (if Config.get ctxt Thy_Output.quotes then quote else I)
+ |> (if Config.get ctxt Thy_Output.display
+ then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else hyper o enclose "\\mbox{\\isa{" "}}")), style)
else ("Bad " ^ kind ^ " " ^ name, false)
end;
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Aug 27 12:57:55 2010 +0200
@@ -91,7 +91,7 @@
| _ => (pair ts, K I))
val discharge = fold (Boogie_VCs.discharge o pair vc_name)
- fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
+ fun after_qed [thms] = ProofContext.background_theory (discharge (vcs ~~ thms))
| after_qed _ = I
in
ProofContext.init_global thy
--- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Aug 27 12:57:55 2010 +0200
@@ -257,7 +257,9 @@
Pretty.str " =" :: Pretty.brk 1 ::
flat (separate [Pretty.brk 1, Pretty.str "| "]
(map (single o pretty_constr) cos)));
- in Thy_Output.output (Thy_Output.maybe_pretty_source (K pretty_datatype) src [()]) end);
+ in
+ Thy_Output.output ctxt (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
+ end);
@@ -428,7 +430,7 @@
unflat rules (map Drule.zero_var_indexes_list raw_thms);
(*FIXME somehow dubious*)
in
- ProofContext.theory_result
+ ProofContext.background_theory_result
(prove_rep_datatype config dt_names alt_names descr vs
raw_inject half_distinct raw_induct)
#-> after_qed
--- a/src/HOL/Tools/Function/function_common.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Fri Aug 27 12:57:55 2010 +0200
@@ -164,7 +164,7 @@
structure Termination_Simps = Named_Thms
(
val name = "termination_simp"
- val description = "Simplification rule for termination proofs"
+ val description = "simplification rules for termination proofs"
)
@@ -175,7 +175,7 @@
type T = Proof.context -> tactic
val empty = (fn _ => error "Termination prover not configured")
val extend = I
- fun merge (a, b) = b (* FIXME ? *)
+ fun merge (a, _) = a
)
val set_termination_prover = TerminationProver.put
--- a/src/HOL/Tools/Function/measure_functions.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML Fri Aug 27 12:57:55 2010 +0200
@@ -20,7 +20,7 @@
(
val name = "measure_function"
val description =
- "Rules that guide the heuristic generation of measure functions"
+ "rules that guide the heuristic generation of measure functions"
);
fun mk_is_measure t =
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Aug 27 12:57:55 2010 +0200
@@ -68,7 +68,7 @@
type T = multiset_setup option
val empty = NONE
val extend = I;
- fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *)
+ fun merge (v1, v2) = if is_some v1 then v1 else v2
)
val multiset_setup = Multiset_Setup.put o SOME
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 12:57:55 2010 +0200
@@ -596,13 +596,14 @@
val _ = tracing "Preprocessing specification..."
val T = Sign.the_const_type (ProofContext.theory_of ctxt) name
val t = Const (name, T)
- val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
- val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
- val ctxt'' = ProofContext.init_global thy'
+ val thy' =
+ Theory.copy (ProofContext.theory_of ctxt)
+ |> Predicate_Compile.preprocess preprocess_options t
+ val ctxt' = ProofContext.init_global thy'
val _ = tracing "Generating prolog program..."
- val (p, constant_table) = generate (#ensure_groundness options) ctxt'' name
+ val (p, constant_table) = generate (#ensure_groundness options) ctxt' name
|> (if #ensure_groundness options then
- add_ground_predicates ctxt'' (#limited_types options)
+ add_ground_predicates ctxt' (#limited_types options)
else I)
val _ = tracing "Running prolog program..."
val tss = run (#prolog_system options)
@@ -622,7 +623,7 @@
mk_set_compr (t :: in_insert) ts xs
else
let
- val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt'' [t]) ("uu", fastype_of t)
+ val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
val set_compr =
HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
@@ -633,7 +634,7 @@
end
in
foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
- (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt'' constant_table) (ts ~~ Ts))) tss) [])
+ (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
end
fun values_cmd print_modes soln raw_t state =
@@ -674,10 +675,9 @@
fun quickcheck ctxt report t size =
let
- val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
- val thy = (ProofContext.theory_of ctxt')
+ val thy = Theory.copy (ProofContext.theory_of ctxt)
val (vs, t') = strip_abs t
- val vs' = Variable.variant_frees ctxt' [] vs
+ val vs' = Variable.variant_frees ctxt [] vs
val Ts = map snd vs'
val t'' = subst_bounds (map Free (rev vs'), t')
val (prems, concl) = strip_horn t''
@@ -693,15 +693,15 @@
val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
- val ctxt'' = ProofContext.init_global thy3
+ val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
- val (p, constant_table) = generate true ctxt'' full_constname
- |> add_ground_predicates ctxt'' (#limited_types (!options))
+ val (p, constant_table) = generate true ctxt' full_constname
+ |> add_ground_predicates ctxt' (#limited_types (!options))
val _ = tracing "Running prolog program..."
val [ts] = run (#prolog_system (!options))
p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
val _ = tracing "Restoring terms..."
- val res = SOME (map (restore_term ctxt'' constant_table) (ts ~~ Ts))
+ val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
val empty_report = ([], false)
in
(res, empty_report)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Aug 27 12:57:55 2010 +0200
@@ -176,9 +176,9 @@
val t = Const (const, T)
val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
in
- if (is_inductify options) then
+ if is_inductify options then
let
- val lthy' = Local_Theory.theory (preprocess options t) lthy
+ val lthy' = Local_Theory.background_theory (preprocess options t) lthy
val const =
case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
SOME c => c
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 27 12:57:55 2010 +0200
@@ -730,9 +730,7 @@
type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
val empty = Symtab.empty;
val extend = I;
- val merge = Symtab.merge ((K true)
- : ((mode * (compilation_funs -> typ -> term)) list *
- (mode * (compilation_funs -> typ -> term)) list -> bool));
+ fun merge data : T = Symtab.merge (K true) data;
);
fun alternative_compilation_of_global thy pred_name mode =
@@ -3033,12 +3031,13 @@
"adding alternative introduction rules for code generation of inductive predicates"
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
+(* FIXME ... this is important to avoid changing the background theory below *)
fun generic_code_pred prep_const options raw_const lthy =
let
val thy = ProofContext.theory_of lthy
val const = prep_const thy raw_const
val ctxt = ProofContext.init_global thy
- val lthy' = Local_Theory.theory (PredData.map
+ val lthy' = Local_Theory.background_theory (PredData.map
(extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy
val thy' = ProofContext.theory_of lthy'
val ctxt' = ProofContext.init_global thy'
@@ -3063,7 +3062,7 @@
val global_thms = ProofContext.export goal_ctxt
(ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms)
in
- goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
+ goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #>
((case compilation options of
Pred => add_equations
| DSeq => add_dseq_equations
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Aug 27 12:57:55 2010 +0200
@@ -21,8 +21,7 @@
structure Fun_Pred = Theory_Data
(
type T = (term * term) Item_Net.T;
- val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
- (single o fst);
+ val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
val extend = I;
val merge = Item_Net.merge;
)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 12:57:55 2010 +0200
@@ -185,10 +185,9 @@
fun compile_term compilation options ctxt t =
let
- val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
- val thy = (ProofContext.theory_of ctxt')
+ val thy = Theory.copy (ProofContext.theory_of ctxt)
val (vs, t') = strip_abs t
- val vs' = Variable.variant_frees ctxt' [] vs
+ val vs' = Variable.variant_frees ctxt [] vs
val t'' = subst_bounds (map Free (rev vs'), t')
val (prems, concl) = strip_horn t''
val constname = "pred_compile_quickcheck"
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Aug 27 12:57:55 2010 +0200
@@ -18,8 +18,7 @@
structure Specialisations = Theory_Data
(
type T = (term * term) Item_Net.T;
- val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
- (single o fst);
+ val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
val extend = I;
val merge = Item_Net.merge;
)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Aug 27 12:57:55 2010 +0200
@@ -56,10 +56,12 @@
type maps_info = {mapfun: string, relmap: string}
structure MapsData = Theory_Data
- (type T = maps_info Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data)
+(
+ type T = maps_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+)
fun maps_defined thy s =
Symtab.defined (MapsData.get thy) s
@@ -70,7 +72,7 @@
| NONE => raise NotFound
fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
-fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
+fun maps_update k minfo = ProofContext.background_theory (maps_update_thy k minfo) (* FIXME *)
fun maps_attribute_aux s minfo = Thm.declaration_attribute
(fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
@@ -120,10 +122,12 @@
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
structure QuotData = Theory_Data
- (type T = quotdata_info Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data)
+(
+ type T = quotdata_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+)
fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
{qtyp = Morphism.typ phi qtyp,
@@ -174,10 +178,12 @@
for example given "nat fset" we need to find "'a fset";
but overloaded constants share the same name *)
structure QConstsData = Theory_Data
- (type T = (qconsts_info list) Symtab.table
- val empty = Symtab.empty
- val extend = I
- val merge = Symtab.merge_list qconsts_info_eq)
+(
+ type T = qconsts_info list Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ val merge = Symtab.merge_list qconsts_info_eq
+)
fun transform_qconsts phi {qconst, rconst, def} =
{qconst = Morphism.term phi qconst,
@@ -229,39 +235,49 @@
(* equivalence relation theorems *)
structure EquivRules = Named_Thms
- (val name = "quot_equiv"
- val description = "Equivalence relation theorems.")
+(
+ val name = "quot_equiv"
+ val description = "equivalence relation theorems"
+)
val equiv_rules_get = EquivRules.get
val equiv_rules_add = EquivRules.add
(* respectfulness theorems *)
structure RspRules = Named_Thms
- (val name = "quot_respect"
- val description = "Respectfulness theorems.")
+(
+ val name = "quot_respect"
+ val description = "respectfulness theorems"
+)
val rsp_rules_get = RspRules.get
val rsp_rules_add = RspRules.add
(* preservation theorems *)
structure PrsRules = Named_Thms
- (val name = "quot_preserve"
- val description = "Preservation theorems.")
+(
+ val name = "quot_preserve"
+ val description = "preservation theorems"
+)
val prs_rules_get = PrsRules.get
val prs_rules_add = PrsRules.add
(* id simplification theorems *)
structure IdSimps = Named_Thms
- (val name = "id_simps"
- val description = "Identity simp rules for maps.")
+(
+ val name = "id_simps"
+ val description = "identity simp rules for maps"
+)
val id_simps_get = IdSimps.get
(* quotient theorems *)
structure QuotientRules = Named_Thms
- (val name = "quot_thm"
- val description = "Quotient theorems.")
+(
+ val name = "quot_thm"
+ val description = "quotient theorems"
+)
val quotient_rules_get = QuotientRules.get
val quotient_rules_add = QuotientRules.add
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Aug 27 12:57:55 2010 +0200
@@ -77,7 +77,8 @@
Typedef.add_typedef false NONE (qty_name, vs, mx)
(typedef_term rel rty lthy) NONE typedef_tac lthy
*)
- Local_Theory.theory_result
+(* FIXME should really use local typedef here *)
+ Local_Theory.background_theory_result
(Typedef.add_typedef_global false NONE
(qty_name, map (rpair dummyS) vs, mx)
(typedef_term rel rty lthy)
--- a/src/HOL/Tools/choice_specification.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Fri Aug 27 12:57:55 2010 +0200
@@ -220,8 +220,8 @@
|> process_all (zip3 alt_names rew_imps frees)
end
- fun after_qed [[thm]] = (ProofContext.theory (fn thy =>
- #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))));
+ fun after_qed [[thm]] = ProofContext.background_theory (fn thy =>
+ #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
in
thy
|> ProofContext.init_global
--- a/src/HOL/Tools/int_arith.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/int_arith.ML Fri Aug 27 12:57:55 2010 +0200
@@ -91,7 +91,7 @@
fun number_of thy T n =
if not (Sign.of_sort thy (T, @{sort number}))
then raise CTERM ("number_of", [])
- else Numeral.mk_cnumber (Thm.ctyp_of thy T) n
+ else Numeral.mk_cnumber (Thm.ctyp_of thy T) n;
val setup =
Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
--- a/src/HOL/Tools/lin_arith.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Aug 27 12:57:55 2010 +0200
@@ -16,8 +16,7 @@
val add_simprocs: simproc list -> Context.generic -> Context.generic
val add_inj_const: string * typ -> Context.generic -> Context.generic
val add_discrete_type: string -> Context.generic -> Context.generic
- val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic ->
- Context.generic
+ val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
val setup: Context.generic -> Context.generic
val global_setup: theory -> theory
val split_limit: int Config.T
@@ -769,29 +768,11 @@
structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
-fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
- {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
- lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
-
-fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
- {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
- lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of};
-
-fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
- {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
- lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
-
-fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
- {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
- lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of};
-
-fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
-fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
-fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
-fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
-
-fun set_number_of f = Fast_Arith.map_data (map_number_of (K (serial (), f)))
-
+val add_inj_thms = Fast_Arith.add_inj_thms;
+val add_lessD = Fast_Arith.add_lessD;
+val add_simps = Fast_Arith.add_simps;
+val add_simprocs = Fast_Arith.add_simprocs;
+val set_number_of = Fast_Arith.set_number_of;
fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
val lin_arith_tac = Fast_Arith.lin_arith_tac;
--- a/src/HOL/Tools/record.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/record.ML Fri Aug 27 12:57:55 2010 +0200
@@ -420,7 +420,7 @@
equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
extfields = extfields, fieldext = fieldext }: data;
-structure Records_Data = Theory_Data
+structure Data = Theory_Data
(
type T = data;
val empty =
@@ -474,25 +474,22 @@
(* access 'records' *)
-val get_info = Symtab.lookup o #records o Records_Data.get;
+val get_info = Symtab.lookup o #records o Data.get;
fun the_info thy name =
(case get_info thy name of
SOME info => info
| NONE => error ("Unknown record type " ^ quote name));
-fun put_record name info thy =
- let
- val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
- Records_Data.get thy;
- val data = make_data (Symtab.update (name, info) records)
- sel_upd equalities extinjects extsplit splits extfields fieldext;
- in Records_Data.put data thy end;
+fun put_record name info =
+ Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ make_data (Symtab.update (name, info) records)
+ sel_upd equalities extinjects extsplit splits extfields fieldext);
(* access 'sel_upd' *)
-val get_sel_upd = #sel_upd o Records_Data.get;
+val get_sel_upd = #sel_upd o Data.get;
val is_selector = Symtab.defined o #selectors o get_sel_upd;
val get_updates = Symtab.lookup o #updates o get_sel_upd;
@@ -517,7 +514,7 @@
val upds = map (suffix updateN) all ~~ all;
val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
- equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
+ equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
val data = make_data records
{selectors = fold Symtab.update_new sels selectors,
updates = fold Symtab.update_new upds updates,
@@ -526,80 +523,61 @@
foldcong = foldcong addcongs folds,
unfoldcong = unfoldcong addcongs unfolds}
equalities extinjects extsplit splits extfields fieldext;
- in Records_Data.put data thy end;
+ in Data.put data thy end;
(* access 'equalities' *)
-fun add_equalities name thm thy =
- let
- val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
- Records_Data.get thy;
- val data = make_data records sel_upd
- (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
- in Records_Data.put data thy end;
-
-val get_equalities = Symtab.lookup o #equalities o Records_Data.get;
+fun add_equalities name thm =
+ Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ make_data records sel_upd
+ (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
+
+val get_equalities = Symtab.lookup o #equalities o Data.get;
(* access 'extinjects' *)
-fun add_extinjects thm thy =
- let
- val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
- Records_Data.get thy;
- val data =
- make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
- extsplit splits extfields fieldext;
- in Records_Data.put data thy end;
-
-val get_extinjects = rev o #extinjects o Records_Data.get;
+fun add_extinjects thm =
+ Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
+ extsplit splits extfields fieldext);
+
+val get_extinjects = rev o #extinjects o Data.get;
(* access 'extsplit' *)
-fun add_extsplit name thm thy =
- let
- val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
- Records_Data.get thy;
- val data =
- make_data records sel_upd equalities extinjects
- (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
- in Records_Data.put data thy end;
+fun add_extsplit name thm =
+ Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ make_data records sel_upd equalities extinjects
+ (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
(* access 'splits' *)
-fun add_splits name thmP thy =
- let
- val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
- Records_Data.get thy;
- val data =
- make_data records sel_upd equalities extinjects extsplit
- (Symtab.update_new (name, thmP) splits) extfields fieldext;
- in Records_Data.put data thy end;
-
-val get_splits = Symtab.lookup o #splits o Records_Data.get;
+fun add_splits name thmP =
+ Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ make_data records sel_upd equalities extinjects extsplit
+ (Symtab.update_new (name, thmP) splits) extfields fieldext);
+
+val get_splits = Symtab.lookup o #splits o Data.get;
(* parent/extension of named record *)
-val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Records_Data.get);
-val get_extension = Option.map #extension oo (Symtab.lookup o #records o Records_Data.get);
+val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
+val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
(* access 'extfields' *)
-fun add_extfields name fields thy =
- let
- val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
- Records_Data.get thy;
- val data =
- make_data records sel_upd equalities extinjects extsplit splits
- (Symtab.update_new (name, fields) extfields) fieldext;
- in Records_Data.put data thy end;
-
-val get_extfields = Symtab.lookup o #extfields o Records_Data.get;
+fun add_extfields name fields =
+ Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ make_data records sel_upd equalities extinjects extsplit splits
+ (Symtab.update_new (name, fields) extfields) fieldext);
+
+val get_extfields = Symtab.lookup o #extfields o Data.get;
fun get_extT_fields thy T =
let
@@ -609,7 +587,7 @@
in Long_Name.implode (rev (nm :: rst)) end;
val midx = maxidx_of_typs (moreT :: Ts);
val varifyT = varifyT midx;
- val {records, extfields, ...} = Records_Data.get thy;
+ val {records, extfields, ...} = Data.get thy;
val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
@@ -628,18 +606,14 @@
(* access 'fieldext' *)
-fun add_fieldext extname_types fields thy =
- let
- val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
- Records_Data.get thy;
- val fieldext' =
- fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
- val data =
- make_data records sel_upd equalities extinjects
- extsplit splits extfields fieldext';
- in Records_Data.put data thy end;
-
-val get_fieldext = Symtab.lookup o #fieldext o Records_Data.get;
+fun add_fieldext extname_types fields =
+ Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ let
+ val fieldext' =
+ fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
+ in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
+
+val get_fieldext = Symtab.lookup o #fieldext o Data.get;
(* parent records *)
@@ -1179,7 +1153,7 @@
((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
if is_selector thy s andalso is_some (get_updates thy u) then
let
- val {sel_upd = {updates, ...}, extfields, ...} = Records_Data.get thy;
+ val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
(case Symtab.lookup updates u of
@@ -1598,15 +1572,17 @@
[] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
(hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
| [x] => (head_of x, false));
- val rule'' = cterm_instantiate (map (pairself cert)
- (case rev params of
- [] =>
- (case AList.lookup (op =) (Term.add_frees g []) s of
- NONE => sys_error "try_param_tac: no such variable"
- | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
- | (_, T) :: _ =>
- [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
- (x, list_abs (params, Bound 0))])) rule';
+ val rule'' =
+ cterm_instantiate
+ (map (pairself cert)
+ (case rev params of
+ [] =>
+ (case AList.lookup (op =) (Term.add_frees g []) s of
+ NONE => sys_error "try_param_tac: no such variable"
+ | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
+ | (_, T) :: _ =>
+ [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
+ (x, list_abs (params, Bound 0))])) rule';
in compose_tac (false, rule'', nprems_of rule) i end);
@@ -1635,7 +1611,8 @@
val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
val ((_, cons), thy') = thy
|> Iso_Tuple_Support.add_iso_tuple_type
- (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right);
+ (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
+ (fastype_of left, fastype_of right);
in
(cons $ left $ right, (thy', i + 1))
end;
@@ -1778,7 +1755,10 @@
("ext_surjective", surject),
("ext_split", split_meta)]);
- in (((ext_name, ext_type), (ext_tyco, alphas_zeta), extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end;
+ in
+ (((ext_name, ext_type), (ext_tyco, alphas_zeta),
+ extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
+ end;
fun chunks [] [] = []
| chunks [] xs = [xs]
@@ -1795,7 +1775,7 @@
(* mk_recordT *)
-(*builds up the record type from the current extension tpye extT and a list
+(*build up the record type from the current extension tpye extT and a list
of parent extensions, starting with the root of the record hierarchy*)
fun mk_recordT extT =
fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
@@ -1834,8 +1814,10 @@
val lhs = HOLogic.mk_random T size;
val tc = HOLogic.mk_return Tm @{typ Random.seed}
(HOLogic.mk_valtermify_app extN params T);
- val rhs = HOLogic.mk_ST
- (map (fn (v, T') => ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
+ val rhs =
+ HOLogic.mk_ST
+ (map (fn (v, T') =>
+ ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
@@ -1860,17 +1842,20 @@
fun add_code ext_tyco vs extT ext simps inject thy =
let
- val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
- (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
- Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
- fun tac eq_def = Class.intro_classes_tac []
+ val eq =
+ (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+ (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
+ Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
+ fun tac eq_def =
+ Class.intro_classes_tac []
THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
THEN ALLGOALS (rtac @{thm refl});
fun mk_eq thy eq_def = Simplifier.rewrite_rule
[(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
- fun mk_eq_refl thy = @{thm HOL.eq_refl}
+ fun mk_eq_refl thy =
+ @{thm HOL.eq_refl}
|> Thm.instantiate
- ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
+ ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
|> AxClass.unoverload thy;
in
thy
@@ -1944,7 +1929,8 @@
val extension_name = full binding;
- val ((ext, (ext_tyco, vs), extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
+ val ((ext, (ext_tyco, vs),
+ extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
thy
|> Sign.qualified_path false binding
|> extension_definition extension_name fields alphas_ext zeta moreT more vars;
--- a/src/HOL/Tools/typedef.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Fri Aug 27 12:57:55 2010 +0200
@@ -186,7 +186,8 @@
||> Thm.term_of;
val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
- Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
+ Local_Theory.background_theory_result
+ (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy);
val typedef =
@@ -246,7 +247,7 @@
in
lthy2
|> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
- |> Local_Theory.theory (Typedef_Interpretation.data full_tname)
+ |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
|> pair (full_tname, info)
end;
--- a/src/HOL/ex/Numeral.thy Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Fri Aug 27 12:57:55 2010 +0200
@@ -97,7 +97,7 @@
structure Dig_Simps = Named_Thms
(
val name = "numeral"
- val description = "Simplification rules for numerals"
+ val description = "simplification rules for numerals"
)
*}
--- a/src/HOLCF/Tools/pcpodef.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Fri Aug 27 12:57:55 2010 +0200
@@ -326,7 +326,7 @@
val args = map (apsnd (prep_constraint ctxt)) raw_args;
val (goal1, goal2, make_result) =
prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
- fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
+ fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
| after_qed _ = raise Fail "cpodef_proof";
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
@@ -337,7 +337,7 @@
val args = map (apsnd (prep_constraint ctxt)) raw_args;
val (goal1, goal2, make_result) =
prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
- fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
+ fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
| after_qed _ = raise Fail "pcpodef_proof";
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Aug 27 12:57:55 2010 +0200
@@ -88,13 +88,19 @@
val cut_lin_arith_tac: simpset -> int -> tactic
val lin_arith_tac: Proof.context -> bool -> int -> tactic
val lin_arith_simproc: simpset -> term -> thm option
- val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
- lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
- number_of : serial * (theory -> typ -> int -> cterm)}
- -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
- lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
- number_of : serial * (theory -> typ -> int -> cterm)})
- -> Context.generic -> Context.generic
+ val map_data:
+ ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
+ lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
+ number_of: (theory -> typ -> int -> cterm) option} ->
+ {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
+ lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
+ number_of: (theory -> typ -> int -> cterm) option}) ->
+ Context.generic -> Context.generic
+ val add_inj_thms: thm list -> Context.generic -> Context.generic
+ val add_lessD: thm -> Context.generic -> Context.generic
+ val add_simps: thm list -> Context.generic -> Context.generic
+ val add_simprocs: simproc list -> Context.generic -> Context.generic
+ val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
val trace: bool Unsynchronized.ref
end;
@@ -105,8 +111,6 @@
(** theory data **)
-fun no_number_of _ _ _ = raise CTERM ("number_of", [])
-
structure Data = Generic_Data
(
type T =
@@ -116,32 +120,57 @@
lessD: thm list,
neqE: thm list,
simpset: Simplifier.simpset,
- number_of : serial * (theory -> typ -> int -> cterm)};
+ number_of: (theory -> typ -> int -> cterm) option};
- val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
- lessD = [], neqE = [], simpset = Simplifier.empty_ss,
- number_of = (serial (), no_number_of) } : T;
+ val empty : T =
+ {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
+ lessD = [], neqE = [], simpset = Simplifier.empty_ss,
+ number_of = NONE};
val extend = I;
fun merge
- ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
- lessD = lessD1, neqE=neqE1, simpset = simpset1,
- number_of = (number_of1 as (s1, _))},
- {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
- lessD = lessD2, neqE=neqE2, simpset = simpset2,
- number_of = (number_of2 as (s2, _))}) =
+ ({add_mono_thms = add_mono_thms1, mult_mono_thms = mult_mono_thms1, inj_thms = inj_thms1,
+ lessD = lessD1, neqE = neqE1, simpset = simpset1, number_of = number_of1},
+ {add_mono_thms = add_mono_thms2, mult_mono_thms = mult_mono_thms2, inj_thms = inj_thms2,
+ lessD = lessD2, neqE = neqE2, simpset = simpset2, number_of = number_of2}) : T =
{add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2),
mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2),
inj_thms = Thm.merge_thms (inj_thms1, inj_thms2),
lessD = Thm.merge_thms (lessD1, lessD2),
neqE = Thm.merge_thms (neqE1, neqE2),
simpset = Simplifier.merge_ss (simpset1, simpset2),
- (* FIXME depends on accidental load order !?! *)
- number_of = if s1 > s2 then number_of1 else number_of2};
+ number_of = if is_some number_of1 then number_of1 else number_of2};
);
val map_data = Data.map;
val get_data = Data.get o Context.Proof;
+fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
+ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
+ lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
+
+fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
+ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+ lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of};
+
+fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
+ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+ lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
+
+fun add_inj_thms thms = map_data (map_inj_thms (append thms));
+fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [thm]));
+fun add_simps thms = map_data (map_simpset (fn simpset => simpset addsimps thms));
+fun add_simprocs procs = map_data (map_simpset (fn simpset => simpset addsimprocs procs));
+
+fun set_number_of f =
+ map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, ...} =>
+ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+ lessD = lessD, neqE = neqE, simpset = simpset, number_of = SOME f});
+
+fun number_of ctxt =
+ (case Data.get (Context.Proof ctxt) of
+ {number_of = SOME f, ...} => f (ProofContext.theory_of ctxt)
+ | _ => fn _ => fn _ => raise CTERM ("number_of", []));
+
(*** A fast decision procedure ***)
@@ -446,8 +475,8 @@
let
val ctxt = Simplifier.the_context ss;
val thy = ProofContext.theory_of ctxt;
- val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset,
- number_of = (_, num_of), ...} = get_data ctxt;
+ val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt;
+ val number_of = number_of ctxt;
val simpset' = Simplifier.inherit_context ss simpset;
fun only_concl f thm =
if Thm.no_prems thm then f (Thm.concl_of thm) else NONE;
@@ -493,7 +522,7 @@
val T = #T (Thm.rep_cterm cv)
in
mth
- |> Thm.instantiate ([], [(cv, num_of thy T n)])
+ |> Thm.instantiate ([], [(cv, number_of T n)])
|> rewrite_concl
|> discharge_prem
handle CTERM _ => mult_by_add n thm
--- a/src/Pure/Isar/class.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/class.ML Fri Aug 27 12:57:55 2010 +0200
@@ -368,7 +368,7 @@
fun gen_classrel mk_prop classrel thy =
let
fun after_qed results =
- ProofContext.theory ((fold o fold) AxClass.add_classrel results);
+ ProofContext.background_theory ((fold o fold) AxClass.add_classrel results);
in
thy
|> ProofContext.init_global
@@ -482,7 +482,7 @@
val type_name = sanitize_name o Long_Name.base_name;
-fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result
+fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
(AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
##> Local_Theory.target synchronize_inst_syntax;
@@ -572,7 +572,7 @@
val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
fun after_qed' results =
- Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
+ Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
#> after_qed;
in
lthy
@@ -608,7 +608,7 @@
val (tycos, vs, sort) = read_multi_arity thy raw_arities;
val sorts = map snd vs;
val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
- fun after_qed results = ProofContext.theory
+ fun after_qed results = ProofContext.background_theory
((fold o fold) AxClass.add_arity results);
in
thy
--- a/src/Pure/Isar/class_declaration.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML Fri Aug 27 12:57:55 2010 +0200
@@ -330,7 +330,7 @@
val some_prop = try the_single props;
val some_dep_morph = try the_single (map snd deps);
fun after_qed some_wit =
- ProofContext.theory (Class.register_subclass (sub, sup)
+ ProofContext.background_theory (Class.register_subclass (sub, sup)
some_dep_morph some_wit export)
#> ProofContext.theory_of #> Named_Target.init sub;
in do_proof after_qed some_prop goal_ctxt end;
--- a/src/Pure/Isar/expression.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/expression.ML Fri Aug 27 12:57:55 2010 +0200
@@ -824,8 +824,9 @@
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- fun after_qed witss eqns = (ProofContext.theory o Context.theory_map)
- (note_eqns_register deps witss attrss eqns export export');
+ fun after_qed witss eqns =
+ (ProofContext.background_theory o Context.theory_map)
+ (note_eqns_register deps witss attrss eqns export export');
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
@@ -872,7 +873,7 @@
val target = intern thy raw_target;
val target_ctxt = Named_Target.init target thy;
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
- fun after_qed witss = ProofContext.theory
+ fun after_qed witss = ProofContext.background_theory
(fold (fn ((dep, morph), wits) => Locale.add_dependency
target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
in Element.witness_proof after_qed propss goal_ctxt end;
--- a/src/Pure/Isar/generic_target.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML Fri Aug 27 12:57:55 2010 +0200
@@ -195,16 +195,16 @@
(Morphism.transform (Local_Theory.global_morphism lthy) decl);
in
lthy
- |> Local_Theory.theory (Context.theory_map global_decl)
+ |> Local_Theory.background_theory (Context.theory_map global_decl)
|> Local_Theory.target (Context.proof_map global_decl)
end;
fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
let
- val (const, lthy2) = lthy |> Local_Theory.theory_result
+ val (const, lthy2) = lthy |> Local_Theory.background_theory_result
(Sign.declare_const ((b, U), mx));
val lhs = list_comb (const, type_params @ term_params);
- val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
+ val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result
(Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
in ((lhs, def), lthy3) end;
@@ -214,12 +214,13 @@
val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
in
lthy
- |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+ |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
|> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
end;
-fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
- (Sign.add_abbrev (#1 prmode) (b, t) #->
- (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
+fun theory_abbrev prmode ((b, mx), t) =
+ Local_Theory.background_theory
+ (Sign.add_abbrev (#1 prmode) (b, t) #->
+ (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
end;
--- a/src/Pure/Isar/local_theory.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML Fri Aug 27 12:57:55 2010 +0200
@@ -21,8 +21,8 @@
val target_of: local_theory -> Proof.context
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
- val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
- val theory: (theory -> theory) -> local_theory -> local_theory
+ val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
+ val background_theory: (theory -> theory) -> local_theory -> local_theory
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
@@ -144,7 +144,7 @@
val checkpoint = raw_theory Theory.checkpoint;
-fun theory_result f lthy =
+fun background_theory_result f lthy =
lthy |> raw_theory_result (fn thy =>
thy
|> Sign.map_naming (K (naming_of lthy))
@@ -152,7 +152,7 @@
||> Sign.restore_naming thy
||> Theory.checkpoint);
-fun theory f = #2 o theory_result (f #> pair ());
+fun background_theory f = #2 o background_theory_result (f #> pair ());
fun target_result f lthy =
let
@@ -169,7 +169,7 @@
fun target f = #2 o target_result (f #> pair ());
fun map_contexts f =
- theory (Context.theory_map f) #>
+ background_theory (Context.theory_map f) #>
target (Context.proof_map f) #>
Context.proof_map f;
@@ -261,7 +261,7 @@
(* exit *)
-val exit = ProofContext.theory Theory.checkpoint o operation #exit;
+val exit = ProofContext.background_theory Theory.checkpoint o operation #exit;
val exit_global = ProofContext.theory_of o exit;
fun exit_result f (x, lthy) =
--- a/src/Pure/Isar/locale.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/locale.ML Fri Aug 27 12:57:55 2010 +0200
@@ -497,8 +497,8 @@
fun add_thmss loc kind args ctxt =
let
val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
- val ctxt'' = ctxt' |> ProofContext.theory (
- (change_locale loc o apfst o apsnd) (cons (args', serial ()))
+ val ctxt'' = ctxt' |> ProofContext.background_theory
+ ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
#>
(* Registrations *)
(fn thy => fold_rev (fn (_, morph) =>
@@ -519,7 +519,7 @@
[([Drule.dummy_thm], [])])];
fun add_syntax_declaration loc decl =
- ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
+ ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
#> add_declaration loc decl;
--- a/src/Pure/Isar/named_target.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/named_target.ML Fri Aug 27 12:57:55 2010 +0200
@@ -118,7 +118,7 @@
(Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
in
lthy
- |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+ |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
|> Local_Theory.target (Locale.add_thmss locale kind local_facts')
end
@@ -129,19 +129,21 @@
(* abbrev *)
-fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
- (Sign.add_abbrev Print_Mode.internal (b, t)) #->
- (fn (lhs, _) => locale_const_declaration ta prmode
- ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+fun locale_abbrev ta prmode ((b, mx), t) xs =
+ Local_Theory.background_theory_result
+ (Sign.add_abbrev Print_Mode.internal (b, t)) #->
+ (fn (lhs, _) => locale_const_declaration ta prmode
+ ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
prmode (b, mx) (global_rhs, t') xs lthy =
- if is_locale
- then lthy
- |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
- |> is_class ? Class.abbrev target prmode ((b, mx), t')
- else lthy
- |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
+ if is_locale then
+ lthy
+ |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
+ |> is_class ? Class.abbrev target prmode ((b, mx), t')
+ else
+ lthy
+ |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
(* pretty *)
@@ -200,9 +202,10 @@
fun init target thy = init_target (named_target thy target) thy;
-fun reinit lthy = case peek lthy
- of SOME {target, ...} => init target o Local_Theory.exit_global
- | NONE => error "Not in a named target";
+fun reinit lthy =
+ (case peek lthy of
+ SOME {target, ...} => init target o Local_Theory.exit_global
+ | NONE => error "Not in a named target");
val theory_init = init_target global_target;
--- a/src/Pure/Isar/overloading.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/overloading.ML Fri Aug 27 12:57:55 2010 +0200
@@ -140,7 +140,7 @@
end
fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
- Local_Theory.theory_result
+ Local_Theory.background_theory_result
(Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
##> Local_Theory.target synchronize_syntax
--- a/src/Pure/Isar/proof_context.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Aug 27 12:57:55 2010 +0200
@@ -38,8 +38,8 @@
val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
val transfer_syntax: theory -> Proof.context -> Proof.context
val transfer: theory -> Proof.context -> Proof.context
- val theory: (theory -> theory) -> Proof.context -> Proof.context
- val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
+ val background_theory: (theory -> theory) -> Proof.context -> Proof.context
+ val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
val extern_fact: Proof.context -> string -> xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
@@ -283,9 +283,9 @@
fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
-fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
+fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
-fun theory_result f ctxt =
+fun background_theory_result f ctxt =
let val (res, thy') = f (theory_of ctxt)
in (res, ctxt |> transfer thy') end;
--- a/src/Pure/Isar/typedecl.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML Fri Aug 27 12:57:55 2010 +0200
@@ -34,7 +34,7 @@
fun basic_decl decl (b, n, mx) lthy =
let val name = Local_Theory.full_name lthy b in
lthy
- |> Local_Theory.theory (decl name)
+ |> Local_Theory.background_theory (decl name)
|> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)]
|> Local_Theory.type_alias b name
|> pair name
--- a/src/Pure/Proof/extraction.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Aug 27 12:57:55 2010 +0200
@@ -204,7 +204,7 @@
realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
defs = Library.merge Thm.eq_thm (defs1, defs2),
expand = Library.merge (op =) (expand1, expand2),
- prep = (case prep1 of NONE => prep2 | _ => prep1)};
+ prep = if is_some prep1 then prep1 else prep2};
);
fun read_condeq thy =
--- a/src/Pure/Thy/thy_load.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML Fri Aug 27 12:57:55 2010 +0200
@@ -195,7 +195,7 @@
val _ = Context.>> Local_Theory.propagate_ml_env;
val provide = provide (src_path, (path, id));
- val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
+ val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide));
in () end;
fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
--- a/src/Pure/Thy/thy_output.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Aug 27 12:57:55 2010 +0200
@@ -6,31 +6,37 @@
signature THY_OUTPUT =
sig
- val display: bool Unsynchronized.ref
- val quotes: bool Unsynchronized.ref
- val indent: int Unsynchronized.ref
- val source: bool Unsynchronized.ref
- val break: bool Unsynchronized.ref
- val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
- val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
+ val display_default: bool Unsynchronized.ref
+ val quotes_default: bool Unsynchronized.ref
+ val indent_default: int Unsynchronized.ref
+ val source_default: bool Unsynchronized.ref
+ val break_default: bool Unsynchronized.ref
+ val display: bool Config.T
+ val quotes: bool Config.T
+ val indent: int Config.T
+ val source: bool Config.T
+ val break: bool Config.T
+ val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
+ val add_option: string -> (string -> Proof.context -> Proof.context) -> unit
val defined_command: string -> bool
val defined_option: string -> bool
val print_antiquotations: unit -> unit
val boolean: string -> bool
val integer: string -> int
val antiquotation: string -> 'a context_parser ->
- ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
+ ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit
datatype markup = Markup | MarkupEnv | Verbatim
val modes: string list Unsynchronized.ref
val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
- val pretty_text: string -> Pretty.T
+ val pretty_text: Proof.context -> string -> Pretty.T
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val str_of_source: Args.src -> string
- val maybe_pretty_source: ('a -> Pretty.T) -> Args.src -> 'a list -> Pretty.T list
- val output: Pretty.T list -> string
+ val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
+ Args.src -> 'a list -> Pretty.T list
+ val output: Proof.context -> Pretty.T list -> string
end;
structure Thy_Output: THY_OUTPUT =
@@ -38,11 +44,31 @@
(** global options **)
-val display = Unsynchronized.ref false;
-val quotes = Unsynchronized.ref false;
-val indent = Unsynchronized.ref 0;
-val source = Unsynchronized.ref false;
-val break = Unsynchronized.ref false;
+val display_default = Unsynchronized.ref false;
+val quotes_default = Unsynchronized.ref false;
+val indent_default = Unsynchronized.ref 0;
+val source_default = Unsynchronized.ref false;
+val break_default = Unsynchronized.ref false;
+
+val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default);
+val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default);
+val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default);
+val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default);
+val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default);
+
+val _ = Context.>> (Context.map_theory
+ (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break));
+
+
+structure Wrappers = Proof_Data
+(
+ type T = ((unit -> string) -> unit -> string) list;
+ fun init _ = [];
+);
+
+fun add_wrapper wrapper = Wrappers.map (cons wrapper);
+
+val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
@@ -51,22 +77,23 @@
local
val global_commands =
- Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
+ Unsynchronized.ref
+ (Symtab.empty: (Args.src -> Toplevel.state -> Proof.context -> string) Symtab.table);
val global_options =
- Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
+ Unsynchronized.ref (Symtab.empty: (string -> Proof.context -> Proof.context) Symtab.table);
-fun add_item kind (name, x) tab =
+fun add_item kind name item tab =
(if not (Symtab.defined tab name) then ()
else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name);
- Symtab.update (name, x) tab);
+ Symtab.update (name, item) tab);
in
-fun add_commands xs =
- CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs));
-fun add_options xs =
- CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs));
+fun add_command name cmd =
+ CRITICAL (fn () => Unsynchronized.change global_commands (add_item "command" name cmd));
+fun add_option name opt =
+ CRITICAL (fn () => Unsynchronized.change global_options (add_item "option" name opt));
fun defined_command name = Symtab.defined (! global_commands) name;
fun defined_option name = Symtab.defined (! global_options) name;
@@ -77,18 +104,15 @@
NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
| SOME f =>
(Position.report (Markup.doc_antiq name) pos;
- (fn state => f src state handle ERROR msg =>
+ (fn state => fn ctxt => f src state ctxt handle ERROR msg =>
cat_error msg ("The error(s) above occurred in document antiquotation: " ^
quote name ^ Position.str_of pos))))
end;
-fun option (name, s) f () =
+fun option (name, s) ctxt =
(case Symtab.lookup (! global_options) name of
NONE => error ("Unknown document antiquotation option: " ^ quote name)
- | SOME opt => opt s f ());
-
-fun options [] f = f
- | options (opt :: opts) f = option opt (options opts f);
+ | SOME opt => opt s ctxt);
fun print_antiquotations () =
@@ -100,10 +124,11 @@
end;
-fun antiquotation name scan out = add_commands [(name, fn src => fn state =>
- let val (x, ctxt) = Args.context_syntax "document antiquotation"
- scan src (Toplevel.presentation_context_of state)
- in out {source = src, state = state, context = ctxt} x end)];
+fun antiquotation name scan out =
+ add_command name
+ (fn src => fn state => fn ctxt =>
+ let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt
+ in out {source = src, state = state, context = ctxt'} x end);
@@ -151,10 +176,13 @@
let
fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
| expand (Antiquote.Antiq (ss, (pos, _))) =
- let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
- options opts (fn () => command src state) (); (*preview errors!*)
- Print_Mode.with_modes (! modes @ Latex.modes)
- (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
+ let
+ val (opts, src) = Token.read_antiq lex antiq (ss, pos);
+ val opts_ctxt = fold option opts (Toplevel.presentation_context_of state);
+ val cmd = wrap opts_ctxt (fn () => command src state opts_ctxt);
+ val _ = cmd (); (*preview errors!*)
+ in
+ Print_Mode.with_modes (! modes @ Latex.modes) (Output.no_warnings_CRITICAL cmd) ()
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
@@ -417,31 +445,31 @@
(* options *)
-val _ = add_options
- [("show_types", setmp_CRITICAL Syntax.show_types o boolean),
- ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
- ("show_structs", setmp_CRITICAL show_structs o boolean),
- ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
- ("long_names", setmp_CRITICAL Name_Space.long_names o boolean),
- ("short_names", setmp_CRITICAL Name_Space.short_names o boolean),
- ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean),
- ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
- ("display", setmp_CRITICAL display o boolean),
- ("break", setmp_CRITICAL break o boolean),
- ("quotes", setmp_CRITICAL quotes o boolean),
- ("mode", fn s => fn f => Print_Mode.with_modes [s] f),
- ("margin", setmp_CRITICAL Pretty.margin_default o integer),
- ("indent", setmp_CRITICAL indent o integer),
- ("source", setmp_CRITICAL source o boolean),
- ("goals_limit", setmp_CRITICAL goals_limit o integer)];
+val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
+val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
+val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean);
+val _ = add_option "show_question_marks" (add_wrapper o setmp_CRITICAL show_question_marks 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);
+val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean);
+val _ = add_option "display" (Config.put display o boolean);
+val _ = add_option "break" (Config.put break o boolean);
+val _ = add_option "quotes" (Config.put quotes o boolean);
+val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
+val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
+val _ = add_option "indent" (Config.put indent o integer);
+val _ = add_option "source" (Config.put source o boolean);
+val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer);
(* basic pretty printing *)
-fun tweak_line s =
- if ! display then s else Symbol.strip_blanks s;
+fun tweak_line ctxt s =
+ if Config.get ctxt display then s else Symbol.strip_blanks s;
-val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
+fun pretty_text ctxt =
+ Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o Library.split_lines;
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
@@ -490,19 +518,19 @@
val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
-fun maybe_pretty_source pretty src xs =
- map pretty xs (*always pretty in order to exhibit errors!*)
- |> (if ! source then K [pretty_text (str_of_source src)] else I);
+fun maybe_pretty_source pretty ctxt src xs =
+ map (pretty ctxt) xs (*always pretty in order to exhibit errors!*)
+ |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
-fun output prts =
+fun output ctxt prts =
prts
- |> (if ! quotes then map Pretty.quote else I)
- |> (if ! display then
- map (Output.output o Pretty.string_of o Pretty.indent (! indent))
+ |> (if Config.get ctxt quotes then map Pretty.quote else I)
+ |> (if Config.get ctxt display then
+ map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
#> space_implode "\\isasep\\isanewline%\n"
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else
- map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of))
+ map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
#> space_implode "\\isasep\\isanewline%\n"
#> enclose "\\isa{" "}");
@@ -515,11 +543,12 @@
local
fun basic_entities name scan pretty = antiquotation name scan
- (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
+ (fn {source, context, ...} => output context o maybe_pretty_source pretty context source);
fun basic_entities_style name scan pretty = antiquotation name scan
(fn {source, context, ...} => fn (style, xs) =>
- output (maybe_pretty_source (fn x => pretty context (style, x)) source xs));
+ output context
+ (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
fun basic_entity name scan = basic_entities name (scan >> single);
@@ -533,7 +562,7 @@
val _ = basic_entity "const" (Args.const_proper false) pretty_const;
val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
-val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);
+val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
@@ -554,7 +583,7 @@
| _ => error "No proof state");
fun goal_state name main_goal = antiquotation name (Scan.succeed ())
- (fn {state, ...} => fn () => output
+ (fn {state, context, ...} => fn () => output context
[Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
in
@@ -578,7 +607,7 @@
val _ = context
|> Proof.theorem NONE (K I) [[(prop, [])]]
|> Proof.global_terminal_proof methods;
- in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
+ in output context (maybe_pretty_source pretty_term context prop_src [prop]) end);
(* ML text *)
@@ -589,8 +618,8 @@
(fn {context, ...} => fn (txt, pos) =>
(ML_Context.eval_in (SOME context) false pos (ml pos txt);
Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
- |> (if ! quotes then quote else I)
- |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+ |> (if Config.get context quotes then quote else I)
+ |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else
split_lines
#> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
--- a/src/Tools/Code/code_simp.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Tools/Code/code_simp.ML Fri Aug 27 12:57:55 2010 +0200
@@ -37,7 +37,8 @@
(* dedicated simpset *)
-structure Simpset = Theory_Data (
+structure Simpset = Theory_Data
+(
type T = simpset;
val empty = empty_ss;
fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
--- a/src/Tools/quickcheck.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/Tools/quickcheck.ML Fri Aug 27 12:57:55 2010 +0200
@@ -78,27 +78,32 @@
datatype test_params = Test_Params of
{ size: int, iterations: int, default_type: typ list, no_assms: bool,
- expect : expectation, report: bool, quiet : bool};
+ expect : expectation, report: bool, quiet : bool};
fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
((size, iterations), ((default_type, no_assms), ((expect, report), quiet)));
+
fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) =
Test_Params { size = size, iterations = iterations, default_type = default_type,
- no_assms = no_assms, expect = expect, report = report, quiet = quiet };
+ no_assms = no_assms, expect = expect, report = report, quiet = quiet };
+
fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))));
-fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
- no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
+
+fun merge_test_params
+ (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
+ no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
- no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
+ no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
structure Data = Theory_Data
(
- type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
- * test_params;
+ type T =
+ (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
+ * test_params;
val empty = ([], Test_Params
{ size = 10, iterations = 100, default_type = [], no_assms = false,
expect = No_Expectation, report = false, quiet = false});