# HG changeset patch
# User paulson
# Date 1174906110 -7200
# Node ID c986140356b8c02344582f090c73105d6349511f
# Parent  f4061faa5fda212d956e754da87bbe57df112f63
Clause cache is now in theory data.

Deleted skolem_use_cache_thm, so cnf_rules_of_ths now calls cnf_axiom.

diff -r f4061faa5fda -r c986140356b8 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Mon Mar 26 12:46:27 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon Mar 26 12:48:30 2007 +0200
@@ -413,12 +413,6 @@
        |> transform_elim |> zero_var_indexes |> freeze_thm
        |> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
 
-(*The cache prevents repeated clausification of a theorem,
-  and also repeated declaration of Skolem functions*)
-  (* FIXME  use theory data!!*)
-val clause_cache = ref (Thmtab.empty : thm list Thmtab.table)
-
-
 (*Generate Skolem functions for a theorem supplied in nnf*)
 fun skolem_of_nnf th =
   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
@@ -479,9 +473,25 @@
       (SOME (to_nnf th)  handle THM _ => NONE)
   end;
 
+structure ThmCache = TheoryDataFun
+(struct
+  val name = "ATP/thm_cache";
+  type T = (thm list) Thmtab.table ref;
+  val empty : T = ref Thmtab.empty;
+  fun copy (ref tab) : T = ref tab;
+  val extend = copy;
+  fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
+  fun print _ _ = ();
+end);
+
+(*The cache prevents repeated clausification of a theorem, and also repeated declaration of 
+  Skolem functions. The global one holds theorems proved prior to this point. Theory data
+  holds the remaining ones.*)
+val global_clause_cache = ref (Thmtab.empty : (thm list) Thmtab.table);
+
 (*Populate the clause cache using the supplied theorem. Return the clausal form
   and modified theory.*)
-fun skolem_cache_thm th thy =
+fun skolem_cache_thm clause_cache th thy =
   case Thmtab.lookup (!clause_cache) th of
       NONE =>
         (case skolem thy (Thm.transfer thy th) of
@@ -496,13 +506,21 @@
 
 (*Exported function to convert Isabelle theorems into axiom clauses*)
 fun cnf_axiom th =
-  case Thmtab.lookup (!clause_cache) th of
-      NONE => 
-	let val cls = map Goal.close_result (skolem_thm th)
-	in Output.debug (fn () => "inserted into cache");
-	   change clause_cache (Thmtab.update (th, cls)); cls 
-	end
-    | SOME cls => cls;
+  let val cache = ThmCache.get (Thm.theory_of_thm th)
+                  handle ERROR _ => global_clause_cache
+      val in_cache = if cache = global_clause_cache then NONE else Thmtab.lookup (!cache) th
+  in
+     case in_cache of
+       NONE => 
+	 (case Thmtab.lookup (!global_clause_cache) th of
+	   NONE => 
+	     let val cls = map Goal.close_result (skolem_thm th)
+	     in Output.debug (fn () => "inserted into cache: " ^ PureThy.get_name_hint th);
+		change cache (Thmtab.update (th, cls)); cls 
+	     end
+	 | SOME cls => cls)
+     | SOME cls => cls
+  end;
 
 fun pairname th = (PureThy.get_name_hint th, th);
 
@@ -557,33 +575,18 @@
 
 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
 
-fun skolem_cache th thy =
-  let val prop = Thm.prop_of th
-  in
-      if lambda_free prop 
-         (*Monomorphic theorems can be Skolemized on demand,
-           but there are problems with re-use of abstraction functions if we don't
-           do them now, even for monomorphic theorems.*)
-      then thy  
-      else #2 (skolem_cache_thm th thy)
-  end;
+fun skolem_cache clause_cache th thy = #2 (skolem_cache_thm clause_cache th thy);
 
-(*The cache can be kept smaller by augmenting the condition above with 
-    orelse (not abstract_lambdas andalso monomorphic prop).
-  However, while this step does not reduce the time needed to build HOL, 
-  it doubles the time taken by the first call to the ATP link-up.*)
+(*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
+  lambda_free, but then the individual theory caches become much bigger.*)
 
-fun clause_cache_setup thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
+fun clause_cache_setup thy = 
+  fold (skolem_cache global_clause_cache) (map #2 (PureThy.all_thms_of thy)) thy;
 
 
 (*** meson proof methods ***)
 
-fun skolem_use_cache_thm th =
-  case Thmtab.lookup (!clause_cache) th of
-      NONE => skolem_thm th
-    | SOME cls => cls;
-
-fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
+fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
 
 val meson_method_setup = Method.add_methods
   [("meson", Method.thms_args (fn ths =>
@@ -611,7 +614,8 @@
 fun neg_conjecture_clauses st0 n =
   let val st = Seq.hd (neg_skolemize_tac n st0)
       val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
-  in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end;
+  in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end
+  handle Option => raise ERROR "unable to Skolemize subgoal";
 
 (*Conversion of a subgoal to conjecture clauses. Each clause has  
   leading !!-bound universal variables, to express generality. *)
@@ -637,9 +641,9 @@
   | conj_rule ths = foldr1 conj2_rule ths;
 
 fun skolem_attr (Context.Theory thy, th) =
-      let val (cls, thy') = skolem_cache_thm th thy
+      let val (cls, thy') = skolem_cache_thm (ThmCache.get thy) th thy
       in (Context.Theory thy', conj_rule cls) end
-  | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
+  | skolem_attr (context, th) = (context, conj_rule (cnf_axiom th));
 
 val setup_attrs = Attrib.add_attributes
   [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
@@ -649,6 +653,6 @@
   [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), 
     "conversion of goal to conjecture clauses")];
      
-val setup = clause_cache_setup #> setup_attrs #> setup_methods;
+val setup = clause_cache_setup #> ThmCache.init #> setup_attrs #> setup_methods;
 
 end;