--- a/doc-src/Sledgehammer/sledgehammer.tex Sun May 01 18:37:23 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sun May 01 18:37:24 2011 +0200
@@ -560,18 +560,6 @@
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:
@@ -581,22 +569,38 @@
its type.
\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with
-their type parameters, which are passed as extra arguments. This value is
-ignored if \textit{full\_types} is enabled.
+their type parameters, which are passed as extra arguments.
\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 disabled.
+This value implicitly enables \textit{monomorphize}.
+
+\item[$\bullet$] \textbf{\textit{many\_typed}:} Use the prover's support for
+many-typed first-order logic logic if available; otherwise, fall back on
+\textit{mangled}. This value implicitly enables \textit{monomorphize}.
\item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
ATP. This value is ignored if \textit{full\_types} is enabled.
\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
this is the same as \textit{tags}; otherwise, this is the
-same as \textit{args} otherwise.
+same as \textit{args}.
\end{enum}
-For SMT solvers, the type system is always \textit{mangled}.
+For SMT solvers, the type system is always \textit{many\_typed}.
+
+\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. If the type system is \textit{mangled} or
+\textit{many\_typed}, monomorphization is implicitly enabled irrespective of
+this option.
+
+\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{Relevance Filter}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:23 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200
@@ -13,9 +13,10 @@
type translated_formula
datatype type_system =
+ Many_Typed |
Tags of bool |
- Args |
- Mangled |
+ Args of bool |
+ Mangled of bool |
No_Types
val risky_overloaded_args : bool Unsynchronized.ref
@@ -63,16 +64,20 @@
ctypes_sorts: typ list}
datatype type_system =
+ Many_Typed |
Tags of bool |
- Args |
- Mangled |
+ Args of bool |
+ Mangled of bool |
No_Types
-fun is_type_system_sound (Tags true) = true
- | is_type_system_sound _ = false
+fun is_type_system_sound Many_Typed = true
+ | is_type_system_sound (Tags full_types) = full_types
+ | is_type_system_sound (Args full_types) = full_types
+ | is_type_system_sound (Mangled full_types) = full_types
+ | is_type_system_sound No_Types = false
fun type_system_types_dangerous_types (Tags _) = true
- | type_system_types_dangerous_types _ = false
+ | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys
(* This is an approximation. If it returns "true" for a constant that isn't
overloaded (i.e., that has one uniform definition), needless clutter is
@@ -86,16 +91,19 @@
fun needs_type_args thy type_sys s =
case type_sys of
- Tags full_types => not full_types andalso is_overloaded thy s
- | Args => is_overloaded thy s
- | Mangled => true
+ Many_Typed => false
+ | Tags full_types => not full_types andalso is_overloaded thy s
+ | Args full_types => not full_types andalso is_overloaded thy s
+ | Mangled full_types => not full_types andalso is_overloaded thy s
| No_Types => false
datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
fun type_arg_policy thy type_sys s =
if needs_type_args thy type_sys s then
- if type_sys = Mangled then Mangled_Types else Explicit_Type_Args
+ case type_sys of
+ Mangled _ => Mangled_Types
+ | _ => Explicit_Type_Args
else
No_Type_Args
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:23 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:24 2011 +0200
@@ -79,11 +79,11 @@
("verbose", "false"),
("overlord", "false"),
("blocking", "false"),
+ ("type_sys", "smart"),
("relevance_thresholds", "0.45 0.85"),
("max_relevant", "smart"),
("monomorphize", "false"),
("monomorphize_limit", "4"),
- ("type_sys", "smart"),
("explicit_apply", "false"),
("isar_proof", "false"),
("isar_shrink_factor", "1"),
@@ -235,22 +235,22 @@
val blocking = auto orelse debug orelse lookup_bool "blocking"
val provers = lookup_string "provers" |> space_explode " "
|> auto ? single o hd
+ val (type_sys, must_monomorphize) =
+ case (lookup_string "type_sys", lookup_bool "full_types") of
+ ("many_typed", _) => (Many_Typed, true)
+ | ("tags", full_types) => (Tags full_types, false)
+ | ("args", full_types) => (Args full_types, false)
+ | ("mangled", full_types) => (Mangled full_types, true)
+ | ("none", false) => (No_Types, false)
+ | (type_sys, full_types) =>
+ if member (op =) ["none", "smart"] type_sys then
+ (if full_types then Tags true else Args false, false)
+ else
+ error ("Unknown type system: " ^ quote type_sys ^ ".")
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_int_option "max_relevant"
- val monomorphize = lookup_bool "monomorphize"
+ val monomorphize = must_monomorphize orelse lookup_bool "monomorphize"
val monomorphize_limit = lookup_int "monomorphize_limit"
- val type_sys =
- case (lookup_string "type_sys", lookup_bool "full_types") of
- ("tags", full_types) => Tags full_types
- | ("args", false) => Args
- | ("mangled", false) => if monomorphize then Mangled else Args
- | ("none", false) => No_Types
- | (type_sys, full_types) =>
- if member (op =) ["args", "mangled", "none", "smart"]
- type_sys then
- if full_types then Tags true else Args
- else
- error ("Unknown type system: " ^ quote type_sys ^ ".")
val explicit_apply = lookup_bool "explicit_apply"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:23 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:24 2011 +0200
@@ -21,11 +21,11 @@
overlord: bool,
blocking: bool,
provers: string list,
+ type_sys: type_system,
relevance_thresholds: real * real,
max_relevant: int option,
monomorphize: bool,
monomorphize_limit: int,
- type_sys: type_system,
explicit_apply: bool,
isar_proof: bool,
isar_shrink_factor: int,
@@ -233,11 +233,11 @@
overlord: bool,
blocking: bool,
provers: string list,
+ type_sys: type_system,
relevance_thresholds: real * real,
max_relevant: int option,
monomorphize: bool,
monomorphize_limit: int,
- type_sys: type_system,
explicit_apply: bool,
isar_proof: bool,
isar_shrink_factor: int,
@@ -337,9 +337,9 @@
fun run_atp auto name
({exec, required_execs, arguments, slices, proof_delims, known_failures,
use_conjecture_for_hypotheses, ...} : atp_config)
- ({debug, verbose, overlord, max_relevant, monomorphize,
- monomorphize_limit, type_sys, explicit_apply, isar_proof,
- isar_shrink_factor, slicing, timeout, ...} : params)
+ ({debug, verbose, overlord, type_sys, max_relevant, monomorphize,
+ monomorphize_limit, explicit_apply, isar_proof, isar_shrink_factor,
+ slicing, timeout, ...} : params)
minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
let
val thy = Proof.theory_of state