--- a/doc-src/Sledgehammer/sledgehammer.tex Wed May 04 22:56:33 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed May 04 23:18:28 2011 +0200
@@ -583,10 +583,14 @@
Constants are annotated with their types, supplied as extra arguments, to
resolve overloading.
+\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
+its type using a function $\mathit{type\_info\/}(\tau, t)$.
+
\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
-the problem is additionally monomorphized. This corresponds to the traditional
-encoding of types in an untyped logic without overloading (e.g., such as
-performed by the ToFoF-E wrapper).
+the problem is additionally monomorphized.
+
+\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
+the problem is additionally monomorphized.
\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
\textit{mono\_preds}, but types are mangled in constant names instead of being
@@ -594,12 +598,6 @@
$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
$\mathit{has\_type\_}\tau(t)$.
-\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
-its type using a function $\mathit{type\_info\/}(\tau, t)$.
-
-\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
-the problem is additionally monomorphized.
-
\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
\textit{mono\_tags}, but types are mangled in constant names instead of being
supplied as ground term arguments. The binary function
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 22:56:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 23:18:28 2011 +0200
@@ -891,7 +891,6 @@
fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
let
fun declare_sym decl decls =
- (* FIXME: use "insert_type" in all cases? *)
case type_sys of
Preds (Polymorphic, All_Types) => insert_type #3 decl decls
| _ => insert (op =) decl decls
@@ -918,12 +917,13 @@
? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
facts
-(* FIXME: use CombVar not CombConst for bound variables? *)
fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
String.isPrefix bound_var_prefix s
| is_var_or_bound_var (CombVar _) = true
| is_var_or_bound_var _ = false
+(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
+ out with monotonicity" paper presented at CADE 2011. *)
fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
| add_combterm_nonmonotonic_types ctxt _
(CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),