# HG changeset patch # User blanchet # Date 1265364874 -3600 # Node ID d79308423aead9c2cbed187ddd2f5f5ef91f3652 # Parent 3df45b0ce8194d3ea7fd2c6e6b999a7264a6ac88 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 diff -r 3df45b0ce819 -r d79308423aea doc-src/Nitpick/nitpick.tex --- 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} diff -r 3df45b0ce819 -r d79308423aea src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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 diff -r 3df45b0ce819 -r d79308423aea src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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}