# HG changeset patch # User blanchet # Date 1392293777 -3600 # Node ID 29ec8680e61f7f0b6bcb4b59be5530668af49c7d # Parent ea1d9408a233e8145ecfd3248bbde27595868a02 avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Feb 13 13:16:17 2014 +0100 @@ -231,7 +231,6 @@ val _ = Proof.assert_backward state val print = if mode = Normal andalso is_none output_result then Output.urgent_message else K () - val state = state |> Proof.map_context (silence_proof_methods debug) val ctxt = Proof.context_of state val {facts = chained, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 13 13:16:17 2014 +0100 @@ -290,7 +290,7 @@ val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty val _ = fold_isar_steps (fn meth => - K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) + K (set_preplay_outcomes_of_isar_step ctxt debug 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 compress_isar preplay_timeout preplay_data + |> compress_isar_proof ctxt debug 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 preplay_data) + #> minimize ? minimize_isar_step_dependencies ctxt debug 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 ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Feb 13 13:16:17 2014 +0100 @@ -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 -> real -> Time.time -> + val compress_isar_proof : Proof.context -> bool -> 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 compress_isar preplay_timeout preplay_data proof = +fun compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data proof = if compress_isar <= 1.0 then proof else @@ -172,11 +172,12 @@ (* 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 timeout hopeless step'' of + (case preplay_isar_step ctxt debug timeout hopeless step'' of meths_outcomes as (_, Played time'') :: _ => (* l' successfully eliminated *) (decrement_step_count (); - set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes; + set_preplay_outcomes_of_isar_step ctxt debug 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)) @@ -215,14 +216,16 @@ val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l) val timeouts = map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0 - val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs' + val meths_outcomess = + map3 (preplay_isar_step ctxt debug) 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 time preplay_data) + map3 (fn time => + set_preplay_outcomes_of_isar_step ctxt debug time preplay_data) times succs' meths_outcomess; map (replace_successor l labels) lfs; steps_before @ update_steps succs' steps_after)) diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu Feb 13 13:16:17 2014 +0100 @@ -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 -> isar_preplay_data Unsynchronized.ref -> - isar_step -> isar_step + val minimize_isar_step_dependencies : Proof.context -> bool -> + 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 preplay_data +fun minimize_isar_step_dependencies ctxt debug 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 (Time.+ (time, slack)) meth + (case preplay_isar_step_for_method ctxt debug (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,11 +53,12 @@ val step' = mk_step_lfs_gfs min_lfs min_gfs in - set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')]; + set_preplay_outcomes_of_isar_step ctxt debug 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 ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Feb 13 13:16:17 2014 +0100 @@ -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 -> Time.time -> proof_method -> isar_step -> - play_outcome - val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step -> + 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 -> (proof_method * play_outcome) list - val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time -> + val set_preplay_outcomes_of_isar_step : Proof.context -> bool -> 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,7 +101,8 @@ end (* may throw exceptions *) -fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) = +fun raw_preplay_step_for_method ctxt debug timeout meth + (Prove (_, xs, _, t, subproofs, facts, _, _)) = let val goal = (case xs of @@ -128,7 +129,7 @@ fun prove () = Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => - HEADGOAL (tac_of_proof_method ctxt assmsp meth)) + HEADGOAL (tac_of_proof_method ctxt debug assmsp meth)) handle ERROR msg => error ("Preplay error: " ^ msg) val play_outcome = take_time timeout prove () @@ -137,13 +138,13 @@ play_outcome end -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_for_method ctxt debug timeout meth = + try (raw_preplay_step_for_method ctxt debug timeout meth) #> the_default Play_Failed -fun preplay_isar_step ctxt timeout hopeless step = +fun preplay_isar_step ctxt debug timeout hopeless step = let fun try_method meth = - (case preplay_isar_step_for_method ctxt timeout meth step of + (case preplay_isar_step_for_method ctxt debug timeout meth step of outcome as Played _ => SOME (meth, outcome) | _ => NONE) @@ -163,11 +164,11 @@ | add_preplay_outcomes play1 play2 = Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2))) -fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data +fun set_preplay_outcomes_of_isar_step ctxt debug timeout preplay_data (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 = let fun lazy_preplay meth = - Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step) + Lazy.lazy (fn () => preplay_isar_step_for_method ctxt debug timeout meth step) val meths_outcomes = meths_outcomes0 |> map (apsnd Lazy.value) |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths @@ -175,7 +176,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 Not_Played diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Feb 13 13:16:17 2014 +0100 @@ -34,11 +34,11 @@ (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int val string_of_proof_method : proof_method -> string - val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic + val tac_of_proof_method : Proof.context -> bool -> 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 : int -> one_line_params -> string - val silence_proof_methods : bool -> Proof.context -> Proof.context end; structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = @@ -89,27 +89,36 @@ | Presburger_Method => "presburger" | Algebra_Method => "algebra") -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) => - Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)] - (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts - | Meson_Method => Meson.meson_tac ctxt global_facts - | SMT_Method => SMT_Solver.smt_tac ctxt global_facts - | _ => - Method.insert_tac global_facts THEN' +(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound + exceeded" warnings and the like. *) +fun silence_proof_methods debug = + Try0.silence_methods debug + #> Config.put SMT_Config.verbose debug + +fun tac_of_proof_method ctxt0 debug (local_facts, global_facts) meth = + let val ctxt = silence_proof_methods debug ctxt0 in + Method.insert_tac local_facts THEN' (case meth of - Blast_Method => blast_tac ctxt - | Simp_Method => Simplifier.asm_full_simp_tac ctxt - | Simp_Size_Method => - Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) - | Auto_Method => K (Clasimp.auto_tac ctxt) - | Fastforce_Method => Clasimp.fast_force_tac ctxt - | Force_Method => Clasimp.force_tac ctxt - | Linarith_Method => Lin_Arith.tac ctxt - | Presburger_Method => Cooper.tac true [] [] ctxt - | Algebra_Method => Groebner.algebra_tac [] [] ctxt)) + Metis_Method (type_enc_opt, lam_trans_opt) => + Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)] + (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts + | Meson_Method => Meson.meson_tac ctxt global_facts + + | SMT_Method => SMT_Solver.smt_tac ctxt global_facts + | _ => + Method.insert_tac global_facts THEN' + (case meth of + Blast_Method => blast_tac ctxt + | Simp_Method => Simplifier.asm_full_simp_tac ctxt + | Simp_Size_Method => + Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) + | Auto_Method => K (Clasimp.auto_tac ctxt) + | Fastforce_Method => Clasimp.fast_force_tac ctxt + | Force_Method => Clasimp.force_tac ctxt + | Linarith_Method => Lin_Arith.tac ctxt + | Presburger_Method => Cooper.tac true [] [] ctxt + | Algebra_Method => Groebner.algebra_tac [] [] ctxt)) + end fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out" @@ -189,10 +198,4 @@ try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end -(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound - exceeded" warnings and the like. *) -fun silence_proof_methods debug = - Try0.silence_methods debug - #> Config.put SMT_Config.verbose debug - end; diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Feb 13 13:16:17 2014 +0100 @@ -78,7 +78,7 @@ 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 -> + val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list -> Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome val remotify_atp_if_not_installed : theory -> string -> string option val isar_supported_prover_of : theory -> string -> string @@ -219,15 +219,15 @@ TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end -fun timed_proof_method meth timeout ths = - timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth) +fun timed_proof_method debug timeout ths meth = + timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], 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 debug verbose timeout pairs state i preferred (meths as meth :: _) = let fun get_preferred meths = if member (op =) meths preferred then preferred else meth in @@ -249,7 +249,7 @@ () val timer = Timer.startRealTimer () in - (case timed_proof_method meth timeout ths state i of + (case timed_proof_method debug timeout ths meth state i of SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer)) | _ => play timed_out meths) end diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Feb 13 13:16:17 2014 +0100 @@ -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 verbose preplay_timeout used_pairs state subgoal (hd meths) - meths + play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal + (hd meths) meths end), fn preplay => let diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Feb 13 13:16:17 2014 +0100 @@ -50,7 +50,7 @@ open Sledgehammer_Prover_ATP open Sledgehammer_Prover_SMT -fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...}) +fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) minimize_command ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) = let @@ -60,8 +60,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) debug 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, diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Feb 13 13:16:17 2014 +0100 @@ -71,7 +71,7 @@ fun weight_smt_fact ctxt num_facts ((info, th), j) = let val thy = Proof_Context.theory_of ctxt in - (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy)) + (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *))) end (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out @@ -212,7 +212,7 @@ do_slice timeout 1 NONE Time.zeroTime end -fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...}) +fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val thy = Proof.theory_of state @@ -233,8 +233,8 @@ (case outcome of NONE => (Lazy.lazy (fn () => - play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal SMT_Method - (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), + play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal + SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), fn preplay => let val one_line_params =