# HG changeset patch
# User blanchet
# Date 1275319241 -7200
# Node ID efcad75948720d0096cfaa08ab2ca14777e604be
# Parent  c40c9b05952c0e276da2bb4a2486046ce79b86ec
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option

diff -r c40c9b05952c -r efcad7594872 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Mon May 31 10:29:04 2010 +0200
+++ b/src/HOL/Nitpick.thy	Mon May 31 17:20:41 2010 +0200
@@ -69,6 +69,9 @@
  apply (erule_tac x = y in allE)
 by (auto simp: mem_def)
 
+lemma split_def [nitpick_def]: "split f = (\<lambda>p. f (fst p) (snd p))"
+by (simp add: prod_case_unfold split_def)
+
 lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
 by simp
 
@@ -245,12 +248,12 @@
     less_eq_frac of_frac
 hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
     word
-hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
-    wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
-    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
-    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
-    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
-    uminus_frac_def number_of_frac_def inverse_frac_def less_eq_frac_def
-    of_frac_def
+hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
+    refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
+    fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
+    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
+    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
+    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
+    inverse_frac_def less_eq_frac_def of_frac_def
 
 end
diff -r c40c9b05952c -r efcad7594872 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 10:29:04 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 17:20:41 2010 +0200
@@ -945,21 +945,32 @@
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
                       step subst orig_assm_ts orig_t =
-  if getenv "KODKODI" = "" then
-    (if auto then ()
-     else warning (Pretty.string_of (plazy install_kodkodi_message));
-     ("unknown", state))
-  else
-    let
-      val deadline = Option.map (curry Time.+ (Time.now ())) timeout
-      val outcome as (outcome_code, _) =
-        time_limit (if debug then NONE else timeout)
-            (pick_them_nits_in_term deadline state params auto i n step subst
-                                    orig_assm_ts) orig_t
-    in
-      if expect = "" orelse outcome_code = expect then outcome
-      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
-    end
+  let
+    val warning_m = if auto then K () else warning
+    val unknown_outcome = ("unknown", state)
+  in
+    if getenv "KODKODI" = "" then
+      (warning_m (Pretty.string_of (plazy install_kodkodi_message));
+       unknown_outcome)
+    else
+      let
+        val deadline = Option.map (curry Time.+ (Time.now ())) timeout
+        val outcome as (outcome_code, _) =
+          time_limit (if debug then NONE else timeout)
+              (pick_them_nits_in_term deadline state params auto i n step subst
+                                      orig_assm_ts) orig_t
+          handle TOO_LARGE (_, details) =>
+                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+               | TOO_SMALL (_, details) =>
+                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+               | Kodkod.SYNTAX (_, details) =>
+                 (warning ("Ill-formed Kodkodi output: " ^ details ^ ".");
+                  unknown_outcome)
+      in
+        if expect = "" orelse outcome_code = expect then outcome
+        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+      end
+  end
 
 fun is_fixed_equation fixes
                       (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
diff -r c40c9b05952c -r efcad7594872 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 10:29:04 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 17:20:41 2010 +0200
@@ -1663,8 +1663,7 @@
 
 (* TODO: Move to "Nitpick.thy" *)
 val basic_ersatz_table =
-  [(@{const_name prod_case}, @{const_name split}),
-   (@{const_name card}, @{const_name card'}),
+  [(@{const_name card}, @{const_name card'}),
    (@{const_name setsum}, @{const_name setsum'}),
    (@{const_name fold_graph}, @{const_name fold_graph'}),
    (@{const_name wf}, @{const_name wf'}),
diff -r c40c9b05952c -r efcad7594872 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 31 10:29:04 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 31 17:20:41 2010 +0200
@@ -316,10 +316,6 @@
          error ("Invalid term" ^ plural_s_for_list ts ^
                 " (" ^ quote loc ^ "): " ^
                 commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
-       | TOO_LARGE (_, details) =>
-         (warning ("Limit reached: " ^ details ^ "."); x)
-       | TOO_SMALL (_, details) =>
-         (warning ("Limit reached: " ^ details ^ "."); x)
        | TYPE (loc, Ts, ts) =>
          error ("Invalid type" ^ plural_s_for_list Ts ^
                 (if null ts then
@@ -329,8 +325,6 @@
                    commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
                 " (" ^ quote loc ^ "): " ^
                 commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
-       | Kodkod.SYNTAX (_, details) =>
-         (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
        | Refute.REFUTE (loc, details) =>
          error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")