# HG changeset patch
# User blanchet
# Date 1277483646 -7200
# Node ID 2e289dc13615393ca5660b3b7d8e2b46e30bb9e3
# Parent  9ce2451647d5b7277e3f5f814cc0b1c3c84f2eba
factor out thread creation

diff -r 9ce2451647d5 -r 2e289dc13615 src/HOL/Tools/ATP_Manager/async_manager.ML
--- a/src/HOL/Tools/ATP_Manager/async_manager.ML	Fri Jun 25 18:05:36 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/async_manager.ML	Fri Jun 25 18:34:06 2010 +0200
@@ -8,9 +8,9 @@
 
 signature ASYNC_MANAGER =
 sig
-  val unregister : bool -> string -> Thread.thread -> unit
-  val register :
-    string -> bool -> Time.time -> Time.time -> Thread.thread * string -> unit
+  val launch :
+    string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
+    -> unit
   val kill_threads : string -> unit
   val running_threads : string -> unit
   val thread_messages : string -> int option -> unit
@@ -158,7 +158,7 @@
 
 (* register thread *)
 
-fun register tool verbose birth_time death_time (thread, desc) =
+fun register tool verbose birth_time death_time desc thread =
  (Synchronized.change global_state
     (fn {manager, timeout_heap, active, canceling, messages, store} =>
       let
@@ -169,6 +169,16 @@
   check_thread_manager tool verbose);
 
 
+fun launch tool verbose birth_time death_time desc f =
+  (Toplevel.thread true
+       (fn () =>
+           let
+             val self = Thread.self ()
+             val _ = register tool verbose birth_time death_time desc self
+             val message = f ()
+           in unregister verbose message self end);
+   ())
+
 
 (** user commands **)
 
diff -r 9ce2451647d5 -r 2e289dc13615 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 18:05:36 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 18:34:06 2010 +0200
@@ -56,9 +56,9 @@
   val add_prover: string * prover -> theory -> theory
   val get_prover: theory -> string -> prover
   val available_atps: theory -> unit
-  val start_prover_thread:
-    params -> Time.time -> Time.time -> int -> int -> relevance_override
-    -> (string -> minimize_command) -> Proof.state -> string -> unit
+  val start_prover_thread :
+    params -> int -> int -> relevance_override -> (string -> minimize_command)
+    -> Proof.state -> string -> unit
 end;
 
 structure ATP_Manager : ATP_MANAGER =
@@ -67,13 +67,12 @@
 open Metis_Clauses
 open Sledgehammer_Fact_Filter
 open Sledgehammer_Proof_Reconstruct
-open Async_Manager
 
 (** The Sledgehammer **)
 
-fun kill_atps () = kill_threads "ATPs"
-fun running_atps () = running_threads "ATPs"
-val messages = thread_messages "ATP"
+fun kill_atps () = Async_Manager.kill_threads "ATPs"
+fun running_atps () = Async_Manager.running_threads "ATPs"
+val messages = Async_Manager.thread_messages "ATP"
 
 (** problems, results, provers, etc. **)
 
@@ -145,29 +144,29 @@
 
 (* start prover thread *)
 
-fun start_prover_thread (params as {verbose, full_types, timeout, ...})
-                        birth_time death_time i n relevance_override
-                        minimize_command proof_state name =
+fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
+                        relevance_override minimize_command proof_state name =
   let
+    val birth_time = Time.now ()
+    val death_time = Time.+ (birth_time, timeout)
     val prover = get_prover (Proof.theory_of proof_state) name
     val {context = ctxt, facts, goal} = Proof.goal proof_state;
     val desc =
       "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
       Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
-    val _ = Toplevel.thread true (fn () =>
-      let
-        val _ = register "Sledgehammer" verbose birth_time death_time
-                         (Thread.self (), desc)
-        val problem =
-          {subgoal = i, goal = (ctxt, (facts, goal)),
-           relevance_override = relevance_override, axiom_clauses = NONE,
-           filtered_clauses = NONE}
-        val message =
-          #message (prover params (minimize_command name) timeout problem)
-          handle TRIVIAL () => metis_line full_types i n []
-               | ERROR message => "Error: " ^ message ^ "\n"
-        val _ = unregister verbose message (Thread.self ());
-      in () end)
-  in () end
+  in
+    Async_Manager.launch "Sledgehammer" verbose birth_time death_time desc
+        (fn () =>
+            let
+              val problem =
+                {subgoal = i, goal = (ctxt, (facts, goal)),
+                 relevance_override = relevance_override, axiom_clauses = NONE,
+                 filtered_clauses = NONE}
+            in
+              prover params (minimize_command name) timeout problem |> #message
+              handle TRIVIAL () => metis_line full_types i n []
+                   | ERROR message => "Error: " ^ message ^ "\n"
+            end)
+  end
 
 end;
diff -r 9ce2451647d5 -r 2e289dc13615 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Jun 25 18:05:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Jun 25 18:34:06 2010 +0200
@@ -25,8 +25,8 @@
   val is_theorem_bad_for_atps: thm -> bool
   val type_has_topsort: typ -> bool
   val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
-  val saturate_skolem_cache: theory -> theory option
-  val auto_saturate_skolem_cache: bool Unsynchronized.ref
+  val saturate_cache: theory -> theory option
+  val auto_saturate_cache: bool Unsynchronized.ref
   val neg_clausify: thm -> thm list
   val neg_conjecture_clauses:
     Proof.context -> thm -> int -> thm list list * (string * typ) list
@@ -504,7 +504,7 @@
 
 in
 
-fun saturate_skolem_cache thy =
+fun saturate_cache thy =
   let
     val facts = PureThy.facts_of thy;
     val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
@@ -536,10 +536,10 @@
 end;
 
 (* For emergency use where the Skolem cache causes problems. *)
-val auto_saturate_skolem_cache = Unsynchronized.ref true
+val auto_saturate_cache = Unsynchronized.ref true
 
-fun conditionally_saturate_skolem_cache thy =
-  if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
+fun conditionally_saturate_cache thy =
+  if !auto_saturate_cache then saturate_cache thy else NONE
 
 
 (*** Converting a subgoal into negated conjecture clauses. ***)
@@ -565,7 +565,7 @@
 (** setup **)
 
 val setup =
-  perhaps conditionally_saturate_skolem_cache
-  #> Theory.at_end conditionally_saturate_skolem_cache
+  perhaps conditionally_saturate_cache
+  #> Theory.at_end conditionally_saturate_cache
 
 end;
diff -r 9ce2451647d5 -r 2e289dc13615 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 18:05:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 18:34:06 2010 +0200
@@ -199,13 +199,10 @@
       0 => priority "No subgoal!"
     | n =>
       let
-        val birth_time = Time.now ()
-        val death_time = Time.+ (birth_time, timeout)
         val _ = kill_atps ()
         val _ = priority "Sledgehammering..."
-        val _ = app (start_prover_thread params birth_time death_time i n
-                                         relevance_override minimize_command
-                                         state) atps
+        val _ = app (start_prover_thread params i n relevance_override
+                                         minimize_command state) atps
       in () end
 
 fun minimize override_params i refs state =