--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jul 30 23:52:56 2014 +0200
@@ -78,8 +78,8 @@
val is_fact_chained : (('a * stature) * 'b) -> bool
val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
- val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
- Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
+ val play_one_line_proof : mode -> Time.time -> ((string * 'a) * thm) list -> Proof.state -> int ->
+ proof_method -> proof_method list -> proof_method * play_outcome
val isar_supported_prover_of : theory -> string -> string
val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
string -> proof_method * play_outcome -> 'a
@@ -104,6 +104,8 @@
open Metis_Tactic
open Sledgehammer_Fact
open Sledgehammer_Proof_Methods
+open Sledgehammer_Isar_Proof
+open Sledgehammer_Isar_Preplay
(* Identifier that distinguishes Sledgehammer from other tools that could use
"Async_Manager". *)
@@ -206,47 +208,37 @@
in (metisN, override_params) end
| extract_proof_method _ SMT2_Method = (smtN, [])
-(* based on "Mirabelle.can_apply" and generalized *)
-fun timed_apply timeout tac state i =
+fun preplay_methods timeout facts meths state i =
let
- val {context = ctxt, facts, goal} = Proof.goal state
- val full_tac = Method.insert_tac facts i THEN tac ctxt i
+ val {context = ctxt, facts = chained, goal} = Proof.goal state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
+ val step =
+ Prove ([], [], ("", 0), Logic.list_implies (map prop_of chained @ hyp_ts, concl_t), [],
+ ([], facts), meths, "")
in
- TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
+ preplay_isar_step ctxt timeout [] step
end
-fun timed_proof_method timeout ths meth =
- timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
-
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
fun filter_used_facts keep_chained used =
filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
-fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) =
+fun play_one_line_proof mode timeout used_facts state i preferred (meths as meth :: _) =
let
- val ctxt = Proof.context_of state
-
- fun get_preferred meths = if member (op =) meths preferred then preferred else meth
+ fun dont_know () =
+ (if member (op =) meths preferred then preferred else meth, Play_Timed_Out Time.zeroTime)
in
if timeout = Time.zeroTime then
- (get_preferred meths, Play_Timed_Out Time.zeroTime)
+ dont_know ()
else
let
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
- val ths = pairs |> sort_wrt (fst o fst) |> map snd
-
- fun play [] [] = (get_preferred meths, Play_Failed)
- | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
- | play timed_out (meth :: meths) =
- let val timer = Timer.startRealTimer () in
- (case timed_proof_method timeout ths meth state i of
- SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
- | _ => play timed_out meths)
- end
- handle TimeLimit.TimeOut => play (meth :: timed_out) meths
+ val gfs = used_facts |> map (fst o fst) |> sort string_ord
in
- play [] meths
+ (case preplay_methods timeout gfs meths state i of
+ res :: _ => res
+ | [] => dont_know ())
end
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Jul 30 23:52:56 2014 +0200
@@ -368,8 +368,7 @@
(used_facts,
Lazy.lazy (fn () =>
let val used_pairs = used_from |> filter_used_facts false used_facts in
- play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths)
- meths
+ play_one_line_proof mode preplay_timeout used_pairs state subgoal (hd meths) meths
end),
fn preplay =>
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Jul 30 23:52:56 2014 +0200
@@ -48,7 +48,7 @@
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_SMT2
-fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...})
+fun run_proof_method mode name (params as {timeout, type_enc, lam_trans, ...})
minimize_command
({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
let
@@ -58,8 +58,8 @@
else raise Fail ("unknown proof_method: " ^ quote name)
val used_facts = facts |> map fst
in
- (case play_one_line_proof (if mode = Minimize then Normal else mode) verbose timeout facts state
- subgoal meth [meth] of
+ (case play_one_line_proof (if mode = Minimize then Normal else mode) timeout facts state subgoal
+ meth [meth] of
play as (_, Played time) =>
{outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
preplay = Lazy.value play,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Wed Jul 30 23:52:56 2014 +0200
@@ -196,10 +196,12 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode verbose preplay_timeout used_named_facts state subgoal
- SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+ play_one_line_proof mode preplay_timeout used_named_facts state subgoal SMT2_Method
+ (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
+ val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+
fun isar_params () =
(verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
goal)