# HG changeset patch # User blanchet # Date 1359651245 -3600 # Node ID afd0213a3dab67a49d04ef4bd13fe4ea0ffea5eb # Parent e8ff34a1fa9a1ddd3c4c4adb86f847a4bfa79fb5 tuned data structure diff -r e8ff34a1fa9a -r afd0213a3dab src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100 @@ -474,21 +474,20 @@ Sledgehammer_Fact.nearly_all_facts ctxt ho_atp Sledgehammer_Fact.no_fact_override reserved css_table chained_ths hyp_ts concl_t - val fact_triple = + val factss = facts |> filter (is_appropriate_prop o prop_of o snd) |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name (the_default default_max_facts max_facts) Sledgehammer_Fact.no_fact_override hyp_ts concl_t - |> tap (fn fact_triple => + |> tap (fn factss => "Line " ^ str0 (Position.line_of pos) ^ ": " ^ - Sledgehammer_Run.string_of_fact_triple fact_triple + Sledgehammer_Run.string_of_factss factss |> Output.urgent_message) val prover = get_prover ctxt prover_name params goal facts val problem = {state = st', goal = goal, subgoal = i, - subgoal_count = Sledgehammer_Util.subgoal_count st, - fact_triple = fact_triple} + subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss} in prover params (K (K (K ""))) problem end)) () handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate diff -r e8ff34a1fa9a -r afd0213a3dab src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100 @@ -42,15 +42,15 @@ |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override hyp_ts concl_t - |> #1 + |> hd |> snd val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - fact_triple = (facts, facts, facts)} + factss = [("", facts)]} in (case prover params (K (K (K ""))) problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME | _ => NONE) - handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) + handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) end fun sledgehammer_with_metis_tac ctxt override_params fact_override i th = diff -r e8ff34a1fa9a -r afd0213a3dab src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 31 17:54:05 2013 +0100 @@ -88,7 +88,7 @@ val mash_weight : real val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list - -> term -> raw_fact list -> fact list * fact list * fact list + -> term -> raw_fact list -> (string * fact list) list val kill_learners : unit -> unit val running_learners : unit -> unit end; @@ -536,7 +536,7 @@ let val problem = {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, - fact_triple = (facts, facts, facts)} + factss = [("", facts)]} in get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) problem @@ -1106,10 +1106,10 @@ error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") else if only then let val facts = facts |> map fact_of_raw_fact in - (facts, facts, facts) + [("", facts)] end else if max_facts <= 0 orelse null facts then - ([], [], []) + [("", [])] else let fun maybe_learn () = @@ -1164,8 +1164,9 @@ in case mess of [(_, (mepo, _)), (_, (mash, _))] => - (mesh, mepo |> map fst |> add_and_take, mash |> map fst |> add_and_take) - | _ => (mesh, mesh, mesh) + [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take), + (mashN, mash |> map fst |> add_and_take)] + | _ => [("", mesh)] end fun kill_learners () = Async_Manager.kill_threads MaShN "learner" diff -r e8ff34a1fa9a -r afd0213a3dab src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 31 17:54:05 2013 +0100 @@ -81,7 +81,7 @@ preplay_timeout = preplay_timeout, expect = ""} val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - fact_triple = (facts, facts, facts)} + factss = [("", facts)]} val result as {outcome, used_facts, run_time, ...} = prover params (K (K (K ""))) problem in @@ -267,8 +267,7 @@ fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...}) - ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...} - : prover_problem) + ({state, 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 @@ -310,7 +309,7 @@ if minimize then minimize_facts do_learn minimize_name params (mode <> Normal orelse not verbose) subgoal subgoal_count state - (filter_used_facts true used_facts (map (apsnd single) facts)) + (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else (SOME used_facts, (preplay, message, "")) diff -r e8ff34a1fa9a -r afd0213a3dab src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100 @@ -68,7 +68,7 @@ goal : thm, subgoal : int, subgoal_count : int, - fact_triple : fact list * fact list * fact list} + factss : (string * fact list) list} type prover_result = {outcome : failure option, @@ -355,7 +355,7 @@ goal : thm, subgoal : int, subgoal_count : int, - fact_triple : fact list * fact list * fact list} + factss : (string * fact list) list} type prover_result = {outcome : failure option, @@ -632,7 +632,7 @@ max_new_mono_instances, isar_proofs, isar_shrink, slice, timeout, preplay_timeout, ...}) minimize_command - ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *) + ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *) ...} : prover_problem) = let val thy = Proof.theory_of state @@ -1064,7 +1064,7 @@ fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command - ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *) + ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *) ...} : prover_problem) = let val ctxt = Proof.context_of state @@ -1108,7 +1108,7 @@ fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) minimize_command - ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...} + ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) = let val reconstr = diff -r e8ff34a1fa9a -r afd0213a3dab src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100 @@ -18,7 +18,7 @@ val noneN : string val timeoutN : string val unknownN : string - val string_of_fact_triple : fact list * fact list * fact list -> string + val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> int -> fact_override -> ((string * string list) list -> string -> minimize_command) @@ -66,9 +66,8 @@ fun launch_prover (params as {debug, verbose, blocking, max_facts, slice, timeout, expect, ...}) - mode minimize_command only learn - {state, goal, subgoal, subgoal_count, - fact_triple as (facts, _, _)} name = + mode minimize_command only learn + {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let val ctxt = Proof.context_of state val hard_timeout = time_mult 3.0 (timeout |> the_default one_day) @@ -82,12 +81,12 @@ val problem = {state = state, goal = goal, subgoal = subgoal, subgoal_count = subgoal_count, - fact_triple = - fact_triple - |> triple_self ((not (is_ho_atp ctxt name) - ? filter_out (fn ((_, (_, Induction)), _) => true - | _ => false)) - #> take num_facts)} + factss = + factss + |> map (apsnd ((not (is_ho_atp ctxt name) + ? filter_out (fn ((_, (_, Induction)), _) => true + | _ => false)) + #> take num_facts))} fun print_used_facts used_facts used_from = tag_list 1 used_from |> map (fn (j, fact) => fact |> apsnd (K j)) @@ -167,21 +166,22 @@ val auto_try_max_facts_divisor = 2 (* FUDGE *) +fun eq_facts p = eq_list (op = o pairself fst) p + fun string_of_facts facts = "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ (facts |> map (fst o fst) |> space_implode " ") ^ "." -fun eq_facts p = eq_list (op = o pairself fst) p - -fun string_of_fact_triple ([], [], []) = "Found no relevant facts." - | string_of_fact_triple (mesh, mepo, mash) = - if eq_facts (mesh, mepo) andalso eq_facts (mesh, mash) then - string_of_facts mesh - else - MeShN ^ ": " ^ string_of_facts mesh ^ "\n\n" ^ - MePoN ^ ": " ^ string_of_facts mepo ^ "\n\n" ^ - MaShN ^ ": " ^ string_of_facts mash +fun string_of_factss factss = + if forall (null o snd) factss then + "Found no relevant facts." + else case factss of + [(_, facts)] => string_of_facts facts + | _ => + factss + |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) + |> space_implode "\n\n" fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts, slice, ...}) @@ -213,7 +213,7 @@ val (smts, (ueq_atps, full_atps)) = provers |> List.partition (is_smt_prover ctxt) ||> List.partition (is_unit_equational_atp ctxt) - fun get_fact_triple label is_appropriate_prop provers = + fun get_factss label is_appropriate_prop provers = let val max_max_facts = case max_facts of @@ -229,20 +229,20 @@ | NONE => I) |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t - |> tap (fn fact_triple => + |> tap (fn factss => if verbose then label ^ plural_s (length provers) ^ ": " ^ - string_of_fact_triple fact_triple + string_of_factss factss |> print else ()) end fun launch_provers state label is_appropriate_prop provers = let - val fact_triple = get_fact_triple label is_appropriate_prop provers + val factss = get_factss label is_appropriate_prop provers val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - fact_triple = fact_triple} + factss = factss} fun learn prover = mash_learn_proof ctxt params prover (prop_of goal) all_facts val launch = launch_prover params mode minimize_command only learn diff -r e8ff34a1fa9a -r afd0213a3dab src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Jan 31 17:54:05 2013 +0100 @@ -11,7 +11,6 @@ val plural_s : int -> string val serial_commas : string -> string list -> string list val simplify_spaces : string -> string - val triple_self : ('a -> 'b) -> 'a * 'a * 'a -> 'b * 'b * 'b val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b val infinite_timeout : Time.time val time_mult : real -> Time.time -> Time.time @@ -44,8 +43,6 @@ val serial_commas = Try.serial_commas val simplify_spaces = strip_spaces false (K true) -fun triple_self f (x, y, z) = (f x, f y, f z) - fun with_cleanup clean_up f x = Exn.capture f x |> tap (fn _ => clean_up x)