optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
this gains one cardinality in the AA tree examples in the Nitpick manual
--- a/doc-src/Nitpick/nitpick.tex Thu Feb 04 16:50:26 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Fri Feb 05 11:14:34 2010 +0100
@@ -1694,7 +1694,7 @@
``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
+{\slshape Nitpick found no counterexample.}
\postw
Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
@@ -1756,7 +1756,7 @@
\prew
\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
\postw
Insertion should transform the set of elements represented by the tree in the
@@ -1766,14 +1766,14 @@
\textbf{theorem} \textit{dataset\_insort}:\kern.4em
``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
\postw
-We could continue like this and sketch a complete theory of AA trees without
-performing a single proof. Once the definitions and main theorems are in place
-and have been thoroughly tested using Nitpick, we could start working on the
-proofs. Developing theories this way usually saves time, because faulty theorems
-and definitions are discovered much earlier in the process.
+We could continue like this and sketch a complete theory of AA trees. Once the
+definitions and main theorems are in place and have been thoroughly tested using
+Nitpick, we could start working on the proofs. Developing theories this way
+usually saves time, because faulty theorems and definitions are discovered much
+earlier in the process.
\section{Option Reference}
\label{option-reference}
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 04 16:50:26 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 05 11:14:34 2010 +0100
@@ -316,7 +316,15 @@
if R2 = Formula Neut then
[ts] |> not exclusive ? cons (KK.TupleSet [])
else
- [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)]
+ [KK.TupleSet [],
+ if exclusive andalso T1 = T2 andalso epsilon > delta then
+ index_seq delta (epsilon - delta)
+ |> map (fn j =>
+ KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
+ KK.TupleAtomSeq (j, j0)))
+ |> foldl1 KK.TupleUnion
+ else
+ KK.TupleProduct (ts, upper_bound_for_rep R2)]
end)
end
| bound_for_sel_rel _ _ _ u =
@@ -944,11 +952,11 @@
(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
fun kodkod_formula_from_nut bits ofs liberal
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
- kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
- kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,
- kk_intersect, kk_product, kk_join, kk_closure, kk_comprehension,
- kk_project, kk_project_seq, kk_not3, kk_nat_less, kk_int_less,
- ...}) u =
+ kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
+ kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
+ kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
+ kk_comprehension, kk_project, kk_project_seq, kk_not3,
+ kk_nat_less, kk_int_less, ...}) u =
let
val main_j0 = offset_of_type ofs bool_T
val bool_j0 = main_j0
@@ -1108,7 +1116,7 @@
else
if is_lone_rep min_R then
if arity_of_rep min_R = 1 then
- kk_subset (kk_product r1 r2) KK.Iden
+ kk_lone (kk_union r1 r2)
else if not both_opt then
(r1, r2) |> is_opt_rep (rep_of u2) ? swap
|-> kk_subset
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 04 16:50:26 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 05 11:14:34 2010 +0100
@@ -426,16 +426,21 @@
{delta = delta, epsilon = delta, exclusive = true, total = false}
end
else if not co andalso num_self_recs > 0 then
- if not self_rec andalso num_non_self_recs = 1 andalso
- domain_card 2 card_assigns T = 1 then
- {delta = 0, epsilon = 1,
- exclusive = (s = @{const_name Nil} andalso length constrs = 2),
- total = true}
- else if s = @{const_name Cons} andalso
- num_self_recs + num_non_self_recs = 2 then
- {delta = 1, epsilon = card, exclusive = true, total = false}
- else
- {delta = 0, epsilon = card, exclusive = false, total = false}
+ (if num_self_recs = 1 andalso 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}
+ | _ => raise SAME ()
+ else
+ if domain_card 2 card_assigns T = 1 then
+ {delta = 0, epsilon = 1, exclusive = true, total = true}
+ else
+ raise SAME ()
+ else
+ raise SAME ())
+ handle SAME () =>
+ {delta = 0, epsilon = card, exclusive = false, total = false}
else if card = sum_dom_cards (card + 1) then
let val delta = next_delta () in
{delta = delta, epsilon = delta + domain_card card card_assigns T,
@@ -473,7 +478,8 @@
map (domain_card max card_assigns o snd) xs |> Integer.sum
val constrs =
fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
- num_non_self_recs) (self_recs ~~ xs) []
+ num_non_self_recs)
+ (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
{typ = T, card = card, co = co, complete = complete, concrete = concrete,
deep = deep, constrs = constrs}