# HG changeset patch # User blanchet # Date 1384882444 -3600 # Node ID b490e15a5e19b41b8b45751edc5b9f92140e9e56 # Parent e7c9a14632d058016f464061ab411c4d90e966ff tuning diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 19 18:34:04 2013 +0100 @@ -374,8 +374,7 @@ fun get_prover ctxt name params goal all_facts = let - fun learn prover = - Sledgehammer_MaSh.mash_learn_proof ctxt params prover (prop_of goal) all_facts + val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (prop_of goal) all_facts in Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal learn name @@ -609,8 +608,8 @@ |> max_new_mono_instancesLST |> max_mono_itersLST) val minimize = - Sledgehammer_Minimize.minimize_facts (K (K ())) prover_name params - true 1 (Sledgehammer_Util.subgoal_count st) + Sledgehammer_Minimize.minimize_facts (K ()) prover_name params true 1 + (Sledgehammer_Util.subgoal_count st) val _ = log separator val (used_facts, (preplay, message, message_tail)) = minimize st goal NONE (these (!named_thms)) diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Tue Nov 19 18:34:04 2013 +0100 @@ -148,10 +148,9 @@ val (get_successors : label -> label list, replace_successor: label -> label list -> label -> unit) = let - fun add_refs (Let _) tab = tab - | add_refs (Prove (_, _, l as v, _, _, By ((lfs, _), _))) tab = - fold (fn lf as key => Canonical_Lbl_Tab.cons_list (key, v)) lfs tab + | add_refs (Prove (_, _, v, _, _, By ((lfs, _), _))) tab = + fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs tab val tab = Canonical_Lbl_Tab.empty @@ -180,7 +179,7 @@ if null subs orelse not (compress_further ()) then (set_preplay_time l (false, time); Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), - By_Metis (lfs, gfs)) ) + By ((lfs, gfs), MetisM))) else case subs of ((sub as Proof(_, Assume assms, sub_steps)) :: subs) => @@ -199,7 +198,7 @@ subtract (op =) (map fst assms) lfs' |> union (op =) lfs val gfs'' = union (op =) gfs' gfs - val by = By_Metis (lfs'', gfs'') + val by = By ((lfs'', gfs''), MetisM) val step'' = Prove (qs, fix, l, t, subs'', by) (* check if the modified step can be preplayed fast enough *) @@ -251,7 +250,7 @@ val candidates = let - fun add_cand (i, Let _) = I + fun add_cand (_, Let _) = I | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t) in @@ -260,7 +259,7 @@ |> fold_index add_cand) [] end - fun try_eliminate (cand as (i, l, _)) succ_lbls steps = + fun try_eliminate (i, l, _) succ_lbls steps = let (* only touch steps that can be preplayed successfully *) val (false, time) = get_preplay_time l diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Nov 19 18:34:04 2013 +0100 @@ -527,7 +527,6 @@ [] else let - val thy = Proof_Context.theory_of ctxt val chained = chained |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) @@ -536,10 +535,6 @@ maps (map (fn ((name, stature), th) => ((K name, stature), th)) o fact_of_ref ctxt reserved chained css) add else - (* The "fact_distinct" call would have cleaner semantics if it called "Pattern.equiv" - instead of "Pattern.matches", but it would also be slower and less precise. - "Pattern.matches" throws out theorems that are strict instances of other theorems, but - only if the instance is met after the general version. *) let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) val facts = diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Nov 19 18:34:04 2013 +0100 @@ -368,7 +368,7 @@ val goal = prop_of (#goal (Proof.goal state)) val facts = nearly_all_facts ctxt false fact_override Symtab.empty Termtab.empty [] [] goal - fun learn prover = mash_learn_proof ctxt params prover goal facts + val learn = mash_learn_proof ctxt params goal facts in run_minimize params learn i (#add fact_override) state end else if subcommand = messagesN then messages opt_i diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Nov 19 18:34:04 2013 +0100 @@ -82,11 +82,8 @@ -> ('b * thm) list -> ('b * thm) list * ('b * thm) list val add_const_counts : term -> int Symtab.table -> int Symtab.table val mash_suggested_facts : - Proof.context -> params -> string -> int -> term list -> term - -> raw_fact list -> fact list * fact list - val mash_learn_proof : - Proof.context -> params -> string -> term -> ('a * thm) list -> thm list - -> unit + Proof.context -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list + val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit @@ -568,8 +565,7 @@ {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, factss = [("", facts)]} in - get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) - problem + get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) problem end val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] @@ -930,8 +926,7 @@ fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) (Term.add_const_names t []) -fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) prover max_facts - hyp_ts concl_t facts = +fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_facts hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val thy_name = Context.theory_name thy @@ -1017,8 +1012,7 @@ val desc = ("Machine learner for Sledgehammer", "") in Async_Manager.thread MaShN birth_time death_time desc task end -fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts - used_ths = +fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths = if is_mash_enabled () then launch_thread (timeout |> the_default one_day) (fn () => let @@ -1328,7 +1322,7 @@ (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts |> weight_facts_steeply, []) fun mash () = - mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts + mash_suggested_facts ctxt params (generous_max_facts max_facts) hyp_ts concl_t facts |>> weight_facts_steeply val mess = (* the order is important for the "case" expression below *) diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Nov 19 18:34:04 2013 +0100 @@ -17,16 +17,14 @@ val auto_minimize_min_facts : int Config.T val auto_minimize_max_time : real Config.T val minimize_facts : - (string -> thm list -> unit) -> string -> params -> bool -> int -> int + (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state -> thm -> play Lazy.lazy option -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option * (play Lazy.lazy * (play -> string) * string) - val get_minimizing_prover : - Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover - val run_minimize : - params -> (string -> thm list -> unit) -> int - -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit + val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover + val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list -> + Proof.state -> unit end; structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = @@ -221,7 +219,7 @@ (case min_facts |> filter is_fact_chained |> length of 0 => "" | n => "\n(including " ^ string_of_int n ^ " chained)") ^ "."); - (if learn then do_learn prover_name (maps snd min_facts) else ()); + (if learn then do_learn (maps snd min_facts) else ()); (SOME min_facts, (if is_some preplay0 andalso length min_facts = length facts then the preplay0 diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Tue Nov 19 18:34:04 2013 +0100 @@ -33,9 +33,6 @@ ArithM | BlastM - (* legacy *) - val By_Metis : facts -> byline - val no_label : label val no_facts : facts @@ -100,9 +97,6 @@ ArithM | BlastM -(* legacy *) -fun By_Metis facts = By (facts, MetisM) - val no_label = ("", ~1) val no_facts = ([],[]) diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 18:34:04 2013 +0100 @@ -312,7 +312,7 @@ accum |> (if tainted = [] then cons (Prove (if outer then [Show] else [], Fix [], no_label, concl_t, [], - By_Metis ([the predecessor], []))) + By (([the predecessor], []), MetisM))) else I) |> rev @@ -320,7 +320,7 @@ let val l = label_of_clause c val t = prop_of_clause c - val by = By_Metis (fold (add_fact_of_dependencies fact_names) gamma no_facts) + val by = By ((fold (add_fact_of_dependencies fact_names) gamma no_facts), MetisM) fun prove sub by = Prove (maybe_show outer c [], Fix [], l, t, sub, by) fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs in @@ -332,7 +332,7 @@ val subproof = Proof (Fix (skolems_of (prop_of_clause g)), Assume [], rev accum) in - do_steps outer (SOME l) [prove [subproof] (By_Metis no_facts)] [] + do_steps outer (SOME l) [prove [subproof] (By (no_facts, MetisM))] [] end else do_rest l (prove [] by) @@ -352,7 +352,7 @@ val t = prop_of_clause c val step = Prove (maybe_show outer c [], Fix [], l, t, map do_case cases, - By_Metis (the_list predecessor, [])) + By ((the_list predecessor, []), MetisM)) in do_steps outer (SOME l) (step :: accum) infs end diff -r e7c9a14632d0 -r b490e15a5e19 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Nov 19 18:14:56 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Nov 19 18:34:04 2013 +0100 @@ -284,10 +284,8 @@ val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss} - fun learn prover = - mash_learn_proof ctxt params prover (prop_of goal) all_facts - val launch = - launch_prover params mode output_result minimize_command only learn + val learn = mash_learn_proof ctxt params (prop_of goal) all_facts + val launch = launch_prover params mode output_result minimize_command only learn in if mode = Auto_Try then (unknownN, state)