# HG changeset patch # User blanchet # Date 1321446156 -3600 # Node ID cd6e78cb6ee847057374e8b2116e35d06f3ca013 # Parent 8ca7e3f25ee43436b8d4de436dbf6af3eb95c5c4 make metis reconstruction handling more flexible diff -r 8ca7e3f25ee4 -r cd6e78cb6ee8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r 8ca7e3f25ee4 -r cd6e78cb6ee8 src/HOL/Tools/ATP/atp_reconstruct.ML --- 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), diff -r 8ca7e3f25ee4 -r cd6e78cb6ee8 src/HOL/Tools/ATP/atp_translate.ML --- 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 diff -r 8ca7e3f25ee4 -r cd6e78cb6ee8 src/HOL/Tools/Metis/metis_tactic.ML --- 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) diff -r 8ca7e3f25ee4 -r cd6e78cb6ee8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 8ca7e3f25ee4 -r cd6e78cb6ee8 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 = diff -r 8ca7e3f25ee4 -r cd6e78cb6ee8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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}