# 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 = (\p. f (fst p) (snd p))" +by (simp add: prod_case_unfold split_def) + lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \ (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 ^ ".")