# HG changeset patch
# User blanchet
# Date 1301936950 -7200
# Node ID 3bf2eea43dac262225ed5dbd3e40b075b760852a
# Parent  662b50b7126fcee4251cf734d026b19eda517232
document "type_sys" option

diff -r 662b50b7126f -r 3bf2eea43dac NEWS
--- a/NEWS	Mon Apr 04 18:53:35 2011 +0200
+++ b/NEWS	Mon Apr 04 19:09:10 2011 +0200
@@ -49,7 +49,7 @@
 * Sledgehammer:
   - sledgehammer available_provers ~> sledgehammer supported_provers
     INCOMPATIBILITY.
-  - Added "monomorphize" and "monomorphize_limit" options.
+  - Added "monomorphize", "monomorphize_limit", and "type_sys" options.
 
 * "try":
   - Added "simp:", "intro:", and "elim:" options.
diff -r 662b50b7126f -r 3bf2eea43dac doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Apr 04 18:53:35 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Apr 04 19:09:10 2011 +0200
@@ -476,7 +476,7 @@
 \end{enum}
 
 By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
-the SMT module's \emph{smt\_solver} configuration option is set to) in
+the SMT module's \textit{smt\_solver} configuration option is set to) in
 parallel---either locally or remotely, depending on the number of processor
 cores available. For historical reasons, the default value of this option can be
 overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
@@ -536,6 +536,55 @@
 tends to slow down the ATPs significantly. For historical reasons, the default
 value of this option can be overridden using the option ``Sledgehammer: Full
 Types'' from the ``Isabelle'' menu in Proof General.
+
+\opfalse{full\_types}{partial\_types}
+Specifies whether full-type information is encoded in ATP problems. Enabling
+this option can prevent the discovery of type-incorrect proofs, but it also
+tends to slow down the ATPs significantly. For historical reasons, the default
+value of this option can be overridden using the option ``Sledgehammer: Full
+Types'' from the ``Isabelle'' menu in Proof General.
+
+\opfalse{monomorphize}{dont\_monomorphize}
+Specifies whether the relevant facts should be monomorphized---i.e., whether
+their type variables should be instantiated with relevant ground types.
+Monomorphization is always performed for SMT solvers, irrespective of this
+option. Monomorphization can simplify reasoning but also leads to larger fact
+bases, which can slow down the ATPs.
+
+\opdefault{monomorphize\_limit}{int}{\upshape 4}
+Specifies the maximum number of iterations for the monomorphization fixpoint
+construction. The higher this limit is, the more monomorphic instances are
+potentially generated.
+
+\opdefault{type\_sys}{string}{smart}
+Specifies the type system to use in ATP problems. The option can take the
+following values:
+
+\begin{enum}
+\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
+its type.
+
+% NOT YET IMPLEMENTED:
+%\item[$\bullet$] \textbf{\textit{preds}:} Types are represented by predicates.
+
+\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names.
+This value is available only if \textit{monomorphize} is enabled and
+\textit{full\_types} is enabled.
+
+\item[$\bullet$] \textbf{\textit{const\_args}:} Constants are annotated with
+their type parameters, which are passed as extra arguments. This value is not
+available if \textit{full\_types} is enabled.
+
+\item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
+ATP.
+
+\item[$\bullet$] \textbf{\textit{smart}:} This is the same as
+\textit{tags} if \textit{full\_types} is enabled; otherwise, this is the
+same as \textit{mangled} if \textit{monomorphize} is enabled and
+\textit{const\_args} otherwise.
+\end{enum}
+
+For SMT solvers, the type system is always \textit{mangled}.
 \end{enum}
 
 \subsection{Relevance Filter}
@@ -556,18 +605,6 @@
 empirically found to be appropriate for the prover. A typical value would be
 300.
 
-\opfalse{monomorphize}{dont\_monomorphize}
-Specifies whether the relevant facts should be monomorphized---i.e., whether
-their type variables should be instantiated with relevant ground types.
-Monomorphization is always performed for SMT solvers, irrespective of this
-option. Monomorphization can simplify reasoning but also leads to larger fact
-bases, which can slow down the ATPs.
-
-\opdefault{monomorphize\_limit}{int}{\upshape 4}
-Specifies the maximum number of iterations for the monomorphization fixpoint
-construction. The higher this limit is, the more monomorphic instances are
-potentially generated.
-
 \end{enum}
 
 \subsection{Output Format}