fixed arity of some empty relations in Nitpick's Kodkod generator;
these previously resulted in Kodkod arity errors (similar to type errors for other logics)
--- a/src/HOL/Tools/Nitpick/HISTORY Tue Nov 24 18:35:21 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Nov 24 18:36:18 2009 +0100
@@ -10,6 +10,7 @@
* Optimized Kodkod encoding of datatypes whose constructors don't appear in
the formula to falsify
* Added support for codatatype view of datatypes
+ * Fixed soundness bug in the "uncurry" optimization
* Fixed soundness bugs related to sets, sets of sets, (co)inductive
predicates, typedefs, "finite", "rel_comp", and negative literals
* Fixed monotonicity check
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 24 18:35:21 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 24 18:36:18 2009 +0100
@@ -1322,7 +1322,7 @@
(kk_rel_if (kk_or (kk_some (kk_join r1 true_atom))
(kk_subset (full_rel_for_rep R)
(kk_join r1 false_atom)))
- (to_rep R u2) Kodkod.None)
+ (to_rep R u2) (empty_rel_for_rep R))
end
else
let val r1 = to_rep (Func (R, Formula Neut)) u1 in
@@ -1335,20 +1335,20 @@
val r2 = to_rep R u2
in
kk_union (kk_rel_if (kk_one (kk_join r1 true_atom))
- (kk_join r1 true_atom) Kodkod.None)
+ (kk_join r1 true_atom) (empty_rel_for_rep R))
(kk_rel_if (kk_or (kk_subset r2 (kk_join r1 true_atom))
(kk_subset (full_rel_for_rep R)
(kk_join r1 false_atom)))
- r2 Kodkod.None)
+ r2 (empty_rel_for_rep R))
end
else
let
val r1 = to_rep (Func (unopt_rep R, Formula Neut)) u1
val r2 = to_rep R u2
in
- kk_union (kk_rel_if (kk_one r1) r1 Kodkod.None)
+ kk_union (kk_rel_if (kk_one r1) r1 (empty_rel_for_rep R))
(kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1))
- r2 Kodkod.None)
+ r2 (empty_rel_for_rep R))
end
| Op2 (Triad, T, Opt (Atom (2, j0)), u1, u2) =>
let
@@ -1754,8 +1754,10 @@
else Kodkod.False
(* nut -> Kodkod.rel_expr -> Kodkod.rel_expr *)
and to_compare_with_unrep u r =
- if is_opt_rep (rep_of u) then kk_rel_if (kk_some (to_r u)) r Kodkod.None
- else r
+ if is_opt_rep (rep_of u) then
+ kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u))
+ else
+ r
in to_f_with_polarity Pos u end
end;