src/HOL/Tools/res_atp.ML

 
 (* a special version of repeat_RS *)
 fun repeat_someI_ex thm = repeat_RS thm someI_ex;
 
 
-(*********************************************************************)
-(* write out a subgoal as tptp clauses to the file "probN"           *)
-(* where N is the number of this subgoal                             *)
-(*********************************************************************)
-
+(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
 fun tptp_inputs_tfrees thms n axclauses =
     let
       val _ = debug ("in tptp_inputs_tfrees 0")
       val clss = map (ResClause.make_conjecture_clause_thm) thms
       val _ = debug ("in tptp_inputs_tfrees 1")

       ResLib.writeln_strs out (tfree_clss @ tptp_clss);
       TextIO.closeOut out;
       debug probfile
     end;
 
-
-(*********************************************************************)
-(* write out a subgoal as DFG clauses to the file "probN"           *)
-(* where N is the number of this subgoal                             *)
-(*********************************************************************)
-
+(* write out a subgoal in DFG format to the file "xxxx_N"*)
 fun dfg_inputs_tfrees thms n axclauses = 
     let val clss = map (ResClause.make_conjecture_clause_thm) thms
         val probfile = prob_pathname() ^ "_" ^ (string_of_int n)
         val _ = debug ("about to write out dfg prob file " ^ probfile)
-        val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
+        val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ string_of_int n)
                         axclauses [] [] []    
 	val out = TextIO.openOut(probfile)
     in
 	(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
-(* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
     end;
 
 
 (*********************************************************************)
 (* call prover with settings and problem file for the current subgoal *)

           let
             val goalstring = proofstring (Sign.string_of_term sign sg_term)
             val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
 
             val probfile = prob_pathname() ^ "_" ^ string_of_int n
-            val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
+            val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
           in
             (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
               versions of Unix.execute treat them differently!*)
             if !prover = "spass"
             then

              else tptp_inputs_tfrees (make_clauses negs) n axclauses;
              write_problem_files axclauses thm (n-1); 
              all_tac))]) n thm;
         ());
 
-
-(*FIXME: WHAT IS THMS FOR????*)
+val last_watcher_pid = ref (NONE : Posix.Process.pid option);
 
 (******************************************************************)
 (* called in Isar automatically                                   *)
 (* writes out the current clasimpset to a tptp file               *)
 (* turns off xsymbol at start of function, restoring it at end    *)
 (******************************************************************)
 (*FIX changed to clasimp_file *)
 val isar_atp = setmp print_mode [] 
- (fn (ctxt, thms, thm) =>
+ (fn (ctxt, thm) =>
   if Thm.no_prems thm then ()
   else
     let
       val _= debug ("in isar_atp")
       val thy = ProofContext.theory_of ctxt
       val prems = Thm.prems_of thm
-      val thms_string = Meson.concat_with_and (map string_of_thm thms)
       val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
 
+      val _ = (case !last_watcher_pid of NONE => ()
+               | SOME pid => (*FIXME: should kill ATP processes too; at least they time out*)
+                  (debug ("Killing old watcher, pid = " ^ 
+                          Int.toString (ResLib.intOfPid pid));
+                   Watcher.killWatcher pid))
+              handle OS.SysErr _ => debug "Attempt to kill watcher failed";
       (*set up variables for writing out the clasimps to a tptp file*)
       val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
               (*FIXME: hack!! need to consider relevance for all prems*)
       val _ = debug ("claset and simprules total clauses = " ^ 
                      string_of_int (Array.length clause_arr))
       val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
     in
-      debug ("initial thms: " ^ thms_string);
+      last_watcher_pid := SOME pid;
       debug ("subgoals: " ^ prems_string);
       debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
       write_problem_files axclauses thm (length prems);
       watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid)
     end);
 
 val isar_atp_writeonly = setmp print_mode [] 
- (fn (ctxt, thms: thm list, thm) =>
+ (fn (ctxt, thm) =>
   if Thm.no_prems thm then ()
   else
     let val prems = Thm.prems_of thm
         val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
     in
       write_problem_files axclauses thm (length prems)
     end);
-
-
-(* convert locally declared rules to axiom clauses: UNUSED *)
-
-fun subtract_simpset thy ctxt =
-  let
-    val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
-    val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt)));
-  in map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2) end;
-
-fun subtract_claset thy ctxt =
-  let
-    val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy));
-    val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt));
-    val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
-  in subtract netI1 netI2 @ subtract netE1 netE2 end;
-
 
 
 (** the Isar toplevel hook **)
 
 val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>

     debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
     debug ("current theory: " ^ Context.theory_name thy);
     hook_count := !hook_count +1;
     debug ("in hook for time: " ^(string_of_int (!hook_count)) );
     ResClause.init thy;
-    if !destdir = "" then isar_atp (ctxt, ProofContext.prems_of ctxt, goal)
-    else isar_atp_writeonly (ctxt, ProofContext.prems_of ctxt, goal)
+    if !destdir = "" then isar_atp (ctxt, goal)
+    else isar_atp_writeonly (ctxt, goal)
   end);
 
 val call_atpP =
   OuterSyntax.improper_command 
     "ProofGeneral.call_atp"