# HG changeset patch
# User blanchet
# Date 1280951777 -7200
# Node ID 44d635ce6da49f63be6bfa8e0fcc712da83e7bf2
# Parent  1a1973c005317c2920871a00a06f73d4961b4e05
improve datatype symmetry breaking;
all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example

diff -r 1a1973c00531 -r 44d635ce6da4 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Aug 04 10:52:29 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Aug 04 21:56:17 2010 +0200
@@ -788,11 +788,13 @@
        these easily. *)
   | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
 
-fun has_nil_like_constr dtypes T =
-  case #constrs (the (datatype_spec dtypes T))
-       |> filter_out (is_self_recursive_constr_type o snd o #const) of
-    [{const = (_, T'), ...}] => T = T'
-  | _ => false
+fun is_nil_like_constr_type dtypes T =
+  case datatype_spec dtypes T of
+    SOME {constrs, ...} =>
+    (case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
+       [{const = (_, T'), ...}] => T = T'
+     | _ => false)
+  | NONE => false
 
 fun sym_break_axioms_for_constr_pair hol_ctxt binarize
        (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset,
@@ -834,6 +836,7 @@
                          (same_constr andalso x = hd sel_xs) orelse
                          (T = dataT andalso
                           (no_direct orelse not (member (op =) sel_xs x)))))
+                                       (* FIXME: why the last disjunct above? *)
         fun subterms_r no_direct sel_xs j =
           loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
                            (filter_out (curry (op =) dataT) (map fst nfa)) dataT
@@ -845,8 +848,7 @@
                  (if delta2 >= epsilon1 then KK.True
                   else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
                  (kk_or
-                      (if has_nil_like_constr dtypes dataT andalso
-                          T1 = dataT then
+                      (if is_nil_like_constr_type dtypes T1 then
                          KK.True
                        else
                          kk_some (kk_intersect (subterms_r false sel_xs2 1)
diff -r 1a1973c00531 -r 44d635ce6da4 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Aug 04 10:52:29 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Aug 04 21:56:17 2010 +0200
@@ -394,11 +394,12 @@
           {delta = delta, epsilon = delta, exclusive = true, total = false}
         end
       else if num_self_recs > 0 then
-        (if num_self_recs = 1 andalso num_non_self_recs = 1 then
+        (if num_non_self_recs = 1 then
            if self_rec then
-             case constrs of
-               [{delta = 0, epsilon = 1, exclusive = true, ...}] =>
-               {delta = 1, epsilon = card, exclusive = true, total = false}
+             case List.last constrs of
+               {delta = 0, epsilon = 1, exclusive = true, ...} =>
+               {delta = 1, epsilon = card, exclusive = (num_self_recs = 1),
+                total = false}
              | _ => raise SAME ()
            else
              if domain_card 2 card_assigns T = 1 then