--- 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))
--- 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
--- 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 =
--- 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
--- 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 *)
--- 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
--- 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 = ([],[])
--- 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
--- 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)