src/HOL/Tools/ATP/VampireCommunication.ML
author paulson
Thu Apr 21 15:05:24 2005 +0200 (2005-04-21)
changeset 15789 4cb16144c81b
parent 15642 028059faa963
child 16480 abf475cf11f2
permissions -rw-r--r--
added hearder lines and deleted some redundant material
     1 (*  Title:      VampireCommunication.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 Vampire process        *)
     9 (***************************************************************************)
    10 
    11 (***********************************)
    12 (*  Write vampire output to a file *)
    13 (***********************************)
    14 
    15 fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
    16 			 in if thisLine = "%==============  End of proof. ==================\n" 
    17 			    then TextIO.output (fd, thisLine)
    18       			  else (
    19 				TextIO.output (fd, thisLine); logVampInput (instr,fd))
    20  			 end;
    21 
    22 (**********************************************************************)
    23 (*  Transfer the vampire output from the watcher to the input pipe of *)
    24 (*  the main Isabelle process                                         *)
    25 (**********************************************************************)
    26 
    27 fun transferVampInput (fromChild, toParent, ppid) = let 
    28                          val thisLine = TextIO.inputLine fromChild 
    29 			 in 
    30                             if (thisLine = "%==============  End of proof. ==================\n" )
    31 			    then ( 
    32                                    TextIO.output (toParent, thisLine);
    33                                    TextIO.flushOut toParent
    34                                   )
    35       			    else (
    36 				TextIO.output (toParent, thisLine); 
    37                                 TextIO.flushOut toParent;
    38                                 transferVampInput (fromChild, toParent, ppid)
    39                                 )
    40  			 end;
    41 
    42 
    43 (*********************************************************************************)
    44 (*  Inspect the output of a vampire process to see if it has found a proof,      *)
    45 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    46 (*********************************************************************************)
    47 
    48 fun startVampireTransfer (fromChild, toParent, ppid, childCmd) = 
    49                                        if (isSome (TextIO.canInput(fromChild, 5)))
    50                                        then
    51                                        (
    52                                        let val thisLine = TextIO.inputLine fromChild  
    53                                            in                 
    54                                              if (thisLine = "% Proof found. Thanks to Tanya!\n" )
    55                                              then      
    56                                               ( 
    57                                                 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
    58                                                 TextIO.output (toParent,childCmd^"\n" );
    59                                                 TextIO.flushOut toParent;
    60                                                 TextIO.output (toParent, thisLine);
    61                                                 TextIO.flushOut toParent;
    62 
    63                                                 transferVampInput (fromChild, toParent, ppid);
    64                                                 true)
    65                                               else if (thisLine = "% Unprovable.\n" ) 
    66                                                    then 
    67                                                        (
    68                                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
    69                                                         TextIO.output (toParent,childCmd^"\n" );
    70                                                         TextIO.flushOut toParent;
    71                                                         TextIO.output (toParent, thisLine);
    72                                                         TextIO.flushOut toParent;
    73 
    74                                                         true)
    75                                                    else if (thisLine = "% Proof not found.\n")
    76                                                         then 
    77                                                             (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);                                                            TextIO.output (toParent,childCmd^"\n" );
    78                                                              TextIO.flushOut toParent;
    79                                                              TextIO.output (toParent, thisLine);
    80                                                              TextIO.flushOut toParent;
    81                                                              true)
    82                                                         else 
    83                                                            (
    84                                                              startVampireTransfer (fromChild, toParent, ppid, childCmd)
    85                                                             )
    86                                             end
    87                                            )
    88                                          else (false)
    89 
    90 
    91 (***********************************************************************)
    92 (*  Function used by the Isabelle process to read in a vampire proof   *)
    93 (***********************************************************************)
    94 
    95 fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
    96 			 in 
    97                            if (thisLine = "%==============  End of proof. ==================\n" )
    98 			    then
    99                                (
   100                                 (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
   101                                )
   102                              else if (thisLine = "% Unprovable.\n" ) 
   103                                   then 
   104                                      (
   105                                       (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
   106                                       )
   107                                    else if (thisLine = "% Proof not found.\n")
   108                                         then 
   109                                             (
   110                                              Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
   111                                              )
   112 
   113 
   114                                          else 
   115                                             (
   116 				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
   117                                              )
   118  			 end;