# HG changeset patch # User blanchet # Date 1381969374 -7200 # Node ID b4e6cd4cab92c1916fa4baeb0f467b6138add36d # Parent 9ee9eee93c0685c4e69d6c138736caf7f897aca2 thread the goal through instead of relying on unreliable (possibly fake) state diff -r 9ee9eee93c06 -r b4e6cd4cab92 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 17 01:34:34 2013 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 17 02:22:54 2013 +0200 @@ -583,6 +583,7 @@ ({pre=st, log, ...}: Mirabelle.run_args) = let val ctxt = Proof.context_of st + val {goal, ...} = Proof.goal st val n0 = length (these (!named_thms)) val prover_name = get_prover_name ctxt args val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default @@ -612,7 +613,7 @@ true 1 (Sledgehammer_Util.subgoal_count st) val _ = log separator val (used_facts, (preplay, message, message_tail)) = - minimize st NONE (these (!named_thms)) + minimize st goal NONE (these (!named_thms)) val msg = message (Lazy.force preplay) ^ message_tail in case used_facts of diff -r 9ee9eee93c06 -r b4e6cd4cab92 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 17 01:34:34 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 17 02:22:54 2013 +0200 @@ -18,7 +18,7 @@ val auto_minimize_max_time : real Config.T val minimize_facts : (string -> thm list -> unit) -> string -> params -> bool -> int -> int - -> Proof.state -> play Lazy.lazy option + -> Proof.state -> thm -> play Lazy.lazy option -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option * (play Lazy.lazy * (play -> string) * string) @@ -59,7 +59,7 @@ max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, isar_compress, isar_try0, preplay_timeout, ...} : params) - silent (prover : prover) timeout i n state facts = + silent (prover : prover) timeout i n state goal facts = let val _ = print silent (fn () => @@ -70,7 +70,6 @@ | _ => "" else "") ^ "...") - val {goal, ...} = Proof.goal state val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true, @@ -191,12 +190,12 @@ end fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent - i n state preplay0 facts = + i n state goal preplay0 facts = let val ctxt = Proof.context_of state 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 + 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. *) @@ -272,7 +271,7 @@ fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...}) - ({state, subgoal, subgoal_count, ...} : prover_problem) + ({state, goal, subgoal, subgoal_count, ...} : prover_problem) (result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} : prover_result) = if is_some outcome orelse null used_facts then @@ -320,7 +319,7 @@ if minimize then minimize_facts do_learn minimize_name params (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal - subgoal_count state (SOME preplay) + subgoal_count state goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else @@ -342,12 +341,10 @@ fun run_minimize (params as {provers, ...}) do_learn i refs state = let val ctxt = Proof.context_of state + val {goal, facts = chained_ths, ...} = Proof.goal state val reserved = reserved_isar_keyword_table () - val chained_ths = #facts (Proof.goal state) val css = clasimpset_rule_table_of ctxt - val facts = - refs |> maps (map (apsnd single) - o fact_of_ref ctxt reserved chained_ths css) + val facts = refs |> maps (map (apsnd single) o fact_of_ref ctxt reserved chained_ths css) in case subgoal_count state of 0 => Output.urgent_message "No subgoal!" @@ -355,7 +352,7 @@ [] => error "No prover is set." | prover :: _ => (kill_provers (); - minimize_facts do_learn prover params false i n state NONE facts + 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))