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