# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID 8c9c31a757f5a58e2ca62d4cdb072b41cf6f6dfe
# Parent  7e90d259790bbdf887fe34d25c5889c8803e940f
make Sledgehammer's relevance filter include the "ext" rule when appropriate

diff -r 7e90d259790b -r 8c9c31a757f5 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -433,6 +433,26 @@
   else
     tab
 
+fun add_arities is_built_in_const th =
+  let
+    fun aux _ _ NONE = NONE
+      | aux t args (SOME tab) =
+        case t of
+          t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
+        | Const (x as (s, _)) =>
+          (if is_built_in_const x args then
+             SOME tab
+           else case Symtab.lookup tab s of
+             NONE => SOME (Symtab.update (s, length args) tab)
+           | SOME n => if n = length args then SOME tab else NONE)
+        | _ => SOME tab
+  in aux (prop_of th) [] end
+
+fun needs_ext is_built_in_const facts =
+  fold (add_arities is_built_in_const o snd) facts (SOME Symtab.empty)
+  |> is_none
+
+
 fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
         (fudge as {threshold_divisor, ridiculous_threshold, ...})
         ({add, del, ...} : relevance_override) facts goal_ts =
@@ -516,8 +536,8 @@
                       |> map string_for_hyper_pconst));
           relevant [] [] hopeful
         end
-    fun add_add_ths accepts =
-      (facts |> filter ((member Thm.eq_thm add_ths
+    fun add_facts ths accepts =
+      (facts |> filter ((member Thm.eq_thm ths
                          andf (not o member (Thm.eq_thm o apsnd snd) accepts))
                         o snd))
       @ accepts
@@ -525,9 +545,12 @@
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
           |> iter 0 max_relevant threshold0 goal_const_tab []
-          |> not (null add_ths) ? add_add_ths
-          |> tap (fn res => trace_msg (fn () =>
-                               "Total relevant: " ^ Int.toString (length res)))
+          |> not (null add_ths) ? add_facts add_ths
+          |> (fn accepts =>
+                 accepts |> needs_ext is_built_in_const accepts
+                            ? add_facts @{thms ext})
+          |> tap (fn accepts => trace_msg (fn () =>
+                      "Total relevant: " ^ Int.toString (length accepts)))
   end