1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Mar 08 15:20:40 2010 -0800
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Mar 09 09:25:23 2010 +0100
1.3 @@ -136,8 +136,8 @@
1.4 suggesting several textual improvements.
1.5 % and Perry James for reporting a typo.
1.6
1.7 -\section{First Steps}
1.8 -\label{first-steps}
1.9 +\section{Overview}
1.10 +\label{overview}
1.11
1.12 This section introduces Nitpick by presenting small examples. If possible, you
1.13 should try out the examples on your workstation. Your theory file should start
1.14 @@ -145,7 +145,7 @@
1.15
1.16 \prew
1.17 \textbf{theory}~\textit{Scratch} \\
1.18 -\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\
1.19 +\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
1.20 \textbf{begin}
1.21 \postw
1.22
1.23 @@ -677,7 +677,7 @@
1.24 \hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
1.25 \hbox{}\qquad Datatypes: \\
1.26 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
1.27 -\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
1.28 +\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
1.29 \hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
1.30 \postw
1.31
1.32 @@ -704,8 +704,6 @@
1.33 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
1.34 \postw
1.35
1.36 -
1.37 -
1.38 Finally, Nitpick provides rudimentary support for rationals and reals using a
1.39 similar approach:
1.40
1.41 @@ -940,9 +938,10 @@
1.42 \label{coinductive-datatypes}
1.43
1.44 While Isabelle regrettably lacks a high-level mechanism for defining coinductive
1.45 -datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
1.46 -list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
1.47 -these lazy lists seamlessly and provides a hook, described in
1.48 +datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
1.49 +\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
1.50 +``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
1.51 +supports these lazy lists seamlessly and provides a hook, described in
1.52 \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
1.53 datatypes.
1.54
1.55 @@ -1165,10 +1164,11 @@
1.56
1.57 {\looseness=-1
1.58 Boxing can be enabled or disabled globally or on a per-type basis using the
1.59 -\textit{box} option. Moreover, setting the cardinality of a function or
1.60 -product type implicitly enables boxing for that type. Nitpick usually performs
1.61 -reasonable choices about which types should be boxed, but option tweaking
1.62 -sometimes helps.
1.63 +\textit{box} option. Nitpick usually performs reasonable choices about which
1.64 +types should be boxed, but option tweaking sometimes helps. A related optimization,
1.65 +``finalization,'' attempts to wrap functions that constant at all but finitely
1.66 +many points (e.g., finite sets); see the documentation for the \textit{finalize}
1.67 +option in \S\ref{scope-of-search} for details.
1.68
1.69 }
1.70
1.71 @@ -1850,7 +1850,7 @@
1.72 The number of options can be overwhelming at first glance. Do not let that worry
1.73 you: Nitpick's defaults have been chosen so that it almost always does the right
1.74 thing, and the most important options have been covered in context in
1.75 -\S\ref{first-steps}.
1.76 +\S\ref{overview}.
1.77
1.78 The descriptions below refer to the following syntactic quantities:
1.79
1.80 @@ -1936,14 +1936,10 @@
1.81 Specifies the sequence of cardinalities to use for a given type.
1.82 For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.83 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.84 -Although function and product types are normally mapped directly to the
1.85 -corresponding Kodkod concepts, setting
1.86 -the cardinality of such types is also allowed and implicitly enables ``boxing''
1.87 -for them, as explained in the description of the \textit{box}~\qty{type}
1.88 -and \textit{box} (\S\ref{scope-of-search}) options.
1.89
1.90 \nopagebreak
1.91 -{\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.92 +{\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
1.93 +(\S\ref{scope-of-search}).}
1.94
1.95 \opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.96 Specifies the default sequence of cardinalities to use. This can be overridden
1.97 @@ -2062,8 +2058,8 @@
1.98 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
1.99 product type in an isomorphic datatype internally. Boxing is an effective mean
1.100 to reduce the search space and speed up Nitpick, because the isomorphic datatype
1.101 -is approximated by a subset of the possible function or pair values;
1.102 -like other drastic optimizations, it can also prevent the discovery of
1.103 +is approximated by a subset of the possible function or pair values.
1.104 +Like other drastic optimizations, it can also prevent the discovery of
1.105 counterexamples. The option can take the following values:
1.106
1.107 \begin{enum}
1.108 @@ -2075,30 +2071,68 @@
1.109 higher-order functions are good candidates for boxing.
1.110 \end{enum}
1.111
1.112 -Setting the \textit{card}~\qty{type} option for a function or product type
1.113 -implicitly enables boxing for that type.
1.114 -
1.115 \nopagebreak
1.116 -{\small See also \textit{verbose} (\S\ref{output-format})
1.117 -and \textit{debug} (\S\ref{output-format}).}
1.118 +{\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
1.119 +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
1.120
1.121 \opsmart{box}{dont\_box}
1.122 Specifies the default boxing setting to use. This can be overridden on a
1.123 per-type basis using the \textit{box}~\qty{type} option described above.
1.124
1.125 +\opargboolorsmart{finitize}{type}{dont\_finitize}
1.126 +Specifies whether Nitpick should attempt to finitize a given type, which can be
1.127 +a function type or an infinite ``shallow datatype'' (an infinite datatype whose
1.128 +constructors don't appear in the problem).
1.129 +
1.130 +For function types, Nitpick performs a monotonicity analysis to detect functions
1.131 +that are constant at all but finitely many points (e.g., finite sets) and treats
1.132 +such occurrences specially, thereby increasing the precision. The option can
1.133 +then take the following values:
1.134 +
1.135 +\begin{enum}
1.136 +\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the type.
1.137 +\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}}: Finitize the
1.138 +type wherever possible.
1.139 +\end{enum}
1.140 +
1.141 +The semantics of the option is somewhat different for infinite shallow
1.142 +datatypes:
1.143 +
1.144 +\begin{enum}
1.145 +\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
1.146 +unsound, counterexamples generated under these conditions are tagged as ``likely
1.147 +genuine.''
1.148 +\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
1.149 +\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
1.150 +detect whether the datatype can be safely finitized before finitizing it.
1.151 +\end{enum}
1.152 +
1.153 +Like other drastic optimizations, finitization can sometimes prevent the
1.154 +discovery of counterexamples.
1.155 +
1.156 +\nopagebreak
1.157 +{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
1.158 +(\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
1.159 +\textit{debug} (\S\ref{output-format}).}
1.160 +
1.161 +\opsmart{finitize}{dont\_finitize}
1.162 +Specifies the default finitization setting to use. This can be overridden on a
1.163 +per-type basis using the \textit{finitize}~\qty{type} option described above.
1.164 +
1.165 \opargboolorsmart{mono}{type}{non\_mono}
1.166 -Specifies whether the given type should be considered monotonic when
1.167 -enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
1.168 -monotonicity check on the type. Setting this option to \textit{true} can reduce
1.169 -the number of scopes tried, but it also diminishes the theoretical chance of
1.170 +Specifies whether the given type should be considered monotonic when enumerating
1.171 +scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
1.172 +performs a monotonicity check on the type. Setting this option to \textit{true}
1.173 +can reduce the number of scopes tried, but it can also diminish the chance of
1.174 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
1.175
1.176 \nopagebreak
1.177 {\small See also \textit{card} (\S\ref{scope-of-search}),
1.178 +\textit{finitize} (\S\ref{scope-of-search}),
1.179 \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
1.180 (\S\ref{output-format}).}
1.181
1.182 -\opsmart{mono}{non\_box}
1.183 +\opsmart{mono}{non\_mono}
1.184 Specifies the default monotonicity setting to use. This can be overridden on a
1.185 per-type basis using the \textit{mono}~\qty{type} option described above.
1.186