# HG changeset patch
# User blanchet
# Date 1304542450 -7200
# Node ID e60326e7ee95dee1c108487e51f80fd36e56876c
# Parent  562046fd8e0c55cd19f6ddde3143685b0665f80d
update type system documentation

diff -r 562046fd8e0c -r e60326e7ee95 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed May 04 22:47:13 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed May 04 22:54:10 2011 +0200
@@ -460,7 +460,7 @@
 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
 servers. This ATP supports a fragment of the TPTP many-typed first-order format
 (TFF). It is supported primarily for experimenting with the
-\textit{type\_sys} $=$ \textit{many\_typed} option (\S\ref{problem-encoding}).
+\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
 
 \item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
 developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
@@ -571,7 +571,7 @@
 following values:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{many\_typed}:} Use the prover's support for
+\item[$\bullet$] \textbf{\textit{simple}:} Use the prover's support for
 many-typed first-order logic if available; otherwise, fall back on
 \textit{mangled\_preds}. The problem is monomorphized, meaning that the
 problem's type variables are instantiated with heuristically chosen ground
@@ -608,35 +608,39 @@
 
 \item[$\bullet$]
 \textbf{%
+\textit{simple}?,
 \textit{preds}?,
 \textit{mono\_preds}?,
 \textit{mangled\_preds}?, \\
 \textit{tags}?,
 \textit{mono\_tags}?,
 \textit{mangled\_tags}?:} \\
-The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds},
-\textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed
-and virtually sound---i.e., except for pathological cases, all found proofs are
-type-correct. For each of these, Sledgehammer also provides a just-as-sound
-partially typed variant identified by a question mark (?)\ that detects and
-erases monotonic types (notably infinite types).
+The type systems \textit{simple}, \textit{preds}, \textit{mono\_preds},
+\textit{mangled\_preds}, \textit{tags}, \textit{mono\_tags}, and
+\textit{mangled\_tags} are fully typed and virtually sound---i.e., except for
+pathological cases, all found proofs are type-correct. For each of these,
+Sledgehammer also provides a just-as-sound partially typed variant identified by
+a question mark (`{?}')\ that detects and erases monotonic types, notably infinite
+types. (For \textit{simple}, the types are not actually erased but rather
+replaced by a shared uniform ``top'' type.)
 
 \item[$\bullet$]
 \textbf{%
+\textit{simple}!,
 \textit{preds}!,
 \textit{mono\_preds}!,
 \textit{mangled\_preds}!, \\
 \textit{tags}!,
 \textit{mono\_tags}!,
 \textit{mangled\_tags}!:} \\
-If the question mark (?)\ is replaced by an exclamation mark (!),\ the
+If the question mark (`{?}')\ is replaced by an exclamation mark (`{!}'),\ the
 translation erases all types except those that are clearly finite (e.g.,
 \textit{bool}). This encoding is unsound.
 
-\item[$\bullet$] \textbf{\textit{const\_args}:}
+\item[$\bullet$] \textbf{\textit{args}:}
 Like for the other sound encodings, constants are annotated with their types to
 resolve overloading, but otherwise no type information is encoded. This encoding
-is hence less sound than the exclamation mark (!)\ variants described above.
+is hence less sound than the exclamation mark (`{!}')\ variants described above.
 
 \item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
 the ATP. Types are simply erased.
@@ -647,7 +651,7 @@
 that ATP.
 \end{enum}
 
-For SMT solvers and ToFoF-E, the type system is always \textit{many\_typed}.
+For SMT solvers and ToFoF-E, the type system is always \textit{simple}.
 
 \opdefault{monomorphize\_limit}{int}{\upshape 4}
 Specifies the maximum number of iterations for the monomorphization fixpoint