# HG changeset patch # User blanchet # Date 1306485008 -7200 # Node ID 18259246abb5a317419e01460fcfd8d5a483288a # Parent c4b9b4be90c4b583c3b7bf4d3a6a689e7c1aa06a try both "metis" and (on failure) "metisFT" in replay diff -r c4b9b4be90c4 -r 18259246abb5 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Fri May 27 10:30:08 2011 +0200 @@ -16,6 +16,7 @@ val metis_tac : Proof.context -> thm list -> int -> tactic val metisF_tac : Proof.context -> thm list -> int -> tactic val metisFT_tac : Proof.context -> thm list -> int -> tactic + val metisHO_tac : Proof.context -> thm list -> int -> tactic val setup : theory -> theory end @@ -52,8 +53,12 @@ models = []} val resolution_params = {active = active_params, waiting = waiting_params} +fun method_binding_for_mode HO = @{binding metis} + | method_binding_for_mode FO = @{binding metisF} + | method_binding_for_mode FT = @{binding metisFT} + (* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE mode ctxt cls ths0 = +fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt val type_lits = Config.get ctxt type_lits val new_skolemizer = @@ -116,21 +121,23 @@ end | Metis_Resolution.Satisfiable _ => (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); - if mode <> FT then + if null fallback_modes then + () + else raise METIS ("FOL_SOLVE", - "No first-order proof with the lemmas supplied") - else - (); + "No first-order proof with the lemmas supplied"); []) end handle METIS (loc, msg) => - if mode <> FT then - (verbose_warning ctxt ("Falling back on \"metisFT\"."); - FOL_SOLVE FT ctxt cls ths0) - else - error ("Failed to replay Metis proof in Isabelle." ^ - (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg - else "")) + case fallback_modes of + [] => error ("Failed to replay Metis proof in Isabelle." ^ + (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg + else "")) + | mode :: _ => + (verbose_warning ctxt + ("Falling back on " ^ + quote (Binding.str_of (method_binding_for_mode mode)) ^ "..."); + FOL_SOLVE fallback_modes ctxt cls ths0) val neg_clausify = single @@ -149,23 +156,30 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) -fun generic_metis_tac mode ctxt ths i st0 = +fun generic_metis_tac modes ctxt ths i st0 = let val _ = trace_msg ctxt (fn () => - "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) + "Metis called with theorems " ^ + cat_lines (map (Display.string_of_thm ctxt) ths)) in if exists_type type_has_top_sort (prop_of st0) then (verbose_warning ctxt "Proof state contains the universal sort {}"; Seq.empty) else Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) - (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) + (fn cls => resolve_tac (FOL_SOLVE modes ctxt cls ths) 1) ctxt i st0 end -val metis_tac = generic_metis_tac HO -val metisF_tac = generic_metis_tac FO -val metisFT_tac = generic_metis_tac FT +val metis_modes = [HO, FT] +val metisF_modes = [FO, FT] +val metisFT_modes = [FT] +val metisHO_modes = [HO] + +val metis_tac = generic_metis_tac metis_modes +val metisF_tac = generic_metis_tac metisF_modes +val metisFT_tac = generic_metis_tac metisFT_modes +val metisHO_tac = generic_metis_tac metisHO_modes (* 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. @@ -174,22 +188,24 @@ applied) and brings few benefits. *) val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of -fun method name mode = - Method.setup name (Attrib.thms >> (fn ths => fn ctxt => - METHOD (fn facts => - let - val (schem_facts, nonschem_facts) = - List.partition has_tvar facts - in - HEADGOAL (Method.insert_tac nonschem_facts THEN' - CHANGED_PROP - o generic_metis_tac mode ctxt (schem_facts @ ths)) - end))) + +fun setup_method (modes as mode :: _) = + Method.setup (method_binding_for_mode mode) + (Attrib.thms >> (fn ths => fn ctxt => + METHOD (fn facts => + let + val (schem_facts, nonschem_facts) = + List.partition has_tvar facts + in + HEADGOAL (Method.insert_tac nonschem_facts THEN' + CHANGED_PROP + o generic_metis_tac modes ctxt (schem_facts @ ths)) + end))) val setup = - method @{binding metis} HO "Metis for FOL/HOL problems" - #> method @{binding metisF} FO "Metis for FOL problems" - #> method @{binding metisFT} FT - "Metis for FOL/HOL problems with fully-typed translation" + [(metis_modes, "Metis for FOL and HOL problems"), + (metisF_modes, "Metis for FOL problems"), + (metisFT_modes, "Metis for FOL/HOL problems with fully-typed translation")] + |> fold (uncurry setup_method) end; diff -r c4b9b4be90c4 -r 18259246abb5 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:08 2011 +0200 @@ -20,7 +20,7 @@ datatype preplay = Preplayed of reconstructor * Time.time | Trust_Playable of reconstructor * Time.time option| - Preplay_Failed + Failed_to_Preplay type minimize_command = string list -> string type one_line_params = @@ -73,7 +73,7 @@ datatype preplay = Preplayed of reconstructor * Time.time | Trust_Playable of reconstructor * Time.time option | - Preplay_Failed + Failed_to_Preplay type minimize_command = string list -> string type one_line_params = @@ -261,7 +261,7 @@ fun string_for_label (s, num) = s ^ string_of_int num fun show_time NONE = "" - | show_time (SOME ext_time) = " ~ " ^ string_from_ext_time ext_time + | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")" fun set_settings "" = "" | set_settings settings = "using [[" ^ settings ^ "]] " @@ -304,7 +304,7 @@ NONE => NONE | SOME time => if time = Time.zeroTime then NONE else SOME (true, time)) - | Preplay_Failed => (NONE, NONE) + | Failed_to_Preplay => (NONE, NONE) val n = Logic.count_prems (prop_of goal) val try_line = case reconstructor of @@ -1085,7 +1085,7 @@ fun proof_text ctxt isar_proof isar_params (one_line_params as (preplay, _, _, _, _, _)) = - (if isar_proof orelse preplay = Preplay_Failed then + (if isar_proof orelse preplay = Failed_to_Preplay then isar_proof_text ctxt isar_params else one_line_proof_text) one_line_params diff -r c4b9b4be90c4 -r 18259246abb5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200 @@ -100,7 +100,7 @@ ("isar_proof", "false"), ("isar_shrink_factor", "1"), ("slicing", "true"), - ("preplay_timeout", "5")] + ("preplay_timeout", "4")] val alias_params = [("prover", "provers"), diff -r c4b9b4be90c4 -r 18259246abb5 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200 @@ -382,24 +382,36 @@ | Minimize => "Try this" (* based on "Mirabelle.can_apply" and generalized *) -fun try_apply timeout tac state i = +fun timed_apply timeout tac state i = let val {context = ctxt, facts, goal} = Proof.goal state val full_tac = Method.insert_tac facts i THEN tac ctxt i - in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end + in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end -fun try_metis debug timeout ths = - try_apply timeout (Config.put Metis_Tactics.verbose debug - #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) +fun tac_for_reconstructor Metis = Metis_Tactics.metisHO_tac + | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac + | tac_for_reconstructor _ = raise Fail "unexpected reconstructor" + +fun timed_reconstructor reconstructor debug timeout ths = + (Config.put Metis_Tactics.verbose debug + #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths)) + |> timed_apply timeout fun filter_used_facts used = filter (member (op =) used o fst) -fun preplay_one_line_proof debug reconstructor_guess timeout ths state i = - let val timer = Timer.startRealTimer () in - case try_metis debug timeout ths state i of - SOME (SOME _) => Preplayed (Metis, Timer.checkRealTimer timer) - | SOME NONE => Preplay_Failed - | NONE => Trust_Playable (reconstructor_guess, SOME timeout) +fun preplay_one_line_proof debug timeout ths state i reconstructor = + let + fun preplay reconstructor = + let val timer = Timer.startRealTimer () in + case timed_reconstructor reconstructor debug timeout ths state i of + SOME (SOME _) => Preplayed (reconstructor, Timer.checkRealTimer timer) + | _ => + if reconstructor = Metis then preplay MetisFT else Failed_to_Preplay + end + handle TimeLimit.TimeOut => Trust_Playable (reconstructor, SOME timeout) + in + if timeout = Time.zeroTime then Trust_Playable (reconstructor, NONE) + else preplay reconstructor end @@ -749,15 +761,15 @@ val used_facts = used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof - val reconstructor_guess = + val reconstructor = if uses_typed_helpers typed_helpers atp_proof then MetisFT else Metis val ths = facts |> map untranslated_fact |> filter_used_facts used_facts |> map snd val preplay = - preplay_one_line_proof debug reconstructor_guess preplay_timeout ths - state subgoal + preplay_one_line_proof debug preplay_timeout ths state subgoal + reconstructor val full_types = uses_typed_helpers typed_helpers atp_proof val isar_params = (debug, full_types, isar_shrink_factor, type_sys, pool, @@ -932,8 +944,8 @@ NONE => let val (settings, method, time) = - case preplay_one_line_proof debug Metis preplay_timeout - (map snd used_facts) state subgoal of + case preplay_one_line_proof debug preplay_timeout + (map snd used_facts) state subgoal Metis of Preplayed (method, time) => ("", reconstructor_name method, SOME (false, time)) | _ => (if name = SMT_Solver.solver_name_of ctxt then "" diff -r c4b9b4be90c4 -r 18259246abb5 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:08 2011 +0200 @@ -61,8 +61,8 @@ fun parse_time_option _ "none" = NONE | parse_time_option name s = let val secs = if has_junk s then NONE else Real.fromString s in - if is_none secs orelse Real.<= (the secs, 0.0) then - error ("Parameter " ^ quote name ^ " must be assigned a positive \ + if is_none secs orelse Real.< (the secs, 0.0) then + error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \ \number of seconds (e.g., \"60\", \"0.5\") or \"none\".") else SOME (seconds (the secs)) @@ -70,9 +70,13 @@ fun string_from_ext_time (plus, time) = let val ms = Time.toMilliseconds time in - if plus then signed_string_of_int ((ms + 999) div 1000) ^ "+ s" - else if ms < 1000 then signed_string_of_int ms ^ " ms" - else string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s" + (if plus then "> " else "") ^ + (if plus andalso ms mod 1000 = 0 then + signed_string_of_int (ms div 1000) ^ " s" + else if ms < 1000 then + signed_string_of_int ms ^ " ms" + else + string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s") end val string_from_time = string_from_ext_time o pair false