src/Provers/classical.ML
changeset 26497 1873915c64a9
parent 26470 e44d24620515
child 26928 ca87aff1ad2d
     1.1 --- a/src/Provers/classical.ML	Sat Mar 29 22:55:49 2008 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Mar 29 22:55:57 2008 +0100
     1.3 @@ -40,7 +40,6 @@
     1.4    type claset
     1.5    val empty_cs: claset
     1.6    val print_cs: claset -> unit
     1.7 -  val print_claset: theory -> unit
     1.8    val rep_cs:
     1.9      claset -> {safeIs: thm list, safeEs: thm list,
    1.10                   hazIs: thm list, hazEs: thm list,
    1.11 @@ -72,7 +71,6 @@
    1.12    val appSWrappers      : claset -> wrapper
    1.13    val appWrappers       : claset -> wrapper
    1.14  
    1.15 -  val change_claset_of: theory -> (claset -> claset) -> unit
    1.16    val change_claset: (claset -> claset) -> unit
    1.17    val claset_of: theory -> claset
    1.18    val claset: unit -> claset
    1.19 @@ -140,9 +138,7 @@
    1.20    val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
    1.21    val del_context_unsafe_wrapper: string -> theory -> theory
    1.22    val get_claset: theory -> claset
    1.23 -  val get_local_claset: Proof.context -> claset
    1.24 -  val put_local_claset: claset -> Proof.context -> Proof.context
    1.25 -  val print_local_claset: Proof.context -> unit
    1.26 +  val map_claset: (claset -> claset) -> theory -> theory
    1.27    val get_cs: Context.generic -> claset
    1.28    val map_cs: (claset -> claset) -> Context.generic -> Context.generic
    1.29    val safe_dest: int option -> attribute
    1.30 @@ -863,27 +859,26 @@
    1.31  
    1.32  structure GlobalClaset = TheoryDataFun
    1.33  (
    1.34 -  type T = claset ref * context_cs;
    1.35 -  val empty = (ref empty_cs, empty_context_cs);
    1.36 -  fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
    1.37 -  val extend = copy;
    1.38 -  fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
    1.39 -    (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
    1.40 +  type T = claset * context_cs;
    1.41 +  val empty = (empty_cs, empty_context_cs);
    1.42 +  val copy = I;
    1.43 +  val extend = I;
    1.44 +  fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
    1.45 +    (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
    1.46  );
    1.47  
    1.48 -val print_claset = print_cs o ! o #1 o GlobalClaset.get;
    1.49 -val get_claset = ! o #1 o GlobalClaset.get;
    1.50 +val get_claset = #1 o GlobalClaset.get;
    1.51 +val map_claset = GlobalClaset.map o apfst;
    1.52  
    1.53  val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
    1.54  fun map_context_cs f = GlobalClaset.map (apsnd
    1.55    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
    1.56  
    1.57 -val change_claset_of = change o #1 o GlobalClaset.get;
    1.58 -fun change_claset f = change_claset_of (ML_Context.the_global_context ()) f;
    1.59 +fun change_claset f = Context.>> (Context.map_theory (map_claset f));
    1.60  
    1.61  fun claset_of thy =
    1.62 -  let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
    1.63 -  in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
    1.64 +  let val (cs, ctxt_cs) = GlobalClaset.get thy
    1.65 +  in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
    1.66  val claset = claset_of o ML_Context.the_global_context;
    1.67  
    1.68  fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
    1.69 @@ -900,15 +895,11 @@
    1.70  
    1.71  (* context dependent components *)
    1.72  
    1.73 -fun add_context_safe_wrapper wrapper = (map_context_cs o apfst)
    1.74 -  (AList.update (op =) wrapper);
    1.75 -fun del_context_safe_wrapper name = (map_context_cs o apfst)
    1.76 -  (AList.delete (op =) name);
    1.77 +fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
    1.78 +fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
    1.79  
    1.80 -fun add_context_unsafe_wrapper wrapper = (map_context_cs o apsnd)
    1.81 -  (AList.update (op =) wrapper);
    1.82 -fun del_context_unsafe_wrapper name = (map_context_cs o apsnd)
    1.83 -  (AList.delete (op =) name);
    1.84 +fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
    1.85 +fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
    1.86  
    1.87  
    1.88  (* local clasets *)
    1.89 @@ -919,29 +910,20 @@
    1.90    val init = get_claset;
    1.91  );
    1.92  
    1.93 -val get_local_claset = LocalClaset.get;
    1.94 -val put_local_claset = LocalClaset.put;
    1.95 -
    1.96  fun local_claset_of ctxt =
    1.97 -  context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
    1.98 -
    1.99 -val print_local_claset = print_cs o local_claset_of;
   1.100 +  context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
   1.101  
   1.102  
   1.103  (* generic clasets *)
   1.104  
   1.105 -fun get_cs (Context.Theory thy) = claset_of thy
   1.106 -  | get_cs (Context.Proof ctxt) = local_claset_of ctxt;
   1.107 -
   1.108 -fun map_cs f (Context.Theory thy) = (change_claset_of thy f; Context.Theory thy)
   1.109 -  | map_cs f (Context.Proof ctxt) = Context.Proof (LocalClaset.map f ctxt);
   1.110 +val get_cs = Context.cases claset_of local_claset_of;
   1.111 +fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f);
   1.112  
   1.113  
   1.114  (* attributes *)
   1.115  
   1.116  fun attrib f = Thm.declaration_attribute (fn th =>
   1.117 -   fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
   1.118 -    | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
   1.119 +  Context.mapping (map_claset (f th)) (LocalClaset.map (f th)));
   1.120  
   1.121  fun safe_dest w = attrib (addSE w o make_elim);
   1.122  val safe_elim = attrib o addSE;
   1.123 @@ -1071,7 +1053,7 @@
   1.124  
   1.125  (** theory setup **)
   1.126  
   1.127 -val setup = GlobalClaset.init #> setup_attrs #> setup_methods;
   1.128 +val setup = setup_attrs #> setup_methods;
   1.129  
   1.130  
   1.131  
   1.132 @@ -1080,9 +1062,7 @@
   1.133  val _ =
   1.134    OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
   1.135      OuterKeyword.diag
   1.136 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
   1.137 -      (Toplevel.node_case
   1.138 -        (Context.cases print_claset print_local_claset)
   1.139 -        (print_local_claset o Proof.context_of)))));
   1.140 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   1.141 +      Toplevel.keep (print_cs o local_claset_of o Toplevel.context_of)));
   1.142  
   1.143  end;