# HG changeset patch # User blanchet # Date 1406757176 -7200 # Node ID 668322cd58f47c3e1582f5b7c42e16bd0e41ccbb # Parent 2c2d5b7f29aa9da29cda8856eb71b4b84769bcb7 use parallel preplay machinery also for one-line proofs diff -r 2c2d5b7f29aa -r 668322cd58f4 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 diff -r 2c2d5b7f29aa -r 668322cd58f4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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 diff -r 2c2d5b7f29aa -r 668322cd58f4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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, diff -r 2c2d5b7f29aa -r 668322cd58f4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- 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)