src/HOL/Tools/ATP/SpassCommunication.ML
author quigley
Wed Apr 06 12:01:37 2005 +0200 (2005-04-06 ago)
changeset 15658 2edb384bf61f
parent 15642 028059faa963
child 15684 5ec4d21889d6
permissions -rw-r--r--
watcher.ML and watcher.sig changed. Debug files now write to tmp.
     1 (*  Title:      SpassCommunication.ml
     2     Author:     Claire Quigley
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 (***************************************************************************)
     7 (*  Code to deal with the transfer of proofs from a Spass process          *)
     8 (***************************************************************************)
     9 
    10 (***********************************)
    11 (*  Write Spass   output to a file *)
    12 (***********************************)
    13 
    14 fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
    15 			 in if thisLine = "--------------------------SPASS-STOP------------------------------\n" 
    16 			    then TextIO.output (fd, thisLine)
    17       			  else (
    18 				TextIO.output (fd, thisLine); logSpassInput (instr,fd))
    19  			 end;
    20 
    21 
    22 (**********************************************************************)
    23 (*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
    24 (*  Isabelle goal to be proved), then transfer the reconstruction     *)
    25 (*  steps as a string to the input pipe of the main Isabelle process  *)
    26 (**********************************************************************)
    27 
    28 
    29 
    30 fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString) = let 
    31                          val thisLine = TextIO.inputLine fromChild 
    32 			 in 
    33                             if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
    34 			    then ( 
    35                                     let val proofextract = extract_proof (currentString^thisLine)
    36                                         val reconstr = spassString_to_reconString (currentString^thisLine) thmstring
    37                                         val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
    38                                in
    39                                          TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
    40                                    
    41                                          TextIO.output (toParent, reconstr^"\n");
    42                                          TextIO.flushOut toParent;
    43                                          TextIO.output (toParent, thmstring^"\n");
    44                                          TextIO.flushOut toParent;
    45                                          TextIO.output (toParent, goalstring^"\n");
    46                                          TextIO.flushOut toParent;
    47                                           
    48                                          Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    49                                          (* Attempt to prevent several signals from turning up simultaneously *)
    50                                          OS.Process.sleep(Time.fromSeconds 1)
    51                                                
    52                                     end
    53                                       
    54                                   )
    55       			    else (
    56 				
    57                                 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine))
    58                                 )
    59  			 end;
    60 
    61 
    62 
    63 (*********************************************************************************)
    64 (*  Inspect the output of a Spass   process to see if it has found a proof,      *)
    65 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    66 (*********************************************************************************)
    67 
    68  
    69 fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) = 
    70                                       (*let val _ = Posix.Process.wait ()
    71                                       in*)
    72                                        if (isSome (TextIO.canInput(fromChild, 5)))
    73                                        then
    74                                        (
    75                                        let val thisLine = TextIO.inputLine fromChild  
    76                                            in                 
    77                                              if (String.isPrefix "Here is a proof" thisLine )
    78                                              then     
    79                                               ( 
    80                                                  
    81                                                 
    82                                                 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine);
    83                                                 true)
    84                                              
    85                                              else 
    86                                                 (
    87                                                  startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd)
    88                                                 )
    89                                             end
    90                                            )
    91                                          else (false)
    92                                      (*  end*)
    93 
    94 fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd) = 
    95                                        let val spass_proof_file =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
    96                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
    97                                             val _ = TextIO.output (outfile, "checking proof found")
    98                                              
    99                                             val _ =  TextIO.closeOut outfile
   100                                        in 
   101                                        if (isSome (TextIO.canInput(fromChild, 5)))
   102                                        then
   103                                        (
   104                                        let val thisLine = TextIO.inputLine fromChild  
   105                                            in if ( thisLine = "SPASS beiseite: Proof found.\n" )
   106                                               then      
   107                                               (  
   108                                                  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
   109                                                      val _ = TextIO.output (outfile, (thisLine))
   110                                              
   111                                                      val _ =  TextIO.closeOut outfile
   112                                                  in 
   113                                                     startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) 
   114                                                  end
   115                                                )   
   116                                                else if (thisLine= "SPASS beiseite: Completion found.\n" )
   117                                                    then  
   118 
   119                                                  (
   120                                                       let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
   121                                                              val _ = TextIO.output (outfile, (thisLine))
   122                                              
   123                                                              val _ =  TextIO.closeOut outfile
   124                                                       in
   125                                                        
   126                                                         (*TextIO.output (toParent,childCmd^"\n" );
   127                                                         TextIO.flushOut toParent;*)
   128                                                         TextIO.output (spass_proof_file, (thisLine));
   129                                                         TextIO.flushOut spass_proof_file;
   130                                                         TextIO.closeOut spass_proof_file;
   131                                                         (*TextIO.output (toParent, thisLine);
   132                                                         TextIO.flushOut toParent;
   133                                                         TextIO.output (toParent, "bar\n");
   134                                                         TextIO.flushOut toParent;*)
   135 
   136                                                        TextIO.output (toParent, thisLine^"\n");
   137                                                        TextIO.flushOut toParent;
   138                                                        TextIO.output (toParent, thmstring^"\n");
   139                                                        TextIO.flushOut toParent;
   140                                                        TextIO.output (toParent, goalstring^"\n");
   141                                                        TextIO.flushOut toParent;
   142                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   143                                                        (* Attempt to prevent several signals from turning up simultaneously *)
   144                                                        OS.Process.sleep(Time.fromSeconds 1);
   145                                                         true  
   146                                                       end) 
   147                                                      else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
   148                                                           then  
   149                                                 (
   150                                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   151                                                         TextIO.output (toParent,childCmd^"\n" );
   152                                                         TextIO.flushOut toParent;
   153                                                         TextIO.output (toParent, thisLine);
   154                                                         TextIO.flushOut toParent;
   155 
   156                                                         true) 
   157                                                           else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" )                                                             then
   158                                                  (
   159                                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   160                                                         TextIO.output (toParent,childCmd^"\n" );
   161                                                         TextIO.flushOut toParent;
   162                                                         TextIO.output (toParent, thisLine);
   163                                                         TextIO.flushOut toParent;
   164 
   165                                                         true)
   166                                                     else
   167                                                        (TextIO.output (spass_proof_file, (thisLine));
   168                                                        TextIO.flushOut spass_proof_file;
   169                                                        checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd))
   170 
   171                                               end
   172                                           )
   173                                          else 
   174                                              (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false)
   175                                       end
   176 
   177   
   178 (***********************************************************************)
   179 (*  Function used by the Isabelle process to read in a spass proof   *)
   180 (***********************************************************************)
   181 
   182 
   183 (***********************************************************************)
   184 (*  Function used by the Isabelle process to read in a vampire proof   *)
   185 (***********************************************************************)
   186 
   187 (*fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
   188 			 in 
   189                            if (thisLine = "%==============  End of proof. ==================\n" )
   190 			    then
   191                                (
   192                                 (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
   193                                )
   194                              else if (thisLine = "% Unprovable.\n" ) 
   195                                   then 
   196                                      (
   197                                       (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
   198                                       )
   199                                    else if (thisLine = "% Proof not found.\n")
   200                                         then 
   201                                             (
   202                                              Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
   203                                              )
   204 
   205 
   206                                          else 
   207                                             (
   208 				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
   209                                              )
   210  			 end;
   211 
   212 *)
   213 
   214 fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
   215                           then
   216                                let val thisLine = TextIO.inputLine instr 
   217                                    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
   218                                              
   219                                    val _ =  TextIO.closeOut outfile
   220 			       in 
   221                                      if ( (substring (thisLine, 0,1))= "[")
   222                                      then 
   223 			                 (*Pretty.writeln(Pretty.str (thisLine))*)
   224                                              let val reconstr = thisLine
   225                                                  val thmstring = TextIO.inputLine instr 
   226                                                  val goalstring = TextIO.inputLine instr   
   227                                              in
   228                                                  (reconstr, thmstring, goalstring)
   229                                              end
   230                                      else if (thisLine = "SPASS beiseite: Completion found.\n" ) 
   231                                           then 
   232                                           (
   233                                              let val reconstr = thisLine
   234                                                  val thmstring = TextIO.inputLine instr
   235                                                  val goalstring = TextIO.inputLine instr
   236                                              in
   237                                                  (reconstr, thmstring, goalstring)
   238                                              end
   239                                           )
   240                                          else if (thisLine = "Proof found but translation failed!")
   241                                               then
   242   						(
   243 						   let val reconstr = thisLine
   244                                                        val thmstring = TextIO.inputLine instr
   245                                                        val goalstring = TextIO.inputLine instr
   246 						      val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_getSpass")));
   247                                     		val _ = TextIO.output (outfile, (thisLine))
   248                                      			 val _ =  TextIO.closeOut outfile
   249                                                    in
   250                                                       (reconstr, thmstring, goalstring)
   251                                                    end
   252 						)
   253                                         	 else
   254                                                      getSpassInput instr
   255                                             
   256  			        end
   257                           else 
   258                               ("No output from Spass.\n","","")
   259 
   260