--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 18:45:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 18:54:18 2010 +0200
@@ -53,9 +53,9 @@
val running_atps: unit -> unit
val messages: int option -> unit
val get_prover_fun : theory -> string -> prover
- val start_prover_thread :
- params -> int -> int -> relevance_override -> (string -> minimize_command)
- -> Proof.state -> string -> unit
+ val run_sledgehammer :
+ params -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> unit
val setup : theory -> theory
end;
@@ -845,7 +845,6 @@
fun get_prover_fun thy name = prover_fun name (get_prover thy name)
-(* start prover thread *)
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
relevance_override minimize_command proof_state name =
let
@@ -871,6 +870,19 @@
end)
end
+fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
+ | run_sledgehammer (params as {atps, ...}) i relevance_override
+ minimize_command state =
+ case subgoal_count state of
+ 0 => priority "No subgoal!"
+ | n =>
+ let
+ val _ = kill_atps ()
+ val _ = priority "Sledgehammering..."
+ val _ = app (start_prover_thread params i n relevance_override
+ minimize_command state) atps
+ in () end
+
val setup =
dest_dir_setup
#> problem_prefix_setup
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 28 18:45:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 28 18:54:18 2010 +0200
@@ -188,22 +188,8 @@
fun get_params thy = extract_params (default_raw_params thy)
fun default_params thy = get_params thy o map (apsnd single)
-val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
-
(* Sledgehammer the given subgoal *)
-fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | run (params as {atps, ...}) i relevance_override minimize_command state =
- case subgoal_count state of
- 0 => priority "No subgoal!"
- | n =>
- let
- val _ = kill_atps ()
- val _ = priority "Sledgehammering..."
- val _ = app (start_prover_thread params i n relevance_override
- minimize_command state) atps
- in () end
-
fun minimize override_params i refs state =
let
val thy = Proof.theory_of state
@@ -252,8 +238,8 @@
in
if subcommand = runN then
let val i = the_default 1 opt_i in
- run (get_params thy override_params) i relevance_override
- (minimize_command override_params i) state
+ run_sledgehammer (get_params thy override_params) i relevance_override
+ (minimize_command override_params i) state
end
else if subcommand = minimizeN then
minimize (map (apfst minimizize_raw_param_name) override_params)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 28 18:45:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 28 18:54:18 2010 +0200
@@ -17,6 +17,7 @@
val maybe_quote : string -> string
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> (string * typ) -> term -> term
+ val subgoal_count : Proof.state -> int
val strip_subgoal : thm -> int -> (string * typ) list * term list * term
end;
@@ -124,6 +125,8 @@
| NONE => raise Type.TYPE_MATCH
end
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
fun strip_subgoal goal i =
let
val (t, frees) = Logic.goal_params (prop_of goal) i