fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
authorblanchet
Mon May 31 17:20:41 2010 +0200 (2010-05-31)
changeset 37213efcad7594872
parent 37207 c40c9b05952c
child 37214 47d1ee50205b
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
     1.1 --- a/src/HOL/Nitpick.thy	Mon May 31 10:29:04 2010 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Mon May 31 17:20:41 2010 +0200
     1.3 @@ -69,6 +69,9 @@
     1.4   apply (erule_tac x = y in allE)
     1.5  by (auto simp: mem_def)
     1.6  
     1.7 +lemma split_def [nitpick_def]: "split f = (\<lambda>p. f (fst p) (snd p))"
     1.8 +by (simp add: prod_case_unfold split_def)
     1.9 +
    1.10  lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.11  by simp
    1.12  
    1.13 @@ -245,12 +248,12 @@
    1.14      less_eq_frac of_frac
    1.15  hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.16      word
    1.17 -hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.18 -    wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    1.19 -    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
    1.20 -    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    1.21 -    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
    1.22 -    uminus_frac_def number_of_frac_def inverse_frac_def less_eq_frac_def
    1.23 -    of_frac_def
    1.24 +hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
    1.25 +    refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.26 +    fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
    1.27 +    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.28 +    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    1.29 +    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    1.30 +    inverse_frac_def less_eq_frac_def of_frac_def
    1.31  
    1.32  end
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 10:29:04 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 17:20:41 2010 +0200
     2.3 @@ -945,21 +945,32 @@
     2.4  
     2.5  fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
     2.6                        step subst orig_assm_ts orig_t =
     2.7 -  if getenv "KODKODI" = "" then
     2.8 -    (if auto then ()
     2.9 -     else warning (Pretty.string_of (plazy install_kodkodi_message));
    2.10 -     ("unknown", state))
    2.11 -  else
    2.12 -    let
    2.13 -      val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    2.14 -      val outcome as (outcome_code, _) =
    2.15 -        time_limit (if debug then NONE else timeout)
    2.16 -            (pick_them_nits_in_term deadline state params auto i n step subst
    2.17 -                                    orig_assm_ts) orig_t
    2.18 -    in
    2.19 -      if expect = "" orelse outcome_code = expect then outcome
    2.20 -      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    2.21 -    end
    2.22 +  let
    2.23 +    val warning_m = if auto then K () else warning
    2.24 +    val unknown_outcome = ("unknown", state)
    2.25 +  in
    2.26 +    if getenv "KODKODI" = "" then
    2.27 +      (warning_m (Pretty.string_of (plazy install_kodkodi_message));
    2.28 +       unknown_outcome)
    2.29 +    else
    2.30 +      let
    2.31 +        val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    2.32 +        val outcome as (outcome_code, _) =
    2.33 +          time_limit (if debug then NONE else timeout)
    2.34 +              (pick_them_nits_in_term deadline state params auto i n step subst
    2.35 +                                      orig_assm_ts) orig_t
    2.36 +          handle TOO_LARGE (_, details) =>
    2.37 +                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
    2.38 +               | TOO_SMALL (_, details) =>
    2.39 +                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
    2.40 +               | Kodkod.SYNTAX (_, details) =>
    2.41 +                 (warning ("Ill-formed Kodkodi output: " ^ details ^ ".");
    2.42 +                  unknown_outcome)
    2.43 +      in
    2.44 +        if expect = "" orelse outcome_code = expect then outcome
    2.45 +        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    2.46 +      end
    2.47 +  end
    2.48  
    2.49  fun is_fixed_equation fixes
    2.50                        (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 10:29:04 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 17:20:41 2010 +0200
     3.3 @@ -1663,8 +1663,7 @@
     3.4  
     3.5  (* TODO: Move to "Nitpick.thy" *)
     3.6  val basic_ersatz_table =
     3.7 -  [(@{const_name prod_case}, @{const_name split}),
     3.8 -   (@{const_name card}, @{const_name card'}),
     3.9 +  [(@{const_name card}, @{const_name card'}),
    3.10     (@{const_name setsum}, @{const_name setsum'}),
    3.11     (@{const_name fold_graph}, @{const_name fold_graph'}),
    3.12     (@{const_name wf}, @{const_name wf'}),
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 31 10:29:04 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 31 17:20:41 2010 +0200
     4.3 @@ -316,10 +316,6 @@
     4.4           error ("Invalid term" ^ plural_s_for_list ts ^
     4.5                  " (" ^ quote loc ^ "): " ^
     4.6                  commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
     4.7 -       | TOO_LARGE (_, details) =>
     4.8 -         (warning ("Limit reached: " ^ details ^ "."); x)
     4.9 -       | TOO_SMALL (_, details) =>
    4.10 -         (warning ("Limit reached: " ^ details ^ "."); x)
    4.11         | TYPE (loc, Ts, ts) =>
    4.12           error ("Invalid type" ^ plural_s_for_list Ts ^
    4.13                  (if null ts then
    4.14 @@ -329,8 +325,6 @@
    4.15                     commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
    4.16                  " (" ^ quote loc ^ "): " ^
    4.17                  commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
    4.18 -       | Kodkod.SYNTAX (_, details) =>
    4.19 -         (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
    4.20         | Refute.REFUTE (loc, details) =>
    4.21           error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
    4.22