src/Pure/simplifier.ML
changeset 18688 abf0f018b5ec
parent 18629 bdf01da93ed4
child 18708 4b3dadb4fe33
     1.1 --- a/src/Pure/simplifier.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -64,16 +64,11 @@
     1.4    val print_local_simpset: Proof.context -> unit
     1.5    val get_local_simpset: Proof.context -> simpset
     1.6    val put_local_simpset: simpset -> Proof.context -> Proof.context
     1.7 -  val change_global_ss: (simpset * thm list -> simpset) -> theory attribute
     1.8 -  val change_local_ss: (simpset * thm list -> simpset) -> Proof.context attribute
     1.9 -  val simp_add_global: theory attribute
    1.10 -  val simp_del_global: theory attribute
    1.11 -  val simp_add_local: Proof.context attribute
    1.12 -  val simp_del_local: Proof.context attribute
    1.13 -  val cong_add_global: theory attribute
    1.14 -  val cong_del_global: theory attribute
    1.15 -  val cong_add_local: Proof.context attribute
    1.16 -  val cong_del_local: Proof.context attribute
    1.17 +  val attrib: (simpset * thm list -> simpset) -> Context.generic attribute
    1.18 +  val simp_add: Context.generic attribute
    1.19 +  val simp_del: Context.generic attribute
    1.20 +  val cong_add: Context.generic attribute
    1.21 +  val cong_del: Context.generic attribute
    1.22    val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.23    val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
    1.24    val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.25 @@ -143,18 +138,14 @@
    1.26  
    1.27  (* attributes *)
    1.28  
    1.29 -fun change_global_ss f (thy, th) = (change_simpset_of thy (fn ss => f (ss, [th])); (thy, th));
    1.30 -fun change_local_ss f (ctxt, th) = (LocalSimpset.map (fn ss => f (ss, [th])) ctxt, th);
    1.31 +fun attrib f = Attrib.declaration (fn th =>
    1.32 +   fn Context.Theory thy => (change_simpset_of thy (fn ss => f (ss, [th])); Context.Theory thy)
    1.33 +    | Context.Proof ctxt => Context.Proof (LocalSimpset.map (fn ss => f (ss, [th])) ctxt));
    1.34  
    1.35 -val simp_add_global = change_global_ss (op addsimps);
    1.36 -val simp_del_global = change_global_ss (op delsimps);
    1.37 -val simp_add_local = change_local_ss (op addsimps);
    1.38 -val simp_del_local = change_local_ss (op delsimps);
    1.39 -
    1.40 -val cong_add_global = change_global_ss (op addcongs);
    1.41 -val cong_del_global = change_global_ss (op delcongs);
    1.42 -val cong_add_local = change_local_ss (op addcongs);
    1.43 -val cong_del_local = change_local_ss (op delcongs);
    1.44 +val simp_add = attrib (op addsimps);
    1.45 +val simp_del = attrib (op delsimps);
    1.46 +val cong_add = attrib (op addcongs);
    1.47 +val cong_del = attrib (op delcongs);
    1.48  
    1.49  
    1.50  
    1.51 @@ -243,14 +234,6 @@
    1.52  val no_asm_simpN = "no_asm_simp";
    1.53  val asm_lrN = "asm_lr";
    1.54  
    1.55 -val simp_attr =
    1.56 - (Attrib.add_del_args simp_add_global simp_del_global,
    1.57 -  Attrib.add_del_args simp_add_local simp_del_local);
    1.58 -
    1.59 -val cong_attr =
    1.60 - (Attrib.add_del_args cong_add_global cong_del_global,
    1.61 -  Attrib.add_del_args cong_add_local cong_del_local);
    1.62 -
    1.63  
    1.64  (* conversions *)
    1.65  
    1.66 @@ -262,15 +245,14 @@
    1.67      Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
    1.68      Scan.succeed asm_full_simplify) |> Scan.lift) x;
    1.69  
    1.70 -fun simplified_att get args =
    1.71 -  Attrib.syntax (conv_mode -- args >> (fn (f, ths) => Attrib.rule (fn x =>
    1.72 -    f ((if null ths then I else MetaSimplifier.clear_ss) (get x) addsimps ths))));
    1.73 +fun get_ss (Context.Theory thy) = simpset_of thy
    1.74 +  | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
    1.75  
    1.76  in
    1.77  
    1.78 -val simplified_attr =
    1.79 - (simplified_att simpset_of Attrib.global_thmss,
    1.80 -  simplified_att local_simpset_of Attrib.local_thmss);
    1.81 +val simplified =
    1.82 +  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Attrib.rule (fn x =>
    1.83 +    f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
    1.84  
    1.85  end;
    1.86  
    1.87 @@ -279,9 +261,11 @@
    1.88  
    1.89  val _ = Context.add_setup
    1.90   [Attrib.add_attributes
    1.91 -   [(simpN, simp_attr, "declaration of simplification rule"),
    1.92 -    (congN, cong_attr, "declaration of Simplifier congruence rule"),
    1.93 -    ("simplified", simplified_attr, "simplified rule")]];
    1.94 +   [(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
    1.95 +      "declaration of Simplifier rule"),
    1.96 +    (congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
    1.97 +      "declaration of Simplifier congruence rule"),
    1.98 +    ("simplified", Attrib.common simplified, "simplified rule")]];
    1.99  
   1.100  
   1.101  
   1.102 @@ -302,22 +286,23 @@
   1.103    >> (curry (Library.foldl op o) I o rev)) x;
   1.104  
   1.105  val cong_modifiers =
   1.106 - [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local): Method.modifier),
   1.107 -  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
   1.108 -  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
   1.109 + [Args.$$$ congN -- Args.colon >> K ((I, Attrib.context cong_add): Method.modifier),
   1.110 +  Args.$$$ congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
   1.111 +  Args.$$$ congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del)];
   1.112  
   1.113  val simp_modifiers =
   1.114 - [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
   1.115 -  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
   1.116 -  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
   1.117 + [Args.$$$ simpN -- Args.colon >> K (I, Attrib.context simp_add),
   1.118 +  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
   1.119 +  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
   1.120    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
   1.121 -    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add_local)]
   1.122 +    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
   1.123     @ cong_modifiers;
   1.124  
   1.125  val simp_modifiers' =
   1.126 - [Args.add -- Args.colon >> K (I, simp_add_local),
   1.127 -  Args.del -- Args.colon >> K (I, simp_del_local),
   1.128 -  Args.$$$ onlyN -- Args.colon >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add_local)]
   1.129 + [Args.add -- Args.colon >> K (I, Attrib.context simp_add),
   1.130 +  Args.del -- Args.colon >> K (I, Attrib.context simp_del),
   1.131 +  Args.$$$ onlyN -- Args.colon
   1.132 +    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
   1.133     @ cong_modifiers;
   1.134  
   1.135  fun simp_args more_mods =