# HG changeset patch # User blanchet # Date 1400722176 -7200 # Node ID fed0329ea8e2b1b446245afe13ea59f1127a2ed4 # Parent 46000c075d07961a878b63dfe8046d487334e04e tuning diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 03:29:36 2014 +0200 @@ -289,7 +289,7 @@ val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty val _ = fold_isar_steps (fn meth => - K (set_preplay_outcomes_of_isar_step ctxt debug preplay_timeout preplay_data meth [])) + K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) (steps_of_isar_proof canonical_isar_proof) () fun str_of_preplay_outcome outcome = @@ -316,11 +316,11 @@ val (play_outcome, isar_proof) = canonical_isar_proof |> tap (trace_isar_proof "Original") - |> compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data + |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data |> tap (trace_isar_proof "Compressed") |> postprocess_isar_proof_remove_unreferenced_steps (keep_fastest_method_of_isar_step (!preplay_data) - #> minimize ? minimize_isar_step_dependencies ctxt debug preplay_data) + #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |> tap (trace_isar_proof "Minimized") (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an unnatural semantics): *) diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu May 22 03:29:36 2014 +0200 @@ -11,7 +11,7 @@ type isar_proof = Sledgehammer_Isar_Proof.isar_proof type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data - val compress_isar_proof : Proof.context -> bool -> real -> Time.time -> + val compress_isar_proof : Proof.context -> real -> Time.time -> isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof end; @@ -109,7 +109,7 @@ val compress_degree = 2 (* Precondition: The proof must be labeled canonically. *) -fun compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data proof = +fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof = if compress_isar <= 1.0 then proof else @@ -172,12 +172,11 @@ (* check if the modified step can be preplayed fast enough *) val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l')) in - (case preplay_isar_step ctxt debug timeout hopeless step'' of + (case preplay_isar_step ctxt timeout hopeless step'' of meths_outcomes as (_, Played time'') :: _ => (* l' successfully eliminated *) (decrement_step_count (); - set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step'' - meths_outcomes; + set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes; map (replace_successor l' [l]) lfs'; elim_one_subproof time'' step'' subs nontriv_subs) | _ => elim_one_subproof time step subs (sub :: nontriv_subs)) @@ -217,15 +216,14 @@ val timeouts = map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0 val meths_outcomess = - map3 (preplay_isar_step ctxt debug) timeouts hopelesses succs' + map3 (preplay_isar_step ctxt) timeouts hopelesses succs' in (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of NONE => steps | SOME times => (* candidate successfully eliminated *) (decrement_step_count (); - map3 (fn time => - set_preplay_outcomes_of_isar_step ctxt debug time preplay_data) + map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times succs' meths_outcomess; map (replace_successor l labels) lfs; steps_before @ update_steps succs' steps_after)) diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu May 22 03:29:36 2014 +0200 @@ -12,8 +12,8 @@ type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step - val minimize_isar_step_dependencies : Proof.context -> bool -> - isar_preplay_data Unsynchronized.ref -> isar_step -> isar_step + val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> + isar_step -> isar_step val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof end; @@ -34,7 +34,7 @@ val slack = seconds 0.025 -fun minimize_isar_step_dependencies ctxt debug preplay_data +fun minimize_isar_step_dependencies ctxt preplay_data (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) = (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of Played time => @@ -43,7 +43,7 @@ fun minimize_facts _ min_facts [] time = (min_facts, time) | minimize_facts mk_step min_facts (fact :: facts) time = - (case preplay_isar_step_for_method ctxt debug (Time.+ (time, slack)) meth + (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth (mk_step (min_facts @ facts)) of Played time' => minimize_facts mk_step min_facts facts time' | _ => minimize_facts mk_step (fact :: min_facts) facts time) @@ -53,12 +53,11 @@ val step' = mk_step_lfs_gfs min_lfs min_gfs in - set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step' - [(meth, Played time'')]; + set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')]; step' end | _ => step (* don't touch steps that time out or fail *)) - | minimize_isar_step_dependencies _ _ _ step = step + | minimize_isar_step_dependencies _ _ step = step fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = let diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu May 22 03:29:36 2014 +0200 @@ -18,11 +18,11 @@ type isar_preplay_data val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context - val preplay_isar_step_for_method : Proof.context -> bool -> Time.time -> proof_method -> - isar_step -> play_outcome - val preplay_isar_step : Proof.context -> bool -> Time.time -> proof_method list -> isar_step -> + val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step -> + play_outcome + val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step -> (proof_method * play_outcome) list - val set_preplay_outcomes_of_isar_step : Proof.context -> bool -> Time.time -> + val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time -> isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method -> @@ -101,8 +101,7 @@ end (* may throw exceptions *) -fun raw_preplay_step_for_method ctxt debug timeout meth - (Prove (_, xs, _, t, subproofs, facts, _, _)) = +fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) = let val goal = (case xs of @@ -129,7 +128,7 @@ fun prove () = Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => - HEADGOAL (tac_of_proof_method ctxt debug assmsp meth)) + HEADGOAL (tac_of_proof_method ctxt assmsp meth)) handle ERROR msg => error ("Preplay error: " ^ msg) val play_outcome = take_time timeout prove () @@ -138,13 +137,13 @@ play_outcome end -fun preplay_isar_step_for_method ctxt debug timeout meth = - try (raw_preplay_step_for_method ctxt debug timeout meth) #> the_default Play_Failed +fun preplay_isar_step_for_method ctxt timeout meth = + try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed -fun preplay_isar_step ctxt debug timeout hopeless step = +fun preplay_isar_step ctxt timeout hopeless step = let fun try_method meth = - (case preplay_isar_step_for_method ctxt debug timeout meth step of + (case preplay_isar_step_for_method ctxt timeout meth step of outcome as Played _ => SOME (meth, outcome) | _ => NONE) @@ -164,11 +163,11 @@ | add_preplay_outcomes play1 play2 = Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2))) -fun set_preplay_outcomes_of_isar_step ctxt debug timeout preplay_data +fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 = let fun lazy_preplay meth = - Lazy.lazy (fn () => preplay_isar_step_for_method ctxt debug timeout meth step) + Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step) val meths_outcomes = meths_outcomes0 |> map (apsnd Lazy.value) |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths @@ -176,7 +175,7 @@ preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes []) (!preplay_data) end - | set_preplay_outcomes_of_isar_step _ _ _ _ _ _ = () + | set_preplay_outcomes_of_isar_step _ _ _ _ _ = () fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu May 22 03:29:36 2014 +0200 @@ -34,8 +34,7 @@ (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int val string_of_proof_method : Proof.context -> string list -> proof_method -> string - val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int -> - tactic + val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic val string_of_play_outcome : play_outcome -> string val play_outcome_ord : play_outcome * play_outcome -> order val one_line_proof_text : Proof.context -> int -> one_line_params -> string @@ -97,7 +96,7 @@ maybe_paren (space_implode " " (meth_s :: ss)) end -fun tac_of_proof_method ctxt debug (local_facts, global_facts) meth = +fun tac_of_proof_method ctxt (local_facts, global_facts) meth = Method.insert_tac local_facts THEN' (case meth of Metis_Method (type_enc_opt, lam_trans_opt) => diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 03:29:36 2014 +0200 @@ -79,7 +79,7 @@ val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list - val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) 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 isar_supported_prover_of : theory -> string -> string val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) -> @@ -214,15 +214,15 @@ TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end -fun timed_proof_method debug timeout ths meth = - timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], ths) meth) +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 debug verbose timeout pairs state i preferred (meths as meth :: _) = +fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) = let val ctxt = Proof.context_of state @@ -246,7 +246,7 @@ () val timer = Timer.startRealTimer () in - (case timed_proof_method debug timeout ths meth state i of + (case timed_proof_method timeout ths meth state i of SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer)) | _ => play timed_out meths) end diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu May 22 03:29:36 2014 +0200 @@ -353,8 +353,8 @@ (used_facts, Lazy.lazy (fn () => let val used_pairs = used_from |> filter_used_facts false used_facts in - play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal - (hd meths) meths + play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths) + meths end), fn preplay => let diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu May 22 03:29:36 2014 +0200 @@ -51,7 +51,7 @@ open Sledgehammer_Prover_SMT open Sledgehammer_Prover_SMT2 -fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) +fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...}) minimize_command ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) = let @@ -61,23 +61,22 @@ 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) debug verbose timeout - facts state subgoal meth [meth] of + (case play_one_line_proof (if mode = Minimize then Normal else mode) verbose 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, - message = - fn play => - let - val ctxt = Proof.context_of state - val (_, override_params) = extract_proof_method params meth - val one_line_params = - (play, proof_banner mode name, used_facts, minimize_command override_params name, - subgoal, subgoal_count) - val num_chained = length (#facts (Proof.goal state)) - in - one_line_proof_text ctxt num_chained one_line_params - end, + message = fn play => + let + val ctxt = Proof.context_of state + val (_, override_params) = extract_proof_method params meth + val one_line_params = + (play, proof_banner mode name, used_facts, minimize_command override_params name, + subgoal, subgoal_count) + val num_chained = length (#facts (Proof.goal state)) + in + one_line_proof_text ctxt num_chained one_line_params + end, message_tail = ""} | play => let @@ -128,10 +127,7 @@ fun n_facts names = let val n = length names in string_of_int n ^ " fact" ^ plural_s n ^ - (if n > 0 then - ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") - else - "") + (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "") end fun print silent f = if silent then () else Output.urgent_message (f ()) @@ -141,10 +137,9 @@ smt_proofs, preplay_timeout, ...} : params) silent (prover : prover) timeout i n state goal facts = let - val _ = - print silent (fn () => - "Testing " ^ n_facts (map fst facts) ^ - (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") + val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ + (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") + val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true, @@ -230,7 +225,7 @@ (case test timeout (sup @ r0) of result as {outcome = NONE, used_facts, ...} => min depth result (filter_used_facts true used_facts sup) - (filter_used_facts true used_facts r0) + (filter_used_facts true used_facts r0) | _ => let val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 @@ -259,8 +254,8 @@ val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name fun test timeout = test_facts params silent prover timeout i n state goal val (chained, non_chained) = List.partition is_fact_chained facts - (* Push chained facts to the back, so that they are less likely to be - kicked out by the linear minimization algorithm. *) + (* Push chained facts to the back, so that they are less likely to be kicked out by the linear + minimization algorithm. *) val facts = non_chained @ chained in (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ "."); @@ -378,8 +373,7 @@ | NONE => result) end -fun get_minimizing_prover ctxt mode do_learn name params minimize_command - problem = +fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem = get_prover ctxt mode name params minimize_command problem |> maybe_minimize ctxt mode do_learn name params problem @@ -393,14 +387,14 @@ in (case subgoal_count state of 0 => Output.urgent_message "No subgoal!" - | n => (case provers of - [] => error "No prover is set." - | prover :: _ => - (kill_provers (); - minimize_facts do_learn prover params false i n state goal NONE facts - |> (fn (_, (preplay, message, message_tail)) => - message (Lazy.force preplay) ^ message_tail - |> Output.urgent_message)))) + | n => + (case provers of + [] => error "No prover is set." + | prover :: _ => + (kill_provers (); + minimize_facts do_learn prover params false i n state goal NONE facts + |> (fn (_, (preplay, message, message_tail)) => + Output.urgent_message (message (Lazy.force preplay) ^ message_tail))))) end end; diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu May 22 03:29:36 2014 +0200 @@ -212,7 +212,7 @@ do_slice timeout 1 NONE Time.zeroTime end -fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...}) +fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val thy = Proof.theory_of state @@ -233,7 +233,7 @@ (case outcome of NONE => (Lazy.lazy (fn () => - play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal + play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), fn preplay => let diff -r 46000c075d07 -r fed0329ea8e2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 03:29:35 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 03:29:36 2014 +0200 @@ -238,7 +238,7 @@ (case outcome of NONE => (Lazy.lazy (fn () => - play_one_line_proof mode debug verbose preplay_timeout used_named_facts state subgoal + 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)), fn preplay => let