adding option show_invalid_clauses for a more detailed message when modes are not inferred

--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Sep 15 09:36:38 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Sep 15 09:36:39 2010 +0200
@@ -676,7 +676,7 @@
 
 val preprocess_options = Predicate_Compile_Aux.Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
@@ -685,6 +685,7 @@
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
+  show_invalid_clauses = false,
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = true,

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 15 09:36:38 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 15 09:36:39 2010 +0200
@@ -164,6 +164,7 @@
       show_mode_inference = chk "show_mode_inference",
       show_compilation = chk "show_compilation",
       show_caught_failures = false,
+      show_invalid_clauses = chk "show_invalid_clauses",
       skip_proof = chk "skip_proof",
       function_flattening = not (chk "no_function_flattening"),
       specialise = chk "specialise",

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 09:36:38 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 09:36:39 2010 +0200
@@ -108,6 +108,7 @@
     show_modes : bool,
     show_compilation : bool,
     show_caught_failures : bool,
+    show_invalid_clauses : bool,
     skip_proof : bool,
     no_topmost_reordering : bool,
     function_flattening : bool,
@@ -128,6 +129,7 @@
   val show_modes : options -> bool
   val show_compilation : options -> bool
   val show_caught_failures : options -> bool
+  val show_invalid_clauses : options -> bool
   val skip_proof : options -> bool
   val no_topmost_reordering : options -> bool
   val function_flattening : options -> bool
@@ -712,6 +714,7 @@
   show_modes : bool,
   show_compilation : bool,
   show_caught_failures : bool,
+  show_invalid_clauses : bool,
   skip_proof : bool,
   no_topmost_reordering : bool,
   function_flattening : bool,
@@ -735,7 +738,7 @@
 fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_compilation (Options opt) = #show_compilation opt
 fun show_caught_failures (Options opt) = #show_caught_failures opt
-
+fun show_invalid_clauses (Options opt) = #show_invalid_clauses opt
 fun skip_proof (Options opt) = #skip_proof opt
 
 fun function_flattening (Options opt) = #function_flattening opt
@@ -761,6 +764,7 @@
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
+  show_invalid_clauses = false,
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = false,
@@ -773,8 +777,8 @@
 }
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
-  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
-  "detect_switches", "specialise", "no_topmost_reordering"]
+  "show_mode_inference", "show_compilation", "show_invalid_clauses", "skip_proof", "inductify",
+  "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering"]
 
 fun print_step options s =
   if show_steps options then tracing s else ()

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 09:36:38 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 09:36:39 2010 +0200
@@ -411,8 +411,9 @@
             error ("expected modes were not inferred:\n"
             ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
             ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
-            ^ "For the following clauses, the following modes could not be inferred: " ^ "\n"
-            ^ cat_lines errors ^
+            ^ (if show_invalid_clauses options then
+            ("For the following clauses, the following modes could not be inferred: " ^ "\n"
+            ^ cat_lines errors) else "") ^
             (if not (null preds_without_modes) then
               "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
             else ""))
@@ -1503,7 +1504,6 @@
 fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
   preds all_modes param_vs clauses =
   let
-    val collect_errors = false
     fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
     fun add_needs_random s (false, m) = ((false, m), false)
       | add_needs_random s (true, m) = ((true, m), needs_random s m)
@@ -1549,7 +1549,7 @@
         (modes @ extra_modes)) modes
     val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
       Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
-      if collect_errors then
+      if show_invalid_clauses options then
         fixp_with_state (fn (modes, errors) =>
           let
             val (modes', new_errors) = split_list (iteration modes)

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 09:36:38 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 09:36:39 2010 +0200
@@ -65,6 +65,7 @@
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
+  show_invalid_clauses = false, 
   skip_proof = false,
   compilation = Random,
   inductify = true,
@@ -78,7 +79,7 @@
 
 val debug_options = Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = true,
   show_intermediate_results = true,
@@ -87,6 +88,7 @@
   show_mode_inference = true,
   show_compilation = false,
   show_caught_failures = true,
+  show_invalid_clauses = false,
   skip_proof = false,
   compilation = Random,
   inductify = true,
@@ -102,13 +104,15 @@
 fun set_function_flattening b
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re})
@@ -116,13 +120,15 @@
 fun set_fail_safe_function_flattening b
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re})
@@ -130,13 +136,15 @@
 fun set_no_higher_order_predicate ss
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re})