--- 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;
--- 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
--- 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"),
--- 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 ""
--- 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