# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID 08346ea46a591d5bb35bfc620baa8b38eb6ab499 # Parent 413b56894f82349dbdc1de3abe90235c31a7e030 added (without implementation yet) new type encodings for Sledgehammer/ATP diff -r 413b56894f82 -r 08346ea46a59 doc-src/Sledgehammer/sledgehammer.tex --- 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} diff -r 413b56894f82 -r 08346ea46a59 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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 diff -r 413b56894f82 -r 08346ea46a59 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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") diff -r 413b56894f82 -r 08346ea46a59 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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