# HG changeset patch # User blanchet # Date 1280911949 -7200 # Node ID 1a1973c005317c2920871a00a06f73d4961b4e05 # Parent 05691ad7407976d0dca6ee46304e94f1990b49c1# Parent deaef70a8c058b75fa94f8912fcc65bced474c59 merged diff -r 05691ad74079 -r 1a1973c00531 doc-src/Nitpick/nitpick.tex --- 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} diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Library/Nat_Infinity.thy --- 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 \ \ \ | Fin m \ (case n of \ \ \ | Fin n \ 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 \ \ if n = 0 then 0 else \ | Fin m \ (case n of \ \ if m = 0 then 0 else \ | Fin n \ Fin (m * n)))" @@ -237,11 +236,11 @@ instantiation inat :: linordered_ab_semigroup_add begin -definition +definition [nitpick_simp]: "m \ n = (case n of Fin n1 \ (case m of Fin m1 \ m1 \ n1 | \ \ False) | \ \ True)" -definition +definition [nitpick_simp]: "m < n = (case m of Fin m1 \ (case n of Fin n1 \ m1 < n1 | \ \ True) | \ \ False)" diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Nitpick_Examples/Core_Nits.thy --- 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\6, unary_ints, max_potential = 0, + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] subsection {* Curry in a Hurry *} diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- 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\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" | diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Nitpick_Examples/Hotel_Nits.thy --- 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 \ reach \ safe s r \ g \ isin s r \ 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 diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Nitpick_Examples/Induct_Nits.thy --- 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\8, unary_ints, sat_solver = MiniSat_JNI, + max_threads = 1, timeout = 60 s] inductive p1 :: "nat \ 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 \ q4 \ {}" nitpick [expect = potential] nitpick [non_wf, expect = potential] -nitpick [non_wf, dont_star_linear_preds, expect = potential] sorry lemma "q3 \ p4 \ {}" nitpick [expect = potential] nitpick [non_wf, expect = potential] -nitpick [non_wf, dont_star_linear_preds, expect = potential] sorry lemma "p3 \ q4 \ UNIV" nitpick [expect = potential] nitpick [non_wf, expect = potential] -nitpick [non_wf, dont_star_linear_preds, expect = potential] sorry lemma "q3 \ p4 \ UNIV" nitpick [expect = potential] nitpick [non_wf, expect = potential] -nitpick [non_wf, dont_star_linear_preds, expect = potential] sorry end diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Nitpick_Examples/Integer_Nits.thy --- 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\6, bits = 1,2,3,4,6,8] +nitpick_params [card = 1\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] diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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 "\n \ 49. even n \ 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\('a list + (nat \ 'a)) set" by auto @@ -225,7 +226,7 @@ lemma "\xs = LCons a xs; ys = LCons a ys\ \ xs = ys" nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine] -nitpick [expect = none] +nitpick [card = 1\5, expect = none] sorry subsection {* 3.10. Boxing *} @@ -268,7 +269,6 @@ lemma "length xs = length ys \ rev (zip xs ys) = zip xs (rev ys)" nitpick [verbose, expect = genuine] -nitpick [card = 8, verbose, expect = genuine] oops lemma "\g. \x\'b. g (f x) = x \ \y\'a. \x. y = f x" @@ -284,19 +284,19 @@ "n \ reach \ n + 2 \ reach" lemma "n \ reach \ 2 dvd n" -nitpick [card = 1\5, bits = 1\5, expect = none] +(* nitpick *) apply (induct set: reach) apply auto - nitpick [card = 1\5, bits = 1\5, expect = none] + nitpick [card = 1\4, bits = 1\4, expect = none] apply (thin_tac "n \ reach") nitpick [expect = genuine] oops lemma "n \ reach \ 2 dvd n \ n \ 0" -nitpick [card = 1\5, bits = 1\5, expect = none] +(* nitpick *) apply (induct set: reach) apply auto - nitpick [card = 1\5, bits = 1\5, expect = none] + nitpick [card = 1\4, bits = 1\4, expect = none] apply (thin_tac "n \ 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\5, expect = none] + nitpick [non_std, card = 1\4, expect = none] by auto qed diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Nitpick_Examples/Record_Nits.thy --- 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\6, max_potential = 0, + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] record point2d = xc :: int diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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\6, max_potential = 0, + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] lemma "P \ Q" apply (rule conjI) diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/kodkod.ML --- 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 () diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/minipick.ML --- 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 diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick.ML --- 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) => diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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\8"), - ("iter", "0,1,2,4,8,12,16,24"), - ("bits", "1,2,3,4,6,8,10,12"), - ("bisim_depth", "7"), + [("card", "1\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, diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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)) diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 @ diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 " \ " 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 () => " \ \ " ^ - Syntax.string_of_term ctxt t ^ " : _?"); + (trace_msg (fn () => " \ \ " ^ + 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 () => " \ \ " ^ - string_for_mterm ctxt m)) + |> tap (fn (m, _) => trace_msg (fn () => " \ \ " ^ + 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 () => " \ \ " ^ - Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^ - string_for_sign sn ^ "?"); + (trace_msg (fn () => " \ \ " ^ + 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 () => "\ \ " ^ - string_for_mterm ctxt m ^ " : o\<^sup>" ^ - string_for_sign sn)) + trace_msg (fn () => "\ \ " ^ + 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]) diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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 diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_rep.ML --- 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) diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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 diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_tests.ML --- 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; diff -r 05691ad74079 -r 1a1973c00531 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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