# HG changeset patch # User wenzelm # Date 1206827757 -3600 # Node ID 1873915c64a98fbeeb88e8f07bc2ec796ff964e9 # Parent 49ae9456eba9ffe99901e7774de579b17511755a purely functional setup of claset/simpset/clasimpset; tuned signature; diff -r 49ae9456eba9 -r 1873915c64a9 src/Provers/clasimp.ML --- 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 diff -r 49ae9456eba9 -r 1873915c64a9 src/Provers/classical.ML --- 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; diff -r 49ae9456eba9 -r 1873915c64a9 src/Pure/simplifier.ML --- 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;