tuned;
authorwenzelm
Sun Oct 18 21:13:29 2009 +0200 (2009-10-18)
changeset 32995304a841fd39c
parent 32994 ccc07fbbfefd
child 32996 d2e48879e65a
tuned;
src/HOL/Tools/ATP_Manager/atp_manager.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Oct 18 20:53:40 2009 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Oct 18 21:13:29 2009 +0200
     1.3 @@ -19,8 +19,8 @@
     1.4    val info: unit -> unit
     1.5    val messages: int option -> unit
     1.6    val add_prover: string * ATP_Wrapper.prover -> theory -> theory
     1.7 +  val get_prover: theory -> string -> ATP_Wrapper.prover option
     1.8    val print_provers: theory -> unit
     1.9 -  val get_prover: theory -> string -> ATP_Wrapper.prover option
    1.10    val sledgehammer: string list -> Proof.state -> unit
    1.11  end;
    1.12  
    1.13 @@ -236,9 +236,9 @@
    1.14  fun kill () = Synchronized.change global_state
    1.15    (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
    1.16      let
    1.17 -      val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active;
    1.18 +      val killing = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active;
    1.19        val state' =
    1.20 -        make_state manager timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store;
    1.21 +        make_state manager timeout_heap oldest_heap [] (killing @ cancelling) messages store;
    1.22      in state' end);
    1.23  
    1.24  
    1.25 @@ -299,14 +299,12 @@
    1.26    Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
    1.27      handle Symtab.DUP dup => err_dup_prover dup;
    1.28  
    1.29 +fun get_prover thy name =
    1.30 +  Option.map #1 (Symtab.lookup (Provers.get thy) name);
    1.31 +
    1.32  fun print_provers thy = Pretty.writeln
    1.33    (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
    1.34  
    1.35 -fun get_prover thy name =
    1.36 -  (case Symtab.lookup (Provers.get thy) name of
    1.37 -    NONE => NONE
    1.38 -  | SOME (prover, _) => SOME prover);
    1.39 -
    1.40  
    1.41  (* start prover thread *)
    1.42  
    1.43 @@ -315,15 +313,14 @@
    1.44      NONE => warning ("Unknown external prover: " ^ quote name)
    1.45    | SOME prover =>
    1.46        let
    1.47 -        val (ctxt, (_, goal)) = Proof.get_goal proof_state;
    1.48 +        val full_goal as (ctxt, (_, goal)) = Proof.get_goal proof_state;
    1.49          val desc =
    1.50            "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
    1.51              Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
    1.52          val _ = SimpleThread.fork true (fn () =>
    1.53            let
    1.54              val _ = register birthtime deadtime (Thread.self (), desc);
    1.55 -            val problem =
    1.56 -              ATP_Wrapper.problem_of_goal (! full_types) i (Proof.get_goal proof_state);
    1.57 +            val problem = ATP_Wrapper.problem_of_goal (! full_types) i full_goal;
    1.58              val result =
    1.59                let val {success, message, ...} = prover (! timeout) problem;
    1.60                in (success, message) end