src/HOL/Tools/ATP/SpassCommunication.ML
author paulson
Thu Apr 21 15:05:24 2005 +0200 (2005-04-21)
changeset 15789 4cb16144c81b
parent 15787 8fad4bd4e53c
child 15919 b30a35432f5a
permissions -rw-r--r--
added hearder lines and deleted some redundant material
     1 (*  Title:      SpassCommunication.ml
     2     ID:         $Id$
     3     Author:     Claire Quigley
     4     Copyright   2004  University of Cambridge
     5 *)
     6 
     7 (***************************************************************************)
     8 (*  Code to deal with the transfer of proofs from a Spass process          *)
     9 (***************************************************************************)
    10 
    11 (***********************************)
    12 (*  Write Spass   output to a file *)
    13 (***********************************)
    14 
    15 fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
    16 			 in if thisLine = "--------------------------SPASS-STOP------------------------------\n" 
    17 			    then TextIO.output (fd, thisLine)
    18       			  else (
    19 				TextIO.output (fd, thisLine); logSpassInput (instr,fd))
    20  			 end;
    21 
    22 
    23 (**********************************************************************)
    24 (*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
    25 (*  Isabelle goal to be proved), then transfer the reconstruction     *)
    26 (*  steps as a string to the input pipe of the main Isabelle process  *)
    27 (**********************************************************************)
    28 
    29 
    30 val atomize_tac =
    31     SUBGOAL
    32      (fn (prop,_) =>
    33 	 let val ts = Logic.strip_assums_hyp prop
    34 	 in EVERY1 
    35 		[METAHYPS
    36 		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
    37 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    38      end);
    39 
    40 
    41 fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num = 
    42  let val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar3")));
    43  in
    44 SELECT_GOAL
    45   (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    46   METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs))]) sg_num
    47  end ;
    48 
    49 
    50 fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let 
    51                          val thisLine = TextIO.inputLine fromChild 
    52 			 in 
    53                             if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
    54 			    then ( 
    55                                     let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    56                                         val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
    57                                 
    58 			            in 
    59 
    60                                         TextIO.output(foo,(proofextract));TextIO.closeOut foo;
    61                                         reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num thm
    62                                                
    63                                     end
    64                                   )
    65       			    else (
    66 				
    67                                 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
    68                                 )
    69  			 end;
    70 
    71 
    72 (*
    73 
    74 fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let 
    75                          val thisLine = TextIO.inputLine fromChild 
    76 			 in 
    77                             if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
    78 			    then ( 
    79                                     let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    80                                         val reconstr = Recon_Transfer.spassString_to_reconString (currentString^thisLine) thmstring thm sg_num
    81                                         val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
    82                                in
    83                                          TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
    84                                    
    85                                          TextIO.output (toParent, reconstr^"\n");
    86                                          TextIO.flushOut toParent;
    87                                          TextIO.output (toParent, thmstring^"\n");
    88                                          TextIO.flushOut toParent;
    89                                          TextIO.output (toParent, goalstring^"\n");
    90                                          TextIO.flushOut toParent;
    91                                           
    92                                          Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    93                                          (* Attempt to prevent several signals from turning up simultaneously *)
    94                                          Posix.Process.sleep(Time.fromSeconds 1); ()
    95                                                
    96                                     end
    97                                       
    98                                   )
    99       			    else (
   100 				
   101                                 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
   102                                 )
   103  			 end;
   104 
   105 *)
   106 
   107 (*********************************************************************************)
   108 (*  Inspect the output of a Spass   process to see if it has found a proof,      *)
   109 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   110 (*********************************************************************************)
   111 
   112  
   113 fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num) = 
   114                                       (*let val _ = Posix.Process.wait ()
   115                                       in*)
   116                                        
   117                                        if (isSome (TextIO.canInput(fromChild, 5)))
   118                                        then
   119                                        (
   120                                        let val thisLine = TextIO.inputLine fromChild  
   121                                            in                 
   122                                              if (String.isPrefix "Here is a proof" thisLine )
   123                                              then     
   124                                               ( 
   125                                                  let 
   126                                                val outfile =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_transfer")));
   127                                                val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
   128                                                val _ =  TextIO.closeOut outfile;
   129                                                in
   130                                                 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num);
   131                                                 true
   132                                                end)
   133                                              
   134                                              else 
   135                                                 (
   136                                                  startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num)
   137                                                 )
   138                                             end
   139                                            )
   140                                          else (false)
   141                                      (*  end*)
   142 
   143 fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num) = 
   144                                        let val spass_proof_file =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
   145                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
   146                                             val _ = TextIO.output (outfile, "checking proof found, thm is: "^(string_of_thm thm))
   147                                              
   148                                             val _ =  TextIO.closeOut outfile
   149                                        in 
   150                                        if (isSome (TextIO.canInput(fromChild, 5)))
   151                                        then
   152                                        (
   153                                        let val thisLine = TextIO.inputLine fromChild  
   154                                            in if ( thisLine = "SPASS beiseite: Proof found.\n" )
   155                                               then      
   156                                               (  
   157                                                  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   158                                                      val _ = TextIO.output (outfile, (thisLine))
   159                                              
   160                                                      val _ =  TextIO.closeOut outfile
   161                                                  in 
   162                                                     startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num) 
   163                                                  end
   164                                                )   
   165                                                else if (thisLine= "SPASS beiseite: Completion found.\n" )
   166                                                    then  
   167 
   168                                                  (
   169                                                       let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   170                                                              val _ = TextIO.output (outfile, (thisLine))
   171                                              
   172                                                              val _ =  TextIO.closeOut outfile
   173                                                       in
   174                                                        
   175                                                         (*TextIO.output (toParent,childCmd^"\n" );
   176                                                         TextIO.flushOut toParent;*)
   177                                                         TextIO.output (spass_proof_file, (thisLine));
   178                                                         TextIO.flushOut spass_proof_file;
   179                                                         TextIO.closeOut spass_proof_file;
   180                                                         (*TextIO.output (toParent, thisLine);
   181                                                         TextIO.flushOut toParent;
   182                                                         TextIO.output (toParent, "bar\n");
   183                                                         TextIO.flushOut toParent;*)
   184 
   185                                                        TextIO.output (toParent, thisLine^"\n");
   186                                                        TextIO.flushOut toParent;
   187                                                        TextIO.output (toParent, thmstring^"\n");
   188                                                        TextIO.flushOut toParent;
   189                                                        TextIO.output (toParent, goalstring^"\n");
   190                                                        TextIO.flushOut toParent;
   191                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   192                                                        (* Attempt to prevent several signals from turning up simultaneously *)
   193                                                        Posix.Process.sleep(Time.fromSeconds 1);
   194                                                         true  
   195                                                       end) 
   196                                                      else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
   197                                                           then  
   198                                                 (
   199                                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   200                                                         TextIO.output (toParent,childCmd^"\n" );
   201                                                         TextIO.flushOut toParent;
   202                                                         TextIO.output (toParent, thisLine);
   203                                                         TextIO.flushOut toParent;
   204 
   205                                                         true) 
   206                                                           else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" )                                                             then
   207                                                  (
   208                                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   209                                                         TextIO.output (toParent,childCmd^"\n" );
   210                                                         TextIO.flushOut toParent;
   211                                                         TextIO.output (toParent, thisLine);
   212                                                         TextIO.flushOut toParent;
   213 
   214                                                         true)
   215                                                     else
   216                                                        (TextIO.output (spass_proof_file, (thisLine));
   217                                                        TextIO.flushOut spass_proof_file;
   218                                                        checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num))
   219 
   220                                               end
   221                                           )
   222                                          else 
   223                                              (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false)
   224                                       end
   225 
   226   
   227 (***********************************************************************)
   228 (*  Function used by the Isabelle process to read in a spass proof   *)
   229 (***********************************************************************)
   230 
   231 
   232 (***********************************************************************)
   233 (*  Function used by the Isabelle process to read in a vampire proof   *)
   234 (***********************************************************************)
   235 
   236 (*fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
   237 			 in 
   238                            if (thisLine = "%==============  End of proof. ==================\n" )
   239 			    then
   240                                (
   241                                 (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
   242                                )
   243                              else if (thisLine = "% Unprovable.\n" ) 
   244                                   then 
   245                                      (
   246                                       (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
   247                                       )
   248                                    else if (thisLine = "% Proof not found.\n")
   249                                         then 
   250                                             (
   251                                              Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
   252                                              )
   253 
   254 
   255                                          else 
   256                                             (
   257 				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
   258                                              )
   259  			 end;
   260 
   261 *)
   262 
   263 fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
   264                           then
   265                                let val thisLine = TextIO.inputLine instr 
   266                                    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
   267                                              
   268                                    val _ =  TextIO.closeOut outfile
   269 			       in 
   270                                      if ( (substring (thisLine, 0,1))= "[")
   271                                      then 
   272 			                 (*Pretty.writeln(Pretty.str (thisLine))*)
   273                                              let val reconstr = thisLine
   274                                                  val thmstring = TextIO.inputLine instr 
   275                                                  val goalstring = TextIO.inputLine instr   
   276                                              in
   277                                                  (reconstr, thmstring, goalstring)
   278                                              end
   279                                      else if (thisLine = "SPASS beiseite: Completion found.\n" ) 
   280                                           then 
   281                                           (
   282                                              let val reconstr = thisLine
   283                                                  val thmstring = TextIO.inputLine instr
   284                                                  val goalstring = TextIO.inputLine instr
   285                                              in
   286                                                  (reconstr, thmstring, goalstring)
   287                                              end
   288                                           )
   289                                          else if (thisLine = "Proof found but translation failed!")
   290                                               then
   291   						(
   292 						   let val reconstr = thisLine
   293                                                        val thmstring = TextIO.inputLine instr
   294                                                        val goalstring = TextIO.inputLine instr
   295 						      val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_getSpass")));
   296                                     		val _ = TextIO.output (outfile, (thisLine))
   297                                      			 val _ =  TextIO.closeOut outfile
   298                                                    in
   299                                                       (reconstr, thmstring, goalstring)
   300                                                    end
   301 						)
   302                                         	 else
   303                                                      getSpassInput instr
   304                                             
   305  			        end
   306                           else 
   307                               ("No output from reconstruction process.\n","","")
   308 
   309