# HG changeset patch # User blanchet # Date 1380895879 -7200 # Node ID 427380d5d1d7efe72937380163b0502fd75d83f6 # Parent 6807b8e95adbec8e9d0b010c16e6fda0eb4122e8 more Sledgehammer spying -- record fact indices diff -r 6807b8e95adb -r 427380d5d1d7 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Oct 04 14:35:00 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Oct 04 16:11:19 2013 +0200 @@ -73,7 +73,7 @@ val ctxt = Proof.context_of state val hard_timeout = time_mult 3.0 (timeout |> the_default one_day) - val _ = spying spy (fn () => (state, subgoal, name, "launched")); + val _ = spying spy (fn () => (state, subgoal, name, "Launched")); val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt slice name) @@ -100,13 +100,21 @@ " proof (of " ^ string_of_int (length facts) ^ "): ") "." |> Output.urgent_message - fun spying_str_of_res ({outcome = NONE, used_facts, ...} : prover_result) = - let val num_used_facts = length used_facts in + fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = + let + val num_used_facts = length used_facts + val indices = + tag_list 1 used_from + |> map (fn (j, fact) => fact |> apsnd (K j)) + |> filter_used_facts false used_facts + |> map (prefix "@" o string_of_int o snd) + in "success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^ - plural_s num_used_facts + plural_s num_used_facts ^ + (if num_used_facts = 0 then "" else " (" ^ commas indices ^ ")") end | spying_str_of_res {outcome = SOME failure, ...} = - "failure: " ^ string_of_atp_failure failure + "Failure: " ^ string_of_atp_failure failure fun really_go () = problem @@ -226,7 +234,7 @@ | NONE => () val _ = print "Sledgehammering..." val _ = - spying spy (fn () => (state, i, "***", "starting " ^ @{make_string} mode ^ " mode")) + spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode")) val (smts, (ueq_atps, full_atps)) = provers |> List.partition (is_smt_prover ctxt) ||> List.partition (is_unit_equational_atp ctxt) @@ -250,8 +258,7 @@ |> (case is_appropriate_prop of SOME is_app => filter (is_app o prop_of o snd) | NONE => I) - |> relevant_facts ctxt params (hd provers) max_max_facts fact_override - hyp_ts concl_t + |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t |> tap (fn factss => if verbose then label ^ plural_s (length provers) ^ ": " ^ @@ -259,9 +266,8 @@ |> print else ()) - |> spy ? tap (fn factss => - spying spy (fn () => - (state, i, label ^ "s", "selected facts: " ^ spying_str_of_factss factss))) + |> spy ? tap (fn factss => spying spy (fn () => + (state, i, label ^ "s", "Selected facts: " ^ spying_str_of_factss factss))) end fun launch_provers state label is_appropriate_prop provers = diff -r 6807b8e95adb -r 427380d5d1d7 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 04 14:35:00 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 04 16:11:19 2013 +0200 @@ -162,7 +162,7 @@ fun hackish_string_of_term ctxt = with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces -val spying_version = "b" +val spying_version = "c" fun spying false _ = () | spying true f =