3 Author: Claire Quigley |
3 Author: Claire Quigley |
4 Copyright 2004 University of Cambridge |
4 Copyright 2004 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 (***************************************************************************) |
7 (***************************************************************************) |
8 (* Code to deal with the transfer of proofs from a Vamp process *) |
8 (* Code to deal with the transfer of proofs from a Vampire process *) |
9 (***************************************************************************) |
9 (***************************************************************************) |
10 signature VAMP_COMM = |
10 signature VAMP_COMM = |
11 sig |
11 sig |
12 val reconstruct : bool ref |
|
13 val getVampInput : TextIO.instream -> string * string * string |
12 val getVampInput : TextIO.instream -> string * string * string |
14 val checkVampProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string * |
13 val checkVampProofFound: |
15 string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array * int -> bool |
14 TextIO.instream * TextIO.outstream * Posix.Process.pid * string * |
16 |
15 string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool |
17 end; |
16 end; |
18 |
17 |
19 structure VampComm :VAMP_COMM = |
18 structure VampComm : VAMP_COMM = |
20 struct |
19 struct |
21 |
20 |
22 (* switch for whether to reconstruct a proof found, or just list the lemmas used *) |
|
23 val reconstruct = ref true; |
|
24 |
|
25 (***********************************) |
21 (***********************************) |
26 (* Write Vamp output to a file *) |
22 (* Write Vampire output to a file *) |
27 (***********************************) |
23 (***********************************) |
28 |
24 |
29 fun logVampInput (instr, fd) = |
25 fun logVampInput (instr, fd) = |
30 let val thisLine = TextIO.inputLine instr |
26 let val thisLine = TextIO.inputLine instr |
31 in if (thisLine = "%============== End of proof. ==================\n" ) |
27 in if (thisLine = "%============== End of proof. ==================\n" ) |
32 then TextIO.output (fd, thisLine) |
28 then TextIO.output (fd, thisLine) |
33 else ( |
29 else (TextIO.output (fd, thisLine); logVampInput (instr,fd)) |
34 TextIO.output (fd, thisLine); logVampInput (instr,fd)) |
|
35 end; |
30 end; |
36 |
31 |
37 (**********************************************************************) |
32 (**********************************************************************) |
38 (* Reconstruct the Vamp proof w.r.t. thmstring (string version of *) |
33 (* Reconstruct the Vampire proof w.r.t. thmstring (string version of *) |
39 (* Isabelle goal to be proved), then transfer the reconstruction *) |
34 (* Isabelle goal to be proved), then transfer the reconstruction *) |
40 (* steps as a string to the input pipe of the main Isabelle process *) |
35 (* steps as a string to the input pipe of the main Isabelle process *) |
41 (**********************************************************************) |
36 (**********************************************************************) |
42 |
37 |
43 |
38 fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num |
44 val atomize_tac = |
39 clause_arr num_of_clauses = |
45 SUBGOAL |
|
46 (fn (prop,_) => |
|
47 let val ts = Logic.strip_assums_hyp prop |
|
48 in EVERY1 |
|
49 [METAHYPS |
|
50 (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), |
|
51 REPEAT_DETERM_N (length ts) o (etac thin_rl)] |
|
52 end); |
|
53 |
|
54 |
|
55 fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr (num_of_clauses:int ) = |
|
56 let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3"))); |
|
57 in |
|
58 SELECT_GOAL |
40 SELECT_GOAL |
59 (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, |
41 (EVERY1 |
60 METAHYPS(fn negs => |
42 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, |
61 ((*if !reconstruct |
43 METAHYPS(fn negs => |
62 then |
44 (Recon_Transfer.vampString_to_lemmaString proofextract thmstring |
63 Recon_Transfer.vampString_to_reconString proofextract thmstring goalstring |
45 goalstring toParent ppid negs clause_arr num_of_clauses ))]) sg_num |
64 toParent ppid negs clause_arr num_of_clauses |
|
65 else*) |
|
66 Recon_Transfer.vampString_to_lemmaString proofextract thmstring goalstring |
|
67 toParent ppid negs clause_arr num_of_clauses ))]) sg_num |
|
68 end ; |
|
69 |
46 |
70 |
47 |
71 fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = |
48 fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = |
72 let |
49 let val thisLine = TextIO.inputLine fromChild |
73 val thisLine = TextIO.inputLine fromChild |
|
74 in |
50 in |
75 if (thisLine = "%============== End of proof. ==================\n" ) |
51 if (thisLine = "%============== End of proof. ==================\n" ) |
76 then ( |
52 then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) |
77 let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) |
53 in |
78 val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2"))); |
54 File.write (File.tmp_path (Path.basic"extracted-prf-vamp")) proofextract; |
79 |
55 reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num |
80 in |
56 clause_arr num_of_clauses thm |
81 |
57 end |
82 TextIO.output(foo,(proofextract));TextIO.closeOut foo; |
58 else transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, |
83 reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr num_of_clauses thm |
59 currentString^thisLine, thm, sg_num, clause_arr, num_of_clauses) |
84 |
|
85 end |
|
86 ) |
|
87 else ( |
|
88 |
|
89 transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr, num_of_clauses) |
|
90 ) |
|
91 end; |
60 end; |
92 |
61 |
93 |
62 |
94 |
|
95 |
|
96 (*********************************************************************************) |
63 (*********************************************************************************) |
97 (* Inspect the output of a Vamp process to see if it has found a proof, *) |
64 (* Inspect the output of a Vampire process to see if it has found a proof, *) |
98 (* and if so, transfer output to the input pipe of the main Isabelle process *) |
65 (* and if so, transfer output to the input pipe of the main Isabelle process *) |
99 (*********************************************************************************) |
66 (*********************************************************************************) |
100 |
67 |
101 |
68 |
102 fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = |
69 fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, |
103 (*let val _ = Posix.Process.wait () |
70 thm, sg_num,clause_arr, num_of_clauses) = |
104 in*) |
71 if isSome (TextIO.canInput(fromChild, 5)) |
105 |
|
106 if (isSome (TextIO.canInput(fromChild, 5))) |
|
107 then |
72 then |
108 ( |
|
109 let val thisLine = TextIO.inputLine fromChild |
73 let val thisLine = TextIO.inputLine fromChild |
110 in |
74 in |
111 if (thisLine = "%================== Proof: ======================\n") |
75 if (thisLine = "%================== Proof: ======================\n") |
112 then |
76 then |
113 ( |
77 (File.append (File.tmp_path (Path.basic "transfer-vamp")) |
114 let |
78 ("about to transfer proof, thm is: " ^ string_of_thm thm); |
115 val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer"))); |
79 transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, |
116 val _= TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm)); |
80 thisLine, thm, sg_num,clause_arr, num_of_clauses); |
117 val _ = TextIO.closeOut outfile; |
81 true) |
118 in |
|
119 transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr, num_of_clauses); |
|
120 true |
|
121 end) |
|
122 |
|
123 else |
82 else |
124 ( |
83 startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring, |
125 startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses) |
84 childCmd, thm, sg_num,clause_arr, num_of_clauses) |
126 ) |
|
127 end |
85 end |
128 ) |
86 else false |
129 else (false) |
87 |
130 (* end*) |
88 |
131 |
89 fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, num_of_clauses) = |
132 |
90 let val vamp_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof"))) |
133 |
91 val _ = File.write (File.tmp_path (Path.basic "checking-prf-vamp")) |
134 fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) = |
92 ("checking if proof found, thm is: " ^ string_of_thm thm) |
135 let val vamp_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof"))) |
|
136 val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkvamp"))); |
|
137 val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm)) |
|
138 |
|
139 val _ = TextIO.closeOut outfile |
|
140 in |
93 in |
141 if (isSome (TextIO.canInput(fromChild, 5))) |
94 if (isSome (TextIO.canInput(fromChild, 5))) |
142 then |
95 then |
143 ( |
96 ( |
144 let val thisLine = TextIO.inputLine fromChild |
97 let val thisLine = TextIO.inputLine fromChild |
145 in if (thisLine = "% Proof found. Thanks to Tanya!\n" ) |
98 in if (thisLine = "% Proof found. Thanks to Tanya!\n" ) |
146 then |
99 then |
147 ( |
100 let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); |
148 let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) |
|
149 val _ = TextIO.output (outfile, (thisLine)) |
101 val _ = TextIO.output (outfile, (thisLine)) |
150 |
102 |
151 val _ = TextIO.closeOut outfile |
103 val _ = TextIO.closeOut outfile |
152 in |
104 in |
153 startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) |
105 startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) |
154 end |
106 end |
155 ) |
|
156 else if (thisLine = "% Unprovable.\n" ) |
107 else if (thisLine = "% Unprovable.\n" ) |
157 then |
108 then |
158 |
|
159 ( |
|
160 let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) |
109 let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) |
161 val _ = TextIO.output (outfile, (thisLine)) |
110 val _ = TextIO.output (outfile, (thisLine)) |
162 |
111 |
163 val _ = TextIO.closeOut outfile |
112 val _ = TextIO.closeOut outfile |
164 in |
113 in |