--- a/src/Provers/clasimp.ML Sat Mar 29 22:55:49 2008 +0100
+++ b/src/Provers/clasimp.ML Sat Mar 29 22:55:57 2008 +0100
@@ -25,8 +25,11 @@
include CLASIMP_DATA
type claset
type clasimpset
+ val get_css: Context.generic -> clasimpset
+ val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic
val change_clasimpset: (clasimpset -> clasimpset) -> unit
val clasimpset: unit -> clasimpset
+ val local_clasimpset_of: Proof.context -> clasimpset
val addSIs2: clasimpset * thm list -> clasimpset
val addSEs2: clasimpset * thm list -> clasimpset
val addSDs2: clasimpset * thm list -> clasimpset
@@ -57,14 +60,12 @@
val slow_simp_tac: clasimpset -> int -> tactic
val best_simp_tac: clasimpset -> int -> tactic
val attrib: (clasimpset * thm list -> clasimpset) -> attribute
- val get_local_clasimpset: Proof.context -> clasimpset
- val local_clasimpset_of: Proof.context -> clasimpset
val iff_add: attribute
val iff_add': attribute
val iff_del: attribute
val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
- val setup: theory -> theory
+ val clasimp_setup: theory -> theory
end;
functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
@@ -72,26 +73,32 @@
open Data;
+
+(* type clasimpset *)
+
type claset = Classical.claset;
type clasimpset = claset * simpset;
-fun change_clasimpset_of thy f =
- let val (cs', ss') = f (Classical.get_claset thy, Simplifier.get_simpset thy) in
- Classical.change_claset_of thy (fn _ => cs');
- Simplifier.change_simpset_of thy (fn _ => ss')
- end;
+fun get_css context = (Classical.get_cs context, Simplifier.get_ss context);
+
+fun map_css f context =
+ let val (cs', ss') = f (get_css context)
+ in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end;
-fun change_clasimpset f = change_clasimpset_of (ML_Context.the_global_context ()) f;
+fun change_clasimpset f = Context.>> (fn context => (Context.the_theory context; map_css f context));
fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
+fun local_clasimpset_of ctxt =
+ (Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
+
(* clasimpset operations *)
(*this interface for updating a clasimpset is rudimentary and just for
convenience for the most common cases*)
-fun pair_upd1 f ((a,b),x) = (f(a,x), b);
-fun pair_upd2 f ((a,b),x) = (a, f(b,x));
+fun pair_upd1 f ((a, b), x) = (f (a, x), b);
+fun pair_upd2 f ((a, b), x) = (a, f (b, x));
fun op addSIs2 arg = pair_upd1 Classical.addSIs arg;
fun op addSEs2 arg = pair_upd1 Classical.addSEs arg;
@@ -156,9 +163,9 @@
in
val op addIffs =
- Library.foldl
+ Library.foldl
(addIff (Classical.addSEs, Classical.addSIs)
- (Classical.addEs, Classical.addIs)
+ (Classical.addEs, Classical.addIs)
Simplifier.addsimps);
val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps);
@@ -251,28 +258,11 @@
(* access clasimpset *)
-fun get_local_clasimpset ctxt =
- (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
-
-fun local_clasimpset_of ctxt =
- (Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
(* attributes *)
-fun attrib f = Thm.declaration_attribute (fn th =>
- fn Context.Theory thy => (change_clasimpset_of thy (fn css => f (css, [th])); Context.Theory thy)
- | Context.Proof ctxt =>
- let
- val cs = Classical.get_local_claset ctxt;
- val ss = Simplifier.get_local_simpset ctxt;
- val (cs', ss') = f ((cs, ss), [th]);
- val ctxt' =
- ctxt
- |> Classical.put_local_claset cs'
- |> Simplifier.put_local_simpset ss';
- in Context.Proof ctxt' end);
-
+fun attrib f = Thm.declaration_attribute (fn th => map_css (fn css => f (css, [th])));
fun attrib' f (x, th) = (f (x, [th]), th);
val iff_add = attrib (op addIffs);
@@ -320,7 +310,7 @@
(* theory setup *)
-val setup =
+val clasimp_setup =
(Attrib.add_attributes
[("iff", iff_att, "declaration of Simplifier / Classical rules")] #>
Method.add_methods
--- a/src/Provers/classical.ML Sat Mar 29 22:55:49 2008 +0100
+++ b/src/Provers/classical.ML Sat Mar 29 22:55:57 2008 +0100
@@ -40,7 +40,6 @@
type claset
val empty_cs: claset
val print_cs: claset -> unit
- val print_claset: theory -> unit
val rep_cs:
claset -> {safeIs: thm list, safeEs: thm list,
hazIs: thm list, hazEs: thm list,
@@ -72,7 +71,6 @@
val appSWrappers : claset -> wrapper
val appWrappers : claset -> wrapper
- val change_claset_of: theory -> (claset -> claset) -> unit
val change_claset: (claset -> claset) -> unit
val claset_of: theory -> claset
val claset: unit -> claset
@@ -140,9 +138,7 @@
val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
val del_context_unsafe_wrapper: string -> theory -> theory
val get_claset: theory -> claset
- val get_local_claset: Proof.context -> claset
- val put_local_claset: claset -> Proof.context -> Proof.context
- val print_local_claset: Proof.context -> unit
+ val map_claset: (claset -> claset) -> theory -> theory
val get_cs: Context.generic -> claset
val map_cs: (claset -> claset) -> Context.generic -> Context.generic
val safe_dest: int option -> attribute
@@ -863,27 +859,26 @@
structure GlobalClaset = TheoryDataFun
(
- type T = claset ref * context_cs;
- val empty = (ref empty_cs, empty_context_cs);
- fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
- val extend = copy;
- fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
- (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
+ type T = claset * context_cs;
+ val empty = (empty_cs, empty_context_cs);
+ val copy = I;
+ val extend = I;
+ fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
+ (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
);
-val print_claset = print_cs o ! o #1 o GlobalClaset.get;
-val get_claset = ! o #1 o GlobalClaset.get;
+val get_claset = #1 o GlobalClaset.get;
+val map_claset = GlobalClaset.map o apfst;
val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
fun map_context_cs f = GlobalClaset.map (apsnd
(fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
-val change_claset_of = change o #1 o GlobalClaset.get;
-fun change_claset f = change_claset_of (ML_Context.the_global_context ()) f;
+fun change_claset f = Context.>> (Context.map_theory (map_claset f));
fun claset_of thy =
- let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
- in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
+ let val (cs, ctxt_cs) = GlobalClaset.get thy
+ in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
val claset = claset_of o ML_Context.the_global_context;
fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
@@ -900,15 +895,11 @@
(* context dependent components *)
-fun add_context_safe_wrapper wrapper = (map_context_cs o apfst)
- (AList.update (op =) wrapper);
-fun del_context_safe_wrapper name = (map_context_cs o apfst)
- (AList.delete (op =) name);
+fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
+fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
-fun add_context_unsafe_wrapper wrapper = (map_context_cs o apsnd)
- (AList.update (op =) wrapper);
-fun del_context_unsafe_wrapper name = (map_context_cs o apsnd)
- (AList.delete (op =) name);
+fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
+fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
(* local clasets *)
@@ -919,29 +910,20 @@
val init = get_claset;
);
-val get_local_claset = LocalClaset.get;
-val put_local_claset = LocalClaset.put;
-
fun local_claset_of ctxt =
- context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
-
-val print_local_claset = print_cs o local_claset_of;
+ context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
(* generic clasets *)
-fun get_cs (Context.Theory thy) = claset_of thy
- | get_cs (Context.Proof ctxt) = local_claset_of ctxt;
-
-fun map_cs f (Context.Theory thy) = (change_claset_of thy f; Context.Theory thy)
- | map_cs f (Context.Proof ctxt) = Context.Proof (LocalClaset.map f ctxt);
+val get_cs = Context.cases claset_of local_claset_of;
+fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f);
(* attributes *)
fun attrib f = Thm.declaration_attribute (fn th =>
- fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
- | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
+ Context.mapping (map_claset (f th)) (LocalClaset.map (f th)));
fun safe_dest w = attrib (addSE w o make_elim);
val safe_elim = attrib o addSE;
@@ -1071,7 +1053,7 @@
(** theory setup **)
-val setup = GlobalClaset.init #> setup_attrs #> setup_methods;
+val setup = setup_attrs #> setup_methods;
@@ -1080,9 +1062,7 @@
val _ =
OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
OuterKeyword.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
- (Toplevel.node_case
- (Context.cases print_claset print_local_claset)
- (print_local_claset o Proof.context_of)))));
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+ Toplevel.keep (print_cs o local_claset_of o Toplevel.context_of)));
end;
--- a/src/Pure/simplifier.ML Sat Mar 29 22:55:49 2008 +0100
+++ b/src/Pure/simplifier.ML Sat Mar 29 22:55:57 2008 +0100
@@ -9,8 +9,6 @@
signature BASIC_SIMPLIFIER =
sig
include BASIC_META_SIMPLIFIER
- val print_simpset: theory -> unit
- val change_simpset_of: theory -> (simpset -> simpset) -> unit
val change_simpset: (simpset -> simpset) -> unit
val simpset_of: theory -> simpset
val simpset: unit -> simpset
@@ -60,10 +58,6 @@
val full_rewrite: simpset -> conv
val asm_lr_rewrite: simpset -> conv
val asm_full_rewrite: simpset -> conv
- val get_simpset: theory -> simpset
- val print_local_simpset: Proof.context -> unit
- val get_local_simpset: Proof.context -> simpset
- val put_local_simpset: simpset -> Proof.context -> Proof.context
val get_ss: Context.generic -> simpset
val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
val attrib: (simpset * thm list -> simpset) -> attribute
@@ -71,6 +65,7 @@
val simp_del: attribute
val cong_add: attribute
val cong_del: attribute
+ val map_simpset: (simpset -> simpset) -> theory -> theory
val get_simproc: Context.generic -> xstring -> simproc
val def_simproc: {name: string, lhss: string list,
proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
@@ -94,28 +89,35 @@
(** simpset data **)
-(* global simpsets *)
-
-structure GlobalSimpset = TheoryDataFun
+structure SimpsetData = GenericDataFun
(
- type T = simpset ref;
- val empty = ref empty_ss;
- fun copy (ref ss) = ref ss: T;
- fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
- fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
+ type T = simpset;
+ val empty = empty_ss;
+ fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
+ fun merge _ = merge_ss;
);
-val _ = Context.>> (Context.map_theory GlobalSimpset.init);
-fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
-val get_simpset = ! o GlobalSimpset.get;
+val get_ss = SimpsetData.get;
+val map_ss = SimpsetData.map;
+
+
+(* attributes *)
+
+fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
-fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f);
-fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_global_context ()) f);
+val simp_add = attrib (op addsimps);
+val simp_del = attrib (op delsimps);
+val cong_add = attrib (op addcongs);
+val cong_del = attrib (op delcongs);
+
-fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
+(* global simpset *)
+
+fun map_simpset f = Context.theory_map (map_ss f);
+fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
+fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
val simpset = simpset_of o ML_Context.the_global_context;
-
fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;
fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st;
@@ -127,43 +129,14 @@
fun Delcongs args = change_simpset (fn ss => ss delcongs args);
-(* local simpsets *)
+(* local simpset *)
-structure LocalSimpset = ProofDataFun
-(
- type T = simpset;
- val init = get_simpset;
-);
-
-val print_local_simpset = print_ss o LocalSimpset.get;
-val get_local_simpset = LocalSimpset.get;
-val put_local_simpset = LocalSimpset.put;
-
-fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt);
+fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
val _ = ML_Context.value_antiq "simpset"
(Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())"));
-(* generic simpsets *)
-
-fun get_ss (Context.Theory thy) = simpset_of thy
- | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
-
-fun map_ss f (Context.Theory thy) = (change_simpset_of thy f; Context.Theory thy)
- | map_ss f (Context.Proof ctxt) = Context.Proof (LocalSimpset.map f ctxt);
-
-
-(* attributes *)
-
-fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
-
-val simp_add = attrib (op addsimps);
-val simp_del = attrib (op delsimps);
-val cong_add = attrib (op addcongs);
-val cong_del = attrib (op delcongs);
-
-
(** named simprocs **)
@@ -399,14 +372,14 @@
Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
- >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
+ >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
@ cong_modifiers;
val simp_modifiers' =
[Args.add -- Args.colon >> K (I, simp_add),
Args.del -- Args.colon >> K (I, simp_del),
Args.$$$ onlyN -- Args.colon
- >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
+ >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
@ cong_modifiers;
fun simp_args more_mods =
@@ -429,7 +402,7 @@
[(simpN, simp_args more_mods simp_method', "simplification"),
("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
-fun easy_setup reflect trivs = method_setup [] #> (fn thy =>
+fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
let
val trivialities = Drule.reflexive_thm :: trivs;
@@ -445,13 +418,12 @@
else [thm RS reflect] handle THM _ => [];
fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
- val _ = CRITICAL (fn () =>
- GlobalSimpset.get thy :=
- empty_ss setsubgoaler asm_simp_tac
- setSSolver safe_solver
- setSolver unsafe_solver
- setmksimps mksimps);
- in thy end);
+ in
+ empty_ss setsubgoaler asm_simp_tac
+ setSSolver safe_solver
+ setSolver unsafe_solver
+ setmksimps mksimps
+ end));
end;