change_claset(_of): more abtract interface;
authorwenzelm
Mon Oct 17 23:10:18 2005 +0200 (2005-10-17 ago)
changeset 178804494c023bf2a
parent 17879 88844eea4ce2
child 17881 2b3709f5e477
change_claset(_of): more abtract interface;
claset_of: init proof context;
added raw get_claset;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Mon Oct 17 23:10:17 2005 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon Oct 17 23:10:18 2005 +0200
     1.3 @@ -72,14 +72,12 @@
     1.4    val appSWrappers      : claset -> wrapper
     1.5    val appWrappers       : claset -> wrapper
     1.6  
     1.7 -  val claset_ref_of: theory -> claset ref
     1.8 -  val claset_ref_of_sg: theory -> claset ref    (*obsolete*)
     1.9 +  val change_claset_of: theory -> (claset -> claset) -> unit
    1.10 +  val change_claset: (claset -> claset) -> unit
    1.11    val claset_of: theory -> claset
    1.12 -  val claset_of_sg: theory -> claset            (*obsolete*)
    1.13 +  val claset: unit -> claset
    1.14    val CLASET: (claset -> tactic) -> tactic
    1.15    val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
    1.16 -  val claset: unit -> claset
    1.17 -  val claset_ref: unit -> claset ref
    1.18    val local_claset_of   : Proof.context -> claset
    1.19  
    1.20    val fast_tac          : claset -> int -> tactic
    1.21 @@ -141,6 +139,7 @@
    1.22    val del_context_safe_wrapper: string -> theory -> theory
    1.23    val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
    1.24    val del_context_unsafe_wrapper: string -> theory -> theory
    1.25 +  val get_claset: theory -> claset
    1.26    val print_local_claset: Proof.context -> unit
    1.27    val get_local_claset: Proof.context -> claset
    1.28    val put_local_claset: claset -> Proof.context -> Proof.context
    1.29 @@ -817,9 +816,9 @@
    1.30  
    1.31  
    1.32  
    1.33 -(** claset theory data **)
    1.34 +(** claset data **)
    1.35  
    1.36 -(* theory data kind 'Provers/claset' *)
    1.37 +(* global clasets *)
    1.38  
    1.39  structure GlobalClaset = TheoryDataFun
    1.40  (struct
    1.41 @@ -835,37 +834,30 @@
    1.42  end);
    1.43  
    1.44  val print_claset = GlobalClaset.print;
    1.45 -val claset_ref_of = #1 o GlobalClaset.get;
    1.46 -val claset_ref_of_sg = claset_ref_of;
    1.47 +val get_claset = ! o #1 o GlobalClaset.get;
    1.48 +
    1.49  val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
    1.50 -
    1.51  fun map_context_cs f = GlobalClaset.map (apsnd
    1.52    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
    1.53  
    1.54 -
    1.55 -(* access claset *)
    1.56 -
    1.57 -val claset_of = ! o claset_ref_of;
    1.58 -val claset_of_sg = claset_of;
    1.59 +val change_claset_of = change o #1 o GlobalClaset.get;
    1.60 +fun change_claset f = change_claset_of (Context.the_context ()) f;
    1.61  
    1.62 -fun CLASET tacf state = tacf (claset_of (Thm.theory_of_thm state)) state;
    1.63 -fun CLASET' tacf i state = tacf (claset_of (Thm.theory_of_thm state)) i state;
    1.64 -
    1.65 +fun claset_of thy = 
    1.66 +  let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
    1.67 +  in context_cs (Context.init_proof thy) (! cs_ref) (ctxt_cs) end;
    1.68  val claset = claset_of o Context.the_context;
    1.69 -val claset_ref = claset_ref_of o Context.the_context;
    1.70  
    1.71 -
    1.72 -(* change claset *)
    1.73 -
    1.74 -fun change_claset f x = claset_ref () := (f (claset (), x));
    1.75 +fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
    1.76 +fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
    1.77  
    1.78 -val AddDs = change_claset (op addDs);
    1.79 -val AddEs = change_claset (op addEs);
    1.80 -val AddIs = change_claset (op addIs);
    1.81 -val AddSDs = change_claset (op addSDs);
    1.82 -val AddSEs = change_claset (op addSEs);
    1.83 -val AddSIs = change_claset (op addSIs);
    1.84 -val Delrules = change_claset (op delrules);
    1.85 +fun AddDs args = change_claset (fn cs => cs addDs args);
    1.86 +fun AddEs args = change_claset (fn cs => cs addEs args);
    1.87 +fun AddIs args = change_claset (fn cs => cs addIs args);
    1.88 +fun AddSDs args = change_claset (fn cs => cs addSDs args);
    1.89 +fun AddSEs args = change_claset (fn cs => cs addSEs args);
    1.90 +fun AddSIs args = change_claset (fn cs => cs addSIs args);
    1.91 +fun Delrules args = change_claset (fn cs => cs delrules args);
    1.92  
    1.93  
    1.94  (* context dependent components *)
    1.95 @@ -883,7 +875,7 @@
    1.96  (struct
    1.97    val name = "Provers/claset";
    1.98    type T = claset;
    1.99 -  val init = claset_of;
   1.100 +  val init = get_claset;
   1.101    fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
   1.102  end);
   1.103  
   1.104 @@ -897,13 +889,8 @@
   1.105  
   1.106  (* attributes *)
   1.107  
   1.108 -fun change_global_cs f (thy, th) =
   1.109 -  let val r = claset_ref_of thy
   1.110 -  in r := f (! r, [th]); (thy, th) end;
   1.111 -
   1.112 -fun change_local_cs f (ctxt, th) =
   1.113 -  let val cs = f (get_local_claset ctxt, [th])
   1.114 -  in (put_local_claset cs ctxt, th) end;
   1.115 +fun change_global_cs f (thy, th) = (change_claset_of thy (fn cs => f (cs, [th])); (thy, th));
   1.116 +fun change_local_cs f (ctxt, th) = (LocalClaset.map (fn cs => f (cs, [th])) ctxt, th);
   1.117  
   1.118  val safe_dest_global = change_global_cs (op addSDs);
   1.119  val safe_elim_global = change_global_cs (op addSEs);