# HG changeset patch
# User bulwahn
# Date 1271844652 -7200
# Node ID 5fd5d732a4eaf986138f27c190e296f753253ba8
# Parent  ad558b642a152614964a07bbcb8fbced7a002092
only add relevant predicates to the list of extra modes

diff -r ad558b642a15 -r 5fd5d732a4ea src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
@@ -38,6 +38,7 @@
   (* premises *)
   datatype indprem = Prem of term | Negprem of term | Sidecond of term
     | Generator of (string * typ)
+  val dest_indprem : indprem -> term
   (* general syntactic functions *)
   val conjuncts : term -> term list
   val is_equationlike : thm -> bool
@@ -388,6 +389,11 @@
 datatype indprem = Prem of term | Negprem of term | Sidecond of term
   | Generator of (string * typ);
 
+fun dest_indprem (Prem t) = t
+  | dest_indprem (Negprem t) = t
+  | dest_indprem (Sidecond t) = t
+  | dest_indprem (Generator _) = raise Fail "cannot destruct generator"
+
 (* general syntactic functions *)
 
 (*Like dest_conj, but flattens conjunctions however nested*)
diff -r ad558b642a15 -r 5fd5d732a4ea src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 12:10:52 2010 +0200
@@ -1485,13 +1485,26 @@
     val prednames = map fst preds
     (* extramodes contains all modes of all constants, should we only use the necessary ones
        - what is the impact on performance? *)
+    fun predname_of (Prem t) =
+        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
+      | predname_of (Negprem t) =
+        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
+      | predname_of _ = I
+    val relevant_prednames = fold (fn (_, clauses') =>
+      fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
     val extra_modes =
       if #infer_pos_and_neg_modes mode_analysis_options then
         let
           val pos_extra_modes =
-            all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name)
+            map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
+            relevant_prednames
+            (* all_modes_of compilation thy *)
+            |> filter_out (fn (name, _) => member (op =) prednames name)
           val neg_extra_modes =
-            all_modes_of (negative_compilation_of compilation) thy
+          map_filter (fn name => Option.map (pair name)
+            (try (modes_of (negative_compilation_of compilation) thy) name))
+            relevant_prednames
+          (*all_modes_of (negative_compilation_of compilation) thy*)
             |> filter_out (fn (name, _) => member (op =) prednames name)
         in
           map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
@@ -1500,7 +1513,10 @@
         end
       else
         map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
-          (all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name))
+          (map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
+            relevant_prednames
+          (*all_modes_of compilation thy*)
+          |> filter_out (fn (name, _) => member (op =) prednames name))
     val _ = print_extra_modes options extra_modes
     val start_modes =
       if #infer_pos_and_neg_modes mode_analysis_options then
@@ -2639,9 +2655,9 @@
       prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames)
     val _ = print_step options "Infering modes..."
     val ((moded_clauses, errors), thy') =
-      (*Output.cond_timeit true "Infering modes"
-      (fn _ =>*) infer_modes mode_analysis_options
-        options compilation preds all_modes param_vs clauses thy
+      Output.cond_timeit true "Infering modes"
+      (fn _ => infer_modes mode_analysis_options
+        options compilation preds all_modes param_vs clauses thy)
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes preds options modes
     (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)