--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 11:16:23 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 13:22:36 2011 +0100
@@ -343,10 +343,16 @@
(case AList.lookup (op =) args reconstructorK of
SOME name => name
| NONE =>
- 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")
+ if String.isSubstring "metis (" msg then
+ msg |> Substring.full
+ |> Substring.position "metis ("
+ |> snd |> Substring.position ")"
+ |> fst |> Substring.string
+ |> suffix ")"
+ else if String.isSubstring "metis" msg then
+ "metis"
+ else
+ "smt")
local
@@ -403,7 +409,8 @@
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
fun failed failure =
({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
- preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis),
+ preplay =
+ K (ATP_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail}
: Sledgehammer_Provers.prover_result,
@@ -577,14 +584,22 @@
ORELSE' Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
else if !reconstructor = "smt" then
SMT_Solver.smt_tac ctxt thms
- else if full orelse !reconstructor = "metis (full_types)" then
- Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc]
- ATP_Translate.combinatorsN ctxt thms
- else if !reconstructor = "metis (no_types)" then
- Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
- ATP_Translate.combinatorsN ctxt thms
+ else if full then
+ Metis_Tactic.metis_tac [ATP_Reconstruct.full_typesN]
+ ATP_Reconstruct.metis_default_lam_trans ctxt thms
+ else if String.isPrefix "metis (" (!reconstructor) then
+ let
+ val (type_encs, lam_trans) =
+ !reconstructor
+ |> Outer_Syntax.scan Position.start
+ |> filter Token.is_proper |> tl
+ |> Metis_Tactic.parse_metis_options |> fst
+ |>> the_default [ATP_Reconstruct.partial_typesN]
+ ||> the_default ATP_Reconstruct.metis_default_lam_trans
+ in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
else if !reconstructor = "metis" then
- Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
+ Metis_Tactic.metis_tac [] ATP_Reconstruct.metis_default_lam_trans ctxt
+ thms
else
K all_tac
end
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Nov 16 11:16:23 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Nov 16 13:22:36 2011 +0100
@@ -14,9 +14,7 @@
type locality = ATP_Translate.locality
datatype reconstructor =
- Metis |
- Metis_Full_Types |
- Metis_No_Types |
+ Metis of string * string |
SMT
datatype play =
@@ -30,6 +28,17 @@
type isar_params =
bool * bool * int * string Symtab.table * int list list * int
* (string * locality) list vector * int Symtab.table * string proof * thm
+
+ val metisN : string
+ val full_typesN : string
+ val partial_typesN : string
+ val no_typesN : string
+ val really_full_type_enc : string
+ val full_type_enc : string
+ val partial_type_enc : string
+ val no_type_enc : string
+ val full_type_encs : string list
+ val partial_type_encs : string list
val used_facts_in_atp_proof :
Proof.context -> int -> (string * locality) list vector -> string proof
-> (string * locality) list
@@ -37,6 +46,9 @@
Proof.context -> int list list -> int -> (string * locality) list vector
-> 'a proof -> string list option
val uses_typed_helpers : int list -> 'a proof -> bool
+ val unalias_type_enc : string -> string list
+ val metis_default_lam_trans : string
+ val metis_call : string -> string -> string
val name_of_reconstructor : reconstructor -> string
val one_line_proof_text : one_line_params -> string
val make_tvar : string -> typ
@@ -62,9 +74,7 @@
open ATP_Translate
datatype reconstructor =
- Metis |
- Metis_Full_Types |
- Metis_No_Types |
+ Metis of string * string |
SMT
datatype play =
@@ -190,10 +200,44 @@
(** Soft-core proof reconstruction: Metis one-liner **)
+val metisN = "metis"
+
+val full_typesN = "full_types"
+val partial_typesN = "partial_types"
+val no_typesN = "no_types"
+
+val really_full_type_enc = "mono_tags"
+val full_type_enc = "poly_guards_query"
+val partial_type_enc = "poly_args"
+val no_type_enc = "erased"
+
+val full_type_encs = [full_type_enc, really_full_type_enc]
+val partial_type_encs = partial_type_enc :: full_type_encs
+
+val type_enc_aliases =
+ [(full_typesN, full_type_encs),
+ (partial_typesN, partial_type_encs),
+ (no_typesN, [no_type_enc])]
+
+fun unalias_type_enc s =
+ AList.lookup (op =) type_enc_aliases s |> the_default [s]
+
+val metis_default_lam_trans = combinatorsN
+
+fun metis_call type_enc lam_trans =
+ let
+ val type_enc =
+ case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases
+ type_enc of
+ [alias] => alias
+ | _ => type_enc
+ val opts = [] |> type_enc <> Metis_Tactic.partial_typesN ? cons type_enc
+ |> lam_trans <> metis_default_lam_trans ? cons lam_trans
+ in "metis" ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
+
(* unfortunate leaking abstraction *)
-fun name_of_reconstructor Metis = "metis"
- | name_of_reconstructor Metis_Full_Types = "metis (full_types)"
- | name_of_reconstructor Metis_No_Types = "metis (no_types)"
+fun name_of_reconstructor (Metis (type_enc, lam_trans)) =
+ metis_call type_enc lam_trans
| name_of_reconstructor SMT = "smt"
fun string_for_label (s, num) = s ^ string_of_int num
@@ -964,7 +1008,9 @@
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 Metis_Full_Types else Metis
+ val reconstructor =
+ Metis (if full_types then Metis_Tactic.full_typesN
+ else Metis_Tactic.partial_typesN, combinatorsN)
fun do_facts (ls, ss) =
reconstructor_command reconstructor 1 1
(ls |> sort_distinct (prod_ord string_ord int_ord),
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Nov 16 11:16:23 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Nov 16 13:22:36 2011 +0100
@@ -1692,7 +1692,7 @@
else if lam_trans = keep_lamsN then
map (Envir.eta_contract) #> rpair []
else
- error ("Unknown lambda translation method: " ^ quote lam_trans ^ ".")
+ error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
concl_t facts =
@@ -2348,7 +2348,7 @@
if is_type_enc_higher_order type_enc then keep_lamsN else combinatorsN
else if lam_trans = keep_lamsN andalso
not (is_type_enc_higher_order type_enc) then
- error ("Lambda translation method incompatible with first-order \
+ error ("Lambda translation scheme incompatible with first-order \
\encoding.")
else
lam_trans
--- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Nov 16 11:16:23 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Wed Nov 16 13:22:36 2011 +0100
@@ -9,22 +9,13 @@
signature METIS_TACTIC =
sig
- val metisN : string
- val full_typesN : string
- val partial_typesN : string
- val no_typesN : string
- val really_full_type_enc : string
- val full_type_enc : string
- val partial_type_enc : string
- val no_type_enc : string
- val full_type_syss : string list
- val partial_type_syss : string list
val trace : bool Config.T
val verbose : bool Config.T
val new_skolemizer : bool Config.T
val type_has_top_sort : typ -> bool
val metis_tac :
string list -> string -> Proof.context -> thm list -> int -> tactic
+ val parse_metis_options : (string list option * string option) parser
val setup : theory -> theory
end
@@ -32,38 +23,10 @@
struct
open ATP_Translate
+open ATP_Reconstruct
open Metis_Translate
open Metis_Reconstruct
-val metisN = "metis"
-
-val full_typesN = "full_types"
-val partial_typesN = "partial_types"
-val no_typesN = "no_types"
-
-val really_full_type_enc = "mono_tags"
-val full_type_enc = "poly_guards_query"
-val partial_type_enc = "poly_args"
-val no_type_enc = "erased"
-
-val full_type_syss = [full_type_enc, really_full_type_enc]
-val partial_type_syss = partial_type_enc :: full_type_syss
-
-val type_enc_aliases =
- [(full_typesN, full_type_syss),
- (partial_typesN, partial_type_syss),
- (no_typesN, [no_type_enc])]
-
-val lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
-val default_lam_trans = combinatorsN
-
-fun method_call_for type_syss lam_trans =
- metisN ^ " (" ^
- (case AList.find (op =) type_enc_aliases type_syss of
- [alias] => alias
- | _ => hd type_syss) ^
- (if lam_trans = default_lam_trans then "" else ", " ^ lam_trans) ^ ")"
-
val new_skolemizer =
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
@@ -135,7 +98,7 @@
val resolution_params = {active = active_params, waiting = waiting_params}
(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE (type_enc :: fallback_type_syss) lam_trans ctxt cls ths0 =
+fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
let val thy = Proof_Context.theory_of ctxt
val new_skolemizer =
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
@@ -211,7 +174,7 @@
end
| Metis_Resolution.Satisfiable _ =>
(trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
- if null fallback_type_syss then
+ if null fallback_type_encs then
()
else
raise METIS ("FOL_SOLVE",
@@ -219,15 +182,15 @@
[])
end
handle METIS (loc, msg) =>
- case fallback_type_syss of
+ case fallback_type_encs of
[] => error ("Failed to replay Metis proof in Isabelle." ^
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
else ""))
- | _ =>
+ | first_fallback :: _ =>
(verbose_warning ctxt
("Falling back on " ^
- quote (method_call_for fallback_type_syss lam_trans) ^ "...");
- FOL_SOLVE fallback_type_syss lam_trans ctxt cls ths0)
+ quote (metis_call first_fallback lam_trans) ^ "...");
+ FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0)
fun neg_clausify ctxt combinators =
single
@@ -246,13 +209,14 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-fun generic_metis_tac type_syss lam_trans ctxt ths i st0 =
+fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
let
val _ = trace_msg ctxt (fn () =>
"Metis called with theorems\n" ^
cat_lines (map (Display.string_of_thm ctxt) ths))
+ val type_encs = type_encs |> maps unalias_type_enc
fun tac clause =
- resolve_tac (FOL_SOLVE type_syss lam_trans ctxt clause ths) 1
+ resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
in
if exists_type type_has_top_sort (prop_of st0) then
verbose_warning ctxt "Proof state contains the universal sort {}"
@@ -262,8 +226,8 @@
(maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0
end
-fun metis_tac [] = generic_metis_tac partial_type_syss
- | metis_tac type_syss = generic_metis_tac type_syss
+fun metis_tac [] = generic_metis_tac partial_type_encs
+ | metis_tac type_encs = generic_metis_tac type_encs
(* 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.
@@ -273,44 +237,45 @@
val has_tvar =
exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
-fun method default_type_syss ((override_type_syss, lam_trans), ths) ctxt facts =
+fun method default_type_encs ((override_type_encs, lam_trans), ths) ctxt facts =
let
val _ =
- if default_type_syss = full_type_syss then
+ if default_type_encs = full_type_encs 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 = override_type_syss |> the_default default_type_syss
- val lam_trans = lam_trans |> the_default default_lam_trans
+ val type_encs = override_type_encs |> the_default default_type_encs
+ val lam_trans = lam_trans |> the_default metis_default_lam_trans
in
HEADGOAL (Method.insert_tac nonschem_facts THEN'
- CHANGED_PROP o generic_metis_tac type_syss lam_trans ctxt
+ CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt
(schem_facts @ ths))
end
-fun consider_arg s =
- if member (op =) lam_transs s then
- apsnd (K (SOME s))
- else
- apfst (K (SOME (AList.lookup (op =) type_enc_aliases s |> the_default [s])))
+val lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
+
+fun consider_opt s =
+ if member (op =) lam_transs s then apsnd (K (SOME s))
+ else apfst (K (SOME [s]))
-fun setup_method (binding, type_syss) =
- (Scan.lift (Scan.optional
- (Args.parens (Parse.short_ident
- -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
- >> (fn (s, s') =>
- (NONE, NONE)
- |> consider_arg s
- |> (case s' of SOME s' => consider_arg s' | _ => I)))
- (NONE, NONE)))
- -- Attrib.thms >> (METHOD oo method type_syss)
+val parse_metis_options =
+ Scan.optional
+ (Args.parens (Parse.short_ident
+ -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
+ >> (fn (s, s') =>
+ (NONE, NONE) |> consider_opt s
+ |> (case s' of SOME s' => consider_opt s' | _ => I)))
+ (NONE, NONE)
+
+fun setup_method (binding, type_encs) =
+ Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo method type_encs)
|> Method.setup binding
val setup =
- [((@{binding metis}, partial_type_syss),
+ [((@{binding metis}, partial_type_encs),
"Metis for FOL and HOL problems"),
- ((@{binding metisFT}, full_type_syss),
+ ((@{binding metisFT}, full_type_encs),
"Metis for FOL/HOL problems with fully-typed translation")]
|> fold (uncurry setup_method)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 16 11:16:23 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 16 13:22:36 2011 +0100
@@ -22,6 +22,7 @@
open ATP_Util
open ATP_Systems
open ATP_Translate
+open ATP_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Filter
open Sledgehammer_Provers
@@ -310,7 +311,7 @@
(* Sledgehammer the given subgoal *)
-val default_minimize_prover = Metis_Tactic.metisN
+val default_minimize_prover = metisN
fun is_raw_param_relevant_for_minimize (name, _) =
member (op =) params_for_minimize name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 11:16:23 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 13:22:36 2011 +0100
@@ -205,7 +205,7 @@
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg =>
- (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg, ""))
+ (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
end
fun run_minimize (params as {provers, ...}) i refs state =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 11:16:23 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 13:22:36 2011 +0100
@@ -76,6 +76,7 @@
val smt_slice_time_frac : real Config.T
val smt_slice_min_secs : int Config.T
val das_tool : string
+ val plain_metis : reconstructor
val select_smt_solver : string -> Proof.context -> Proof.context
val prover_name_for_reconstructor : reconstructor -> string
val is_reconstructor : string -> bool
@@ -128,15 +129,16 @@
"Async_Manager". *)
val das_tool = "Sledgehammer"
-val metisN = Metis_Tactic.metisN
-val metis_full_typesN = metisN ^ "_" ^ Metis_Tactic.full_typesN
-val metis_no_typesN = metisN ^ "_" ^ Metis_Tactic.no_typesN
+val metisN = metisN
+val metis_full_typesN = metisN ^ "_" ^ full_typesN
+val metis_no_typesN = metisN ^ "_" ^ no_typesN
val smtN = name_of_reconstructor SMT
+val plain_metis = Metis (hd partial_type_encs, combinatorsN)
val reconstructor_infos =
- [(metisN, Metis),
- (metis_full_typesN, Metis_Full_Types),
- (metis_no_typesN, Metis_No_Types),
+ [(metisN, plain_metis),
+ (metis_full_typesN, Metis (hd full_type_encs, combinatorsN)),
+ (metis_no_typesN, Metis (no_type_enc, combinatorsN)),
(smtN, SMT)]
val prover_name_for_reconstructor = AList.find (op =) reconstructor_infos #> hd
@@ -410,12 +412,8 @@
val full_tac = Method.insert_tac facts i THEN tac ctxt i
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
-fun tac_for_reconstructor Metis =
- Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc] combinatorsN
- | tac_for_reconstructor Metis_Full_Types =
- Metis_Tactic.metis_tac Metis_Tactic.full_type_syss combinatorsN
- | tac_for_reconstructor Metis_No_Types =
- Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] combinatorsN
+fun tac_for_reconstructor (Metis (type_enc, lam_trans)) =
+ Metis_Tactic.metis_tac [type_enc] lam_trans
| tac_for_reconstructor SMT = SMT_Solver.smt_tac
fun timed_reconstructor reconstructor debug timeout ths =
@@ -787,7 +785,7 @@
|> map snd
in
play_one_line_proof mode debug verbose preplay_timeout used_ths
- state subgoal Metis all_reconstructors
+ state subgoal plain_metis all_reconstructors
end,
fn preplay =>
let
@@ -812,7 +810,8 @@
""))
end
| SOME failure =>
- ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
+ ([], K (Failed_to_Play plain_metis),
+ fn _ => string_for_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}
@@ -980,7 +979,7 @@
else
"")
| SOME failure =>
- (K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
+ (K (Failed_to_Play plain_metis), fn _ => string_for_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}