src/HOL/Tools/ATP_Manager/atp_manager.ML

 Central manager component for ATP threads.
 *)
 
 signature ATP_MANAGER =
 sig
+  type problem =
+   {with_full_types: bool,
+    subgoal: int,
+    goal: Proof.context * (thm list * thm),
+    axiom_clauses: (thm * (string * int)) list option,
+    filtered_clauses: (thm * (string * int)) list option}
+  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
+  type prover_result =
+   {success: bool,
+    message: string,
+    theorem_names: string list,
+    runtime: int,
+    proof: string,
+    internal_thm_names: string Vector.vector,
+    filtered_clauses: (thm * (string * int)) list}
+  type prover = int -> problem -> prover_result
+
   val atps: string Unsynchronized.ref
   val get_atps: unit -> string list
   val timeout: int Unsynchronized.ref
   val full_types: bool Unsynchronized.ref
   val kill: unit -> unit
   val info: unit -> unit
   val messages: int option -> unit
-  val add_prover: string * ATP_Wrapper.prover -> theory -> theory
-  val get_prover: theory -> string -> ATP_Wrapper.prover option
+  val add_prover: string * prover -> theory -> theory
+  val get_prover: theory -> string -> prover option
   val print_provers: theory -> unit
   val sledgehammer: string list -> Proof.state -> unit
 end;
 
 structure ATP_Manager : ATP_MANAGER =
 struct
+
+(** problems, results, and provers **)
+
+type problem =
+ {with_full_types: bool,
+  subgoal: int,
+  goal: Proof.context * (thm list * thm),
+  axiom_clauses: (thm * (string * int)) list option,
+  filtered_clauses: (thm * (string * int)) list option};
+
+fun problem_of_goal with_full_types subgoal goal : problem =
+ {with_full_types = with_full_types,
+  subgoal = subgoal,
+  goal = goal,
+  axiom_clauses = NONE,
+  filtered_clauses = NONE};
+
+type prover_result =
+ {success: bool,
+  message: string,
+  theorem_names: string list,  (*relevant theorems*)
+  runtime: int,  (*user time of the ATP, in milliseconds*)
+  proof: string,
+  internal_thm_names: string Vector.vector,
+  filtered_clauses: (thm * (string * int)) list};
+
+type prover = int -> problem -> prover_result;
+
 
 (** preferences **)
 
 val message_store_limit = 20;
 val message_display_limit = 5;

 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
 structure Provers = Theory_Data
 (
-  type T = (ATP_Wrapper.prover * stamp) Symtab.table;
+  type T = (prover * stamp) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data : T = Symtab.merge (eq_snd op =) data
     handle Symtab.DUP dup => err_dup_prover dup;
 );

             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
 
         val _ = Toplevel.thread true (fn () =>
           let
             val _ = register birth_time death_time (Thread.self (), desc);
-            val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
+            val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
             val message = #message (prover (! timeout) problem)
               handle Sledgehammer_HOL_Clause.TRIVIAL =>   (* FIXME !? *)
                   "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
                 | ERROR msg => ("Error: " ^ msg);
             val _ = unregister message (Thread.self ());