src/HOL/Tools/res_axioms.ML
changeset 22516 c986140356b8
parent 22471 7c51f1a799f3
child 22596 d0d2af4db18f
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Mar 26 12:46:27 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Mar 26 12:48:30 2007 +0200
     1.3 @@ -413,12 +413,6 @@
     1.4         |> transform_elim |> zero_var_indexes |> freeze_thm
     1.5         |> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
     1.6  
     1.7 -(*The cache prevents repeated clausification of a theorem,
     1.8 -  and also repeated declaration of Skolem functions*)
     1.9 -  (* FIXME  use theory data!!*)
    1.10 -val clause_cache = ref (Thmtab.empty : thm list Thmtab.table)
    1.11 -
    1.12 -
    1.13  (*Generate Skolem functions for a theorem supplied in nnf*)
    1.14  fun skolem_of_nnf th =
    1.15    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
    1.16 @@ -479,9 +473,25 @@
    1.17        (SOME (to_nnf th)  handle THM _ => NONE)
    1.18    end;
    1.19  
    1.20 +structure ThmCache = TheoryDataFun
    1.21 +(struct
    1.22 +  val name = "ATP/thm_cache";
    1.23 +  type T = (thm list) Thmtab.table ref;
    1.24 +  val empty : T = ref Thmtab.empty;
    1.25 +  fun copy (ref tab) : T = ref tab;
    1.26 +  val extend = copy;
    1.27 +  fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
    1.28 +  fun print _ _ = ();
    1.29 +end);
    1.30 +
    1.31 +(*The cache prevents repeated clausification of a theorem, and also repeated declaration of 
    1.32 +  Skolem functions. The global one holds theorems proved prior to this point. Theory data
    1.33 +  holds the remaining ones.*)
    1.34 +val global_clause_cache = ref (Thmtab.empty : (thm list) Thmtab.table);
    1.35 +
    1.36  (*Populate the clause cache using the supplied theorem. Return the clausal form
    1.37    and modified theory.*)
    1.38 -fun skolem_cache_thm th thy =
    1.39 +fun skolem_cache_thm clause_cache th thy =
    1.40    case Thmtab.lookup (!clause_cache) th of
    1.41        NONE =>
    1.42          (case skolem thy (Thm.transfer thy th) of
    1.43 @@ -496,13 +506,21 @@
    1.44  
    1.45  (*Exported function to convert Isabelle theorems into axiom clauses*)
    1.46  fun cnf_axiom th =
    1.47 -  case Thmtab.lookup (!clause_cache) th of
    1.48 -      NONE => 
    1.49 -	let val cls = map Goal.close_result (skolem_thm th)
    1.50 -	in Output.debug (fn () => "inserted into cache");
    1.51 -	   change clause_cache (Thmtab.update (th, cls)); cls 
    1.52 -	end
    1.53 -    | SOME cls => cls;
    1.54 +  let val cache = ThmCache.get (Thm.theory_of_thm th)
    1.55 +                  handle ERROR _ => global_clause_cache
    1.56 +      val in_cache = if cache = global_clause_cache then NONE else Thmtab.lookup (!cache) th
    1.57 +  in
    1.58 +     case in_cache of
    1.59 +       NONE => 
    1.60 +	 (case Thmtab.lookup (!global_clause_cache) th of
    1.61 +	   NONE => 
    1.62 +	     let val cls = map Goal.close_result (skolem_thm th)
    1.63 +	     in Output.debug (fn () => "inserted into cache: " ^ PureThy.get_name_hint th);
    1.64 +		change cache (Thmtab.update (th, cls)); cls 
    1.65 +	     end
    1.66 +	 | SOME cls => cls)
    1.67 +     | SOME cls => cls
    1.68 +  end;
    1.69  
    1.70  fun pairname th = (PureThy.get_name_hint th, th);
    1.71  
    1.72 @@ -557,33 +575,18 @@
    1.73  
    1.74  (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
    1.75  
    1.76 -fun skolem_cache th thy =
    1.77 -  let val prop = Thm.prop_of th
    1.78 -  in
    1.79 -      if lambda_free prop 
    1.80 -         (*Monomorphic theorems can be Skolemized on demand,
    1.81 -           but there are problems with re-use of abstraction functions if we don't
    1.82 -           do them now, even for monomorphic theorems.*)
    1.83 -      then thy  
    1.84 -      else #2 (skolem_cache_thm th thy)
    1.85 -  end;
    1.86 +fun skolem_cache clause_cache th thy = #2 (skolem_cache_thm clause_cache th thy);
    1.87  
    1.88 -(*The cache can be kept smaller by augmenting the condition above with 
    1.89 -    orelse (not abstract_lambdas andalso monomorphic prop).
    1.90 -  However, while this step does not reduce the time needed to build HOL, 
    1.91 -  it doubles the time taken by the first call to the ATP link-up.*)
    1.92 +(*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
    1.93 +  lambda_free, but then the individual theory caches become much bigger.*)
    1.94  
    1.95 -fun clause_cache_setup thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
    1.96 +fun clause_cache_setup thy = 
    1.97 +  fold (skolem_cache global_clause_cache) (map #2 (PureThy.all_thms_of thy)) thy;
    1.98  
    1.99  
   1.100  (*** meson proof methods ***)
   1.101  
   1.102 -fun skolem_use_cache_thm th =
   1.103 -  case Thmtab.lookup (!clause_cache) th of
   1.104 -      NONE => skolem_thm th
   1.105 -    | SOME cls => cls;
   1.106 -
   1.107 -fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
   1.108 +fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
   1.109  
   1.110  val meson_method_setup = Method.add_methods
   1.111    [("meson", Method.thms_args (fn ths =>
   1.112 @@ -611,7 +614,8 @@
   1.113  fun neg_conjecture_clauses st0 n =
   1.114    let val st = Seq.hd (neg_skolemize_tac n st0)
   1.115        val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
   1.116 -  in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end;
   1.117 +  in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end
   1.118 +  handle Option => raise ERROR "unable to Skolemize subgoal";
   1.119  
   1.120  (*Conversion of a subgoal to conjecture clauses. Each clause has  
   1.121    leading !!-bound universal variables, to express generality. *)
   1.122 @@ -637,9 +641,9 @@
   1.123    | conj_rule ths = foldr1 conj2_rule ths;
   1.124  
   1.125  fun skolem_attr (Context.Theory thy, th) =
   1.126 -      let val (cls, thy') = skolem_cache_thm th thy
   1.127 +      let val (cls, thy') = skolem_cache_thm (ThmCache.get thy) th thy
   1.128        in (Context.Theory thy', conj_rule cls) end
   1.129 -  | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
   1.130 +  | skolem_attr (context, th) = (context, conj_rule (cnf_axiom th));
   1.131  
   1.132  val setup_attrs = Attrib.add_attributes
   1.133    [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
   1.134 @@ -649,6 +653,6 @@
   1.135    [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), 
   1.136      "conversion of goal to conjecture clauses")];
   1.137       
   1.138 -val setup = clause_cache_setup #> setup_attrs #> setup_methods;
   1.139 +val setup = clause_cache_setup #> ThmCache.init #> setup_attrs #> setup_methods;
   1.140  
   1.141  end;