# HG changeset patch
# User blanchet
# Date 1381258595 -7200
# Node ID 540835cf11edba787b24f80244101a0de4e68a16
# Parent  cb33b304e743a35cef5ba8d5fd2a22bc7c2910b2
more gracefully handle huge theories in relevance filters

diff -r cb33b304e743 -r 540835cf11ed src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 20:53:37 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 20:56:35 2013 +0200
@@ -57,6 +57,12 @@
    del : (Facts.ref * Attrib.src list) list,
    only : bool}
 
+(* gracefully handle huge background theories *)
+val max_facts_for_duplicates = 50000
+val max_facts_for_duplicate_matching = 25000
+val max_facts_for_complex_check = 25000
+val max_simps_for_clasimpset = 5000
+
 (* experimental feature *)
 val instantiate_inducts =
   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
@@ -301,9 +307,6 @@
 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
 fun backquote_thm ctxt = backquote_term ctxt o prop_of
 
-(* gracefully handle huge background theories *)
-val max_simps_for_clasimpset = 10000
-
 fun clasimpset_rule_table_of ctxt =
   let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
     if length simps >= max_simps_for_clasimpset then
@@ -378,12 +381,9 @@
     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   in (plain_name_tab, inclass_name_tab) end
 
-(* The function would have slightly cleaner semantics if it called "Pattern.equiv" instead of
-   "Pattern.matches", but it would also be slower. "Pattern.matches" throws out theorems that are
-   strict instances of other theorems, but only if the instance is met after the general version. *)
-fun fact_distinct thy facts =
+fun fact_distinct eq facts =
   fold (fn fact as (_, th) =>
-      Net.insert_term_safe (Pattern.matches thy o swap o pairself (normalize_eq o prop_of o snd))
+      Net.insert_term_safe (eq o pairself (normalize_eq o prop_of o snd))
         (normalize_eq (prop_of th), fact))
     facts Net.empty
   |> Net.entries
@@ -449,9 +449,6 @@
 
 fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0
 
-(* gracefully handle huge background theories *)
-val max_facts_for_complex_check = 25000
-
 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -541,10 +538,21 @@
          maps (map (fn ((name, stature), th) => ((K name, stature), th))
                o fact_of_ref ctxt reserved chained css) add
        else
-         let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
-           all_facts ctxt false ho_atp reserved add chained css
-           |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
-           |> fact_distinct thy
+        (* The "fact_distinct" call would have cleaner semantics if it called "Pattern.equiv"
+           instead of "Pattern.matches", but it would also be slower and less precise.
+           "Pattern.matches" throws out theorems that are strict instances of other theorems, but
+           only if the instance is met after the general version. *)
+         let
+           val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
+           val facts =
+             all_facts ctxt false ho_atp reserved add chained css
+             |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
+            val num_facts = length facts
+         in
+           facts
+           |> num_facts <= max_facts_for_duplicates
+              ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
+                  else Pattern.matches thy o swap)
          end)
       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
     end