tuned interfaces -- plain prover function, without thread;
misc tuning and simplification;
reduced NJ basis library stuff to bare minimum;

--- a/src/HOL/Tools/atp_wrapper.ML	Tue Oct 14 20:10:44 2008 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Tue Oct 14 20:10:45 2008 +0200
@@ -7,144 +7,159 @@
 
 signature ATP_WRAPPER =
 sig
-  (* hooks for writing problemfiles *)
   val destdir: string ref
   val problem_name: string ref
-  (* basic template *)
   val external_prover:
     ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
     Path.T * string ->
     (string * int -> bool) ->
     (string * string vector * Proof.context * thm * int -> string) ->
-    int -> Proof.state -> Thread.thread
-  (* provers as functions returning threads *)
-  val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
-  val tptp_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
-  val remote_prover_filter_opts: int -> bool -> string -> string -> int -> Proof.state -> Thread.thread
-  val full_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
-  val tptp_prover: Path.T * string -> int -> Proof.state -> Thread.thread
-  val remote_prover: string -> string -> int -> Proof.state -> Thread.thread
-  val full_prover: Path.T * string  -> int -> Proof.state -> Thread.thread
-  val spass_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
-  val eprover_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
-  val eprover_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
-  val vampire_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread
-  val vampire_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
-  val spass: int -> Proof.state -> Thread.thread
-  val eprover: int -> Proof.state -> Thread.thread
-  val eprover_full: int -> Proof.state -> Thread.thread
-  val vampire: int -> Proof.state -> Thread.thread
-  val vampire_full: int -> Proof.state -> Thread.thread
+    AtpManager.prover
+  val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
+  val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
+  val tptp_prover: Path.T * string -> AtpManager.prover
+  val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
+  val full_prover: Path.T * string  -> AtpManager.prover
+  val vampire_opts: int -> bool -> AtpManager.prover
+  val vampire: AtpManager.prover
+  val vampire_opts_full: int -> bool -> AtpManager.prover
+  val vampire_full: AtpManager.prover
+  val eprover_opts: int -> bool  -> AtpManager.prover
+  val eprover: AtpManager.prover
+  val eprover_opts_full: int -> bool -> AtpManager.prover
+  val eprover_full: AtpManager.prover
+  val spass_opts: int -> bool  -> AtpManager.prover
+  val spass: AtpManager.prover
+  val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
+  val remote_prover: string -> string -> AtpManager.prover
 end;
 
 structure AtpWrapper: ATP_WRAPPER =
 struct
-  
-  (* preferences for path and filename to problemfiles *)
-  val destdir = ref "";   (*Empty means write files to /tmp*)
-  val problem_name = ref "prob";
-      
-  (*Setting up a Thread for an external prover*)
-  fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
-    let
+
+(** generic ATP wrapper **)
+
+(* global hooks for writing problemfiles *)
+
+val destdir = ref "";   (*Empty means write files to /tmp*)
+val problem_name = ref "prob";
+
+
+(* basic template *)
+
+fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
+  let
+    (* path to unique problem file *)
     val destdir' = ! destdir
     val problem_name' = ! problem_name
-    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
-    (* path to unique problem file *)
     fun prob_pathname nr =
-      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr)
+      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
       in if destdir' = "" then File.tmp_path probfile
         else if File.exists (Path.explode (destdir'))
         then Path.append  (Path.explode (destdir')) probfile
         else error ("No such directory: " ^ destdir')
       end
+
     (* write out problem file and call prover *)
-    fun call_prover () =
-      let
-      val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
-      val (filenames, thm_names_list) =
-        write_problem_files prob_pathname (ctxt, chain_ths, goal)
-      val thm_names = List.nth (thm_names_list, subgoalno - 1); (*(i-1)th element for i-th subgoal*)
+    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
+    val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
+    val (filenames, thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, goal)
+    val thm_names = nth thm_names_list (subgoalno - 1)
+
+    val cmdline =
+      if File.exists cmd then File.shell_path cmd ^ " " ^ args
+      else error ("Bad executable: " ^ Path.implode cmd)
+    val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1))
+    val _ =
+      if rc <> 0 then
+        warning ("Sledgehammer prover exited with return code " ^ string_of_int rc ^ "\n" ^ cmdline)
+      else ()
 
-      val cmdline =
-        if File.exists cmd then File.shell_path cmd ^ " " ^ args
-        else error ("Bad executable: " ^ Path.implode cmd);
-      val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno - 1))
-      val _ =
-        if rc <> 0
-        then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc)
-        else ()
-      (* remove *temporary* files *)
-      val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else ()
-      in
-        if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno)
-        else NONE
-      end
-    in
-      AtpManager.atp_thread call_prover produce_answer
-    end;
+    (* remove *temporary* files *)
+    val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else ()
 
