diff -r fee01e85605f -r ff2bf50505ab doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Mon Mar 08 15:20:40 2010 -0800 +++ b/doc-src/Nitpick/nitpick.tex Tue Mar 09 09:25:23 2010 +0100 @@ -136,8 +136,8 @@ suggesting several textual improvements. % and Perry James for reporting a typo. -\section{First Steps} -\label{first-steps} +\section{Overview} +\label{overview} This section introduces Nitpick by presenting small examples. If possible, you should try out the examples on your workstation. Your theory file should start @@ -145,7 +145,7 @@ \prew \textbf{theory}~\textit{Scratch} \\ -\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\ +\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\ \textbf{begin} \postw @@ -677,7 +677,7 @@ \hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\ \hbox{}\qquad Datatypes: \\ \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\ -\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\ +\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\ \hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$ \postw @@ -704,8 +704,6 @@ & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$ \postw - - Finally, Nitpick provides rudimentary support for rationals and reals using a similar approach: @@ -940,9 +938,10 @@ \label{coinductive-datatypes} While Isabelle regrettably lacks a high-level mechanism for defining coinductive -datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy -list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports -these lazy lists seamlessly and provides a hook, described in +datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's +\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive +``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick +supports these lazy lists seamlessly and provides a hook, described in \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive datatypes. @@ -1165,10 +1164,11 @@ {\looseness=-1 Boxing can be enabled or disabled globally or on a per-type basis using the -\textit{box} option. Moreover, setting the cardinality of a function or -product type implicitly enables boxing for that type. Nitpick usually performs -reasonable choices about which types should be boxed, but option tweaking -sometimes helps. +\textit{box} option. Nitpick usually performs reasonable choices about which +types should be boxed, but option tweaking sometimes helps. A related optimization, +``finalization,'' attempts to wrap functions that constant at all but finitely +many points (e.g., finite sets); see the documentation for the \textit{finalize} +option in \S\ref{scope-of-search} for details. } @@ -1850,7 +1850,7 @@ The number of options can be overwhelming at first glance. Do not let that worry you: Nitpick's defaults have been chosen so that it almost always does the right thing, and the most important options have been covered in context in -\S\ref{first-steps}. +\S\ref{overview}. The descriptions below refer to the following syntactic quantities: @@ -1936,14 +1936,10 @@ Specifies the sequence of cardinalities to use for a given type. For free types, and often also for \textbf{typedecl}'d types, it usually makes sense to specify cardinalities as a range of the form \textit{$1$--$n$}. -Although function and product types are normally mapped directly to the -corresponding Kodkod concepts, setting -the cardinality of such types is also allowed and implicitly enables ``boxing'' -for them, as explained in the description of the \textit{box}~\qty{type} -and \textit{box} (\S\ref{scope-of-search}) options. \nopagebreak -{\small See also \textit{mono} (\S\ref{scope-of-search}).} +{\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}$} Specifies the default sequence of cardinalities to use. This can be overridden @@ -2062,8 +2058,8 @@ Specifies whether Nitpick should attempt to wrap (``box'') a given function or product type in an isomorphic datatype internally. Boxing is an effective mean to reduce the search space and speed up Nitpick, because the isomorphic datatype -is approximated by a subset of the possible function or pair values; -like other drastic optimizations, it can also prevent the discovery of +is approximated by a subset of the possible function or pair values. +Like other drastic optimizations, it can also prevent the discovery of counterexamples. The option can take the following values: \begin{enum} @@ -2075,30 +2071,68 @@ higher-order functions are good candidates for boxing. \end{enum} -Setting the \textit{card}~\qty{type} option for a function or product type -implicitly enables boxing for that type. - \nopagebreak -{\small See also \textit{verbose} (\S\ref{output-format}) -and \textit{debug} (\S\ref{output-format}).} +{\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose} +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).} \opsmart{box}{dont\_box} Specifies the default boxing setting to use. This can be overridden on a per-type basis using the \textit{box}~\qty{type} option described above. +\opargboolorsmart{finitize}{type}{dont\_finitize} +Specifies whether Nitpick should attempt to finitize a given type, which can be +a function type or an infinite ``shallow datatype'' (an infinite datatype whose +constructors don't appear in the problem). + +For function types, Nitpick performs a monotonicity analysis to detect functions +that are constant at all but finitely many points (e.g., finite sets) and treats +such occurrences specially, thereby increasing the precision. The option can +then take the following values: + +\begin{enum} +\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the type. +\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}}: Finitize the +type wherever possible. +\end{enum} + +The semantics of the option is somewhat different for infinite shallow +datatypes: + +\begin{enum} +\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is +unsound, counterexamples generated under these conditions are tagged as ``likely +genuine.'' +\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype. +\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to +detect whether the datatype can be safely finitized before finitizing it. +\end{enum} + +Like other drastic optimizations, finitization can sometimes prevent the +discovery of counterexamples. + +\nopagebreak +{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono} +(\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and +\textit{debug} (\S\ref{output-format}).} + +\opsmart{finitize}{dont\_finitize} +Specifies the default finitization setting to use. This can be overridden on a +per-type basis using the \textit{finitize}~\qty{type} option described above. + \opargboolorsmart{mono}{type}{non\_mono} -Specifies whether the given type should be considered monotonic when -enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a -monotonicity check on the type. Setting this option to \textit{true} can reduce -the number of scopes tried, but it also diminishes the theoretical chance of +Specifies whether the given type should be considered monotonic when enumerating +scopes and finitizing types. If the option is set to \textit{smart}, Nitpick +performs a monotonicity check on the type. Setting this option to \textit{true} +can reduce the number of scopes tried, but it can also diminish the chance of finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}. \nopagebreak {\small See also \textit{card} (\S\ref{scope-of-search}), +\textit{finitize} (\S\ref{scope-of-search}), \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose} (\S\ref{output-format}).} -\opsmart{mono}{non\_box} +\opsmart{mono}{non\_mono} Specifies the default monotonicity setting to use. This can be overridden on a per-type basis using the \textit{mono}~\qty{type} option described above.