src/Pure/simplifier.ML
changeset 26497 1873915c64a9
parent 26463 9283b4185fdf
child 26653 60e0cf6bef89
     1.1 --- a/src/Pure/simplifier.ML	Sat Mar 29 22:55:49 2008 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sat Mar 29 22:55:57 2008 +0100
     1.3 @@ -9,8 +9,6 @@
     1.4  signature BASIC_SIMPLIFIER =
     1.5  sig
     1.6    include BASIC_META_SIMPLIFIER
     1.7 -  val print_simpset: theory -> unit
     1.8 -  val change_simpset_of: theory -> (simpset -> simpset) -> unit
     1.9    val change_simpset: (simpset -> simpset) -> unit
    1.10    val simpset_of: theory -> simpset
    1.11    val simpset: unit -> simpset
    1.12 @@ -60,10 +58,6 @@
    1.13    val     full_rewrite: simpset -> conv
    1.14    val   asm_lr_rewrite: simpset -> conv
    1.15    val asm_full_rewrite: simpset -> conv
    1.16 -  val get_simpset: theory -> simpset
    1.17 -  val print_local_simpset: Proof.context -> unit
    1.18 -  val get_local_simpset: Proof.context -> simpset
    1.19 -  val put_local_simpset: simpset -> Proof.context -> Proof.context
    1.20    val get_ss: Context.generic -> simpset
    1.21    val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
    1.22    val attrib: (simpset * thm list -> simpset) -> attribute
    1.23 @@ -71,6 +65,7 @@
    1.24    val simp_del: attribute
    1.25    val cong_add: attribute
    1.26    val cong_del: attribute
    1.27 +  val map_simpset: (simpset -> simpset) -> theory -> theory
    1.28    val get_simproc: Context.generic -> xstring -> simproc
    1.29    val def_simproc: {name: string, lhss: string list,
    1.30      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    1.31 @@ -94,28 +89,35 @@
    1.32  
    1.33  (** simpset data **)
    1.34  
    1.35 -(* global simpsets *)
    1.36 -
    1.37 -structure GlobalSimpset = TheoryDataFun
    1.38 +structure SimpsetData = GenericDataFun
    1.39  (
    1.40 -  type T = simpset ref;
    1.41 -  val empty = ref empty_ss;
    1.42 -  fun copy (ref ss) = ref ss: T;
    1.43 -  fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
    1.44 -  fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
    1.45 +  type T = simpset;
    1.46 +  val empty = empty_ss;
    1.47 +  fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
    1.48 +  fun merge _ = merge_ss;
    1.49  );
    1.50  
    1.51 -val _ = Context.>> (Context.map_theory GlobalSimpset.init);
    1.52 -fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
    1.53 -val get_simpset = ! o GlobalSimpset.get;
    1.54 +val get_ss = SimpsetData.get;
    1.55 +val map_ss = SimpsetData.map;
    1.56 +
    1.57 +
    1.58 +(* attributes *)
    1.59 +
    1.60 +fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
    1.61  
    1.62 -fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f);
    1.63 -fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_global_context ()) f);
    1.64 +val simp_add = attrib (op addsimps);
    1.65 +val simp_del = attrib (op delsimps);
    1.66 +val cong_add = attrib (op addcongs);
    1.67 +val cong_del = attrib (op delcongs);
    1.68 +
    1.69  
    1.70 -fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
    1.71 +(* global simpset *)
    1.72 +
    1.73 +fun map_simpset f = Context.theory_map (map_ss f);
    1.74 +fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
    1.75 +fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
    1.76  val simpset = simpset_of o ML_Context.the_global_context;
    1.77  
    1.78 -
    1.79  fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;
    1.80  fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st;
    1.81  
    1.82 @@ -127,43 +129,14 @@
    1.83  fun Delcongs args = change_simpset (fn ss => ss delcongs args);
    1.84  
    1.85  
    1.86 -(* local simpsets *)
    1.87 +(* local simpset *)
    1.88  
    1.89 -structure LocalSimpset = ProofDataFun
    1.90 -(
    1.91 -  type T = simpset;
    1.92 -  val init = get_simpset;
    1.93 -);
    1.94 -
    1.95 -val print_local_simpset = print_ss o LocalSimpset.get;
    1.96 -val get_local_simpset = LocalSimpset.get;
    1.97 -val put_local_simpset = LocalSimpset.put;
    1.98 -
    1.99 -fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt);
   1.100 +fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
   1.101  
   1.102  val _ = ML_Context.value_antiq "simpset"
   1.103    (Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())"));
   1.104  
   1.105  
   1.106 -(* generic simpsets *)
   1.107 -
   1.108 -fun get_ss (Context.Theory thy) = simpset_of thy
   1.109 -  | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
   1.110 -
   1.111 -fun map_ss f (Context.Theory thy) = (change_simpset_of thy f; Context.Theory thy)
   1.112 -  | map_ss f (Context.Proof ctxt) = Context.Proof (LocalSimpset.map f ctxt);
   1.113 -
   1.114 -
   1.115 -(* attributes *)
   1.116 -
   1.117 -fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
   1.118 -
   1.119 -val simp_add = attrib (op addsimps);
   1.120 -val simp_del = attrib (op delsimps);
   1.121 -val cong_add = attrib (op addcongs);
   1.122 -val cong_del = attrib (op delcongs);
   1.123 -
   1.124 -
   1.125  
   1.126  (** named simprocs **)
   1.127  
   1.128 @@ -399,14 +372,14 @@
   1.129    Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
   1.130    Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
   1.131    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
   1.132 -    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
   1.133 +    >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
   1.134     @ cong_modifiers;
   1.135  
   1.136  val simp_modifiers' =
   1.137   [Args.add -- Args.colon >> K (I, simp_add),
   1.138    Args.del -- Args.colon >> K (I, simp_del),
   1.139    Args.$$$ onlyN -- Args.colon
   1.140 -    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
   1.141 +    >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
   1.142     @ cong_modifiers;
   1.143  
   1.144  fun simp_args more_mods =
   1.145 @@ -429,7 +402,7 @@
   1.146   [(simpN, simp_args more_mods simp_method', "simplification"),
   1.147    ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
   1.148  
   1.149 -fun easy_setup reflect trivs = method_setup [] #> (fn thy =>
   1.150 +fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
   1.151    let
   1.152      val trivialities = Drule.reflexive_thm :: trivs;
   1.153  
   1.154 @@ -445,13 +418,12 @@
   1.155        else [thm RS reflect] handle THM _ => [];
   1.156  
   1.157      fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
   1.158 -    val _ = CRITICAL (fn () =>
   1.159 -      GlobalSimpset.get thy :=
   1.160 -        empty_ss setsubgoaler asm_simp_tac
   1.161 -        setSSolver safe_solver
   1.162 -        setSolver unsafe_solver
   1.163 -        setmksimps mksimps);
   1.164 -  in thy end);
   1.165 +  in
   1.166 +    empty_ss setsubgoaler asm_simp_tac
   1.167 +    setSSolver safe_solver
   1.168 +    setSolver unsafe_solver
   1.169 +    setmksimps mksimps
   1.170 +  end));
   1.171  
   1.172  end;
   1.173