purely functional setup of claset/simpset/clasimpset;
authorwenzelm
Sat Mar 29 22:55:49 2008 +0100 (2008-03-29)
changeset 2649649ae9456eba9
parent 26495 dd8996960cb0
child 26497 1873915c64a9
purely functional setup of claset/simpset/clasimpset;
NEWS
src/FOL/FOL.thy
src/FOL/cladata.ML
src/FOL/simpdata.ML
src/HOL/HOL.thy
src/HOL/Library/Word.thy
src/HOL/Orderings.thy
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/record_package.ML
src/HOLCF/Tools/cont_proc.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/NEWS	Sat Mar 29 19:24:57 2008 +0100
     1.2 +++ b/NEWS	Sat Mar 29 22:55:49 2008 +0100
     1.3 @@ -29,8 +29,9 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* Eliminated destructive theorem database.  Potential INCOMPATIBILITY,
     1.8 -really need to observe linear functional update of theories.
     1.9 +* Eliminated destructive theorem database, simpset, claset, and
    1.10 +clasimpset.  Potential INCOMPATIBILITY, really need to observe linear
    1.11 +update of theories within ML code.
    1.12  
    1.13  * Commands 'use' and 'ML' are now purely functional, operating on
    1.14  theory/local_theory.  Removed former 'ML_setup' (on theory), use 'ML'
     2.1 --- a/src/FOL/FOL.thy	Sat Mar 29 19:24:57 2008 +0100
     2.2 +++ b/src/FOL/FOL.thy	Sat Mar 29 22:55:49 2008 +0100
     2.3 @@ -293,7 +293,7 @@
     2.4  setup simpsetup
     2.5  setup "Simplifier.method_setup Splitter.split_modifiers"
     2.6  setup Splitter.setup
     2.7 -setup Clasimp.setup
     2.8 +setup clasimp_setup
     2.9  setup EqSubst.setup
    2.10  
    2.11  
     3.1 --- a/src/FOL/cladata.ML	Sat Mar 29 19:24:57 2008 +0100
     3.2 +++ b/src/FOL/cladata.ML	Sat Mar 29 22:55:49 2008 +0100
     3.3 @@ -36,7 +36,7 @@
     3.4  val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
     3.5                       addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
     3.6  
     3.7 -val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));
     3.8 +val cla_setup = Cla.map_claset (K FOL_cs);
     3.9  
    3.10  val case_setup =
    3.11   (Method.add_methods
     4.1 --- a/src/FOL/simpdata.ML	Sat Mar 29 19:24:57 2008 +0100
     4.2 +++ b/src/FOL/simpdata.ML	Sat Mar 29 22:55:49 2008 +0100
     4.3 @@ -155,7 +155,7 @@
     4.4  (*classical simprules too*)
     4.5  val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
     4.6  
     4.7 -val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy));
     4.8 +val simpsetup = Simplifier.map_simpset (K FOL_ss);
     4.9  
    4.10  
    4.11  (*** integration of simplifier with classical reasoner ***)
     5.1 --- a/src/HOL/HOL.thy	Sat Mar 29 19:24:57 2008 +0100
     5.2 +++ b/src/HOL/HOL.thy	Sat Mar 29 22:55:49 2008 +0100
     5.3 @@ -1285,9 +1285,9 @@
     5.4  
     5.5  setup {*
     5.6    Simplifier.method_setup Splitter.split_modifiers
     5.7 -  #> (fn thy => (change_simpset_of thy (fn _ => Simpdata.simpset_simprocs); thy))
     5.8 +  #> Simplifier.map_simpset (K Simpdata.simpset_simprocs)
     5.9    #> Splitter.setup
    5.10 -  #> Clasimp.setup
    5.11 +  #> clasimp_setup
    5.12    #> EqSubst.setup
    5.13  *}
    5.14  
     6.1 --- a/src/HOL/Library/Word.thy	Sat Mar 29 19:24:57 2008 +0100
     6.2 +++ b/src/HOL/Library/Word.thy	Sat Mar 29 22:55:49 2008 +0100
     6.3 @@ -2325,8 +2325,7 @@
     6.4    (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
     6.5    val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
     6.6  in
     6.7 -  (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2]);
     6.8 -    thy))
     6.9 +  Simplifier.map_simpset (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2])
    6.10  end*}
    6.11  
    6.12  declare bv_to_nat1 [simp del]
     7.1 --- a/src/HOL/Orderings.thy	Sat Mar 29 19:24:57 2008 +0100
     7.2 +++ b/src/HOL/Orderings.thy	Sat Mar 29 22:55:49 2008 +0100
     7.3 @@ -516,12 +516,12 @@
     7.4    handle THM _ => NONE;
     7.5  
     7.6  fun add_simprocs procs thy =
     7.7 -  (Simplifier.change_simpset_of thy (fn ss => ss
     7.8 +  Simplifier.map_simpset (fn ss => ss
     7.9      addsimprocs (map (fn (name, raw_ts, proc) =>
    7.10 -      Simplifier.simproc thy name raw_ts proc)) procs); thy);
    7.11 -fun add_solver name tac thy =
    7.12 -  (Simplifier.change_simpset_of thy (fn ss => ss addSolver
    7.13 -    (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy);
    7.14 +      Simplifier.simproc thy name raw_ts proc) procs)) thy;
    7.15 +fun add_solver name tac =
    7.16 +  Simplifier.map_simpset (fn ss => ss addSolver
    7.17 +    mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss)));
    7.18  
    7.19  in
    7.20    add_simprocs [
     8.1 --- a/src/HOL/Statespace/state_fun.ML	Sat Mar 29 19:24:57 2008 +0100
     8.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat Mar 29 22:55:49 2008 +0100
     8.3 @@ -381,8 +381,7 @@
     8.4              | _ => (lookup_ss addsimps [thm], ex_lookup_ss))
     8.5       fun activate_simprocs ctxt =
     8.6            if simprocs_active then ctxt
     8.7 -          else StateSpace.change_simpset 
     8.8 -                (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
     8.9 +          else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
    8.10                 
    8.11  
    8.12       val ctxt' = ctxt 
     9.1 --- a/src/HOL/Statespace/state_space.ML	Sat Mar 29 19:24:57 2008 +0100
     9.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Mar 29 22:55:49 2008 +0100
     9.3 @@ -46,9 +46,6 @@
     9.4      val distinct_simproc : MetaSimplifier.simproc
     9.5  
     9.6  
     9.7 -    val change_simpset : (MetaSimplifier.simpset -> MetaSimplifier.simpset) ->
     9.8 -       Context.generic -> Context.generic
     9.9 -
    9.10      val get_comp : Context.generic -> string -> (Term.typ * string) Option.option
    9.11      val get_silent : Context.generic -> bool
    9.12      val set_silent : bool -> Context.generic -> Context.generic
    9.13 @@ -247,11 +244,6 @@
    9.14          | NONE => NONE)
    9.15        | _ => NONE))
    9.16  
    9.17 -fun change_simpset f =
    9.18 -     Context.mapping
    9.19 -       (fn thy  => (change_simpset_of thy f; thy))
    9.20 -       (fn ctxt => Simplifier.put_local_simpset (f (Simplifier.get_local_simpset ctxt)) ctxt);
    9.21 -
    9.22  fun read_typ thy s =
    9.23    Sign.read_typ thy s;
    9.24  
    9.25 @@ -309,7 +301,7 @@
    9.26            val tt' = tt |> fold upd all_names;
    9.27            val activate_simproc =
    9.28                Output.no_warnings
    9.29 -               (change_simpset (fn ss => ss addsimprocs [distinct_simproc]));
    9.30 +               (Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
    9.31            val ctxt' =
    9.32                ctxt
    9.33                |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent}
    10.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Mar 29 19:24:57 2008 +0100
    10.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Mar 29 22:55:49 2008 +0100
    10.3 @@ -428,7 +428,7 @@
    10.4  
    10.5  val simproc_setup =
    10.6    Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t) #>
    10.7 -  (fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy));
    10.8 +  Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
    10.9  
   10.10  
   10.11  (**** translation rules for case ****)
    11.1 --- a/src/HOL/Tools/record_package.ML	Sat Mar 29 19:24:57 2008 +0100
    11.2 +++ b/src/HOL/Tools/record_package.ML	Sat Mar 29 22:55:49 2008 +0100
    11.3 @@ -2295,8 +2295,8 @@
    11.4  val setup =
    11.5    Sign.add_trfuns ([], parse_translation, [], []) #>
    11.6    Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
    11.7 -  (fn thy => (Simplifier.change_simpset_of thy
    11.8 -    (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy));
    11.9 +  Simplifier.map_simpset (fn ss =>
   11.10 +    ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
   11.11  
   11.12  (* outer syntax *)
   11.13  
    12.1 --- a/src/HOLCF/Tools/cont_proc.ML	Sat Mar 29 19:24:57 2008 +0100
    12.2 +++ b/src/HOLCF/Tools/cont_proc.ML	Sat Mar 29 22:55:49 2008 +0100
    12.3 @@ -138,9 +138,6 @@
    12.4      Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
    12.5  end;
    12.6  
    12.7 -val setup =
    12.8 -  (fn thy =>
    12.9 -    (Simplifier.change_simpset_of thy
   12.10 -      (fn ss => ss addsimprocs [cont_proc thy]); thy));
   12.11 +fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy;
   12.12  
   12.13  end;
    13.1 --- a/src/ZF/Tools/typechk.ML	Sat Mar 29 19:24:57 2008 +0100
    13.2 +++ b/src/ZF/Tools/typechk.ML	Sat Mar 29 22:55:49 2008 +0100
    13.3 @@ -129,6 +129,6 @@
    13.4  val setup =
    13.5    Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
    13.6    Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
    13.7 -  (fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));
    13.8 +  Simplifier.map_simpset (fn ss => ss setSolver type_solver);
    13.9  
   13.10  end;