src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 32864 a226f29d4bdc
parent 32824 712ad8109fff
child 32865 f8d1e16ec758
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Oct 02 04:44:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Oct 03 12:05:40 2009 +0200
     1.3 @@ -21,13 +21,9 @@
     1.4    val kill: unit -> unit
     1.5    val info: unit -> unit
     1.6    val messages: int option -> unit
     1.7 -  type prover = int -> (thm * (string * int)) list option ->
     1.8 -    (thm * (string * int)) list option -> string -> int ->
     1.9 -    Proof.context * (thm list * thm) ->
    1.10 -    bool * (string * string list) * int * string * string vector * (thm * (string * int)) list
    1.11 -  val add_prover: string -> prover -> theory -> theory
    1.12 +  val add_prover: string * AtpWrapper.prover -> theory -> theory
    1.13    val print_provers: theory -> unit
    1.14 -  val get_prover: string -> theory -> prover option
    1.15 +  val get_prover: string -> theory -> AtpWrapper.prover option
    1.16    val sledgehammer: string list -> Proof.state -> unit
    1.17  end;
    1.18  
    1.19 @@ -302,16 +298,11 @@
    1.20  
    1.21  (* named provers *)
    1.22  
    1.23 -type prover = int -> (thm * (string * int)) list option ->
    1.24 -  (thm * (string * int)) list option -> string -> int ->
    1.25 -  Proof.context * (thm list * thm) ->
    1.26 -  bool * (string * string list) * int * string * string vector * (thm * (string * int)) list
    1.27 -
    1.28  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
    1.29  
    1.30  structure Provers = TheoryDataFun
    1.31  (
    1.32 -  type T = (prover * stamp) Symtab.table
    1.33 +  type T = (AtpWrapper.prover * stamp) Symtab.table
    1.34    val empty = Symtab.empty
    1.35    val copy = I
    1.36    val extend = I
    1.37 @@ -319,7 +310,7 @@
    1.38      handle Symtab.DUP dup => err_dup_prover dup
    1.39  );
    1.40  
    1.41 -fun add_prover name prover thy =
    1.42 +fun add_prover (name, prover) thy =
    1.43    Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
    1.44      handle Symtab.DUP dup => err_dup_prover dup;
    1.45  
    1.46 @@ -344,9 +335,11 @@
    1.47          val _ = SimpleThread.fork true (fn () =>
    1.48            let
    1.49              val _ = register birthtime deadtime (Thread.self (), desc)
    1.50 +            val problem = AtpWrapper.atp_problem_of_goal (get_full_types ()) i
    1.51 +              (Proof.get_goal proof_state)
    1.52              val result =
    1.53 -              let val (success, (message, _), _, _, _, _) =
    1.54 -                prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
    1.55 +              let val AtpWrapper.Prover_Result {success, message, ...} =
    1.56 +                prover problem (get_timeout ())
    1.57                in (success, message) end
    1.58                handle ResHolClause.TOO_TRIVIAL
    1.59                  => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")