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