# HG changeset patch
# User blanchet
# Date 1259084178 -3600
# Node ID 3937da7e13eaae291e9fd3d3d1d0caa6a6073858
# Parent  48463e8876bde4ea72040b013e94b1c9620efcfa
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)

diff -r 48463e8876bd -r 3937da7e13ea src/HOL/Tools/Nitpick/HISTORY
--- 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
diff -r 48463e8876bd -r 3937da7e13ea src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- 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;