src/HOL/Tools/ATP/SpassCommunication.ML

Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
Will now signal if ATP has run out of time and then kill the watcher.

(*  Title:      SpassCommunication.ml
    ID:         $Id$
    Author:     Claire Quigley
    Copyright   2004  University of Cambridge
*)

(***************************************************************************)
(*  Code to deal with the transfer of proofs from a Spass process          *)
(***************************************************************************)
signature SPASS_COMM =
  sig
    val reconstruct : bool ref
    val spass: bool ref
    val getSpassInput : TextIO.instream -> string * string * string
    val checkSpassProofFound:  TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
                               string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array  * int -> bool
    
  end;

structure SpassComm :SPASS_COMM =
struct

(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
val reconstruct = ref true;
val spass = ref true;

(***********************************)
(*  Write Spass   output to a file *)
(***********************************)

fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
			 in if thisLine = "--------------------------SPASS-STOP------------------------------\n" 
			    then TextIO.output (fd, thisLine)
      			  else (
				TextIO.output (fd, thisLine); logSpassInput (instr,fd))
 			 end;

(**********************************************************************)
(*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
(*  Isabelle goal to be proved), then transfer the reconstruction     *)
(*  steps as a string to the input pipe of the main Isabelle process  *)
(**********************************************************************)


val atomize_tac =    SUBGOAL
     (fn (prop,_) =>
	 let val ts = Logic.strip_assums_hyp prop
	 in EVERY1 
		[METAHYPS
		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
     end);


fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr  (num_of_clauses:int ) = 
 let val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3")));
 in
SELECT_GOAL
  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
  METAHYPS(fn negs => (if !reconstruct 
		       then 
			   Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring 
								     toParent ppid negs clause_arr  num_of_clauses 
		       else
			   Recon_Transfer.spassString_to_lemmaString proofextract thmstring goalstring 
								     toParent ppid negs clause_arr  num_of_clauses ))]) sg_num	
 end ;


fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr,  num_of_clauses) = let 
                         val thisLine = TextIO.inputLine fromChild 
			 in 
                            if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
			    then ( 
                                    let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
                                        val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2")));
                                
			            in 

                                        TextIO.output(foo,(proofextract));TextIO.closeOut foo;
                                        reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  clause_arr  num_of_clauses thm
                                               
                                    end
                                  )
      			    else (
				
                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr,  num_of_clauses)
                                )
 			 end;




(*********************************************************************************)
(*  Inspect the output of a Spass   process to see if it has found a proof,      *)
(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
(*********************************************************************************)

 
fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = 
                                      (*let val _ = Posix.Process.wait ()
                                      in*)
                                       
                                       if (isSome (TextIO.canInput(fromChild, 5)))
                                       then
                                       (
                                       let val thisLine = TextIO.inputLine fromChild  
                                           in                 
                                             if (String.isPrefix "Here is a proof" thisLine )
                                             then     
                                              ( 
                                                 let 
                                               val outfile =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer")));
                                               val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
                                               val _ =  TextIO.closeOut outfile;
                                               in
                                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr,  num_of_clauses);
                                                true
                                               end)
                                             
                                             else 
                                                (
                                                 startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses)
                                                )
                                            end
                                           )
                                         else (false)
                                     (*  end*)



fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  (num_of_clauses:int )) = 
                                       let val spass_proof_file =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "spass_proof")))
                                            val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
                                            val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm))
                                             
                                            val _ =  TextIO.closeOut outfile
                                       in 
                                       if (isSome (TextIO.canInput(fromChild, 5)))
                                       then
                                       (
                                       let val thisLine = TextIO.inputLine fromChild  
                                           in if ( thisLine = "SPASS beiseite: Proof found.\n" )
                                              then      
                                              (  
                                                 let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
                                                     val _ = TextIO.output (outfile, (thisLine))
                                             
                                                     val _ =  TextIO.closeOut outfile
                                                 in 
                                                    startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses) 
                                                 end
                                               )   
                                               else if (thisLine= "SPASS beiseite: Completion found.\n" )
                                                   then  

                                                 (
                                                      let    val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
                                                             val _ = TextIO.output (outfile, (thisLine))
                                             
                                                             val _ =  TextIO.closeOut outfile
                                                      in
                                                       
                                                        TextIO.output (toParent,childCmd^"\n" );
                                                        TextIO.flushOut toParent;
                                                        TextIO.output (spass_proof_file, (thisLine));
                                                        TextIO.flushOut spass_proof_file;
                                                        TextIO.closeOut spass_proof_file;
                                                        (*TextIO.output (toParent, thisLine);
                                                        TextIO.flushOut toParent;
                                                        TextIO.output (toParent, "bar\n");
                                                        TextIO.flushOut toParent;*)

                                                       TextIO.output (toParent, thisLine^"\n");
                                                       TextIO.flushOut toParent;
                                                       TextIO.output (toParent, thmstring^"\n");
                                                       TextIO.flushOut toParent;
                                                       TextIO.output (toParent, goalstring^"\n");
                                                       TextIO.flushOut toParent;
                                                       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
                                                       (* Attempt to prevent several signals from turning up simultaneously *)
                                                       Posix.Process.sleep(Time.fromSeconds 1);
                                                        true  
                                                      end) 
                                                     else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
                                                          then  
                                                		( let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                          	(*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
                                                     		val _ = TextIO.output (outfile, (thisLine))
                                             	
                                                    
                                                     		in TextIO.output (toParent, thisLine^"\n");
                                                     		  TextIO.flushOut toParent;
                                                     		  TextIO.output (toParent, thmstring^"\n");
                                                     		  TextIO.flushOut toParent;
                                                     		  TextIO.output (toParent, goalstring^"\n");
                                                     		  TextIO.flushOut toParent;
                                                     		  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
                                                    		  TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile;

                                                	       (* Attempt to prevent several signals from turning up simultaneously *)
                                                       		Posix.Process.sleep(Time.fromSeconds 1);
                                                       		 true 
                                                       		end)


 
                                                    else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" )                                                           		    then
                                                 (
                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
                                                        TextIO.output (toParent,childCmd^"\n" );
                                                        TextIO.flushOut toParent;
                                                        TextIO.output (toParent, thisLine);
                                                        TextIO.flushOut toParent;

                                                        true)
                                                    else
                                                       (TextIO.output (spass_proof_file, (thisLine));
                                                       TextIO.flushOut spass_proof_file;
                                                       checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses))

                                              end
                                          )
                                         else 
                                             (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false)
                                      end

  
(***********************************************************************)
(*  Function used by the Isabelle process to read in a spass proof   *)
(***********************************************************************)



fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
                          then
                               let val thisLine = TextIO.inputLine instr 
                                   val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))

                                             
                                   val _ =  TextIO.closeOut outfile
			       in 
                                     if ( (substring (thisLine, 0,1))= "[")
                                     then 
			                 (*Pretty.writeln(Pretty.str (thisLine))*)
                                             let val reconstr = thisLine
                                                 val thmstring = TextIO.inputLine instr 
                                                 val goalstring = TextIO.inputLine instr   
                                             in
                                                 (reconstr, thmstring, goalstring)
                                             end
                                     else if (String.isPrefix "SPASS beiseite:" thisLine ) 
                                          then 
                                          (
                                             let val reconstr = thisLine
                                                 val thmstring = TextIO.inputLine instr
                                                 val goalstring = TextIO.inputLine instr
                                             in
                                                 (reconstr, thmstring, goalstring)
                                             end
                                          )

					else if (String.isPrefix   "Rules from"  thisLine)
                                        then 
                                          (
                                             let val reconstr = thisLine
                                                 val thmstring = TextIO.inputLine instr
                                                 val goalstring = TextIO.inputLine instr
                                             in
                                                 (reconstr, thmstring, goalstring)
                                             end
                                          )

                                         else if ((substring (thisLine, 0,5)) = "Proof") 
                                              then
  						(
						   let val reconstr = thisLine
                                                       val thmstring = TextIO.inputLine instr
                                                       val goalstring = TextIO.inputLine instr
						      val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getSpass")));
                                    		val _ = TextIO.output (outfile, (thisLine))
                                     			 val _ =  TextIO.closeOut outfile
                                                   in
                                                      (reconstr, thmstring, goalstring)
                                                   end
						)
                                        	 else
                                                     getSpassInput instr
                                            
 			        end
                          else 
                              ("No output from reconstruction process.\n","","")


end;