--- a/src/HOL/Nitpick_Examples/ROOT.ML Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Nitpick_Examples/ROOT.ML Tue Nov 17 22:51:00 2009 +0100
@@ -5,7 +5,6 @@
Nitpick examples.
*)
-Toplevel.debug := true;
if getenv "KODKODI" = "" then
()
else
--- a/src/HOL/Tools/Nitpick/HISTORY Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Nov 17 22:51:00 2009 +0100
@@ -12,6 +12,8 @@
* Added support for codatatype view of datatypes
* Fixed soundness bugs related to sets and sets of sets
* Fixed monotonicity check
+ * Fixed error when processing definitions that resulted in an exception
+ * Fixed error in Kodkod encoding of "The" and "Eps"
* Fixed error in display of uncurried constants
* Speeded up scope enumeration
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 17 22:51:00 2009 +0100
@@ -1109,13 +1109,13 @@
|> map_filter (try (Refute.specialize_type thy x))
|> filter (equal (Const x) o term_under_def)
-(* term -> term *)
+(* theory -> term -> term option *)
fun normalized_rhs_of thy t =
let
- (* term -> term *)
- fun aux (v as Var _) t = lambda v t
- | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t
- | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
+ (* term option -> term option *)
+ fun aux (v as Var _) (SOME t) = SOME (lambda v t)
+ | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
+ | aux _ _ = NONE
val (lhs, rhs) =
case t of
Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
@@ -1123,7 +1123,7 @@
(t1, t2)
| _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
val args = strip_comb lhs |> snd
- in fold_rev aux args rhs end
+ in fold_rev aux args (SOME rhs) end
(* theory -> const_table -> styp -> term option *)
fun def_of_const thy table (x as (s, _)) =
@@ -1131,7 +1131,7 @@
NONE
else
x |> def_props_for_const thy false table |> List.last
- |> normalized_rhs_of thy |> prefix_abs_vars s |> SOME
+ |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
datatype fixpoint_kind = Lfp | Gfp | NoFp
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 17 22:51:00 2009 +0100
@@ -1092,6 +1092,12 @@
else
kk_rel_eq r1 r2
end)
+ | Op2 (The, T, _, u1, u2) =>
+ to_f_with_polarity polar
+ (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2))
+ | Op2 (Eps, T, _, u1, u2) =>
+ to_f_with_polarity polar
+ (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2))
| Op2 (Apply, T, _, u1, u2) =>
(case (polar, rep_of u1) of
(Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Nov 17 22:51:00 2009 +0100
@@ -1158,8 +1158,10 @@
let
val u1' = sub u1
val opt1 = is_opt_rep (rep_of u1')
+ val opt = (oper = Eps orelse opt1)
val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
- val R = unopt_R |> (oper = Eps orelse opt1) ? opt_rep ofs T
+ val R = if is_boolean_type T then bool_rep polar opt
+ else unopt_R |> opt ? opt_rep ofs T
val u = Op2 (oper, T, R, u1', sub u2)
in
if is_precise_type datatypes T orelse not opt1 then