--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 28 18:54:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 28 19:01:07 2010 +0200
@@ -8,11 +8,8 @@
signature SLEDGEHAMMER_FACT_MINIMIZER =
sig
type params = Sledgehammer.params
- type prover_result = Sledgehammer.prover_result
- val minimize_theorems :
- params -> int -> int -> Proof.state -> (string * thm list) list
- -> (string * thm list) list option * string
+ val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit
end;
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
@@ -20,6 +17,7 @@
open Metis_Clauses
open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
open Sledgehammer
@@ -38,7 +36,6 @@
fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
filtered_clauses name_thms_pairs =
let
- val thy = Proof.theory_of state
val num_theorems = length name_thms_pairs
val _ =
priority ("Testing " ^ string_of_int num_theorems ^
@@ -123,4 +120,17 @@
handle ERROR msg => (NONE, "Error: " ^ msg)
end
+fun run_minimizer params i refs state =
+ let
+ val ctxt = Proof.context_of state
+ val chained_ths = #facts (Proof.goal state)
+ val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
+ in
+ case subgoal_count state of
+ 0 => priority "No subgoal!"
+ | n =>
+ (kill_atps ();
+ priority (#2 (minimize_theorems params i n state name_thms_pairs)))
+ end
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 28 18:54:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 28 19:01:07 2010 +0200
@@ -19,7 +19,6 @@
open ATP_Systems
open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
open Sledgehammer
open Sledgehammer_Fact_Minimizer
@@ -190,21 +189,6 @@
(* Sledgehammer the given subgoal *)
-fun minimize override_params i refs state =
- let
- val thy = Proof.theory_of state
- val ctxt = Proof.context_of state
- val chained_ths = #facts (Proof.goal state)
- val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
- in
- case subgoal_count state of
- 0 => priority "No subgoal!"
- | n =>
- (kill_atps ();
- priority (#2 (minimize_theorems (get_params thy override_params) i n
- state name_thms_pairs)))
- end
-
val sledgehammerN = "sledgehammer"
val sledgehammer_paramsN = "sledgehammer_params"
@@ -242,8 +226,9 @@
(minimize_command override_params i) state
end
else if subcommand = minimizeN then
- minimize (map (apfst minimizize_raw_param_name) override_params)
- (the_default 1 opt_i) (#add relevance_override) state
+ run_minimizer (get_params thy (map (apfst minimizize_raw_param_name)
+ override_params))
+ (the_default 1 opt_i) (#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
else if subcommand = available_atpsN then