# HG changeset patch
# User wenzelm
# Date 1212097601 -7200
# Node ID b5b8afc9fdcda1135edba99729adecbd592be91d
# Parent  9ad9d6554d05baaa510483132607d3e05baa0388
added warning_count for issued reconstruction failure messages (limit 10);
less nesting of let expressions;

diff -r 9ad9d6554d05 -r b5b8afc9fdcd src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu May 29 23:46:40 2008 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu May 29 23:46:41 2008 +0200
@@ -92,6 +92,7 @@
                      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset})
                 -> Context.generic -> Context.generic
   val trace: bool ref
+  val warning_count: int ref;
   val cut_lin_arith_tac: simpset -> int -> tactic
   val lin_arith_tac: Proof.context -> bool -> int -> tactic
   val lin_arith_simproc: simpset -> term -> thm option
@@ -419,6 +420,9 @@
 fun trace_msg msg =
   if !trace then tracing msg else ();
 
+val warning_count = ref 0;
+val warning_count_max = 10;
+
 val union_term = curry (gen_union Pattern.aeconv);
 val union_bterm = curry (gen_union
   (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')));
@@ -435,6 +439,7 @@
 local
   exception FalseE of thm
 in
+
 fun mkthm ss asms (just: injust) =
   let
     val ctxt = Simplifier.the_context ss;
@@ -492,20 +497,30 @@
         | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j)))
         | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j)))
 
-  in trace_msg "mkthm";
-     let val thm = trace_thm "Final thm:" (mk just)
-     in let val fls = simplify simpset' thm
-        in trace_thm "After simplification:" fls;
-           if LA_Logic.is_False fls then fls
-           else
-            (tracing "Assumptions:"; List.app (tracing o Display.string_of_thm) asms;
-             tracing "Proved:"; tracing (Display.string_of_thm fls);
-             warning "Linear arithmetic should have refuted the assumptions.\n\
-                     \Please inform Tobias Nipkow (nipkow@in.tum.de).";
-             fls)
-        end
-     end handle FalseE thm => trace_thm "False reached early:" thm
-  end
+  in
+    let
+      val _ = trace_msg "mkthm";
+      val thm = trace_thm "Final thm:" (mk just);
+      val fls = simplify simpset' thm;
+      val _ = trace_thm "After simplification:" fls;
+      val _ =
+        if LA_Logic.is_False fls then ()
+        else
+          let val count = CRITICAL (fn () => inc warning_count) in
+            if count > warning_count_max then ()
+            else
+              (tracing (cat_lines
+                (["Assumptions:"] @ map Display.string_of_thm asms @ [""] @
+                 ["Proved:", Display.string_of_thm fls, ""] @
+                 (if count <> warning_count_max then []
+                  else ["\n(Reached maximal message count -- disabling future warnings)"])));
+                warning "Linear arithmetic should have refuted the assumptions.\n\
+                  \Please inform Tobias Nipkow (nipkow@in.tum.de).")
+          end;
+    in fls end
+    handle FalseE thm => trace_thm "False reached early:" thm
+  end;
+
 end;
 
 fun coeff poly atom =