--- a/doc-src/Nitpick/nitpick.tex Tue Aug 03 18:52:42 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Wed Aug 04 10:52:29 2010 +0200
@@ -247,22 +247,22 @@
The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
containing type variables, Nitpick enumerates the possible domains for each type
-variable, up to a given cardinality (8 by default), looking for a finite
+variable, up to a given cardinality (10 by default), looking for a finite
countermodel:
\prew
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
\slshape
-Trying 8 scopes: \nopagebreak \\
+Trying 10 scopes: \nopagebreak \\
\hbox{}\qquad \textit{card}~$'a$~= 1; \\
\hbox{}\qquad \textit{card}~$'a$~= 2; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
-\hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount]
+\hbox{}\qquad \textit{card}~$'a$~= 10. \\[2\smallskipamount]
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
-Total time: 580 ms.
+Total time: 768 ms.
\postw
Nitpick found a counterexample in which $'a$ has cardinality 3. (For
@@ -370,7 +370,7 @@
\slshape Nitpick found no counterexample.
\postw
-Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
+Let's see if Sledgehammer can find a proof:
\prew
\textbf{sledgehammer} \\[2\smallskipamount]
@@ -552,7 +552,7 @@
cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
example above is an exception to this principle.) Nitpick nonetheless enumerates
-all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
+all cardinalities from 1 to 10 for \textit{nat}, mainly because smaller
cardinalities are fast to handle and give rise to simpler counterexamples. This
is explained in more detail in \S\ref{scope-monotonicity}.
@@ -767,7 +767,7 @@
Inductively defined predicates (and sets) are particularly problematic for
counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
-the problem is that they are defined using a least fixed point construction.
+the problem is that they are defined using a least fixed-point construction.
Nitpick's philosophy is that not all inductive predicates are equal. Consider
the \textit{even} predicate below:
@@ -797,7 +797,7 @@
\postw
Wellfoundedness is desirable because it enables Nitpick to use a very efficient
-fixed point computation.%
+fixed-point computation.%
\footnote{If an inductive predicate is
well-founded, then it has exactly one fixed point, which is simultaneously the
least and the greatest fixed point. In these circumstances, the computation of
@@ -818,8 +818,8 @@
\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
-Nitpick could not find a better counterexample. It checked 1 of 1 scope. \\[2\smallskipamount]
-Total time: 2274 ms.
+Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount]
+Total time: 1439 ms.
\postw
No genuine counterexample is possible because Nitpick cannot rule out the
@@ -872,7 +872,7 @@
& 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
& 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
-Total time: 1140 ms.
+Total time: 2420 ms.
\postw
Nitpick's output is very instructive. First, it tells us that the predicate is
@@ -892,7 +892,7 @@
predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
\textit{True} or $\unk$, never \textit{False}.
-When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
+When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, 20, 24, and 28
iterations. However, these numbers are bounded by the cardinality of the
predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
ever needed to compute the value of a \textit{nat} predicate. You can specify
@@ -1019,12 +1019,12 @@
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
\slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
some scopes. \\[2\smallskipamount]
-Trying 8 scopes: \\
+Trying 10 scopes: \\
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
and \textit{bisim\_depth}~= 0. \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
-\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 8,
-and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
+\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10,
+and \textit{bisim\_depth}~= 9. \\[2\smallskipamount]
Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
\textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
depth}~= 1:
@@ -1034,7 +1034,7 @@
\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
-Total time: 726 ms.
+Total time: 1027 ms.
\postw
The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
@@ -1166,11 +1166,11 @@
\textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
\slshape
-Trying 8 scopes: \nopagebreak \\
+Trying 10 scopes: \nopagebreak \\
\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
-\hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
+\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 10. \\[2\smallskipamount]
Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
@@ -1182,7 +1182,7 @@
4 := \textit{Var}~0,\>
5 := \textit{Var}~0)\end{aligned}$ \\
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
-Total time: $4679$ ms.
+Total time: $3560$ ms.
\postw
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
@@ -1193,14 +1193,14 @@
replaced with $\textit{lift}~(\sigma~m)~0$.
An interesting aspect of Nitpick's verbose output is that it assigned inceasing
-cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
+cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$.
For the formula of interest, knowing 6 values of that type was enough to find
the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
considered, a hopeless undertaking:
\prew
\textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 3 of 10 scopes.}
\postw
{\looseness=-1
@@ -1221,7 +1221,7 @@
exhaust all models below a certain cardinality bound, the number of scopes that
Nitpick must consider increases exponentially with the number of type variables
(and \textbf{typedecl}'d types) occurring in the formula. Given the default
-cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
+cardinality specification of 1--10, no fewer than $10^4 = 10\,000$ scopes must be
considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
Fortunately, many formulas exhibit a property called \textsl{scope
@@ -1235,8 +1235,8 @@
\postw
where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
-$'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
-exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
+$'b~\textit{list}$. A priori, Nitpick would need to consider $1\,000$ scopes to
+exhaust the specification \textit{card}~= 1--10. However, our intuition tells us
that any counterexample found with a small scope would still be a counterexample
in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
by the larger scope. Nitpick comes to the same conclusion after a careful
@@ -1248,7 +1248,7 @@
The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
Nitpick might be able to skip some scopes.
\\[2\smallskipamount]
-Trying 8 scopes: \\
+Trying 10 scopes: \\
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
\textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
\textit{list\/}''~= 1, \\
@@ -1260,11 +1260,11 @@
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
-\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
-\textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
-\textit{list\/}''~= 8, \\
-\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 8, and
-\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 8.
+\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} $'b$~= 10,
+\textit{card} \textit{nat}~= 10, \textit{card} ``$('a \times {'}b)$
+\textit{list\/}''~= 10, \\
+\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 10, and
+\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 10.
\\[2\smallskipamount]
Nitpick found a counterexample for
\textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
@@ -1281,7 +1281,7 @@
In theory, it should be sufficient to test a single scope:
\prew
-\textbf{nitpick}~[\textit{card}~= 8]
+\textbf{nitpick}~[\textit{card}~= 10]
\postw
However, this is often less efficient in practice and may lead to overly complex
@@ -1312,9 +1312,9 @@
\S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
are normally monotonic and treated as such. The same is true for record types,
\textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
-cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
+cardinality specification 1--10, a formula involving \textit{nat}, \textit{int},
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
-consider only 8~scopes instead of $32\,768$.
+consider only 10~scopes instead of $10\,000$.
\subsection{Inductive Properties}
\label{inductive-properties}
@@ -1658,7 +1658,7 @@
``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-\slshape Nitpick ran out of time after checking 7 of 8 scopes.
+\slshape Nitpick found no counterexample.
\postw
\subsection{AA Trees}
@@ -1767,7 +1767,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 ran out of time after checking 9 of 10 scopes.}
\postw
Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
@@ -1829,7 +1829,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 7 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 8 of 10 scopes.}
\postw
Insertion should transform the set of elements represented by the tree in the
@@ -1839,7 +1839,7 @@
\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 6 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 7 of 10 scopes.}
\postw
We could continue like this and sketch a complete theory of AA trees. Once the
@@ -1984,7 +1984,7 @@
{\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
(\S\ref{scope-of-search}).}
-\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
+\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{10}$}
Specifies the default sequence of cardinalities to use. This can be overridden
on a per-type basis using the \textit{card}~\qty{type} option described above.
@@ -2032,7 +2032,7 @@
{\small See also \textit{bits} (\S\ref{scope-of-search}) and
\textit{show\_datatypes} (\S\ref{output-format}).}
-\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
+\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12},\mathbf{14},\mathbf{16}$}
Specifies the number of bits to use to represent natural numbers and integers in
binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
@@ -2056,7 +2056,7 @@
\item[$\bullet$] \textbf{\textit{smart}:} Try to prove that the inductive
predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
\textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
-appropriate polarity in the formula to falsify), use an efficient fixed point
+appropriate polarity in the formula to falsify), use an efficient fixed-point
equation as specification of the predicate; otherwise, unroll the predicates
according to the \textit{iter}~\qty{const} and \textit{iter} options.
\end{enum}
@@ -2082,12 +2082,12 @@
{\small See also \textit{wf} (\S\ref{scope-of-search}) and
\textit{star\_linear\_preds} (\S\ref{optimizations}).}
-\opdefault{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
+\opdefault{iter}{int\_seq}{$\mathbf{0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}$}
Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
predicates. This can be overridden on a per-predicate basis using the
\textit{iter} \qty{const} option above.
-\opdefault{bisim\_depth}{int\_seq}{$\mathbf{7}$}
+\opdefault{bisim\_depth}{int\_seq}{$\mathbf{9}$}
Specifies the sequence of iteration counts to use when unrolling the
bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
of $-1$ means that no predicate is generated, in which case Nitpick performs an
@@ -2454,7 +2454,7 @@
together ensures that Kodkodi is launched less often, but it makes the verbose
output less readable and is sometimes detrimental to performance. If
\textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
-\textit{debug} (\S\ref{output-format}) is set and 64 otherwise.
+\textit{debug} (\S\ref{output-format}) is set and 50 otherwise.
\optrue{destroy\_constrs}{dont\_destroy\_constrs}
Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
@@ -2585,7 +2585,7 @@
and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
\textit{simps} rules. The equations must be of the form
-\qquad $c~t_1~\ldots\ t_n \,=\, u.$
+\qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr].$
\flushitem{\textit{nitpick\_psimp}}
@@ -2595,14 +2595,13 @@
corresponds to the \textit{psimps} rules. The conditional equations must be of
the form
-\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
+\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$.
\flushitem{\textit{nitpick\_choice\_spec}}
\nopagebreak
This attribute specifies the (free-form) specification of a constant defined
using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
-
\end{enum}
When faced with a constant, Nitpick proceeds as follows:
@@ -2623,17 +2622,24 @@
\item[4.] Otherwise, it looks up the definition of the constant:
\begin{enum}
-\item[1.] If the \textit{nitpick\_def} set associated with the constant
-is not empty, it uses the latest rule added to the set as the definition of the
-constant; otherwise it uses the actual definition axiom.
+\item[1.] If the \textit{nitpick\_def} set associated with the constant is not
+empty, it uses the latest rule added to the set as the definition of the
+constant; otherwise it uses the actual definition axiom. In addition, the
+constant is \textsl{unfolded} wherever it appears (as opposed to defined
+equationally).
\item[2.] If the definition is of the form
-\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$,
-
-then Nitpick assumes that the definition was made using an inductive package and
-based on the introduction rules marked with \textit{nitpick\_\allowbreak
-\allowbreak intros} tries to determine whether the definition is
-well-founded.
+\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$
+
+or
+
+\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{gfp}~(\lambda f.\; t)$
+
+Nitpick assumes that the definition was made using a (co)inductive package
+based on the user-specified introduction rules registered in Isabelle's internal
+\textit{Spec\_Rules} table. The tool uses the introduction rules to ascertain
+whether the definition is well-founded and the definition to generate a
+fixed-point equation or an unrolled equation.
\end{enum}
\end{enum}
@@ -2646,18 +2652,18 @@
\postw
By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
-the introduction rules. To override this, we can specify an alternative
+the introduction rules. To override this, you can specify an alternative
definition as follows:
\prew
-\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
+\textbf{lemma} $\mathit{odd\_alt\_def}$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
\postw
Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
-= 1$. Alternatively, we can specify an equational specification of the constant:
+= 1$. Alternatively, you can specify an equational specification of the constant:
\prew
-\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
+\textbf{lemma} $\mathit{odd\_simp}$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
\postw
Such tweaks should be done with great care, because Nitpick will assume that the
@@ -2667,6 +2673,44 @@
(\S\ref{output-format}) option is extremely useful to understand what is going
on when experimenting with \textit{nitpick\_} attributes.
+Because of its internal three-valued logic, Nitpick tends to lose a
+lot of precision in the presence of partially specified constants. For example,
+
+\prew
+\textbf{lemma} \textit{odd\_simp} [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd~x} = \lnot\, \textit{even}~x$''
+\postw
+
+is superior to
+
+\prew
+\textbf{lemma} \textit{odd\_psimps} [\textit{nitpick\_simp}]: \\
+``$\textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{False\/}$'' \\
+``$\lnot\, \textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{True\/}$''
+\postw
+
+Because Nitpick unfolds definitions but not simplification rules, it often pays
+off to declare long-winded definitions as \textit{nitpick\_simp}. For example:
+
+\prew
+\textbf{definition}~\textit{optimum} \textbf{where} [\textit{nitpick\_simp}]: \\
+``$\textit{optimum}~t =
+ (\forall u.\; \textit{consistent}~u \mathrel{\land} \textit{alphabet}~t = \textit{alphabet}~u$ \\
+\phantom{``$\textit{optimum}~t = (\forall u.\;$}${\mathrel{\land}}\; \textit{freq}~t = \textit{freq}~u \longrightarrow
+ \textit{cost}~t \le \textit{cost}~u)$''
+\postw
+
+In some rare occasions, you might want to provide an inductive or coinductive
+view on top of an existing constant $c$. The easiest way to achieve this is to
+define a new constant $c'$ (co)inductively. Then prove that $c$ equals $c'$
+and let Nitpick know about it:
+
+\prew
+\textbf{lemma} \textit{c\_alt\_def} [\textit{nitpick\_def}]:\kern.4em ``$c \equiv c'$\kern2pt ''
+\postw
+
+This ensures that Nitpick will substitute $c'$ for $c$ and use the (co)inductive
+definition.
+
\section{Standard ML Interface}
\label{standard-ml-interface}
--- a/src/HOL/Library/Nat_Infinity.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Wed Aug 04 10:52:29 2010 +0200
@@ -125,7 +125,7 @@
instantiation inat :: comm_monoid_add
begin
-definition
+definition [nitpick_simp]:
"m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
lemma plus_inat_simps [simp, code]:
@@ -176,8 +176,7 @@
instantiation inat :: comm_semiring_1
begin
-definition
- times_inat_def:
+definition times_inat_def [nitpick_simp]:
"m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
(case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
@@ -237,11 +236,11 @@
instantiation inat :: linordered_ab_semigroup_add
begin
-definition
+definition [nitpick_simp]:
"m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
| \<infinity> \<Rightarrow> True)"
-definition
+definition [nitpick_simp]:
"m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
| \<infinity> \<Rightarrow> False)"
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Aug 04 10:52:29 2010 +0200
@@ -11,8 +11,8 @@
imports Main
begin
-nitpick_params [unary_ints, max_potential = 0, sat_solver = MiniSat_JNI,
- max_threads = 1, timeout = 60 s]
+nitpick_params [card = 1\<midarrow>6, unary_ints, max_potential = 0,
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
subsection {* Curry in a Hurry *}
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Aug 04 10:52:29 2010 +0200
@@ -11,8 +11,8 @@
imports Main
begin
-nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60 s]
+nitpick_params [card = 1\<midarrow>8, max_potential = 0,
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
primrec rot where
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Aug 04 10:52:29 2010 +0200
@@ -52,7 +52,7 @@
theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
nitpick [card room = 1, card guest = 2, card "guest option" = 3,
card key = 4, card state = 6, expect = genuine]
-nitpick [card room = 1, card guest = 2, expect = genuine]
+(* nitpick [card room = 1, card guest = 2, expect = genuine] *)
oops
end
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Aug 04 10:52:29 2010 +0200
@@ -11,7 +11,8 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI,
+ max_threads = 1, timeout = 60 s]
inductive p1 :: "nat \<Rightarrow> bool" where
"p1 0" |
@@ -114,58 +115,42 @@
lemma "p3 = q3"
nitpick [expect = none]
-nitpick [dont_star_linear_preds, expect = none]
-nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_box, expect = none]
-nitpick [non_wf, dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = none]
sorry
lemma "p4 = q4"
nitpick [expect = none]
-nitpick [dont_star_linear_preds, expect = none]
-nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_box, expect = none]
-nitpick [non_wf, dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = none]
sorry
lemma "p3 = UNIV - p4"
nitpick [expect = none]
-nitpick [dont_star_linear_preds, expect = none]
-nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_box, expect = none]
-nitpick [non_wf, dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = none]
sorry
lemma "q3 = UNIV - q4"
nitpick [expect = none]
-nitpick [dont_star_linear_preds, expect = none]
nitpick [non_wf, expect = none]
-nitpick [non_wf, dont_box, expect = none]
-nitpick [non_wf, dont_star_linear_preds, expect = none]
sorry
lemma "p3 \<inter> q4 \<noteq> {}"
nitpick [expect = potential]
nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_star_linear_preds, expect = potential]
sorry
lemma "q3 \<inter> p4 \<noteq> {}"
nitpick [expect = potential]
nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_star_linear_preds, expect = potential]
sorry
lemma "p3 \<union> q4 \<noteq> UNIV"
nitpick [expect = potential]
nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_star_linear_preds, expect = potential]
sorry
lemma "q3 \<union> p4 \<noteq> UNIV"
nitpick [expect = potential]
nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_star_linear_preds, expect = potential]
sorry
end
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Aug 04 10:52:29 2010 +0200
@@ -11,8 +11,8 @@
imports Nitpick
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
- card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
+nitpick_params [card = 1\<midarrow>6, bits = 1,2,3,4,6,8,
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
lemma "Suc x = x + 1"
nitpick [unary_ints, expect = none]
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Aug 04 10:52:29 2010 +0200
@@ -158,7 +158,7 @@
oops
lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
-nitpick [card nat = 50, unary_ints, verbose, expect = genuine]
+nitpick [card nat = 50, unary_ints, expect = genuine]
oops
inductive even' where
@@ -192,8 +192,9 @@
subsection {* 3.9. Coinductive Datatypes *}
(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
-we cannot rely on its presence, we expediently provide our own axiomatization.
-The examples also work unchanged with Lochbihler's "Coinductive_List" theory. *)
+ we cannot rely on its presence, we expediently provide our own
+ axiomatization. The examples also work unchanged with Lochbihler's
+ "Coinductive_List" theory. *)
typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
@@ -225,7 +226,7 @@
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
sorry
subsection {* 3.10. Boxing *}
@@ -268,7 +269,6 @@
lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
nitpick [verbose, expect = genuine]
-nitpick [card = 8, verbose, expect = genuine]
oops
lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
@@ -284,19 +284,19 @@
"n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
-nitpick [card = 1\<midarrow>5, bits = 1\<midarrow>5, expect = none]
+(* nitpick *)
apply (induct set: reach)
apply auto
- nitpick [card = 1\<midarrow>5, bits = 1\<midarrow>5, expect = none]
+ nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
apply (thin_tac "n \<in> reach")
nitpick [expect = genuine]
oops
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
-nitpick [card = 1\<midarrow>5, bits = 1\<midarrow>5, expect = none]
+(* nitpick *)
apply (induct set: reach)
apply auto
- nitpick [card = 1\<midarrow>5, bits = 1\<midarrow>5, expect = none]
+ nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
apply (thin_tac "n \<in> reach")
nitpick [expect = genuine]
oops
@@ -335,7 +335,7 @@
case Leaf thus ?case by simp
next
case (Branch t u) thus ?case
- nitpick [non_std, card = 1\<midarrow>5, expect = none]
+ nitpick [non_std, card = 1\<midarrow>4, expect = none]
by auto
qed
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Aug 04 10:52:29 2010 +0200
@@ -11,8 +11,8 @@
imports Main
begin
-nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60 s]
+nitpick_params [card = 1\<midarrow>6, max_potential = 0,
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
record point2d =
xc :: int
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Aug 04 10:52:29 2010 +0200
@@ -11,8 +11,8 @@
imports Main
begin
-nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60 s]
+nitpick_params [card = 1\<midarrow>6, max_potential = 0,
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
lemma "P \<and> Q"
apply (rule conjI)
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Aug 04 10:52:29 2010 +0200
@@ -1106,8 +1106,9 @@
fun solve_any_problem overlord deadline max_threads max_solutions problems =
let
- fun do_solve () = uncached_solve_any_problem overlord deadline max_threads
- max_solutions problems
+ fun do_solve () =
+ uncached_solve_any_problem overlord deadline max_threads max_solutions
+ problems
in
if overlord then
do_solve ()
--- a/src/HOL/Tools/Nitpick/minipick.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Aug 04 10:52:29 2010 +0200
@@ -37,7 +37,7 @@
fun check_type ctxt (Type (@{type_name fun}, Ts)) =
List.app (check_type ctxt) Ts
- | check_type ctxt (Type (@{type_name Product_Type.prod}, Ts)) =
+ | check_type ctxt (Type (@{type_name prod}, Ts)) =
List.app (check_type ctxt) Ts
| check_type _ @{typ bool} = ()
| check_type _ (TFree (_, @{sort "{}"})) = ()
@@ -51,7 +51,7 @@
atom_schema_of SRep card T1
| atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
- | atom_schema_of _ card (Type (@{type_name Product_Type.prod}, Ts)) =
+ | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
maps (atom_schema_of SRep card) Ts
| atom_schema_of _ card T = [card T]
val arity_of = length ooo atom_schema_of
@@ -290,7 +290,7 @@
val thy = ProofContext.theory_of ctxt
fun card (Type (@{type_name fun}, [T1, T2])) =
reasonable_power (card T2) (card T1)
- | card (Type (@{type_name Product_Type.prod}, [T1, T2])) = card T1 * card T2
+ | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
| card @{typ bool} = 2
| card T = Int.max (1, raw_card T)
val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Aug 04 10:52:29 2010 +0200
@@ -180,7 +180,7 @@
fun plazy f = Pretty.blk (0, pstrs (f ()))
fun pick_them_nits_in_term deadline state (params : params) auto i n step
- subst orig_assm_ts orig_t =
+ subst assm_ts orig_t =
let
val timer = Timer.startRealTimer ()
val thy = Proof.theory_of state
@@ -223,7 +223,7 @@
if passed_deadline deadline then raise TimeLimit.TimeOut
else raise Interrupt
- val orig_assm_ts = if assms orelse auto then orig_assm_ts else []
+ val assm_ts = if assms orelse auto then assm_ts else []
val _ =
if step = 0 then
print_m (fn () => "Nitpicking formula...")
@@ -233,13 +233,18 @@
(if i <> 1 orelse n <> 1 then
"subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
else
- "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
+ "goal")) [Logic.list_implies (assm_ts, orig_t)]))
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
else orig_t
- val assms_t = Logic.mk_conjunction_list (neg_t :: orig_assm_ts)
- val (assms_t, evals) =
- assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms
- |> pairf hd tl
+ val tfree_table =
+ if merge_type_vars then
+ merged_type_var_table_for_terms (neg_t :: assm_ts @ evals)
+ else
+ []
+ val neg_t = merge_type_vars_in_term merge_type_vars tfree_table neg_t
+ val assm_ts = map (merge_type_vars_in_term merge_type_vars tfree_table)
+ assm_ts
+ val evals = map (merge_type_vars_in_term merge_type_vars tfree_table) evals
val original_max_potential = max_potential
val original_max_genuine = max_genuine
val max_bisim_depth = fold Integer.max bisim_depths ~1
@@ -269,11 +274,12 @@
skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
- val frees = Term.add_frees assms_t []
- val _ = null (Term.add_tvars assms_t []) orelse
+ val pseudo_frees = fold Term.add_frees assm_ts []
+ val real_frees = subtract (op =) pseudo_frees (Term.add_frees neg_t [])
+ val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
raise NOT_SUPPORTED "schematic type variables"
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
- binarize) = preprocess_term hol_ctxt finitizes monos assms_t
+ binarize) = preprocess_formulas hol_ctxt finitizes monos assm_ts neg_t
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
@@ -288,9 +294,10 @@
"\" could not be proved well-founded. Nitpick might need to \
\unroll it.")))
val _ = if verbose then List.app print_wf (!wf_cache) else ()
+ val das_wort_formula = if falsify then "Negated conjecture" else "Formula"
val _ =
pprint_d (fn () => Pretty.chunks
- (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
+ (pretties_for_formulas ctxt das_wort_formula [hd nondef_ts] @
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
pretties_for_formulas ctxt "Relevant nondefinitional axiom"
(tl nondef_ts)))
@@ -314,14 +321,16 @@
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
fun monotonicity_message Ts extra =
- let val ss = map (quote o string_for_type ctxt) Ts in
- "The type" ^ plural_s_for_list ss ^ " " ^
- space_implode " " (serial_commas "and" ss) ^ " " ^
- (if none_true monos then
- "passed the monotonicity test"
- else
- (if length ss = 1 then "is" else "are") ^ " considered monotonic") ^
- ". " ^ extra
+ let val pretties = map (pretty_maybe_quote o pretty_for_type ctxt) Ts in
+ Pretty.blk (0,
+ pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @
+ pretty_serial_commas "and" pretties @
+ pstrs (" " ^
+ (if none_true monos then
+ "passed the monotonicity test"
+ else
+ (if length pretties = 1 then "is" else "are") ^ " considered monotonic") ^
+ ". " ^ extra))
end
fun is_type_fundamentally_monotonic T =
(is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso
@@ -366,8 +375,8 @@
case filter_out is_type_fundamentally_monotonic mono_Ts of
[] => ()
| interesting_mono_Ts =>
- print_v (K (monotonicity_message interesting_mono_Ts
- "Nitpick might be able to skip some scopes."))
+ pprint_v (K (monotonicity_message interesting_mono_Ts
+ "Nitpick might be able to skip some scopes."))
else
()
val (deep_dataTs, shallow_dataTs) =
@@ -378,8 +387,8 @@
|> filter is_shallow_datatype_finitizable
val _ =
if verbose andalso not (null finitizable_dataTs) then
- print_v (K (monotonicity_message finitizable_dataTs
- "Nitpick can use a more precise finite encoding."))
+ pprint_v (K (monotonicity_message finitizable_dataTs
+ "Nitpick can use a more precise finite encoding."))
else
()
(* This detection code is an ugly hack. Fortunately, it is used only to
@@ -446,7 +455,6 @@
(Typtab.dest ofs)
*)
val all_exact = forall (is_exact_type datatypes true) all_Ts
- val repify_consts = choose_reps_for_consts scope all_exact
val main_j0 = offset_of_type ofs bool_T
val (nat_card, nat_j0) = spec_of_type scope nat_T
val (int_card, int_j0) = spec_of_type scope int_T
@@ -455,15 +463,20 @@
"bad offsets")
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
val (free_names, rep_table) =
- choose_reps_for_free_vars scope free_names NameTable.empty
+ choose_reps_for_free_vars scope pseudo_frees free_names
+ NameTable.empty
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
- val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table
- val min_highest_arity =
- NameTable.fold (Integer.max o arity_of_rep o snd) rep_table 1
+ val (nonsel_names, rep_table) =
+ choose_reps_for_consts scope all_exact nonsel_names rep_table
+ val (guiltiest_party, min_highest_arity) =
+ NameTable.fold (fn (name, R) => fn (s, n) =>
+ let val n' = arity_of_rep R in
+ if n' > n then (nickname_of name, n') else (s, n)
+ end) rep_table ("", 1)
val min_univ_card =
NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table
(univ_card nat_card int_card main_j0 [] KK.True)
- val _ = check_arity min_univ_card min_highest_arity
+ val _ = check_arity guiltiest_party min_univ_card min_highest_arity
val def_us = map (choose_reps_in_nut scope unsound rep_table true)
def_us
@@ -525,7 +538,7 @@
val formula = fold_rev s_and axioms formula
val _ = if bits = 0 then () else check_bits bits formula
val _ = if formula = KK.False then ()
- else check_arity univ_card highest_arity
+ else check_arity "" univ_card highest_arity
in
SOME ({comment = comment, settings = settings, univ_card = univ_card,
tuple_assigns = [], bounds = bounds,
@@ -584,11 +597,12 @@
val (reconstructed_model, codatatypes_ok) =
reconstruct_hol_model {show_datatypes = show_datatypes,
show_consts = show_consts}
- scope formats atomss frees free_names sel_names nonsel_names
- rel_table bounds
+ scope formats atomss real_frees pseudo_frees free_names sel_names
+ nonsel_names rel_table bounds
val genuine_means_genuine =
got_all_user_axioms andalso none_true wfs andalso
sound_finitizes andalso codatatypes_ok
+ fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
in
(pprint (Pretty.chunks
[Pretty.blk (0,
@@ -604,7 +618,7 @@
if genuine then
(if check_genuine andalso standard then
case prove_hol_model scope tac_timeout free_names sel_names
- rel_table bounds assms_t of
+ rel_table bounds (assms_prop ()) of
SOME true =>
print ("Confirmation by \"auto\": The above " ^
das_wort_model ^ " is really genuine.")
@@ -648,7 +662,7 @@
options
in
print ("Try again with " ^
- space_implode " " (serial_commas "and" ss) ^
+ implode (serial_commas "and" ss) ^
" to confirm that the " ^ das_wort_model ^
" is genuine.")
end
@@ -665,7 +679,8 @@
if check_potential then
let
val status = prove_hol_model scope tac_timeout free_names
- sel_names rel_table bounds assms_t
+ sel_names rel_table bounds
+ (assms_prop ())
in
(case status of
SOME true => print ("Confirmation by \"auto\": The \
@@ -953,7 +968,7 @@
error "Nitpick was interrupted."
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
- step subst orig_assm_ts orig_t =
+ step subst assm_ts orig_t =
let val warning_m = if auto then K () else warning in
if getenv "KODKODI" = "" then
(* The "expect" argument is deliberately ignored if Kodkodi is missing so
@@ -967,7 +982,7 @@
val outcome as (outcome_code, _) =
time_limit (if debug then NONE else timeout)
(pick_them_nits_in_term deadline state params auto i n step subst
- orig_assm_ts) orig_t
+ assm_ts) orig_t
handle TOO_LARGE (_, details) =>
(warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
| TOO_SMALL (_, details) =>
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Aug 04 10:52:29 2010 +0200
@@ -76,6 +76,7 @@
val unarize_unbox_etc_type : typ -> typ
val uniterize_unarize_unbox_etc_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
+ val pretty_for_type : Proof.context -> typ -> Pretty.T
val prefix_name : string -> string -> string
val shortest_name : string -> string
val short_name : string -> string
@@ -210,7 +211,8 @@
val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
val equational_fun_axioms : hol_context -> styp -> term list
val is_equational_fun_surely_complete : hol_context -> styp -> bool
- val merge_type_vars_in_terms : term list -> term list
+ val merged_type_var_table_for_terms : term list -> (sort * string) list
+ val merge_type_vars_in_term : bool -> (sort * string) list -> term -> term
val ground_types_in_type : hol_context -> bool -> typ -> typ list
val ground_types_in_terms : hol_context -> bool -> term list -> typ list
end;
@@ -398,7 +400,6 @@
(@{const_name "op -->"}, 2),
(@{const_name If}, 3),
(@{const_name Let}, 2),
- (@{const_name Unity}, 0),
(@{const_name Pair}, 2),
(@{const_name fst}, 1),
(@{const_name snd}, 1),
@@ -454,7 +455,7 @@
| unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
| unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
- Type (@{type_name Product_Type.prod}, map unarize_unbox_etc_type Ts)
+ Type (@{type_name prod}, map unarize_unbox_etc_type Ts)
| unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
| unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
| unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
@@ -466,6 +467,7 @@
val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
+fun pretty_for_type ctxt = Syntax.pretty_typ ctxt o unarize_unbox_etc_type
val prefix_name = Long_Name.qualify o Long_Name.base_name
fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
@@ -509,7 +511,7 @@
| is_fun_type _ = false
fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
| is_set_type _ = false
-fun is_pair_type (Type (@{type_name Product_Type.prod}, _)) = true
+fun is_pair_type (Type (@{type_name prod}, _)) = true
| is_pair_type _ = false
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
| is_lfp_iterator_type _ = false
@@ -546,7 +548,7 @@
| strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
val nth_range_type = snd oo strip_n_binders
-fun num_factors_in_type (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) =
fold (Integer.add o num_factors_in_type) [T1, T2] 0
| num_factors_in_type _ = 1
fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
@@ -557,7 +559,7 @@
(if is_pair_type (body_type T) then binder_types else curried_binder_types) T
fun mk_flat_tuple _ [t] = t
- | mk_flat_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) (t :: ts) =
+ | mk_flat_tuple (Type (@{type_name prod}, [T1, T2])) (t :: ts) =
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
| mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
fun dest_n_tuple 1 t = [t]
@@ -595,8 +597,8 @@
(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
e.g., by adding a field to "Datatype_Aux.info". *)
fun is_basic_datatype thy stds s =
- member (op =) [@{type_name Product_Type.prod}, @{type_name bool}, @{type_name unit},
- @{type_name int}, "Code_Numeral.code_numeral"] s orelse
+ member (op =) [@{type_name prod}, @{type_name bool}, @{type_name int},
+ "Code_Numeral.code_numeral"] s orelse
(s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
fun instantiate_type thy T1 T1' T2 =
@@ -792,7 +794,7 @@
Type (@{type_name fun}, _) =>
(boxy = InPair orelse boxy = InFunLHS) andalso
not (is_boolean_type (body_type T))
- | Type (@{type_name Product_Type.prod}, Ts) =>
+ | Type (@{type_name prod}, Ts) =>
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
((boxy = InExpr orelse boxy = InFunLHS) andalso
exists (is_boxing_worth_it hol_ctxt InPair)
@@ -812,12 +814,12 @@
else
box_type hol_ctxt (in_fun_lhs_for boxy) T1
--> box_type hol_ctxt (in_fun_rhs_for boxy) T2
- | Type (z as (@{type_name Product_Type.prod}, Ts)) =>
+ | Type (z as (@{type_name prod}, Ts)) =>
if boxy <> InConstr andalso boxy <> InSel
andalso should_box_type hol_ctxt boxy z then
Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
else
- Type (@{type_name Product_Type.prod},
+ Type (@{type_name prod},
map (box_type hol_ctxt
(if boxy = InConstr orelse boxy = InSel then boxy
else InPair)) Ts)
@@ -979,7 +981,7 @@
Const (nth_sel_for_constr x n)
else
let
- fun aux m (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ fun aux m (Type (@{type_name prod}, [T1, T2])) =
let
val (m, t1) = aux m T1
val (m, t2) = aux m T2
@@ -1069,7 +1071,7 @@
| (Type (new_s, new_Ts as [new_T1, new_T2]),
Type (old_s, old_Ts as [old_T1, old_T2])) =>
if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
- old_s = @{type_name pair_box} orelse old_s = @{type_name Product_Type.prod} then
+ old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then
case constr_expand hol_ctxt old_T t of
Const (old_s, _) $ t1 =>
if new_s = @{type_name fun} then
@@ -1081,7 +1083,7 @@
(Type (@{type_name fun}, old_Ts)) t1]
| Const _ $ t1 $ t2 =>
construct_value ctxt stds
- (if new_s = @{type_name Product_Type.prod} then @{const_name Pair}
+ (if new_s = @{type_name prod} then @{const_name Pair}
else @{const_name PairBox}, new_Ts ---> new_T)
(map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
[t1, t2])
@@ -1092,12 +1094,11 @@
fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
- | card_of_type assigns (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
card_of_type assigns T1 * card_of_type assigns T2
| card_of_type _ (Type (@{type_name itself}, _)) = 1
| card_of_type _ @{typ prop} = 2
| card_of_type _ @{typ bool} = 2
- | card_of_type _ @{typ unit} = 1
| card_of_type assigns T =
case AList.lookup (op =) assigns T of
SOME k => k
@@ -1113,7 +1114,7 @@
else Int.min (max, reasonable_power k2 k1)
end
| bounded_card_of_type max default_card assigns
- (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ (Type (@{type_name prod}, [T1, T2])) =
let
val k1 = bounded_card_of_type max default_card assigns T1
val k2 = bounded_card_of_type max default_card assigns T2
@@ -1143,7 +1144,7 @@
else if k1 >= max orelse k2 >= max then max
else Int.min (max, reasonable_power k2 k1)
end
- | Type (@{type_name Product_Type.prod}, [T1, T2]) =>
+ | Type (@{type_name prod}, [T1, T2]) =>
let
val k1 = aux avoid T1
val k2 = aux avoid T2
@@ -1155,7 +1156,6 @@
| Type (@{type_name itself}, _) => 1
| @{typ prop} => 2
| @{typ bool} => 2
- | @{typ unit} => 1
| Type _ =>
(case datatype_constrs hol_ctxt T of
[] => if is_integer_type T orelse is_bit_type T then 0
@@ -1195,9 +1195,10 @@
fun special_bounds ts =
fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
+(* FIXME: detect "rep_datatype"? *)
fun is_funky_typedef_name thy s =
- member (op =) [@{type_name unit}, @{type_name Product_Type.prod}, @{type_name Sum_Type.sum},
- @{type_name int}] s orelse
+ member (op =) [@{type_name unit}, @{type_name prod},
+ @{type_name Sum_Type.sum}, @{type_name int}] s orelse
is_frac_type thy (Type (s, []))
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
| is_funky_typedef _ _ = false
@@ -1373,7 +1374,8 @@
case t |> strip_abs_body |> strip_comb of
(Const x, ts as (_ :: _)) =>
(case def_of_const thy table x of
- SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
+ SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso
+ forall is_good_arg ts
| NONE => false)
| _ => false
end
@@ -1725,25 +1727,41 @@
(** Axiom extraction/generation **)
+fun equationalize t =
+ case Logic.strip_horn t of
+ (_, @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ _)) => t
+ | (prems, @{const Trueprop} $ t') =>
+ Logic.list_implies (prems,
+ @{const Trueprop} $ HOLogic.mk_eq (t', @{const True}))
+ | _ => t
+
fun pair_for_prop t =
case term_under_def t of
Const (s, _) => (s, t)
| t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
+
fun def_table_for get ctxt subst =
ctxt |> get |> map (pair_for_prop o subst_atomic subst)
|> AList.group (op =) |> Symtab.make
-fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
+
fun const_def_table ctxt subst ts =
def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
|> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
(map pair_for_prop ts)
+
+fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
fun const_nondef_table ts =
fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
-val const_simp_table = def_table_for (map prop_of o Nitpick_Simps.get)
-val const_psimp_table = def_table_for (map prop_of o Nitpick_Psimps.get)
+
+val const_simp_table =
+ def_table_for (map (equationalize o prop_of) o Nitpick_Simps.get)
+val const_psimp_table =
+ def_table_for (map (equationalize o prop_of) o Nitpick_Psimps.get)
+
fun const_choice_spec_table ctxt subst =
map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
|> const_nondef_table
+
fun inductive_intro_table ctxt subst def_table =
let val thy = ProofContext.theory_of ctxt in
def_table_for
@@ -1753,6 +1771,7 @@
cat = Spec_Rules.Co_Inductive)
o Spec_Rules.get) ctxt subst
end
+
fun ground_theorem_table thy =
fold ((fn @{const Trueprop} $ t1 =>
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
@@ -1842,7 +1861,6 @@
val xs = datatype_constrs hol_ctxt T
val set_T = T --> bool_T
val iter_T = @{typ bisim_iterator}
- val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
val bisim_max = @{const bisim_iterator_max}
val n_var = Var (("n", 0), iter_T)
val n_var_minus_1 =
@@ -1851,8 +1869,10 @@
$ (suc_const iter_T $ Bound 0) $ n_var)
val x_var = Var (("x", 0), T)
val y_var = Var (("y", 0), T)
+ fun bisim_const T =
+ Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
fun nth_sub_bisim x n nth_T =
- (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
+ (if is_codatatype thy nth_T then bisim_const nth_T $ n_var_minus_1
else HOLogic.eq_const nth_T)
$ select_nth_constr_arg ctxt stds x x_var n nth_T
$ select_nth_constr_arg ctxt stds x y_var n nth_T
@@ -1865,12 +1885,12 @@
|> foldr1 s_conj
in List.foldr absdummy core_t arg_Ts end
in
- [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
- $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
- $ (s_betapply []
- (optimized_case_def hol_ctxt T bool_T (map case_func xs),
- x_var))),
- HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
+ [HOLogic.mk_imp
+ (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
+ s_betapply [] (optimized_case_def hol_ctxt T bool_T
+ (map case_func xs), x_var)),
+ bisim_const T $ n_var $ x_var $ y_var),
+ HOLogic.eq_const set_T $ (bisim_const T $ bisim_max $ x_var)
$ (Const (@{const_name insert}, T --> set_T --> set_T)
$ x_var $ Const (@{const_name bot_class.bot}, set_T))]
|> map HOLogic.mk_Trueprop
@@ -2066,7 +2086,7 @@
val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
val set_T = tuple_T --> bool_T
val curried_T = tuple_T --> set_T
- val uncurried_T = Type (@{type_name Product_Type.prod}, [tuple_T, tuple_T]) --> bool_T
+ val uncurried_T = Type (@{type_name prod}, [tuple_T, tuple_T]) --> bool_T
val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
@@ -2087,6 +2107,10 @@
|> unfold_defs_in_term hol_ctxt
end
+fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
+ forall (not o (is_fun_type orf is_pair_type)) Ts
+ | is_good_starred_linear_pred_type _ = false
+
fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
def_table, simp_table, ...})
gfp (x as (s, T)) =
@@ -2098,8 +2122,9 @@
in
if is_equational_fun hol_ctxt x' then
unrolled_const (* already done *)
- else if not gfp andalso is_linear_inductive_pred_def def andalso
- star_linear_preds then
+ else if not gfp andalso star_linear_preds andalso
+ is_linear_inductive_pred_def def andalso
+ is_good_starred_linear_pred_type T then
starred_linear_pred_const hol_ctxt x def
else
let
@@ -2166,7 +2191,7 @@
(** Type preprocessing **)
-fun merge_type_vars_in_terms ts =
+fun merged_type_var_table_for_terms ts =
let
fun add_type (TFree (s, S)) table =
(case AList.lookup (op =) table S of
@@ -2175,21 +2200,23 @@
else table
| NONE => (S, s) :: table)
| add_type _ table = table
- val table = fold (fold_types (fold_atyps add_type)) ts []
- fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
- | coalesce T = T
- in map (map_types (map_atyps coalesce)) ts end
+ in fold (fold_types (fold_atyps add_type)) ts [] end
+
+fun merge_type_vars_in_term merge_type_vars table =
+ merge_type_vars
+ ? map_types (map_atyps
+ (fn TFree (_, S) => TFree (AList.lookup (op =) table S |> the, S)
+ | T => T))
fun add_ground_types hol_ctxt binarize =
let
fun aux T accum =
case T of
Type (@{type_name fun}, Ts) => fold aux Ts accum
- | Type (@{type_name Product_Type.prod}, Ts) => fold aux Ts accum
+ | Type (@{type_name prod}, Ts) => fold aux Ts accum
| Type (@{type_name itself}, [T1]) => aux T1 accum
| Type (_, Ts) =>
- if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
- T then
+ if member (op =) (@{typ prop} :: @{typ bool} :: accum) T then
accum
else
T :: accum
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Aug 04 10:52:29 2010 +0200
@@ -34,10 +34,10 @@
type raw_param = string * string list
val default_default_params =
- [("card", "1\<midarrow>8"),
- ("iter", "0,1,2,4,8,12,16,24"),
- ("bits", "1,2,3,4,6,8,10,12"),
- ("bisim_depth", "7"),
+ [("card", "1\<midarrow>10"),
+ ("iter", "0,1,2,4,8,12,16,20,24,28"),
+ ("bits", "1,2,3,4,6,8,10,12,14,16"),
+ ("bisim_depth", "9"),
("box", "smart"),
("finitize", "smart"),
("mono", "smart"),
@@ -265,7 +265,7 @@
val batch_size =
case lookup_int_option "batch_size" of
SOME n => Int.max (1, n)
- | NONE => if debug then 1 else 64
+ | NONE => if debug then 1 else 50
val expect = lookup_string "expect"
in
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Aug 04 10:52:29 2010 +0200
@@ -17,7 +17,7 @@
val univ_card :
int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
val check_bits : int -> Kodkod.formula -> unit
- val check_arity : int -> int -> unit
+ val check_arity : string -> int -> int -> unit
val kk_tuple : bool -> int -> int list -> Kodkod.tuple
val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
val sequential_int_bounds : int -> Kodkod.int_bound list
@@ -93,11 +93,17 @@
int_expr_func = int_expr_func}
in KK.fold_formula expr_F formula () end
-fun check_arity univ_card n =
+fun check_arity guilty_party univ_card n =
if n > KK.max_arity univ_card then
raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
- "arity " ^ string_of_int n ^ " too large for universe of \
- \cardinality " ^ string_of_int univ_card)
+ "arity " ^ string_of_int n ^
+ (if guilty_party = "" then
+ ""
+ else
+ " of Kodkod relation associated with " ^
+ quote guilty_party) ^
+ " too large for universe of cardinality " ^
+ string_of_int univ_card)
else
()
@@ -200,7 +206,7 @@
fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0
(x as (n, _)) =
- (check_arity univ_card n;
+ (check_arity "" univ_card n;
if x = not3_rel then
("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
else if x = suc_rel then
@@ -259,8 +265,10 @@
fun axiom_for_built_in_rel (x as (n, j)) =
if n = 2 andalso j <= suc_rels_base then
let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
- if tabulate orelse k < 2 then
+ if tabulate then
NONE
+ else if k < 2 then
+ SOME (KK.No (KK.Rel x))
else
SOME (KK.TotalOrdering (x, KK.AtomSeq y, KK.Atom j0, KK.Atom (j0 + 1)))
end
@@ -434,13 +442,11 @@
case arity_of_rep R1 of
1 => kk_join r1 r2
| arity1 =>
- let
- val unpacked_rs1 =
- if inline_rel_expr r1 then unpack_vect_in_chunks kk 1 arity1 r1
- else unpack_products r1
- in
+ let val unpacked_rs1 = unpack_products r1 in
if one andalso length unpacked_rs1 = arity1 then
fold kk_join unpacked_rs1 r2
+ else if one andalso inline_rel_expr r1 then
+ fold kk_join (unpack_vect_in_chunks kk 1 arity1 r1) r2
else
kk_project_seq
(kk_intersect (kk_product r1 (full_rel_for_rep res_R)) r2)
@@ -486,24 +492,19 @@
case old_R of
Atom _ => lone_rep_fallback kk (Struct Rs) old_R r
| Struct Rs' =>
- let
- val Rs = filter (not_equal Unit) Rs
- val Rs' = filter (not_equal Unit) Rs'
- in
- if Rs' = Rs then
- r
- else if map card_of_rep Rs' = map card_of_rep Rs then
- let
- val old_arities = map arity_of_rep Rs'
- val old_offsets = offset_list old_arities
- val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities
- in
- fold1 (#kk_product kk)
- (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
- end
- else
- lone_rep_fallback kk (Struct Rs) old_R r
- end
+ if Rs' = Rs then
+ r
+ else if map card_of_rep Rs' = map card_of_rep Rs then
+ let
+ val old_arities = map arity_of_rep Rs'
+ val old_offsets = offset_list old_arities
+ val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities
+ in
+ fold1 (#kk_product kk)
+ (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
+ end
+ else
+ lone_rep_fallback kk (Struct Rs) old_R r
| _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
and vect_from_rel_expr kk k R old_R r =
case old_R of
@@ -519,7 +520,6 @@
(all_singletons_for_rep R1))
else
raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
- | Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r
| Func (R1, R2) =>
fold1 (#kk_product kk)
(map (fn arg_r =>
@@ -535,20 +535,6 @@
func_from_no_opt_rel_expr kk R1 R2 (Vect (dom_card, R2'))
(vect_from_rel_expr kk dom_card R2' (Atom x) r)
end
- | func_from_no_opt_rel_expr kk Unit R2 old_R r =
- (case old_R of
- Vect (_, R') => rel_expr_from_rel_expr kk R2 R' r
- | Func (Unit, R2') => rel_expr_from_rel_expr kk R2 R2' r
- | Func (Atom (1, _), Formula Neut) =>
- (case unopt_rep R2 of
- Atom (2, j0) => atom_from_formula kk j0 (#kk_some kk r)
- | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
- [old_R, Func (Unit, R2)]))
- | Func (R1', R2') =>
- rel_expr_from_rel_expr kk R2 R2' (#kk_project_seq kk r (arity_of_rep R1')
- (arity_of_rep R2'))
- | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
- [old_R, Func (Unit, R2)]))
| func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =
(case old_R of
Vect (k, Atom (2, j0)) =>
@@ -572,9 +558,6 @@
in
#kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
end
- | Func (Unit, (Atom (2, j0))) =>
- #kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1)))
- (full_rel_for_rep R1) (empty_rel_for_rep R1)
| Func (R1', Atom (2, j0)) =>
func_from_no_opt_rel_expr kk R1 (Formula Neut)
(Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1)))
@@ -609,11 +592,6 @@
end
| _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
[old_R, Func (R1, R2)]))
- | Func (Unit, R2') =>
- let val j0 = some_j0 in
- func_from_no_opt_rel_expr kk R1 R2 (Func (Atom (1, j0), R2'))
- (#kk_product kk (KK.Atom j0) r)
- end
| Func (R1', R2') =>
if R1 = R1' andalso R2 = R2' then
r
@@ -819,10 +797,9 @@
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,
kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes
- (constr1 as {const = const1 as (_, T1), delta = delta1,
- epsilon = epsilon1, ...},
- constr2 as {const = const2 as (_, T2), delta = delta2,
- epsilon = epsilon2, ...}) =
+ (({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
+ {const = const2 as (_, T2), delta = delta2, epsilon = epsilon2, ...})
+ : constr_spec * constr_spec) =
let
val dataT = body_type T1
val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
@@ -1093,9 +1070,7 @@
val R2 = rep_of u2
val (dom_R, ran_R) =
case min_rep R1 R2 of
- Func (Unit, R') =>
- (Atom (1, offset_of_type ofs dom_T), R')
- | Func Rp => Rp
+ Func Rp => Rp
| R => (Atom (card_of_domain_from_rep 2 R,
offset_of_type ofs dom_T),
if is_opt_rep R then Opt bool_atom_R else Formula Neut)
@@ -1120,8 +1095,7 @@
end
| Op2 (DefEq, _, _, u1, u2) =>
(case min_rep (rep_of u1) (rep_of u2) of
- Unit => KK.True
- | Formula polar =>
+ Formula polar =>
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
| min_R =>
let
@@ -1139,8 +1113,7 @@
end)
| Op2 (Eq, _, _, u1, u2) =>
(case min_rep (rep_of u1) (rep_of u2) of
- Unit => KK.True
- | Formula polar =>
+ Formula polar =>
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
| min_R =>
if is_opt_rep min_R then
@@ -1420,11 +1393,10 @@
rel_expr_from_rel_expr kk R R' (kk_closure (to_rep R' u1))
end
| Op1 (SingletonSet, _, Func (R1, Opt _), Cst (Unrep, _, _)) =>
- (if R1 = Unit then I else kk_product (full_rel_for_rep R1)) false_atom
+ kk_product (full_rel_for_rep R1) false_atom
| Op1 (SingletonSet, _, R, u1) =>
(case R of
Func (R1, Formula Neut) => to_rep R1 u1
- | Func (Unit, Opt R) => to_guard [u1] R true_atom
| Func (R1, Opt _) =>
single_rel_rel_let kk
(fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
@@ -1670,10 +1642,8 @@
Struct Rs => to_product Rs us
| Vect (k, R) => to_product (replicate k R) us
| Atom (1, j0) =>
- (case filter (not_equal Unit o rep_of) us of
- [] => KK.Atom j0
- | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
- (KK.Atom j0) KK.None)
+ kk_rel_if (kk_some (fold1 kk_product (map to_r us)))
+ (KK.Atom j0) KK.None
| _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
| Construct ([u'], _, _, []) => to_r u'
| Construct (discr_u :: sel_us, _, _, arg_us) =>
@@ -1709,21 +1679,10 @@
and to_atom (x as (k, j0)) u =
case rep_of u of
Formula _ => atom_from_formula kk j0 (to_f u)
- | Unit => if k = 1 then KK.Atom j0
- else raise NUT ("Nitpick_Kodkod.to_atom", [u])
| R => atom_from_rel_expr kk x R (to_r u)
- and to_struct Rs u =
- case rep_of u of
- Unit => full_rel_for_rep (Struct Rs)
- | R' => struct_from_rel_expr kk Rs R' (to_r u)
- and to_vect k R u =
- case rep_of u of
- Unit => full_rel_for_rep (Vect (k, R))
- | R' => vect_from_rel_expr kk k R R' (to_r u)
- and to_func R1 R2 u =
- case rep_of u of
- Unit => full_rel_for_rep (Func (R1, R2))
- | R' => rel_expr_to_func kk R1 R2 R' (to_r u)
+ and to_struct Rs u = struct_from_rel_expr kk Rs (rep_of u) (to_r u)
+ and to_vect k R u = vect_from_rel_expr kk k R (rep_of u) (to_r u)
+ and to_func R1 R2 u = rel_expr_to_func kk R1 R2 (rep_of u) (to_r u)
and to_opt R u =
let val old_R = rep_of u in
if is_opt_rep old_R then
@@ -1758,10 +1717,7 @@
and to_project new_R old_R r j0 =
rel_expr_from_rel_expr kk new_R old_R
(kk_project_seq r j0 (arity_of_rep old_R))
- and to_product Rs us =
- case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of
- [] => raise REP ("Nitpick_Kodkod.to_product", Rs)
- | rs => fold1 kk_product rs
+ and to_product Rs us = fold1 kk_product (map (uncurry to_opt) (Rs ~~ us))
and to_nth_pair_sel n res_T res_R u =
case u of
Tuple (_, _, us) => to_rep res_R (nth us n)
@@ -1783,12 +1739,7 @@
end
val nth_R = nth Rs n
val j0 = if n = 0 then 0 else arity_of_rep (hd Rs)
- in
- case arity_of_rep nth_R of
- 0 => to_guard [u] res_R
- (to_rep res_R (Cst (Unity, res_T, Unit)))
- | _ => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
- end
+ in to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0 end
and to_set_bool_op connective set_oper u1 u2 =
let
val min_R = min_rep (rep_of u1) (rep_of u2)
@@ -1798,8 +1749,6 @@
case min_R of
Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2
| Func (_, Formula Neut) => set_oper r1 r2
- | Func (Unit, Atom (2, j0)) =>
- connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)
| Func (_, Atom _) => set_oper (kk_join r1 true_atom)
(kk_join r2 true_atom)
| _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
@@ -1837,12 +1786,7 @@
raise REP ("Nitpick_Kodkod.to_apply", [R])
| to_apply res_R func_u arg_u =
case unopt_rep (rep_of func_u) of
- Unit =>
- let val j0 = offset_of_type ofs (type_of func_u) in
- to_guard [arg_u] res_R
- (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0))
- end
- | Atom (1, j0) =>
+ Atom (1, j0) =>
to_guard [arg_u] res_R
(rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))
| Atom (k, _) =>
@@ -1861,9 +1805,6 @@
| Func (R, Formula Neut) =>
to_guard [arg_u] res_R (rel_expr_from_formula kk res_R
(kk_subset (to_opt R arg_u) (to_r func_u)))
- | Func (Unit, R2) =>
- to_guard [arg_u] res_R
- (rel_expr_from_rel_expr kk res_R R2 (to_r func_u))
| Func (R1, R2) =>
rel_expr_from_rel_expr kk res_R R2
(kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Aug 04 10:52:29 2010 +0200
@@ -32,8 +32,8 @@
val dest_plain_fun : term -> bool * (term list * term list)
val reconstruct_hol_model :
params -> scope -> (term option * int list) list
- -> (typ option * string list) list -> styp list -> nut list -> nut list
- -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
+ -> (typ option * string list) list -> styp list -> styp list -> nut list
+ -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
-> Pretty.T * bool
val prove_hol_model :
scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
@@ -170,7 +170,7 @@
Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
$ t1 $ t2) =
let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
- Const (@{const_name Pair}, Ts ---> Type (@{type_name Product_Type.prod}, Ts))
+ Const (@{const_name Pair}, Ts ---> Type (@{type_name prod}, Ts))
$ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
end
| unarize_unbox_etc_term (Const (s, T)) =
@@ -185,27 +185,27 @@
| unarize_unbox_etc_term (Abs (s, T, t')) =
Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
-fun factor_out_types (T1 as Type (@{type_name Product_Type.prod}, [T11, T12]))
- (T2 as Type (@{type_name Product_Type.prod}, [T21, T22])) =
+fun factor_out_types (T1 as Type (@{type_name prod}, [T11, T12]))
+ (T2 as Type (@{type_name prod}, [T21, T22])) =
let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
if n1 = n2 then
let
val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
in
- ((Type (@{type_name Product_Type.prod}, [T11, T11']), opt_T12'),
- (Type (@{type_name Product_Type.prod}, [T21, T21']), opt_T22'))
+ ((Type (@{type_name prod}, [T11, T11']), opt_T12'),
+ (Type (@{type_name prod}, [T21, T21']), opt_T22'))
end
else if n1 < n2 then
case factor_out_types T1 T21 of
(p1, (T21', NONE)) => (p1, (T21', SOME T22))
| (p1, (T21', SOME T22')) =>
- (p1, (T21', SOME (Type (@{type_name Product_Type.prod}, [T22', T22]))))
+ (p1, (T21', SOME (Type (@{type_name prod}, [T22', T22]))))
else
swap (factor_out_types T2 T1)
end
- | factor_out_types (Type (@{type_name Product_Type.prod}, [T11, T12])) T2 =
+ | factor_out_types (Type (@{type_name prod}, [T11, T12])) T2 =
((T11, SOME T12), (T2, NONE))
- | factor_out_types T1 (Type (@{type_name Product_Type.prod}, [T21, T22])) =
+ | factor_out_types T1 (Type (@{type_name prod}, [T21, T22])) =
((T1, NONE), (T21, SOME T22))
| factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
@@ -239,7 +239,7 @@
val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
-fun pair_up (Type (@{type_name Product_Type.prod}, [T1', T2']))
+fun pair_up (Type (@{type_name prod}, [T1', T2']))
(t1 as Const (@{const_name Pair},
Type (@{type_name fun},
[_, Type (@{type_name fun}, [_, T1])]))
@@ -287,8 +287,8 @@
and do_term (Type (@{type_name fun}, [T1', T2']))
(Type (@{type_name fun}, [T1, T2])) t =
do_fun T1' T2' T1 T2 t
- | do_term (T' as Type (@{type_name Product_Type.prod}, Ts' as [T1', T2']))
- (Type (@{type_name Product_Type.prod}, [T1, T2]))
+ | do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2']))
+ (Type (@{type_name prod}, [T1, T2]))
(Const (@{const_name Pair}, _) $ t1 $ t2) =
Const (@{const_name Pair}, Ts' ---> T')
$ do_term T1' T1 t1 $ do_term T2' T2 t2
@@ -303,7 +303,7 @@
| truth_const_sort_key @{const False} = "2"
| truth_const_sort_key _ = "1"
-fun mk_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) ts =
+fun mk_tuple (Type (@{type_name prod}, [T1, T2])) ts =
HOLogic.mk_prod (mk_tuple T1 ts,
mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
| mk_tuple _ (t :: _) = t
@@ -463,7 +463,7 @@
signed_string_of_int j ^ " for " ^
string_for_rep (Vect (k1, Atom (k2, 0))))
end
- | term_for_atom seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _ j k =
+ | term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k =
let
val k1 = card_of_type card_assigns T1
val k2 = k div k1
@@ -476,7 +476,6 @@
HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
| term_for_atom _ @{typ bool} _ j _ =
if j = 0 then @{const False} else @{const True}
- | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
| term_for_atom seen T _ j k =
if T = nat_T andalso is_standard_datatype thy stds nat_T then
HOLogic.mk_number nat_T j
@@ -588,11 +587,10 @@
(map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
(map (term_for_rep true seen T2 T2 R o single)
(batch_list (arity_of_rep R) js))
- and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
- | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
+ and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
- | term_for_rep _ seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _
+ | term_for_rep _ seen (Type (@{type_name prod}, [T1, T2])) _
(Struct [R1, R2]) [js] =
let
val arity1 = arity_of_rep R1
@@ -861,8 +859,8 @@
ground_thm_table, ersatz_table, skolems, special_funs,
unrolled_preds, wf_cache, constr_cache},
binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
- formats atomss all_frees free_names sel_names nonsel_names rel_table
- bounds =
+ formats atomss real_frees pseudo_frees free_names sel_names nonsel_names
+ rel_table bounds =
let
val pool = Unsynchronized.ref []
val (wacky_names as (_, base_step_names), ctxt) =
@@ -937,7 +935,7 @@
end
fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
Pretty.block (Pretty.breaks
- (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
+ (pretty_for_type ctxt typ ::
(case typ of
Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
| Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
@@ -977,6 +975,14 @@
(sort_wrt (original_name o nickname_of) names)
else
[]
+ fun free_name_for_term keep_all (x as (s, T)) =
+ case filter (curry (op =) x
+ o pairf nickname_of (uniterize_unarize_unbox_etc_type
+ o type_of)) free_names of
+ [name] => SOME name
+ | [] => if keep_all then SOME (FreeName (s, T, Any)) else NONE
+ | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model.\
+ \free_name_for_term", [Const x])
val (skolem_names, nonskolem_nonsel_names) =
List.partition is_skolem_name nonsel_names
val (eval_names, noneval_nonskolem_nonsel_names) =
@@ -985,17 +991,9 @@
||> filter_out (member (op =) [@{const_name bisim},
@{const_name bisim_iterator_max}]
o nickname_of)
- val free_names =
- map (fn x as (s, T) =>
- case filter (curry (op =) x
- o pairf nickname_of
- (uniterize_unarize_unbox_etc_type o type_of))
- free_names of
- [name] => name
- | [] => FreeName (s, T, Any)
- | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
- [Const x])) all_frees
- val chunks = block_of_names true "Free variable" free_names @
+ ||> append (map_filter (free_name_for_term false) pseudo_frees)
+ val real_free_names = map_filter (free_name_for_term true) real_frees
+ val chunks = block_of_names true "Free variable" real_free_names @
block_of_names true "Skolem constant" skolem_names @
block_of_names true "Evaluated term" eval_names @
block_of_datatypes @ block_of_codatatypes @
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Aug 04 10:52:29 2010 +0200
@@ -9,6 +9,7 @@
sig
type hol_context = Nitpick_HOL.hol_context
+ val trace : bool Unsynchronized.ref
val formulas_monotonic :
hol_context -> bool -> typ -> term list * term list -> bool
val finitize_funs :
@@ -54,9 +55,8 @@
exception MTYPE of string * mtyp list * typ list
exception MTERM of string * mterm list
-val debug_mono = false
-
-fun print_g f = () |> debug_mono ? tracing o f
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if !trace then tracing (msg ()) else ()
val string_for_var = signed_string_of_int
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
@@ -254,7 +254,7 @@
else case T of
Type (@{type_name fun}, [T1, T2]) =>
MFun (fresh_mfun_for_fun_type mdata false T1 T2)
- | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
+ | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
| Type (z as (s, _)) =>
if could_exist_alpha_sub_mtype ctxt alpha_T T then
case AList.lookup (op =) (!datatype_mcache) z of
@@ -402,10 +402,10 @@
[M1, M2], [])
fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
- (print_g (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
- string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
+ (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
+ string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
- NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
+ NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
| SOME (lits, comps) => (lits, comps, sexps))
val add_mtypes_equal = add_mtype_comp Eq
@@ -447,11 +447,11 @@
raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
- (print_g (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
- (case sn of Minus => "concrete" | Plus => "complete") ^
- ".");
+ (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
+ (case sn of Minus => "concrete" | Plus => "complete") ^
+ ".");
case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
- NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
+ NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
| SOME (lits, sexps) => (lits, comps, sexps))
val add_mtype_is_concrete = add_notin_mtype_fv Minus
@@ -493,16 +493,16 @@
subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
fun print_problem lits comps sexps =
- print_g (fn () => "*** Problem:\n" ^
- cat_lines (map string_for_literal lits @
- map string_for_comp comps @
- map string_for_sign_expr sexps))
+ trace_msg (fn () => "*** Problem:\n" ^
+ cat_lines (map string_for_literal lits @
+ map string_for_comp comps @
+ map string_for_sign_expr sexps))
fun print_solution lits =
let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
- print_g (fn () => "*** Solution:\n" ^
- "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
- "-: " ^ commas (map (string_for_var o fst) neg))
+ trace_msg (fn () => "*** Solution:\n" ^
+ "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
+ "-: " ^ commas (map (string_for_var o fst) neg))
end
fun solve max_var (lits, comps, sexps) =
@@ -628,8 +628,8 @@
end
and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
cset)) =
- (print_g (fn () => " \<Gamma> \<turnstile> " ^
- Syntax.string_of_term ctxt t ^ " : _?");
+ (trace_msg (fn () => " \<Gamma> \<turnstile> " ^
+ Syntax.string_of_term ctxt t ^ " : _?");
case t of
Const (x as (s, T)) =>
(case AList.lookup (op =) consts x of
@@ -652,9 +652,9 @@
end
| @{const_name "op ="} => do_equals T accum
| @{const_name The} =>
- (print_g (K "*** The"); raise UNSOLVABLE ())
+ (trace_msg (K "*** The"); raise UNSOLVABLE ())
| @{const_name Eps} =>
- (print_g (K "*** Eps"); raise UNSOLVABLE ())
+ (trace_msg (K "*** Eps"); raise UNSOLVABLE ())
| @{const_name If} =>
do_robust_set_operation (range_type T) accum
|>> curry3 MFun bool_M (S Minus)
@@ -742,7 +742,7 @@
(M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
frees = (x, M) :: frees, consts = consts}, cset))
end) |>> curry MRaw t
- | Var _ => (print_g (K "*** Var"); raise UNSOLVABLE ())
+ | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
| Bound j => (MRaw (t, nth bound_Ms j), accum)
| Abs (s, T, t') =>
(case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
@@ -793,8 +793,8 @@
val M2 = mtype_of_mterm m2
in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
end)
- |> tap (fn (m, _) => print_g (fn () => " \<Gamma> \<turnstile> " ^
- string_for_mterm ctxt m))
+ |> tap (fn (m, _) => trace_msg (fn () => " \<Gamma> \<turnstile> " ^
+ string_for_mterm ctxt m))
in do_term end
fun force_minus_funs 0 _ = I
@@ -848,9 +848,9 @@
Plus => do_term t accum
| Minus => consider_general_equals mdata false x t1 t2 accum
in
- (print_g (fn () => " \<Gamma> \<turnstile> " ^
- Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
- string_for_sign sn ^ "?");
+ (trace_msg (fn () => " \<Gamma> \<turnstile> " ^
+ Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
+ string_for_sign sn ^ "?");
case t of
Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
do_quantifier x s1 T1 t1
@@ -898,9 +898,9 @@
| _ => do_term t accum)
end
|> tap (fn (m, _) =>
- print_g (fn () => "\<Gamma> \<turnstile> " ^
- string_for_mterm ctxt m ^ " : o\<^sup>" ^
- string_for_sign sn))
+ trace_msg (fn () => "\<Gamma> \<turnstile> " ^
+ string_for_mterm ctxt m ^ " : o\<^sup>" ^
+ string_for_sign sn))
in do_formula end
(* The harmless axiom optimization below is somewhat too aggressive in the face
@@ -983,7 +983,7 @@
Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
- print_g (fn () =>
+ trace_msg (fn () =>
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
|> cat_lines)
@@ -994,9 +994,9 @@
fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
(nondef_ts, def_ts) =
let
- val _ = print_g (fn () => "****** " ^ which ^ " analysis: " ^
- string_for_mtype MAlpha ^ " is " ^
- Syntax.string_of_typ ctxt alpha_T)
+ val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
+ string_for_mtype MAlpha ^ " is " ^
+ Syntax.string_of_typ ctxt alpha_T)
val mdata as {max_fresh, constr_mcache, ...} =
initial_mdata hol_ctxt binarize no_harmless alpha_T
val accum = (initial_gamma, ([], [], []))
@@ -1043,8 +1043,8 @@
| (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
Type (if should_finitize T a then @{type_name fin_fun}
else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
- | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) =>
- Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2])
+ | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
+ Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
| (MType _, _) => T
| _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
[M], [T])
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Aug 04 10:52:29 2010 +0200
@@ -7,13 +7,13 @@
signature NITPICK_NUT =
sig
+ type styp = Nitpick_Util.styp
type hol_context = Nitpick_HOL.hol_context
type scope = Nitpick_Scope.scope
type name_pool = Nitpick_Peephole.name_pool
type rep = Nitpick_Rep.rep
datatype cst =
- Unity |
False |
True |
Iden |
@@ -104,7 +104,8 @@
val nut_from_term : hol_context -> op2 -> term -> nut
val is_fully_representable_set : nut -> bool
val choose_reps_for_free_vars :
- scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
+ scope -> styp list -> nut list -> rep NameTable.table
+ -> nut list * rep NameTable.table
val choose_reps_for_consts :
scope -> bool -> nut list -> rep NameTable.table
-> nut list * rep NameTable.table
@@ -130,7 +131,6 @@
structure KK = Kodkod
datatype cst =
- Unity |
False |
True |
Iden |
@@ -200,8 +200,7 @@
exception NUT of string * nut list
-fun string_for_cst Unity = "Unity"
- | string_for_cst False = "False"
+fun string_for_cst False = "False"
| string_for_cst True = "True"
| string_for_cst Iden = "Iden"
| string_for_cst (Num j) = "Num " ^ signed_string_of_int j
@@ -427,7 +426,7 @@
let val res_T = snd (HOLogic.dest_prodT T) in
(res_T, Const (@{const_name snd}, T --> res_T) $ t)
end
-fun factorize (z as (Type (@{type_name Product_Type.prod}, _), _)) =
+fun factorize (z as (Type (@{type_name prod}, _), _)) =
maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
@@ -532,7 +531,6 @@
sub t1, sub_abs s T' t2)
| (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
sub (t0 $ t1 $ eta_expand Ts t2 1)
- | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
| (Const (@{const_name Pair}, T), [t1, t2]) =>
Tuple (nth_range_type 2 T, Any, map sub [t1, t2])
| (Const (@{const_name fst}, T), [t1]) =>
@@ -671,9 +669,12 @@
Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
end
-fun choose_rep_for_free_var scope v (vs, table) =
+fun choose_rep_for_free_var scope pseudo_frees v (vs, table) =
let
- val R = best_non_opt_set_rep_for_type scope (type_of v)
+ val R = (if exists (curry (op =) (nickname_of v) o fst) pseudo_frees then
+ best_opt_set_rep_for_type
+ else
+ best_non_opt_set_rep_for_type) scope (type_of v)
val v = modify_name_rep v R
in (v :: vs, NameTable.update (v, R) table) end
fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
@@ -701,8 +702,8 @@
val v = modify_name_rep v R
in (v :: vs, NameTable.update (v, R) table) end
-fun choose_reps_for_free_vars scope vs table =
- fold (choose_rep_for_free_var scope) vs ([], table)
+fun choose_reps_for_free_vars scope pseudo_frees vs table =
+ fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
fun choose_reps_for_consts scope all_exact vs table =
fold (choose_rep_for_const scope all_exact) vs ([], table)
@@ -741,8 +742,7 @@
(not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
case u of
Cst (Num _, _, _) => true
- | Cst (cst, T, _) =>
- cst = Suc orelse (body_type T = nat_T andalso cst = Add)
+ | Cst (cst, T, _) => body_type T = nat_T andalso (cst = Suc orelse cst = Add)
| Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]
| Op3 (If, _, _, u1, u2, u3) =>
not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3]
@@ -750,8 +750,6 @@
| Construct (_, _, _, us) => forall is_constructive us
| _ => false
-fun optimize_unit u =
- if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u
fun unknown_boolean T R =
Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
T, R)
@@ -764,7 +762,6 @@
else
raise SAME ())
handle SAME () => Op1 (oper, T, R, u1))
- |> optimize_unit
fun s_op2 oper T R u1 u2 =
((case oper of
All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2
@@ -806,7 +803,6 @@
raise SAME ()
| _ => raise SAME ())
handle SAME () => Op2 (oper, T, R, u1, u2))
- |> optimize_unit
fun s_op3 oper T R u1 u2 u3 =
((case oper of
Let =>
@@ -816,13 +812,11 @@
raise SAME ()
| _ => raise SAME ())
handle SAME () => Op3 (oper, T, R, u1, u2, u3))
- |> optimize_unit
fun s_tuple T R us =
- (if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us))
- |> optimize_unit
+ if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)
fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
- | untuple f u = if rep_of u = Unit then [] else [f u]
+ | untuple f u = [f u]
fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
unsound table def =
@@ -851,17 +845,14 @@
Cst (if is_twos_complement_representable bits j then Num j
else Unrep, T, best_opt_set_rep_for_type scope T)
else
- (case spec_of_type scope T of
- (1, j0) => if j = 0 then Cst (Unity, T, Unit)
- else Cst (Unrep, T, Opt (Atom (1, j0)))
- | (k, j0) =>
- let
- val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
- else j < k)
- in
- if ok then Cst (Num j, T, Atom (k, j0))
- else Cst (Unrep, T, Opt (Atom (k, j0)))
- end)
+ let
+ val (k, j0) = spec_of_type scope T
+ val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
+ else j < k)
+ in
+ if ok then Cst (Num j, T, Atom (k, j0))
+ else Cst (Unrep, T, Opt (Atom (k, j0)))
+ end
| Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
let val R = Atom (spec_of_type scope T1) in
Cst (Suc, T, Func (R, Opt R))
@@ -1031,8 +1022,7 @@
in s_op2 Apply T ran_R u1 u2 end
| Op2 (Lambda, T, _, u1, u2) =>
(case best_set_rep_for_type scope T of
- Unit => Cst (Unity, T, Unit)
- | R as Func (R1, _) =>
+ R as Func (R1, _) =>
let
val table' = NameTable.update (u1, R1) table
val u1' = aux table' false Neut u1
@@ -1145,8 +1135,8 @@
let
val Rs = map (best_one_rep_for_type scope o type_of) us
val us = map sub us
- val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs
- val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R
+ val R' = Struct Rs
+ |> exists (is_opt_rep o rep_of) us ? opt_rep ofs T
in s_tuple T R' us end
| Construct (us', T, _, us) =>
let
@@ -1166,7 +1156,6 @@
s_op1 Cast (type_of u) (Formula polar) u
end
end
- |> optimize_unit
in aux table def Pos end
fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
@@ -1199,7 +1188,7 @@
val w = constr (j, type_of v, rep_of v)
in (w :: ws, pool, NameTable.update (v, w) table) end
-fun shape_tuple (T as Type (@{type_name Product_Type.prod}, [T1, T2])) (R as Struct [R1, R2])
+fun shape_tuple (T as Type (@{type_name prod}, [T1, T2])) (R as Struct [R1, R2])
us =
let val arity1 = arity_of_rep R1 in
Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
@@ -1209,7 +1198,6 @@
Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
| shape_tuple T _ [u] =
if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
- | shape_tuple T Unit [] = Cst (Unity, T, Unit)
| shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
fun rename_n_ary_var rename_free v (ws, pool, table) =
@@ -1255,7 +1243,6 @@
fun rename_free_vars vs pool table =
let
- val vs = filter (not_equal Unit o rep_of) vs
val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table)
in (rev vs, pool, table) end
@@ -1276,7 +1263,7 @@
Op2 (oper, T, R, rename_vars_in_nut pool table u1,
rename_vars_in_nut pool table u2)
| Op3 (Let, T, R, u1, u2, u3) =>
- if rep_of u2 = Unit orelse inline_nut u2 then
+ if inline_nut u2 then
let
val u2 = rename_vars_in_nut pool table u2
val table = NameTable.update (u1, u2) table
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Aug 04 10:52:29 2010 +0200
@@ -8,9 +8,9 @@
signature NITPICK_PREPROC =
sig
type hol_context = Nitpick_HOL.hol_context
- val preprocess_term :
+ val preprocess_formulas :
hol_context -> (typ option * bool option) list
- -> (typ option * bool option) list -> term
+ -> (typ option * bool option) list -> term list -> term
-> term list * term list * bool * bool * bool
end;
@@ -132,8 +132,8 @@
let
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
Type (@{type_name fun}, map box_relational_operator_type Ts)
- | box_relational_operator_type (Type (@{type_name Product_Type.prod}, Ts)) =
- Type (@{type_name Product_Type.prod}, map (box_type hol_ctxt InPair) Ts)
+ | box_relational_operator_type (Type (@{type_name prod}, Ts)) =
+ Type (@{type_name prod}, map (box_type hol_ctxt InPair) Ts)
| box_relational_operator_type T = T
fun add_boxed_types_for_var (z as (_, T)) (T', t') =
case t' of
@@ -583,11 +583,9 @@
handle SAME () =>
Const (quant_s, quant_T)
$ Abs (abs_s, abs_T,
- if is_higher_order_type abs_T then
- t
- else
- aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
- skolemizable polar t)
+ aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
+ (skolemizable andalso
+ not (is_higher_order_type abs_T)) polar t)
in
case t of
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
@@ -642,8 +640,8 @@
else
Const x
| t1 $ t2 =>
- s_betapply Ts (aux ss Ts [] false polar t1,
- aux ss Ts [] skolemizable Neut t2)
+ s_betapply Ts (aux ss Ts js false polar t1,
+ aux ss Ts js false Neut t2)
| Abs (s, T, t1) =>
Abs (s, T, aux ss Ts (incrs js) skolemizable polar t1)
| _ => t
@@ -728,6 +726,10 @@
val bound_var_prefix = "b"
+fun special_fun_aconv ((x1, js1, ts1), (x2, js2, ts2)) =
+ x1 = x2 andalso js1 = js2 andalso length ts1 = length ts2 andalso
+ forall (op aconv) (ts1 ~~ ts2)
+
fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table,
special_funs, ...}) depth t =
if not specialize orelse depth > special_max_depth then
@@ -769,7 +771,7 @@
(map var_for_bound_no (index_seq 0 (length Ts))))
fixed_args
in
- case AList.lookup (op =) (!special_funs)
+ case AList.lookup special_fun_aconv (!special_funs)
(x, fixed_js, fixed_args_in_axiom) of
SOME x' => list_comb (Const x', extra_args)
| NONE =>
@@ -819,25 +821,25 @@
apsnd (pairself (cons v))
end) (max_j downto 0) ([], ([], []))
in
- Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
+ Logic.list_implies (eqs |> filter_out (op aconv) |> distinct (op =)
|> map Logic.mk_equals,
Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
list_comb (Const x2, bounds2 @ args2)))
- |> close_form (* TODO: needed? *)
end
-fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
+fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) ts =
let
val groups =
!special_funs
|> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
|> AList.group (op =)
|> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
- |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
+ |> map (fn (x, zs) =>
+ (x, zs |> member (op =) ts (Const x) ? cons ([], [], x)))
fun generality (js, _, _) = ~(length js)
fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
- x1 <> x2 andalso OrdList.subset (prod_ord int_ord Term_Ord.term_ord)
- (j2 ~~ t2, j1 ~~ t1)
+ x1 <> x2 andalso length j2 < length j1 andalso
+ OrdList.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
fun do_pass_1 _ [] [_] [_] = I
| do_pass_1 T skipped _ [] = do_pass_2 T skipped
| do_pass_1 T skipped all (z :: zs) =
@@ -853,6 +855,25 @@
(** Axiom selection **)
+fun defined_free_by_assumption t =
+ let
+ fun do_equals x def =
+ if exists_subterm (curry (op aconv) (Free x)) def then NONE else SOME x
+ in
+ case t of
+ Const (@{const_name "=="}, _) $ Free x $ def => do_equals x def
+ | @{const Trueprop} $ (Const (@{const_name "=="}, _) $ Free x $ def) =>
+ do_equals x def
+ | _ => NONE
+ end
+
+fun assumption_exclusively_defines_free assm_ts t =
+ case defined_free_by_assumption t of
+ SOME x =>
+ length (filter ((fn SOME x' => x = x' | NONE => false)
+ o defined_free_by_assumption) assm_ts) = 1
+ | NONE => false
+
fun all_table_entries table = Symtab.fold (append o snd) table []
fun extra_table table s = Symtab.make [(s, all_table_entries table)]
@@ -867,20 +888,23 @@
fun axioms_for_term
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
fast_descrs, evals, def_table, nondef_table,
- choice_spec_table, user_nondefs, ...}) t =
+ choice_spec_table, user_nondefs, ...}) assm_ts neg_t =
let
+ val (def_assm_ts, nondef_assm_ts) =
+ List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
+ val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts
type accumulator = styp list * (term list * term list)
- fun add_axiom get app depth t (accum as (xs, axs)) =
+ fun add_axiom get app depth t (accum as (seen, axs)) =
let
val t = t |> unfold_defs_in_term hol_ctxt
- |> skolemize_term_and_more hol_ctxt ~1
+ |> skolemize_term_and_more hol_ctxt ~1 (*### why ~1? *)
in
if is_trivial_equation t then
accum
else
let val t' = t |> specialize_consts_in_term hol_ctxt depth in
if exists (member (op aconv) (get axs)) [t, t'] then accum
- else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
+ else add_axioms_for_term (depth + 1) t' (seen, app (cons t') axs)
end
end
and add_def_axiom depth = add_axiom fst apfst depth
@@ -891,15 +915,15 @@
and add_eq_axiom depth t =
(if is_constr_pattern_formula ctxt t then add_def_axiom
else add_nondef_axiom) depth t
- and add_axioms_for_term depth t (accum as (xs, axs)) =
+ and add_axioms_for_term depth t (accum as (seen, axs)) =
case t of
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
| Const (x as (s, T)) =>
- (if member (op =) xs x orelse
+ (if member (op aconv) seen t orelse
is_built_in_const thy stds fast_descrs x then
accum
else
- let val accum = (x :: xs, axs) in
+ let val accum = (t :: seen, axs) in
if depth > axioms_max_depth then
raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
\add_axioms_for_term",
@@ -962,7 +986,13 @@
(nondef_props_for_const thy false nondef_table x)
end)
|> add_axioms_for_type depth T
- | Free (_, T) => add_axioms_for_type depth T accum
+ | Free (x as (_, T)) =>
+ (if member (op aconv) seen t then
+ accum
+ else case AList.lookup (op =) def_assm_table x of
+ SOME t => add_def_axiom depth t accum
+ | NONE => accum)
+ |> add_axioms_for_type depth T
| Var (_, T) => add_axioms_for_type depth T accum
| Bound _ => accum
| Abs (_, T, t) => accum |> add_axioms_for_term depth t
@@ -970,10 +1000,9 @@
and add_axioms_for_type depth T =
case T of
Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
- | Type (@{type_name Product_Type.prod}, Ts) => fold (add_axioms_for_type depth) Ts
+ | Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts
| @{typ prop} => I
| @{typ bool} => I
- | @{typ unit} => I
| TFree (_, S) => add_axioms_for_sort depth T S
| TVar (_, S) => add_axioms_for_sort depth T S
| Type (z as (_, Ts)) =>
@@ -1007,15 +1036,18 @@
List.partition (null o Term.hidden_polymorphism) user_nondefs
val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
evals
- val (xs, (defs, nondefs)) =
- ([], ([], [])) |> add_axioms_for_term 1 t
- |> fold_rev (add_def_axiom 1) eval_axioms
- |> user_axioms = SOME true
- ? fold (add_nondef_axiom 1) mono_user_nondefs
- val defs = defs @ special_congruence_axioms hol_ctxt xs
+ val (seen, (defs, nondefs)) =
+ ([], ([], []))
+ |> add_axioms_for_term 1 neg_t
+ |> fold_rev (add_nondef_axiom 1) nondef_assm_ts
+ |> fold_rev (add_def_axiom 1) eval_axioms
+ |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs
+ val defs = defs @ special_congruence_axioms hol_ctxt seen
val got_all_mono_user_axioms =
(user_axioms = SOME true orelse null mono_user_nondefs)
- in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end
+ in
+ (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs)
+ end
(** Simplification of constructor/selector terms **)
@@ -1234,15 +1266,16 @@
val max_skolem_depth = 3
-fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
- boxes, ...}) finitizes monos t =
+fun preprocess_formulas
+ (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
+ ...}) finitizes monos assm_ts neg_t =
let
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
- t |> unfold_defs_in_term hol_ctxt
- |> close_form
- |> skolemize_term_and_more hol_ctxt max_skolem_depth
- |> specialize_consts_in_term hol_ctxt 0
- |> axioms_for_term hol_ctxt
+ neg_t |> unfold_defs_in_term hol_ctxt
+ |> close_form
+ |> skolemize_term_and_more hol_ctxt max_skolem_depth
+ |> specialize_consts_in_term hol_ctxt 0
+ |> axioms_for_term hol_ctxt assm_ts
val binarize =
is_standard_datatype thy stds nat_T andalso
case binary_ints of
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Wed Aug 04 10:52:29 2010 +0200
@@ -13,7 +13,6 @@
datatype rep =
Any |
Formula of polarity |
- Unit |
Atom of int * int |
Struct of rep list |
Vect of int * rep |
@@ -68,7 +67,6 @@
datatype rep =
Any |
Formula of polarity |
- Unit |
Atom of int * int |
Struct of rep list |
Vect of int * rep |
@@ -88,7 +86,6 @@
end
and string_for_rep Any = "X"
| string_for_rep (Formula polar) = "F" ^ string_for_polarity polar
- | string_for_rep Unit = "U"
| string_for_rep (Atom (k, j0)) =
"A" ^ string_of_int k ^ (if j0 = 0 then "" else "@" ^ string_of_int j0)
| string_for_rep (Struct rs) = "[" ^ commas (map string_for_rep rs) ^ "]"
@@ -108,7 +105,6 @@
fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any])
| card_of_rep (Formula _) = 2
- | card_of_rep Unit = 1
| card_of_rep (Atom (k, _)) = k
| card_of_rep (Struct rs) = Integer.prod (map card_of_rep rs)
| card_of_rep (Vect (k, R)) = reasonable_power (card_of_rep R) k
@@ -117,7 +113,6 @@
| card_of_rep (Opt R) = card_of_rep R
fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any])
| arity_of_rep (Formula _) = 0
- | arity_of_rep Unit = 0
| arity_of_rep (Atom _) = 1
| arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs)
| arity_of_rep (Vect (k, R)) = k * arity_of_rep R
@@ -126,7 +121,6 @@
fun min_univ_card_of_rep Any =
raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any])
| min_univ_card_of_rep (Formula _) = 0
- | min_univ_card_of_rep Unit = 0
| min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1
| min_univ_card_of_rep (Struct Rs) =
fold Integer.max (map min_univ_card_of_rep Rs) 0
@@ -135,8 +129,7 @@
Int.max (min_univ_card_of_rep R1, min_univ_card_of_rep R2)
| min_univ_card_of_rep (Opt R) = min_univ_card_of_rep R
-fun is_one_rep Unit = true
- | is_one_rep (Atom _) = true
+fun is_one_rep (Atom _) = true
| is_one_rep (Struct _) = true
| is_one_rep (Vect _) = true
| is_one_rep _ = false
@@ -145,8 +138,7 @@
fun dest_Func (Func z) = z
| dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
-fun lazy_range_rep _ _ _ Unit = Unit
- | lazy_range_rep _ _ _ (Vect (_, R)) = R
+fun lazy_range_rep _ _ _ (Vect (_, R)) = R
| lazy_range_rep _ _ _ (Func (_, R2)) = R2
| lazy_range_rep ofs T ran_card (Opt R) =
Opt (lazy_range_rep ofs T ran_card R)
@@ -201,8 +193,6 @@
Formula (min_polarity polar1 polar2)
| min_rep (Formula polar) _ = Formula polar
| min_rep _ (Formula polar) = Formula polar
- | min_rep Unit _ = Unit
- | min_rep _ Unit = Unit
| min_rep (Atom x) _ = Atom x
| min_rep _ (Atom x) = Atom x
| min_rep (Struct Rs1) (Struct Rs2) = Struct (min_reps Rs1 Rs2)
@@ -231,8 +221,7 @@
fun card_of_domain_from_rep ran_card R =
case R of
- Unit => 1
- | Atom (k, _) => exact_log ran_card k
+ Atom (k, _) => exact_log ran_card k
| Vect (k, _) => k
| Func (R1, _) => card_of_rep R1
| Opt R => card_of_domain_from_rep ran_card R
@@ -246,24 +235,12 @@
fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
(Type (@{type_name fun}, [T1, T2])) =
- (case best_one_rep_for_type scope T2 of
- Unit => Unit
- | R2 => Vect (card_of_type card_assigns T1, R2))
- | best_one_rep_for_type scope (Type (@{type_name Product_Type.prod}, [T1, T2])) =
- (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
- (Unit, Unit) => Unit
- | (R1, R2) => Struct [R1, R2])
+ Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2))
+ | best_one_rep_for_type scope (Type (@{type_name prod}, Ts)) =
+ Struct (map (best_one_rep_for_type scope) Ts)
| best_one_rep_for_type {card_assigns, datatypes, ofs, ...} T =
- (case card_of_type card_assigns T of
- 1 => if is_some (datatype_spec datatypes T) orelse
- is_iterator_type T then
- Atom (1, offset_of_type ofs T)
- else
- Unit
- | k => Atom (k, offset_of_type ofs T))
+ Atom (card_of_type card_assigns T, offset_of_type ofs T)
-(* Datatypes are never represented by Unit, because it would confuse
- "nfa_transitions_for_ctor". *)
fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
| best_opt_set_rep_for_type (scope as {ofs, ...}) T =
@@ -272,10 +249,7 @@
(Type (@{type_name fun}, [T1, T2])) =
(case (best_one_rep_for_type scope T1,
best_non_opt_set_rep_for_type scope T2) of
- (_, Unit) => Unit
- | (Unit, Atom (2, _)) =>
- Func (Atom (1, offset_of_type ofs T1), Formula Neut)
- | (R1, Atom (2, _)) => Func (R1, Formula Neut)
+ (R1, Atom (2, _)) => Func (R1, Formula Neut)
| z => Func z)
| best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
fun best_set_rep_for_type (scope as {datatypes, ...}) T =
@@ -290,7 +264,6 @@
fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any])
| atom_schema_of_rep (Formula _) = []
- | atom_schema_of_rep Unit = []
| atom_schema_of_rep (Atom x) = [x]
| atom_schema_of_rep (Struct Rs) = atom_schema_of_reps Rs
| atom_schema_of_rep (Vect (k, R)) = replicate_list k (atom_schema_of_rep R)
@@ -300,9 +273,8 @@
and atom_schema_of_reps Rs = maps atom_schema_of_rep Rs
fun type_schema_of_rep _ (Formula _) = []
- | type_schema_of_rep _ Unit = []
| type_schema_of_rep T (Atom _) = [T]
- | type_schema_of_rep (Type (@{type_name Product_Type.prod}, [T1, T2])) (Struct [R1, R2]) =
+ | type_schema_of_rep (Type (@{type_name prod}, [T1, T2])) (Struct [R1, R2]) =
type_schema_of_reps [T1, T2] [R1, R2]
| type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
replicate_list k (type_schema_of_rep T2 R)
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Aug 04 10:52:29 2010 +0200
@@ -114,7 +114,7 @@
is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
| is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
- | is_complete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
+ | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) =
forall (is_complete_type dtypes facto) Ts
| is_complete_type dtypes facto T =
not (is_integer_like_type T) andalso not (is_bit_type T) andalso
@@ -124,7 +124,7 @@
is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
| is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
is_concrete_type dtypes facto T2
- | is_concrete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
+ | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
forall (is_concrete_type dtypes facto) Ts
| is_concrete_type dtypes facto T =
fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
@@ -141,7 +141,7 @@
(card_of_type card_assigns T
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
-fun quintuple_for_scope quote
+fun quintuple_for_scope code_type code_term code_string
({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
datatypes, ...} : scope) =
let
@@ -154,26 +154,26 @@
card_assigns
|> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst)
val cards =
- map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
- string_of_int k)
+ map (fn (T, k) =>
+ [code_type ctxt T, code_string (" = " ^ string_of_int k)])
fun maxes () =
maps (map_filter
(fn {const, explicit_max, ...} =>
if explicit_max < 0 then
NONE
else
- SOME (Syntax.string_of_term ctxt (Const const) ^ " = " ^
- string_of_int explicit_max))
+ SOME [code_term ctxt (Const const),
+ code_string (" = " ^ string_of_int explicit_max)])
o #constrs) datatypes
fun iters () =
map (fn (T, k) =>
- quote (Syntax.string_of_term ctxt
- (Const (const_for_iterator_type T))) ^ " = " ^
- string_of_int (k - 1)) iter_assigns
+ [code_term ctxt (Const (const_for_iterator_type T)),
+ code_string (" = " ^ string_of_int (k - 1))]) iter_assigns
fun miscs () =
- (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
+ (if bits = 0 then []
+ else [code_string ("bits = " ^ string_of_int bits)]) @
(if bisim_depth < 0 andalso forall (not o #co) datatypes then []
- else ["bisim_depth = " ^ signed_string_of_int bisim_depth])
+ else [code_string ("bisim_depth = " ^ signed_string_of_int bisim_depth)])
in
setmp_show_all_types
(fn () => (cards primary_card_assigns, cards secondary_card_assigns,
@@ -182,31 +182,33 @@
fun pretties_for_scope scope verbose =
let
- val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
- quintuple_for_scope maybe_quote scope
- val ss = map (prefix "card ") primary_cards @
- (if verbose then
- map (prefix "card ") secondary_cards @
- map (prefix "max ") maxes @
- map (prefix "iter ") iters @
- bisim_depths
- else
- [])
+ fun standard_blocks s = map (Pretty.block o cons (Pretty.str (s ^ " ")))
+ val (primary_cards, secondary_cards, maxes, iters, miscs) =
+ quintuple_for_scope (pretty_maybe_quote oo pretty_for_type)
+ (pretty_maybe_quote oo Syntax.pretty_term)
+ Pretty.str scope
in
- if null ss then []
- else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
+ standard_blocks "card" primary_cards @
+ (if verbose then
+ standard_blocks "card" secondary_cards @
+ standard_blocks "max" maxes @
+ standard_blocks "iter" iters @
+ miscs
+ else
+ [])
+ |> pretty_serial_commas "and"
end
fun multiline_string_for_scope scope =
let
- val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
- quintuple_for_scope I scope
+ val (primary_cards, secondary_cards, maxes, iters, miscs) =
+ quintuple_for_scope Syntax.string_of_typ Syntax.string_of_term I scope
val cards = primary_cards @ secondary_cards
in
- case (if null cards then [] else ["card: " ^ commas cards]) @
- (if null maxes then [] else ["max: " ^ commas maxes]) @
- (if null iters then [] else ["iter: " ^ commas iters]) @
- bisim_depths of
+ case (if null cards then [] else ["card: " ^ commas (map implode cards)]) @
+ (if null maxes then [] else ["max: " ^ commas (map implode maxes)]) @
+ (if null iters then [] else ["iter: " ^ commas (map implode iters)]) @
+ miscs of
[] => "empty"
| lines => space_implode "\n" lines
end
@@ -272,27 +274,20 @@
in mono_block :: nonmono_blocks end
val sync_threshold = 5
+val linearity = 5
-fun all_combinations_ordered_smartly ks =
+val all_combinations_ordered_smartly =
let
- fun cost_with_monos [] = 0
- | cost_with_monos (k :: ks) =
+ fun cost [] = 0
+ | cost [k] = k
+ | cost (k :: ks) =
if k < sync_threshold andalso forall (curry (op =) k) ks then
k - sync_threshold
else
- k * (k + 1) div 2 + Integer.sum ks
- fun cost_without_monos [] = 0
- | cost_without_monos [k] = k
- | cost_without_monos (_ :: k :: ks) =
- if k < sync_threshold andalso forall (curry (op =) k) ks then
- k - sync_threshold
- else
- Integer.sum (k :: ks)
+ k :: ks |> map (fn k => (k + linearity) * (k + linearity))
+ |> Integer.sum
in
- ks |> all_combinations
- |> map (`(if fst (hd ks) > 1 then cost_with_monos
- else cost_without_monos))
- |> sort (int_ord o pairself fst) |> map snd
+ all_combinations #> map (`cost) #> sort (int_ord o pairself fst) #> map snd
end
fun is_self_recursive_constr_type T =
@@ -387,7 +382,7 @@
fun domain_card max card_assigns =
Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types
-fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
+fun add_constr_spec (card_assigns, max_assigns) acyclic card sum_dom_cards
num_self_recs num_non_self_recs (self_rec, x as (_, T))
constrs =
let
@@ -398,7 +393,7 @@
let val delta = next_delta () in
{delta = delta, epsilon = delta, exclusive = true, total = false}
end
- else if not co andalso num_self_recs > 0 then
+ else if num_self_recs > 0 then
(if num_self_recs = 1 andalso num_non_self_recs = 1 then
if self_rec then
case constrs of
@@ -407,7 +402,7 @@
| _ => raise SAME ()
else
if domain_card 2 card_assigns T = 1 then
- {delta = 0, epsilon = 1, exclusive = true, total = true}
+ {delta = 0, epsilon = 1, exclusive = acyclic, total = acyclic}
else
raise SAME ()
else
@@ -457,8 +452,8 @@
fun sum_dom_cards max =
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)
+ fold_rev (add_constr_spec desc (not co andalso standard) card
+ sum_dom_cards num_self_recs num_non_self_recs)
(sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
{typ = T, card = card, co = co, standard = standard, self_rec = self_rec,
@@ -493,8 +488,8 @@
| repair_cards_assigns_wrt_boxing_etc thy Ts ((NONE, ks) :: cards_assigns) =
(NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
-val max_scopes = 4096
-val distinct_threshold = 512
+val max_scopes = 5000
+val distinct_threshold = 1000
fun all_scopes (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Aug 04 10:52:29 2010 +0200
@@ -23,10 +23,8 @@
fun cast_to_rep R u = Op1 (Cast, type_of u, R, u)
-val unit_T = @{typ unit}
val dummy_T = @{typ 'a}
-val unity = Cst (Unity, unit_T, Unit)
val atom1_v1 = FreeName ("atom1_v1", dummy_T, Atom (1, 0))
val atom2_v1 = FreeName ("atom2_v1", dummy_T, Atom (2, 0))
val atom6_v1 = FreeName ("atom6_v1", dummy_T, Atom (6, 0))
@@ -36,19 +34,14 @@
val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
val struct_atom1_atom1_v1 =
FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])
-val struct_atom1_unit_v1 =
- FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Unit])
-val struct_unit_atom1_v1 =
- FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Unit, Atom (1, 0)])
(*
- Formula Unit Atom Struct Vect Func
- Formula X N/A X X N/A N/A
- Unit N/A N/A N/A N/A N/A N/A
- Atom X N/A X X X X
- Struct N/A N/A X X N/A N/A
- Vect N/A N/A X N/A X X
- Func N/A N/A X N/A X X
+ Formula Atom Struct Vect Func
+ Formula X X X N/A N/A
+ Atom X X X X X
+ Struct N/A X X N/A N/A
+ Vect N/A X N/A X X
+ Func N/A X N/A X X
*)
val tests =
@@ -77,22 +70,6 @@
Struct [Atom (2, 0), Atom (3, 0)]])
atom24_v1),
atom24_v1)),
- ("rep_conversion_struct_struct_4",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Struct [Atom (24, 0), Unit])
- (cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)]) atom24_v1),
- atom24_v1)),
- ("rep_conversion_struct_struct_5",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)])
- (cast_to_rep (Struct [Atom (24, 0), Unit]) atom24_v1),
- atom24_v1)),
- ("rep_conversion_struct_struct_6",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)])
- (cast_to_rep (Struct [Atom (1, 0), Unit])
- (cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1)),
- atom1_v1)),
("rep_conversion_vect_vect_1",
Op2 (Eq, bool_T, Formula Neut,
cast_to_rep (Atom (16, 0))
@@ -133,50 +110,10 @@
Struct [Atom (2, 0), Atom (3, 0)]))
atom36_v1)),
atom36_v1)),
- ("rep_conversion_func_func_3",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (36, 0))
- (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
- (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
- atom36_v1)),
- ("rep_conversion_func_func_4",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (36, 0))
- (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
- (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
- atom36_v1)),
- atom36_v1)),
- ("rep_conversion_func_func_5",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (36, 0))
- (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
- (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
- atom36_v1)),
- ("rep_conversion_func_func_6",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (36, 0))
- (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
- (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
- atom36_v1)),
- atom36_v1)),
- ("rep_conversion_func_func_7",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (2, 0))
- (cast_to_rep (Func (Unit, Atom (2, 0)))
- (cast_to_rep (Func (Atom (1, 0), Formula Neut)) atom2_v1)),
- atom2_v1)),
- ("rep_conversion_func_func_8",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (2, 0))
- (cast_to_rep (Func (Atom (1, 0), Formula Neut))
- (cast_to_rep (Func (Unit, Atom (2, 0))) atom2_v1)),
- atom2_v1)),
("rep_conversion_atom_formula_atom",
Op2 (Eq, bool_T, Formula Neut,
cast_to_rep (Atom (2, 0)) (cast_to_rep (Formula Neut) atom2_v1),
atom2_v1)),
- ("rep_conversion_unit_atom",
- Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (1, 0)) unity, unity)),
("rep_conversion_atom_struct_atom1",
Op2 (Eq, bool_T, Formula Neut,
cast_to_rep (Atom (6, 0))
@@ -188,17 +125,6 @@
(cast_to_rep (Struct [Struct [Atom (3, 0), Atom (4, 0)],
Atom (2, 0)]) atom24_v1),
atom24_v1)),
- ("rep_conversion_atom_struct_atom_3",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (6, 0))
- (cast_to_rep (Struct [Atom (6, 0), Unit]) atom6_v1),
- atom6_v1)),
- ("rep_conversion_atom_struct_atom_4",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (6, 0))
- (cast_to_rep (Struct [Struct [Atom (3, 0), Unit], Atom (2, 0)])
- atom6_v1),
- atom6_v1)),
("rep_conversion_atom_vect_func_atom_1",
Op2 (Eq, bool_T, Formula Neut,
cast_to_rep (Atom (16, 0))
@@ -217,18 +143,6 @@
(cast_to_rep (Vect (4, Atom (2, 0)))
(cast_to_rep (Func (Atom (4, 0), Formula Neut)) atom16_v1)),
atom16_v1)),
- ("rep_conversion_atom_vect_func_atom_4",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (16, 0))
- (cast_to_rep (Vect (1, Atom (16, 0)))
- (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
- atom16_v1)),
- ("rep_conversion_atom_vect_func_atom_5",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (16, 0))
- (cast_to_rep (Vect (1, Atom (16, 0)))
- (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
- atom16_v1)),
("rep_conversion_atom_func_vect_atom_1",
Op2 (Eq, bool_T, Formula Neut,
cast_to_rep (Atom (16, 0))
@@ -247,12 +161,6 @@
(cast_to_rep (Func (Atom (4, 0), Formula Neut))
(cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
atom16_v1)),
- ("rep_conversion_atom_func_vect_atom_4",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Atom (16, 0))
- (cast_to_rep (Func (Unit, Atom (16, 0)))
- (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
- atom16_v1)),
("rep_conversion_atom_func_vect_atom_5",
Op2 (Eq, bool_T, Formula Neut,
cast_to_rep (Atom (16, 0))
@@ -274,23 +182,7 @@
("rep_conversion_struct_atom1_1",
Op2 (Eq, bool_T, Formula Neut,
cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)]) atom1_v1,
- struct_atom1_atom1_v1)),
- ("rep_conversion_struct_atom1_2",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Struct [Atom (1, 0), Unit]) atom1_v1,
- struct_atom1_unit_v1)),
- ("rep_conversion_struct_atom1_3",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1,
- struct_unit_atom1_v1))
-(*
- ("rep_conversion_struct_formula_struct_1",
- Op2 (Eq, bool_T, Formula Neut,
- cast_to_rep (Struct [Atom (2, 0), Unit])
- (cast_to_rep (Formula Neut) struct_atom_2_unit_v1),
- struct_atom_2_unit_v1))
-*)
- ]
+ struct_atom1_atom1_v1))]
fun problem_for_nut ctxt (name, u) =
let
@@ -318,9 +210,15 @@
end
fun run_all_tests () =
- case Kodkod.solve_any_problem false NONE 0 1
- (map (problem_for_nut @{context}) tests) of
- Kodkod.Normal ([], _, _) => ()
- | _ => error "Tests failed."
+ let
+ val {overlord, ...} = Nitpick_Isar.default_params @{theory} []
+ val max_threads = 1
+ val max_solutions = 1
+ in
+ case Kodkod.solve_any_problem overlord NONE max_threads max_solutions
+ (map (problem_for_nut @{context}) tests) of
+ Kodkod.Normal ([], _, _) => ()
+ | _ => error "Tests failed."
+ end
end;
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Aug 03 18:52:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Aug 04 10:52:29 2010 +0200
@@ -49,6 +49,7 @@
val plural_s : int -> string
val plural_s_for_list : 'a list -> string
val serial_commas : string -> string list -> string list
+ val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
val flip_polarity : polarity -> polarity
@@ -72,7 +73,7 @@
val indent_size : int
val pstrs : string -> Pretty.T list
val unyxml : string -> string
- val maybe_quote : string -> string
+ val pretty_maybe_quote : Pretty.T -> Pretty.T
val hashw : word * word -> word
val hashw_string : string * word -> word
end;
@@ -222,6 +223,16 @@
val serial_commas = Sledgehammer_Util.serial_commas
+fun pretty_serial_commas _ [] = []
+ | pretty_serial_commas _ [p] = [p]
+ | pretty_serial_commas conj [p1, p2] =
+ [p1, Pretty.brk 1, Pretty.str conj, Pretty.brk 1, p2]
+ | pretty_serial_commas conj [p1, p2, p3] =
+ [p1, Pretty.str ",", Pretty.brk 1, p2, Pretty.str ",", Pretty.brk 1,
+ Pretty.str conj, Pretty.brk 1, p3]
+ | pretty_serial_commas conj (p :: ps) =
+ p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps
+
val parse_bool_option = Sledgehammer_Util.parse_bool_option
val parse_time_option = Sledgehammer_Util.parse_time_option
@@ -262,14 +273,19 @@
fun setmp_show_all_types f =
setmp_CRITICAL show_all_types
- (! show_types orelse ! show_sorts orelse ! show_all_types) f
+ (!show_types orelse !show_sorts orelse !show_all_types) f
val indent_size = 2
val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
val unyxml = Sledgehammer_Util.unyxml
+
val maybe_quote = Sledgehammer_Util.maybe_quote
+fun pretty_maybe_quote pretty =
+ let val s = Pretty.str_of pretty in
+ if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
+ end
(* This hash function is recommended in Compilers: Principles, Techniques, and
Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they