-    
-  (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*)
+    val success = check_success (proof, rc)
+    val message =
+      if success
+      then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
+      else "Failed."
+  in (success, message) end;
+
 
-  fun tptp_prover_filter_opts_full max_new theory_const full command sg =
-    external_prover
+
+(** common provers **)
+
+(* generic TPTP-based provers *)
+
+fun tptp_prover_opts_full max_new theory_const full command =
+  external_prover
     (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
     command
     ResReconstruct.check_success_e_vamp_spass
-    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
-    sg
-    
-  (* arbitrary atp with tptp input/output and problemfile as last argument*)
-  fun tptp_prover_filter_opts max_new theory_const =
-    tptp_prover_filter_opts_full max_new theory_const false;
-  (* default settings*)  
-  val tptp_prover = tptp_prover_filter_opts 60 true;
+    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
+
+(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
+fun tptp_prover_opts max_new theory_const =
+  tptp_prover_opts_full max_new theory_const false;
+
+val tptp_prover = tptp_prover_opts 60 true;
+
+(*for structured proofs: prover must support TSTP*)
+fun full_prover_opts max_new theory_const =
+  tptp_prover_opts_full max_new theory_const true;
+
+val full_prover = full_prover_opts 60 true;
+
 
-  (* for structured proofs: prover must support TSTP *)
-  fun full_prover_filter_opts max_new theory_const =
-    tptp_prover_filter_opts_full max_new theory_const true;
-  (* default settings*)
-  val full_prover = full_prover_filter_opts 60 true;
+(* Vampire *)
+
+(*NB: Vampire does not work without explicit timelimit*)
+
+fun vampire_opts max_new theory_const = tptp_prover_opts
+  max_new theory_const
+  (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600");
+
+val vampire = vampire_opts 60 false;
+
+fun vampire_opts_full max_new theory_const = full_prover_opts
+  max_new theory_const
+  (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600");
+
+val vampire_full = vampire_opts 60 false;
+
 
-  fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts
-    max_new theory_const
-    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
-  (* default settings*)
-  val vampire = vampire_filter_opts 60 false;
-    
-  (* a vampire for full proof output *)
-  fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts
-    max_new theory_const
-    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
-  (* default settings*)
-  val vampire_full = vampire_filter_opts 60 false;
+(* E prover *)
+
+fun eprover_opts max_new theory_const = tptp_prover_opts
+  max_new theory_const
+  (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent");
+
+val eprover = eprover_opts 100 false;
+
+fun eprover_opts_full max_new theory_const = full_prover_opts
+  max_new theory_const
+  (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent");
+
+val eprover_full = eprover_opts_full 100 false;
+
+
+(* SPASS *)
 
-  fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts
-    max_new theory_const
-    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
-  (* default settings *)
-  val eprover = eprover_filter_opts 100 false;
-    
-  (* an E for full proof output*)
-  fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts
-    max_new theory_const
-    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
-  (* default settings *)
-  val eprover_full = eprover_filter_opts_full 100 false;
+fun spass_opts max_new theory_const = external_prover
+  (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
+  (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
+  ResReconstruct.check_success_e_vamp_spass
+  ResReconstruct.lemma_list_dfg;
+
+val spass = spass_opts 40 true;
 
-  fun spass_filter_opts max_new theory_const = external_prover
-    (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
-    (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
-    ResReconstruct.check_success_e_vamp_spass
-    ResReconstruct.lemma_list_dfg
-  (* default settings*)
-  val spass = spass_filter_opts 40 true;
-    
-  (* remote prover invocation via SystemOnTPTP *)
-  fun remote_prover_filter_opts max_new theory_const name command =
-    tptp_prover_filter_opts max_new theory_const
-    (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command)
-  val remote_prover = remote_prover_filter_opts 60 false
+
+(* remote prover invocation via SystemOnTPTP *)
+
+fun remote_prover_opts max_new theory_const name command =
+  tptp_prover_opts max_new theory_const
+  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command);
+
+val remote_prover = remote_prover_opts 60 false;
 
 end;