improve datatype symmetry breaking;
all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example
--- 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)
--- 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