
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.
 




