# HG changeset patch # User blanchet # Date 1454353078 -3600 # Node ID dbac573b27e792a3b596b7a4dc8819d12454046f # Parent 42202671777c3f1153218079e025e10c1fba1dd0 preplaying of 'smt' and 'metis' more in sync with actual method diff -r 42202671777c -r dbac573b27e7 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 01 18:45:18 2016 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 01 19:57:58 2016 +0100 @@ -17,7 +17,7 @@ thm list * thm Seq.seq val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list -> - thm -> thm Seq.seq + tactic val metis_lam_transs : string list val parse_metis_options : (string list option * string option) parser end diff -r 42202671777c -r dbac573b27e7 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 01 18:45:18 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 01 19:57:58 2016 +0100 @@ -63,11 +63,6 @@ fun is_metis_method (Metis_Method _) = true | is_metis_method _ = false -fun add_chained [] t = t - | add_chained chained ((t as Const (@{const_name Pure.all}, _)) $ Abs (s, T, u)) = - t $ Abs (s, T, add_chained chained u) - | add_chained chained t = Logic.list_implies (chained, t) - fun play_one_line_proof minimize timeout used_facts0 state i (preferred_meth, methss) = let val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts0 in if timeout = Time.zeroTime then @@ -79,7 +74,6 @@ val fact_names = map fst used_facts val {facts = chained, goal, ...} = Proof.goal state val goal_t = Logic.get_goal (Thm.prop_of goal) i - |> add_chained (map (Thm.prop_of o forall_intr_vars) chained) fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) | try_methss ress [] = @@ -92,7 +86,7 @@ fun mk_step fact_names meths = Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") in - (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of + (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of (res as (meth, Played time)) :: _ => (* if a fact is needed by an ATP, it will be needed by "metis" *) if not minimize orelse is_metis_method meth then diff -r 42202671777c -r dbac573b27e7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 01 18:45:18 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 01 19:57:58 2016 +0100 @@ -173,7 +173,7 @@ (* 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 [] timeout hopeless step'' of meths_outcomes as (_, Played time'') :: _ => (* "l'" successfully eliminated *) (decrement_step_count (); @@ -218,7 +218,8 @@ val total_time = Library.foldl Time.+ (reference_time l, times0) val timeout = adjust_merge_timeout preplay_timeout (Time.fromReal (Time.toReal total_time / Real.fromInt n)) - val meths_outcomess = @{map 2} (preplay_isar_step ctxt timeout) hopelesses succs' + val meths_outcomess = + @{map 2} (preplay_isar_step ctxt [] timeout) hopelesses succs' in (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of NONE => steps diff -r 42202671777c -r dbac573b27e7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 01 18:45:18 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 01 19:57:58 2016 +0100 @@ -45,7 +45,7 @@ fun minimize_half _ min_facts [] time = (min_facts, time) | minimize_half 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 [] (Time.+ (time, slack)) meth (mk_step (min_facts @ facts)) of Played time' => minimize_half mk_step min_facts facts time' | _ => minimize_half mk_step (fact :: min_facts) facts time) diff -r 42202671777c -r dbac573b27e7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 01 18:45:18 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 01 19:57:58 2016 +0100 @@ -19,10 +19,10 @@ val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome 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 -> - (proof_method * play_outcome) list + val preplay_isar_step_for_method : Proof.context -> thm list -> Time.time -> proof_method -> + isar_step -> play_outcome + val preplay_isar_step : Proof.context -> thm list -> Time.time -> proof_method list -> + isar_step -> (proof_method * play_outcome) list 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 @@ -126,7 +126,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 chained timeout meth + (Prove (_, xs, _, t, subproofs, facts, _, _)) = let val goal = (case xs of @@ -150,6 +151,7 @@ val assmsp = resolve_fact_names ctxt facts |>> append (map (thm_of_proof ctxt) subproofs) + |>> append chained fun prove () = Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => @@ -162,14 +164,14 @@ 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 chained timeout meth = + try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed val min_preplay_timeout = seconds 0.002 -fun preplay_isar_step ctxt timeout0 hopeless step = +fun preplay_isar_step ctxt chained timeout0 hopeless step = let - fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt timeout meth step) + fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt chained timeout meth step) fun get_time (_, Played time) = SOME time | get_time _ = NONE @@ -194,7 +196,7 @@ (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 [] timeout meth step) val meths_outcomes = meths_outcomes0 |> map (apsnd Lazy.value) |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths diff -r 42202671777c -r dbac573b27e7 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Feb 01 18:45:18 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Feb 01 19:57:58 2016 +0100 @@ -114,7 +114,6 @@ end fun tac_of_proof_method ctxt (local_facts, global_facts) meth = - Method.insert_tac ctxt local_facts THEN' (case meth of Metis_Method (type_enc_opt, lam_trans_opt) => let @@ -122,26 +121,29 @@ |> Config.put Metis_Tactic.verbose false |> Config.put Metis_Tactic.trace false in - 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 + SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt), + global_facts) ctxt local_facts) end - | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts - | SMT_Method => SMT_Solver.smt_tac ctxt global_facts - | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) - | Simp_Size_Method => - Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts)) + | SMT_Method => SMT_Solver.smt_tac ctxt (local_facts @ global_facts) | _ => - Method.insert_tac ctxt global_facts THEN' + Method.insert_tac ctxt local_facts THEN' (case meth of - SATx_Method => SAT.satx_tac ctxt - | Blast_Method => blast_tac ctxt - | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt) - | Fastforce_Method => Clasimp.fast_force_tac ctxt - | Force_Method => Clasimp.force_tac ctxt - | Moura_Method => moura_tac ctxt - | Linarith_Method => Lin_Arith.tac ctxt - | Presburger_Method => Cooper.tac true [] [] ctxt - | Algebra_Method => Groebner.algebra_tac [] [] ctxt)) + Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts + | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) + | Simp_Size_Method => + Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts)) + | _ => + Method.insert_tac ctxt global_facts THEN' + (case meth of + SATx_Method => SAT.satx_tac ctxt + | Blast_Method => blast_tac ctxt + | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt) + | Fastforce_Method => Clasimp.fast_force_tac ctxt + | Force_Method => Clasimp.force_tac ctxt + | Moura_Method => moura_tac ctxt + | Linarith_Method => Lin_Arith.tac ctxt + | Presburger_Method => Cooper.tac true [] [] ctxt + | Algebra_Method => Groebner.algebra_tac [] [] ctxt))) fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) | string_of_play_outcome (Play_Timed_Out time) =