# HG changeset patch # User blanchet # Date 1307429555 -7200 # Node ID 2ed2f092e990084e18102fa650761169606a7d5e # Parent 359c190ede756284a171ccadcb4285c3b65eed40 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be diff -r 359c190ede75 -r 2ed2f092e990 NEWS --- a/NEWS Tue Jun 07 07:57:24 2011 +0200 +++ b/NEWS Tue Jun 07 08:52:35 2011 +0200 @@ -86,7 +86,8 @@ - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options. * Metis: - - Obsoleted "metisF" -- use "metis" instead. + - Removed "metisF" -- use "metis" instead. + - Obsoleted "metisFT" -- use "metis (full_types)" instead. * "try": - Added "simp:", "intro:", and "elim:" options. diff -r 359c190ede75 -r 2ed2f092e990 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 07:57:24 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 08:52:35 2011 +0200 @@ -495,30 +495,35 @@ set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger value or to try several provers and keep the nicest-looking proof. -\point{What is metisFT?} +\point{What is the \textit{full\_types}/\textit{no\_types} argument to Metis?} -The \textit{metisFT} proof method is the fully-typed version of Metis. It is -much slower than \textit{metis}, but the proof search is fully typed, and it -also includes more powerful rules such as the axiom ``$x = \mathit{True} -\mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places (e.g., -in set comprehensions). The method kicks in automatically as a fallback when -\textit{metis} fails, and it is sometimes generated by Sledgehammer instead of -\textit{metis} if the proof obviously requires type information or if -\textit{metis} failed when Sledgehammer preplayed the proof. (By default, -Sledgehammer tries to run \textit{metis} and/or \textit{metisFT} for 4 seconds -to ensure that the generated one-line proofs actually work and to display timing -information. This can be configured using the \textit{preplay\_timeout} option -(\S\ref{timeouts}).) +The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed +version of Metis. It is somewhat slower than \textit{metis}, but the proof +search is fully typed, and it also includes more powerful rules such as the +axiom ``$x = \mathit{True} \mathrel{\lor} x = \mathit{False}$'' for reasoning in +higher-order places (e.g., in set comprehensions). The method kicks in +automatically as a fallback when \textit{metis} fails, and it is sometimes +generated by Sledgehammer instead of \textit{metis} if the proof obviously +requires type information or if \textit{metis} failed when Sledgehammer +preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with +various options for up to 4 seconds to ensure that the generated one-line proofs +actually work and to display timing information. This can be configured using +the \textit{preplay\_timeout} option (\S\ref{timeouts}).) If you see the warning \prew \slshape -Metis: Falling back on ``\textit{metisFT\/}''. +Metis: Falling back on ``\textit{metis} (\textit{full\_types})''. \postw -in a successful Metis proof, you can advantageously replace the \textit{metis} -call with \textit{metisFT}. +in a successful Metis proof, you can advantageously pass the +\textit{full\_types} option to \textit{metis} directly. + +At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) +uses no type information at all during the proof search, which is more efficient +but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally +generated by Sledgehammer. \point{Are generated proofs minimal?} @@ -664,8 +669,8 @@ Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and \qty{facts} is a list of arbitrary facts. \qty{type\_sys} may also be \textit{full\_types}, in which case an appropriate type-sound encoding is -chosen. The companion proof method \textit{metisFT} is an abbreviation for -``\textit{metis}~(\textit{full\_types})''. +chosen, \textit{partial\_types} (the default), or \textit{no\_types}, a synonym +for \textit{erased}. \section{Option Reference} \label{option-reference} @@ -764,7 +769,11 @@ \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than the external provers, Metis itself can be used for proof search. -\item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis. +\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of +Metis, corresponding to \textit{metis} (\textit{full\_types}). + +\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis, +corresponding to \textit{metis} (\textit{no\_types}). \end{enum} In addition, the following remote provers are supported: @@ -903,14 +912,12 @@ arguments, to resolve overloading. \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is -tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. This -coincides with the encoding used by the \textit{metisFT} command. +tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):} Like for \textit{poly\_preds} constants are annotated with their types to resolve overloading, but otherwise no type information is encoded. This -coincides with the encoding used by the \textit{metis} command (before it falls -back on \textit{metisFT}). +coincides with the default encoding used by the \textit{metis} command. \item[$\bullet$] \textbf{% diff -r 359c190ede75 -r 2ed2f092e990 src/HOL/Metis_Examples/Clausification.thy --- a/src/HOL/Metis_Examples/Clausification.thy Tue Jun 07 07:57:24 2011 +0200 +++ b/src/HOL/Metis_Examples/Clausification.thy Tue Jun 07 08:52:35 2011 +0200 @@ -28,13 +28,13 @@ by (metis qax) lemma "\b. \a. (q b a \ q a b)" -by (metisFT qax) +by (metis (full_types) qax) lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" by (metis qax) lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" -by (metisFT qax) +by (metis (full_types) qax) declare [[metis_new_skolemizer]] @@ -42,13 +42,13 @@ by (metis qax) lemma "\b. \a. (q b a \ q a b)" -by (metisFT qax) +by (metis (full_types) qax) lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" by (metis qax) lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" -by (metisFT qax) +by (metis (full_types) qax) declare [[meson_max_clauses = 60]] @@ -64,7 +64,7 @@ by (metis rax) lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" -by (metisFT rax) +by (metis (full_types) rax) declare [[metis_new_skolemizer]] @@ -72,7 +72,7 @@ by (metis rax) lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" -by (metisFT rax) +by (metis (full_types) rax) lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ @@ -84,7 +84,7 @@ (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" -by (metisFT rax) +by (metis (full_types) rax) text {* Definitional CNF for goal *} @@ -100,7 +100,7 @@ lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" -by (metisFT pax) +by (metis (full_types) pax) declare [[metis_new_skolemizer]] @@ -110,7 +110,7 @@ lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" -by (metisFT pax) +by (metis (full_types) pax) text {* New Skolemizer *} @@ -134,7 +134,7 @@ assumes a: "Quotient R Abs Rep" shows "symp R" using a unfolding Quotient_def using sympI -by metisFT +by (metis (full_types)) lemma "(\x \ set xs. P x) \ diff -r 359c190ede75 -r 2ed2f092e990 src/HOL/Metis_Examples/Proxies.thy --- a/src/HOL/Metis_Examples/Proxies.thy Tue Jun 07 07:57:24 2011 +0200 +++ b/src/HOL/Metis_Examples/Proxies.thy Tue Jun 07 08:52:35 2011 +0200 @@ -66,7 +66,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (metisFT id_apply) +by (metis (full_types) id_apply) lemma "id True" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -127,7 +127,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] () sledgehammer [type_sys = mangled_preds?, expect = some] () sledgehammer [type_sys = mangled_preds, expect = some] () -by metisFT +by (metis (full_types)) lemma "id (\ a) \ \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) diff -r 359c190ede75 -r 2ed2f092e990 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 07 07:57:24 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 07 08:52:35 2011 +0200 @@ -342,7 +342,8 @@ (case AList.lookup (op =) args reconstructorK of SOME name => name | NONE => - if String.isSubstring "metisFT" msg then "metisFT" + if String.isSubstring "metis (full_types)" msg then "metis (full_types)" + else if String.isSubstring "metis (no_types)" msg then "metis (no_types)" else if String.isSubstring "metis" msg then "metis" else "smt") @@ -541,8 +542,10 @@ Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt) else if !reconstructor = "smt" then SMT_Solver.smt_tac - else if full orelse !reconstructor = "metisFT" then - Metis_Tactics.metisFT_tac + else if full orelse !reconstructor = "metis (full_types)" then + Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys] + else if !reconstructor = "metis (no_types)" then + Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys] else Metis_Tactics.metis_tac []) ctxt thms fun apply_reconstructor thms = diff -r 359c190ede75 -r 2ed2f092e990 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 07:57:24 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 08:52:35 2011 +0200 @@ -16,7 +16,8 @@ datatype reconstructor = Metis | - MetisFT | + Metis_Full_Types | + Metis_No_Types | SMT of string datatype play = @@ -67,7 +68,8 @@ datatype reconstructor = Metis | - MetisFT | + Metis_Full_Types | + Metis_No_Types | SMT of string datatype play = @@ -251,8 +253,10 @@ (** Soft-core proof reconstruction: Metis one-liner **) +(* unfortunate leaking abstraction *) fun reconstructor_name Metis = "metis" - | reconstructor_name MetisFT = "metisFT" + | reconstructor_name Metis_Full_Types = "metis (full_types)" + | reconstructor_name Metis_No_Types = "metis (no_types)" | reconstructor_name (SMT _) = "smt" fun reconstructor_settings (SMT settings) = settings @@ -1042,7 +1046,7 @@ else if member (op =) qs Show then "show" else "have") val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) - val reconstructor = if full_types then MetisFT else Metis + val reconstructor = if full_types then Metis_Full_Types else Metis fun do_facts (ls, ss) = reconstructor_command reconstructor 1 1 (ls |> sort_distinct (prod_ord string_ord int_ord), diff -r 359c190ede75 -r 2ed2f092e990 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Jun 07 07:57:24 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Jun 07 08:52:35 2011 +0200 @@ -10,14 +10,16 @@ signature METIS_TACTICS = sig val metisN : string - val metisFT_N : string - val default_unsound_type_sys : string - val default_sound_type_sys : string + val full_typesN : string + val partial_typesN : string + val no_typesN : string + val full_type_sys : string + val partial_type_sys : string + val no_type_sys : string val trace : bool Config.T val verbose : bool Config.T val new_skolemizer : bool Config.T val metis_tac : string list -> Proof.context -> thm list -> int -> tactic - val metisFT_tac : Proof.context -> thm list -> int -> tactic val setup : theory -> theory end @@ -29,18 +31,25 @@ open Metis_Reconstruct val metisN = Binding.qualified_name_of @{binding metis} -val metisFT_N = Binding.qualified_name_of @{binding metisFT} + val full_typesN = "full_types" +val partial_typesN = "partial_types" +val no_typesN = "no_types" -val default_unsound_type_sys = "poly_args" -val default_sound_type_sys = "poly_preds_heavy_query" +val full_type_sys = "poly_preds_heavy_query" +val partial_type_sys = "poly_args" +val no_type_sys = "erased" + +val type_sys_aliases = + [(full_typesN, full_type_sys), + (partial_typesN, partial_type_sys), + (no_typesN, no_type_sys)] fun method_call_for_type_sys type_sys = - if type_sys = default_sound_type_sys then - (@{binding metisFT}, "") - else - (@{binding metis}, - if type_sys = default_unsound_type_sys then "" else type_sys) + metisN ^ " (" ^ + (case AList.find (op =) type_sys_aliases type_sys of + [alias] => alias + | _ => type_sys) ^ ")" val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) @@ -168,13 +177,10 @@ (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg else "")) | type_sys :: _ => - let val (binding, arg) = method_call_for_type_sys type_sys in - (verbose_warning ctxt - ("Falling back on " ^ - quote (Binding.qualified_name_of binding ^ - (arg |> arg <> "" ? enclose " (" ")")) ^ "..."); - FOL_SOLVE fallback_type_syss ctxt cls ths0) - end + (verbose_warning ctxt + ("Falling back on " ^ + quote (method_call_for_type_sys type_sys) ^ "..."); + FOL_SOLVE fallback_type_syss ctxt cls ths0) val neg_clausify = single @@ -207,12 +213,11 @@ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 end -val metis_default_type_syss = [default_unsound_type_sys, default_sound_type_sys] -val metisFT_type_syss = [default_sound_type_sys] +val metis_default_type_syss = [partial_type_sys, full_type_sys] +val metisFT_type_syss = [full_type_sys] fun metis_tac [] = generic_metis_tac metis_default_type_syss | metis_tac type_syss = generic_metis_tac type_syss -val metisFT_tac = generic_metis_tac metisFT_type_syss (* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. @@ -224,6 +229,12 @@ fun method type_syss (type_sys, ths) ctxt facts = let + val _ = + if type_syss = metisFT_type_syss then + legacy_feature "Old 'metisFT' method -- \ + \use 'metis (full_types)' instead" + else + () val (schem_facts, nonschem_facts) = List.partition has_tvar facts val type_syss = type_sys |> Option.map single |> the_default type_syss in @@ -232,19 +243,20 @@ o generic_metis_tac type_syss ctxt (schem_facts @ ths)) end -fun setup_method (type_syss as type_sys :: _) = +fun setup_method (binding, type_syss as type_sys :: _) = (if type_syss = metis_default_type_syss then (Args.parens Parse.short_ident - >> (fn s => if s = full_typesN then default_sound_type_sys else s)) + >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s)) |> Scan.option |> Scan.lift else Scan.succeed NONE) -- Attrib.thms >> (METHOD oo method type_syss) - |> Method.setup (fst (method_call_for_type_sys type_sys)) + |> Method.setup binding val setup = - [(metis_default_type_syss, "Metis for FOL and HOL problems"), - (metisFT_type_syss, + [((@{binding metis}, metis_default_type_syss), + "Metis for FOL and HOL problems"), + ((@{binding metisFT}, metisFT_type_syss), "Metis for FOL/HOL problems with fully-typed translation")] |> fold (uncurry setup_method) diff -r 359c190ede75 -r 2ed2f092e990 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 07:57:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 08:52:35 2011 +0200 @@ -128,9 +128,18 @@ "Async_Manager". *) val das_tool = "Sledgehammer" -val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N] +val metisN = Metis_Tactics.metisN +val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN +val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN -val is_metis_prover = member (op =) metis_prover_names +val metis_prover_infos = + [(metisN, Metis), + (metis_full_typesN, Metis_Full_Types), + (metis_no_typesN, Metis_No_Types)] + +val metis_reconstructors = map snd metis_prover_infos + +val is_metis_prover = AList.defined (op =) metis_prover_infos val is_atp = member (op =) o supported_atps val select_smt_solver = @@ -265,7 +274,7 @@ let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = - metis_prover_names @ + map fst metis_prover_infos @ sort_strings (supported_atps thy) @ sort_strings (SMT_Solver.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) @@ -407,8 +416,11 @@ in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end fun tac_for_reconstructor Metis = - Metis_Tactics.metis_tac [Metis_Tactics.default_unsound_type_sys] - | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac + Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys] + | tac_for_reconstructor Metis_Full_Types = + Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys] + | tac_for_reconstructor Metis_No_Types = + Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys] | tac_for_reconstructor _ = raise Fail "unexpected reconstructor" fun timed_reconstructor reconstructor debug timeout ths = @@ -519,7 +531,9 @@ (case preplay of Played (reconstructor, time) => if Time.<= (time, metis_minimize_max_time) then - reconstructor_name reconstructor + case AList.find (op =) metis_prover_infos reconstructor of + metis_name :: _ => metis_name + | [] => name else name | _ => name) @@ -780,7 +794,7 @@ |> map snd in play_one_line_proof debug preplay_timeout used_ths state subgoal - [Metis, MetisFT] + metis_reconstructors end, fn preplay => let @@ -974,7 +988,7 @@ else "smt_solver = " ^ maybe_quote name in case play_one_line_proof debug preplay_timeout used_ths state - subgoal [Metis, MetisFT] of + subgoal metis_reconstructors of p as Played _ => p | _ => Trust_Playable (SMT (smt_settings ()), NONE) end, @@ -1004,9 +1018,10 @@ fun run_metis mode name ({debug, timeout, ...} : params) minimize_command ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let - val reconstructor = if name = Metis_Tactics.metisN then Metis - else if name = Metis_Tactics.metisFT_N then MetisFT - else raise Fail ("unknown Metis version: " ^ quote name) + val reconstructor = + case AList.lookup (op =) metis_prover_infos name of + SOME r => r + | NONE => raise Fail ("unknown Metis version: " ^ quote name) val (used_facts, used_ths) = facts |> map untranslated_fact |> ListPair.unzip in