src/HOL/Tools/res_atp.ML
changeset 17772 818cec5f82a4
parent 17764 fde495b9e24b
child 17773 a7258e1020b7
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 06 10:13:34 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Oct 06 10:14:22 2005 +0200
     1.3 @@ -89,11 +89,9 @@
     1.4      fun make_atp_list [] n = []
     1.5        | make_atp_list (sg_term::xs) n =
     1.6            let
     1.7 -            val goalstring = Sign.string_of_term sign sg_term
     1.8              val probfile = prob_pathname n
     1.9              val time = Int.toString (!time_limit)
    1.10            in
    1.11 -            debug ("goalstring in make_atp_lists is\n" ^ goalstring);
    1.12              debug ("problem file in watcher_call_provers is " ^ probfile);
    1.13              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    1.14                versions of Unix.execute treat them differently!*)
    1.15 @@ -111,7 +109,7 @@
    1.16                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    1.17                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.18                in 
    1.19 -                  ([("spass", goalstring,
    1.20 +                  ([("spass", 
    1.21                       getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
    1.22                       optionline, probfile)] @ 
    1.23                    (make_atp_list xs (n+1)))
    1.24 @@ -120,14 +118,14 @@
    1.25  	    then 
    1.26                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
    1.27                in
    1.28 -                ([("vampire", goalstring, vampire, "-m 100000%-t " ^ time, probfile)] @
    1.29 +                ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
    1.30                   (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    1.31                end
    1.32        	     else if !prover = "E"
    1.33        	     then
    1.34  	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    1.35  	       in
    1.36 -		  ([("E", goalstring, Eprover, 
    1.37 +		  ([("E", Eprover, 
    1.38  		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
    1.39  		     probfile)] @
    1.40  		   (make_atp_list xs (n+1)))
    1.41 @@ -156,21 +154,20 @@
    1.42        val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.43        val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
    1.44        fun writenext n =
    1.45 -	if n=0 then ()
    1.46 +	if n=0 then []
    1.47  	 else
    1.48  	   (SELECT_GOAL
    1.49  	    (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
    1.50  	      METAHYPS(fn negs => 
    1.51  		(write (make_clauses negs) pf n 
    1.52  		       (axclauses,classrel_clauses,arity_clauses);
    1.53 -		 writenext (n-1); 
    1.54  		 all_tac))]) n th;
    1.55 -	    ())
    1.56 -      in writenext (length prems); clause_arr end;
    1.57 +	    pf n :: writenext (n-1))
    1.58 +      in (writenext (length prems), clause_arr) end;
    1.59  
    1.60  val last_watcher_pid =
    1.61 -  ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid) option);
    1.62 -
    1.63 +  ref (NONE : (TextIO.instream * TextIO.outstream * 
    1.64 +               Posix.Process.pid * string list) option);
    1.65  
    1.66  (*writes out the current clasimpset to a tptp file;
    1.67    turns off xsymbol at start of function, restoring it at end    *)
    1.68 @@ -179,22 +176,24 @@
    1.69    if Thm.no_prems th then ()
    1.70    else
    1.71      let
    1.72 -      val _ = (*Set up signal handler to tidy away dead processes*)
    1.73 -	      IsaSignal.signal (IsaSignal.chld, 
    1.74 -	        IsaSignal.SIG_HANDLE (fn _ =>
    1.75 -		  (Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []);
    1.76 -		   debug "Child signal received\n")));  
    1.77 +      fun reap s = (*Signal handler to tidy away dead processes*)
    1.78 +	   (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
    1.79 +		SOME _ => reap s | NONE => ()) 
    1.80 +           handle OS.SysErr _ => ()
    1.81 +      val _ = 
    1.82 +	      IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)
    1.83        val _ = (case !last_watcher_pid of NONE => ()
    1.84 -               | SOME (_, childout, pid) => 
    1.85 +               | SOME (_, childout, pid, files) => 
    1.86                    (debug ("Killing old watcher, pid = " ^ 
    1.87                            Int.toString (ResLib.intOfPid pid));
    1.88 -                   Watcher.killWatcher pid))
    1.89 +                   Watcher.killWatcher pid;
    1.90 +                   ignore (map (try OS.FileSys.remove) files)))
    1.91                handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    1.92 -      val clause_arr = write_problem_files prob_pathname (ctxt,th)
    1.93 +      val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th)
    1.94        val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
    1.95      in
    1.96 -      last_watcher_pid := SOME (childin, childout, pid);
    1.97 -      debug ("proof state: " ^ string_of_thm th);
    1.98 +      last_watcher_pid := SOME (childin, childout, pid, files);
    1.99 +      debug ("problem files: " ^ space_implode ", " files); 
   1.100        debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
   1.101        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   1.102      end);
   1.103 @@ -217,8 +216,6 @@
   1.104          handle Proof.STATE _ => error "No goal present";
   1.105      val thy = ProofContext.theory_of ctxt;
   1.106    in
   1.107 -    debug ("initial thm in isar_atp:\n" ^ 
   1.108 -           Pretty.string_of (ProofContext.pretty_thm ctxt goal));
   1.109      debug ("subgoals in isar_atp:\n" ^ 
   1.110             Pretty.string_of (ProofContext.pretty_term ctxt
   1.111               (Logic.mk_conjunction_list (Thm.prems_of goal))));