obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
authorblanchet
Tue Jun 07 08:52:35 2011 +0200 (2011-06-07)
changeset 432282ed2f092e990
parent 43227 359c190ede75
child 43229 443708f05bb2
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
NEWS
doc-src/Sledgehammer/sledgehammer.tex
src/HOL/Metis_Examples/Clausification.thy
src/HOL/Metis_Examples/Proxies.thy
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP/atp_reconstruct.ML
src/HOL/Tools/Metis/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/NEWS	Tue Jun 07 07:57:24 2011 +0200
     1.2 +++ b/NEWS	Tue Jun 07 08:52:35 2011 +0200
     1.3 @@ -86,7 +86,8 @@
     1.4    - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
     1.5  
     1.6  * Metis:
     1.7 -  - Obsoleted "metisF" -- use "metis" instead.
     1.8 +  - Removed "metisF" -- use "metis" instead.
     1.9 +  - Obsoleted "metisFT" -- use "metis (full_types)" instead.
    1.10  
    1.11  * "try":
    1.12    - Added "simp:", "intro:", and "elim:" options.
     2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Jun 07 07:57:24 2011 +0200
     2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Jun 07 08:52:35 2011 +0200
     2.3 @@ -495,30 +495,35 @@
     2.4  set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
     2.5  value or to try several provers and keep the nicest-looking proof.
     2.6  
     2.7 -\point{What is metisFT?}
     2.8 +\point{What is the \textit{full\_types}/\textit{no\_types} argument to Metis?}
     2.9  
    2.10 -The \textit{metisFT} proof method is the fully-typed version of Metis. It is
    2.11 -much slower than \textit{metis}, but the proof search is fully typed, and it
    2.12 -also includes more powerful rules such as the axiom ``$x = \mathit{True}
    2.13 -\mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places (e.g.,
    2.14 -in set comprehensions). The method kicks in automatically as a fallback when
    2.15 -\textit{metis} fails, and it is sometimes generated by Sledgehammer instead of
    2.16 -\textit{metis} if the proof obviously requires type information or if
    2.17 -\textit{metis} failed when Sledgehammer preplayed the proof. (By default,
    2.18 -Sledgehammer tries to run \textit{metis} and/or \textit{metisFT} for 4 seconds
    2.19 -to ensure that the generated one-line proofs actually work and to display timing
    2.20 -information. This can be configured using the \textit{preplay\_timeout} option
    2.21 -(\S\ref{timeouts}).)
    2.22 +The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed
    2.23 +version of Metis. It is somewhat slower than \textit{metis}, but the proof
    2.24 +search is fully typed, and it also includes more powerful rules such as the
    2.25 +axiom ``$x = \mathit{True} \mathrel{\lor} x = \mathit{False}$'' for reasoning in
    2.26 +higher-order places (e.g., in set comprehensions). The method kicks in
    2.27 +automatically as a fallback when \textit{metis} fails, and it is sometimes
    2.28 +generated by Sledgehammer instead of \textit{metis} if the proof obviously
    2.29 +requires type information or if \textit{metis} failed when Sledgehammer
    2.30 +preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
    2.31 +various options for up to 4 seconds to ensure that the generated one-line proofs
    2.32 +actually work and to display timing information. This can be configured using
    2.33 +the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
    2.34  
    2.35  If you see the warning
    2.36  
    2.37  \prew
    2.38  \slshape
    2.39 -Metis: Falling back on ``\textit{metisFT\/}''.
    2.40 +Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
    2.41  \postw
    2.42  
    2.43 -in a successful Metis proof, you can advantageously replace the \textit{metis}
    2.44 -call with \textit{metisFT}.
    2.45 +in a successful Metis proof, you can advantageously pass the
    2.46 +\textit{full\_types} option to \textit{metis} directly.
    2.47 +
    2.48 +At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
    2.49 +uses no type information at all during the proof search, which is more efficient
    2.50 +but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
    2.51 +generated by Sledgehammer.
    2.52  
    2.53  \point{Are generated proofs minimal?}
    2.54  
    2.55 @@ -664,8 +669,8 @@
    2.56  Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and
    2.57  \qty{facts} is a list of arbitrary facts. \qty{type\_sys} may also be
    2.58  \textit{full\_types}, in which case an appropriate type-sound encoding is
    2.59 -chosen. The companion proof method \textit{metisFT} is an abbreviation for
    2.60 -``\textit{metis}~(\textit{full\_types})''.
    2.61 +chosen, \textit{partial\_types} (the default), or \textit{no\_types}, a synonym
    2.62 +for \textit{erased}.
    2.63  
    2.64  \section{Option Reference}
    2.65  \label{option-reference}
    2.66 @@ -764,7 +769,11 @@
    2.67  \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
    2.68  the external provers, Metis itself can be used for proof search.
    2.69  
    2.70 -\item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis.
    2.71 +\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
    2.72 +Metis, corresponding to \textit{metis} (\textit{full\_types}).
    2.73 +
    2.74 +\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
    2.75 +corresponding to \textit{metis} (\textit{no\_types}).
    2.76  \end{enum}
    2.77  
    2.78  In addition, the following remote provers are supported:
    2.79 @@ -903,14 +912,12 @@
    2.80  arguments, to resolve overloading.
    2.81  
    2.82  \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
    2.83 -tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. This
    2.84 -coincides with the encoding used by the \textit{metisFT} command.
    2.85 +tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
    2.86  
    2.87  \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
    2.88  Like for \textit{poly\_preds} constants are annotated with their types to
    2.89  resolve overloading, but otherwise no type information is encoded. This
    2.90 -coincides with the encoding used by the \textit{metis} command (before it falls
    2.91 -back on \textit{metisFT}).
    2.92 +coincides with the default encoding used by the \textit{metis} command.
    2.93  
    2.94  \item[$\bullet$]
    2.95  \textbf{%
     3.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Tue Jun 07 07:57:24 2011 +0200
     3.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Tue Jun 07 08:52:35 2011 +0200
     3.3 @@ -28,13 +28,13 @@
     3.4  by (metis qax)
     3.5  
     3.6  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
     3.7 -by (metisFT qax)
     3.8 +by (metis (full_types) qax)
     3.9  
    3.10  lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    3.11  by (metis qax)
    3.12  
    3.13  lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    3.14 -by (metisFT qax)
    3.15 +by (metis (full_types) qax)
    3.16  
    3.17  declare [[metis_new_skolemizer]]
    3.18  
    3.19 @@ -42,13 +42,13 @@
    3.20  by (metis qax)
    3.21  
    3.22  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    3.23 -by (metisFT qax)
    3.24 +by (metis (full_types) qax)
    3.25  
    3.26  lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    3.27  by (metis qax)
    3.28  
    3.29  lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    3.30 -by (metisFT qax)
    3.31 +by (metis (full_types) qax)
    3.32  
    3.33  declare [[meson_max_clauses = 60]]
    3.34  
    3.35 @@ -64,7 +64,7 @@
    3.36  by (metis rax)
    3.37  
    3.38  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    3.39 -by (metisFT rax)
    3.40 +by (metis (full_types) rax)
    3.41  
    3.42  declare [[metis_new_skolemizer]]
    3.43  
    3.44 @@ -72,7 +72,7 @@
    3.45  by (metis rax)
    3.46  
    3.47  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    3.48 -by (metisFT rax)
    3.49 +by (metis (full_types) rax)
    3.50  
    3.51  lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
    3.52         (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
    3.53 @@ -84,7 +84,7 @@
    3.54         (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
    3.55         (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
    3.56         (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
    3.57 -by (metisFT rax)
    3.58 +by (metis (full_types) rax)
    3.59  
    3.60  
    3.61  text {* Definitional CNF for goal *}
    3.62 @@ -100,7 +100,7 @@
    3.63  
    3.64  lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
    3.65                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    3.66 -by (metisFT pax)
    3.67 +by (metis (full_types) pax)
    3.68  
    3.69  declare [[metis_new_skolemizer]]
    3.70  
    3.71 @@ -110,7 +110,7 @@
    3.72  
    3.73  lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
    3.74                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    3.75 -by (metisFT pax)
    3.76 +by (metis (full_types) pax)
    3.77  
    3.78  
    3.79  text {* New Skolemizer *}
    3.80 @@ -134,7 +134,7 @@
    3.81    assumes a: "Quotient R Abs Rep"
    3.82    shows "symp R"
    3.83  using a unfolding Quotient_def using sympI
    3.84 -by metisFT
    3.85 +by (metis (full_types))
    3.86  
    3.87  lemma
    3.88    "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
     4.1 --- a/src/HOL/Metis_Examples/Proxies.thy	Tue Jun 07 07:57:24 2011 +0200
     4.2 +++ b/src/HOL/Metis_Examples/Proxies.thy	Tue Jun 07 08:52:35 2011 +0200
     4.3 @@ -66,7 +66,7 @@
     4.4  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
     4.5  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
     4.6  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
     4.7 -by (metisFT id_apply)
     4.8 +by (metis (full_types) id_apply)
     4.9  
    4.10  lemma "id True"
    4.11  sledgehammer [type_sys = erased, expect = some] (id_apply)
    4.12 @@ -127,7 +127,7 @@
    4.13  sledgehammer [type_sys = mangled_tags, expect = some] ()
    4.14  sledgehammer [type_sys = mangled_preds?, expect = some] ()
    4.15  sledgehammer [type_sys = mangled_preds, expect = some] ()
    4.16 -by metisFT
    4.17 +by (metis (full_types))
    4.18  
    4.19  lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
    4.20  sledgehammer [type_sys = erased, expect = some] (id_apply)
     5.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 07 07:57:24 2011 +0200
     5.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 07 08:52:35 2011 +0200
     5.3 @@ -342,7 +342,8 @@
     5.4    (case AList.lookup (op =) args reconstructorK of
     5.5      SOME name => name
     5.6    | NONE =>
     5.7 -    if String.isSubstring "metisFT" msg then "metisFT"
     5.8 +    if String.isSubstring "metis (full_types)" msg then "metis (full_types)"
     5.9 +    else if String.isSubstring "metis (no_types)" msg then "metis (no_types)"
    5.10      else if String.isSubstring "metis" msg then "metis"
    5.11      else "smt")
    5.12  
    5.13 @@ -541,8 +542,10 @@
    5.14              Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
    5.15         else if !reconstructor = "smt" then
    5.16           SMT_Solver.smt_tac
    5.17 -       else if full orelse !reconstructor = "metisFT" then
    5.18 -         Metis_Tactics.metisFT_tac
    5.19 +       else if full orelse !reconstructor = "metis (full_types)" then
    5.20 +         Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
    5.21 +       else if !reconstructor = "metis (no_types)" then
    5.22 +         Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
    5.23         else
    5.24           Metis_Tactics.metis_tac []) ctxt thms
    5.25      fun apply_reconstructor thms =
     6.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Jun 07 07:57:24 2011 +0200
     6.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Jun 07 08:52:35 2011 +0200
     6.3 @@ -16,7 +16,8 @@
     6.4  
     6.5    datatype reconstructor =
     6.6      Metis |
     6.7 -    MetisFT |
     6.8 +    Metis_Full_Types |
     6.9 +    Metis_No_Types |
    6.10      SMT of string
    6.11  
    6.12    datatype play =
    6.13 @@ -67,7 +68,8 @@
    6.14  
    6.15  datatype reconstructor =
    6.16    Metis |
    6.17 -  MetisFT |
    6.18 +  Metis_Full_Types |
    6.19 +  Metis_No_Types |
    6.20    SMT of string
    6.21  
    6.22  datatype play =
    6.23 @@ -251,8 +253,10 @@
    6.24  
    6.25  (** Soft-core proof reconstruction: Metis one-liner **)
    6.26  
    6.27 +(* unfortunate leaking abstraction *)
    6.28  fun reconstructor_name Metis = "metis"
    6.29 -  | reconstructor_name MetisFT = "metisFT"
    6.30 +  | reconstructor_name Metis_Full_Types = "metis (full_types)"
    6.31 +  | reconstructor_name Metis_No_Types = "metis (no_types)"
    6.32    | reconstructor_name (SMT _) = "smt"
    6.33  
    6.34  fun reconstructor_settings (SMT settings) = settings
    6.35 @@ -1042,7 +1046,7 @@
    6.36         else
    6.37           if member (op =) qs Show then "show" else "have")
    6.38      val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
    6.39 -    val reconstructor = if full_types then MetisFT else Metis
    6.40 +    val reconstructor = if full_types then Metis_Full_Types else Metis
    6.41      fun do_facts (ls, ss) =
    6.42        reconstructor_command reconstructor 1 1
    6.43            (ls |> sort_distinct (prod_ord string_ord int_ord),
     7.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Jun 07 07:57:24 2011 +0200
     7.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Jun 07 08:52:35 2011 +0200
     7.3 @@ -10,14 +10,16 @@
     7.4  signature METIS_TACTICS =
     7.5  sig
     7.6    val metisN : string
     7.7 -  val metisFT_N : string
     7.8 -  val default_unsound_type_sys : string
     7.9 -  val default_sound_type_sys : string
    7.10 +  val full_typesN : string
    7.11 +  val partial_typesN : string
    7.12 +  val no_typesN : string
    7.13 +  val full_type_sys : string
    7.14 +  val partial_type_sys : string
    7.15 +  val no_type_sys : string
    7.16    val trace : bool Config.T
    7.17    val verbose : bool Config.T
    7.18    val new_skolemizer : bool Config.T
    7.19    val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
    7.20 -  val metisFT_tac : Proof.context -> thm list -> int -> tactic
    7.21    val setup : theory -> theory
    7.22  end
    7.23  
    7.24 @@ -29,18 +31,25 @@
    7.25  open Metis_Reconstruct
    7.26  
    7.27  val metisN = Binding.qualified_name_of @{binding metis}
    7.28 -val metisFT_N = Binding.qualified_name_of @{binding metisFT}
    7.29 +
    7.30  val full_typesN = "full_types"
    7.31 +val partial_typesN = "partial_types"
    7.32 +val no_typesN = "no_types"
    7.33  
    7.34 -val default_unsound_type_sys = "poly_args"
    7.35 -val default_sound_type_sys = "poly_preds_heavy_query"
    7.36 +val full_type_sys = "poly_preds_heavy_query"
    7.37 +val partial_type_sys = "poly_args"
    7.38 +val no_type_sys = "erased"
    7.39 +
    7.40 +val type_sys_aliases =
    7.41 +  [(full_typesN, full_type_sys),
    7.42 +   (partial_typesN, partial_type_sys),
    7.43 +   (no_typesN, no_type_sys)]
    7.44  
    7.45  fun method_call_for_type_sys type_sys =
    7.46 -  if type_sys = default_sound_type_sys then
    7.47 -    (@{binding metisFT}, "")
    7.48 -  else
    7.49 -    (@{binding metis},
    7.50 -     if type_sys = default_unsound_type_sys then "" else type_sys)
    7.51 +  metisN ^ " (" ^
    7.52 +  (case AList.find (op =) type_sys_aliases type_sys of
    7.53 +     [alias] => alias
    7.54 +   | _ => type_sys) ^ ")"
    7.55  
    7.56  val new_skolemizer =
    7.57    Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    7.58 @@ -168,13 +177,10 @@
    7.59                          (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
    7.60                           else ""))
    7.61           | type_sys :: _ =>
    7.62 -           let val (binding, arg) = method_call_for_type_sys type_sys in
    7.63 -             (verbose_warning ctxt
    7.64 -                  ("Falling back on " ^
    7.65 -                   quote (Binding.qualified_name_of binding ^
    7.66 -                          (arg |> arg <> "" ? enclose " (" ")")) ^ "...");
    7.67 -              FOL_SOLVE fallback_type_syss ctxt cls ths0)
    7.68 -            end
    7.69 +           (verbose_warning ctxt
    7.70 +                ("Falling back on " ^
    7.71 +                 quote (method_call_for_type_sys type_sys) ^ "...");
    7.72 +            FOL_SOLVE fallback_type_syss ctxt cls ths0)
    7.73  
    7.74  val neg_clausify =
    7.75    single
    7.76 @@ -207,12 +213,11 @@
    7.77        Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
    7.78    end
    7.79  
    7.80 -val metis_default_type_syss = [default_unsound_type_sys, default_sound_type_sys]
    7.81 -val metisFT_type_syss = [default_sound_type_sys]
    7.82 +val metis_default_type_syss = [partial_type_sys, full_type_sys]
    7.83 +val metisFT_type_syss = [full_type_sys]
    7.84  
    7.85  fun metis_tac [] = generic_metis_tac metis_default_type_syss
    7.86    | metis_tac type_syss = generic_metis_tac type_syss
    7.87 -val metisFT_tac = generic_metis_tac metisFT_type_syss
    7.88  
    7.89  (* Whenever "X" has schematic type variables, we treat "using X by metis" as
    7.90     "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
    7.91 @@ -224,6 +229,12 @@
    7.92  
    7.93  fun method type_syss (type_sys, ths) ctxt facts =
    7.94    let
    7.95 +    val _ =
    7.96 +      if type_syss = metisFT_type_syss then
    7.97 +        legacy_feature "Old 'metisFT' method -- \
    7.98 +                       \use 'metis (full_types)' instead"
    7.99 +      else
   7.100 +        ()
   7.101      val (schem_facts, nonschem_facts) = List.partition has_tvar facts
   7.102      val type_syss = type_sys |> Option.map single |> the_default type_syss
   7.103    in
   7.104 @@ -232,19 +243,20 @@
   7.105                o generic_metis_tac type_syss ctxt (schem_facts @ ths))
   7.106    end
   7.107  
   7.108 -fun setup_method (type_syss as type_sys :: _) =
   7.109 +fun setup_method (binding, type_syss as type_sys :: _) =
   7.110    (if type_syss = metis_default_type_syss then
   7.111       (Args.parens Parse.short_ident
   7.112 -      >> (fn s => if s = full_typesN then default_sound_type_sys else s))
   7.113 +      >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s))
   7.114       |> Scan.option |> Scan.lift
   7.115     else
   7.116       Scan.succeed NONE)
   7.117    -- Attrib.thms >> (METHOD oo method type_syss)
   7.118 -  |> Method.setup (fst (method_call_for_type_sys type_sys))
   7.119 +  |> Method.setup binding
   7.120  
   7.121  val setup =
   7.122 -  [(metis_default_type_syss, "Metis for FOL and HOL problems"),
   7.123 -   (metisFT_type_syss,
   7.124 +  [((@{binding metis}, metis_default_type_syss),
   7.125 +    "Metis for FOL and HOL problems"),
   7.126 +   ((@{binding metisFT}, metisFT_type_syss),
   7.127      "Metis for FOL/HOL problems with fully-typed translation")]
   7.128    |> fold (uncurry setup_method)
   7.129  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 07:57:24 2011 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 08:52:35 2011 +0200
     8.3 @@ -128,9 +128,18 @@
     8.4     "Async_Manager". *)
     8.5  val das_tool = "Sledgehammer"
     8.6  
     8.7 -val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N]
     8.8 +val metisN = Metis_Tactics.metisN
     8.9 +val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN
    8.10 +val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN
    8.11  
    8.12 -val is_metis_prover = member (op =) metis_prover_names
    8.13 +val metis_prover_infos =
    8.14 +  [(metisN, Metis),
    8.15 +   (metis_full_typesN, Metis_Full_Types),
    8.16 +   (metis_no_typesN, Metis_No_Types)]
    8.17 +
    8.18 +val metis_reconstructors = map snd metis_prover_infos
    8.19 +
    8.20 +val is_metis_prover = AList.defined (op =) metis_prover_infos
    8.21  val is_atp = member (op =) o supported_atps
    8.22  
    8.23  val select_smt_solver =
    8.24 @@ -265,7 +274,7 @@
    8.25    let
    8.26      val thy = Proof_Context.theory_of ctxt
    8.27      val (remote_provers, local_provers) =
    8.28 -      metis_prover_names @
    8.29 +      map fst metis_prover_infos @
    8.30        sort_strings (supported_atps thy) @
    8.31        sort_strings (SMT_Solver.available_solvers_of ctxt)
    8.32        |> List.partition (String.isPrefix remote_prefix)
    8.33 @@ -407,8 +416,11 @@
    8.34    in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
    8.35  
    8.36  fun tac_for_reconstructor Metis =
    8.37 -    Metis_Tactics.metis_tac [Metis_Tactics.default_unsound_type_sys]
    8.38 -  | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
    8.39 +    Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys]
    8.40 +  | tac_for_reconstructor Metis_Full_Types =
    8.41 +    Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
    8.42 +  | tac_for_reconstructor Metis_No_Types =
    8.43 +    Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
    8.44    | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
    8.45  
    8.46  fun timed_reconstructor reconstructor debug timeout ths =
    8.47 @@ -519,7 +531,9 @@
    8.48    (case preplay of
    8.49       Played (reconstructor, time) =>
    8.50       if Time.<= (time, metis_minimize_max_time) then
    8.51 -       reconstructor_name reconstructor
    8.52 +       case AList.find (op =) metis_prover_infos reconstructor of
    8.53 +         metis_name :: _ => metis_name
    8.54 +       | [] => name
    8.55       else
    8.56         name
    8.57     | _ => name)
    8.58 @@ -780,7 +794,7 @@
    8.59                          |> map snd
    8.60                in
    8.61                  play_one_line_proof debug preplay_timeout used_ths state subgoal
    8.62 -                                    [Metis, MetisFT]
    8.63 +                                    metis_reconstructors
    8.64                end,
    8.65             fn preplay =>
    8.66                let
    8.67 @@ -974,7 +988,7 @@
    8.68                  else "smt_solver = " ^ maybe_quote name
    8.69              in
    8.70                case play_one_line_proof debug preplay_timeout used_ths state
    8.71 -                                       subgoal [Metis, MetisFT] of
    8.72 +                                       subgoal metis_reconstructors of
    8.73                  p as Played _ => p
    8.74                | _ => Trust_Playable (SMT (smt_settings ()), NONE)
    8.75              end,
    8.76 @@ -1004,9 +1018,10 @@
    8.77  fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
    8.78                ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
    8.79    let
    8.80 -    val reconstructor = if name = Metis_Tactics.metisN then Metis
    8.81 -                        else if name = Metis_Tactics.metisFT_N then MetisFT
    8.82 -                        else raise Fail ("unknown Metis version: " ^ quote name)
    8.83 +    val reconstructor =
    8.84 +      case AList.lookup (op =) metis_prover_infos name of
    8.85 +        SOME r => r
    8.86 +      | NONE => raise Fail ("unknown Metis version: " ^ quote name)
    8.87      val (used_facts, used_ths) =
    8.88        facts |> map untranslated_fact |> ListPair.unzip
    8.89    in