--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/VampireCommunication.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,117 @@
+(* Title: VampireCommunication.ml
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
+(***************************************************************************)
+(* Code to deal with the transfer of proofs from a Vampire process *)
+(***************************************************************************)
+
+(***********************************)
+(* Write vampire output to a file *)
+(***********************************)
+
+fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr
+ in if thisLine = "%============== End of proof. ==================\n"
+ then TextIO.output (fd, thisLine)
+ else (
+ TextIO.output (fd, thisLine); logVampInput (instr,fd))
+ end;
+
+(**********************************************************************)
+(* Transfer the vampire output from the watcher to the input pipe of *)
+(* the main Isabelle process *)
+(**********************************************************************)
+
+fun transferVampInput (fromChild, toParent, ppid) = let
+ val thisLine = TextIO.inputLine fromChild
+ in
+ if (thisLine = "%============== End of proof. ==================\n" )
+ then (
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent
+ )
+ else (
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+ transferVampInput (fromChild, toParent, ppid)
+ )
+ end;
+
+
+(*********************************************************************************)
+(* Inspect the output of a vampire process to see if it has found a proof, *)
+(* and if so, transfer output to the input pipe of the main Isabelle process *)
+(*********************************************************************************)
+
+fun startVampireTransfer (fromChild, toParent, ppid, childCmd) =
+ if (isSome (TextIO.canInput(fromChild, 5)))
+ then
+ (
+ let val thisLine = TextIO.inputLine fromChild
+ in
+ if (thisLine = "% Proof found. Thanks to Tanya!\n" )
+ then
+ (
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
+ TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+
+ transferVampInput (fromChild, toParent, ppid);
+ true)
+ else if (thisLine = "% Unprovable.\n" )
+ then
+ (
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
+ TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+
+ true)
+ else if (thisLine = "% Proof not found.\n")
+ then
+ (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1); TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+ true)
+ else
+ (
+ startVampireTransfer (fromChild, toParent, ppid, childCmd)
+ )
+ end
+ )
+ else (false)
+
+
+(***********************************************************************)
+(* Function used by the Isabelle process to read in a vampire proof *)
+(***********************************************************************)
+
+fun getVampInput instr = let val thisLine = TextIO.inputLine instr
+ in
+ if (thisLine = "%============== End of proof. ==================\n" )
+ then
+ (
+ (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
+ )
+ else if (thisLine = "% Unprovable.\n" )
+ then
+ (
+ (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
+ )
+ else if (thisLine = "% Proof not found.\n")
+ then
+ (
+ Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
+ )
+
+
+ else
+ (
+ Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
+ )
+ end;