paulson@21978
|
1 |
(* ID: $Id$
|
paulson@21979
|
2 |
Author: L C Paulson and Claire Quigley
|
paulson@21978
|
3 |
Copyright 2004 University of Cambridge
|
paulson@21978
|
4 |
*)
|
paulson@21978
|
5 |
|
paulson@21978
|
6 |
(***************************************************************************)
|
paulson@21979
|
7 |
(* Code to deal with the transfer of proofs from a prover process *)
|
paulson@21978
|
8 |
(***************************************************************************)
|
paulson@21978
|
9 |
signature RES_RECONSTRUCT =
|
paulson@24425
|
10 |
sig
|
paulson@24425
|
11 |
datatype atp = E | SPASS | Vampire
|
paulson@24425
|
12 |
val modulus: int ref
|
paulson@24425
|
13 |
val recon_sorts: bool ref
|
paulson@24425
|
14 |
val checkEProofFound:
|
paulson@24425
|
15 |
TextIO.instream * TextIO.outstream * Posix.Process.pid *
|
paulson@24425
|
16 |
string * Proof.context * thm * int * string Vector.vector -> bool
|
paulson@24425
|
17 |
val checkVampProofFound:
|
paulson@24425
|
18 |
TextIO.instream * TextIO.outstream * Posix.Process.pid *
|
paulson@24425
|
19 |
string * Proof.context * thm * int * string Vector.vector -> bool
|
paulson@24425
|
20 |
val checkSpassProofFound:
|
paulson@24425
|
21 |
TextIO.instream * TextIO.outstream * Posix.Process.pid *
|
paulson@24425
|
22 |
string * Proof.context * thm * int * string Vector.vector -> bool
|
paulson@24425
|
23 |
val signal_parent: TextIO.outstream * Posix.Process.pid * string * string -> unit
|
paulson@24425
|
24 |
val txt_path: string -> Path.T
|
paulson@24425
|
25 |
val fix_sorts: sort Vartab.table -> term -> term
|
paulson@24425
|
26 |
val invert_const: string -> string
|
paulson@24425
|
27 |
val invert_type_const: string -> string
|
paulson@24425
|
28 |
val num_typargs: Context.theory -> string -> int
|
paulson@24425
|
29 |
val make_tvar: string -> typ
|
paulson@24425
|
30 |
val strip_prefix: string -> string -> string option
|
paulson@24425
|
31 |
end;
|
paulson@21978
|
32 |
|
paulson@24425
|
33 |
structure ResReconstruct : RES_RECONSTRUCT =
|
paulson@21978
|
34 |
struct
|
paulson@21978
|
35 |
|
paulson@21978
|
36 |
val trace_path = Path.basic "atp_trace";
|
paulson@21978
|
37 |
|
wenzelm@23139
|
38 |
fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
|
paulson@21978
|
39 |
else ();
|
paulson@21978
|
40 |
|
paulson@24425
|
41 |
datatype atp = E | SPASS | Vampire;
|
paulson@21978
|
42 |
|
paulson@23833
|
43 |
val recon_sorts = ref true;
|
paulson@22491
|
44 |
|
paulson@22491
|
45 |
val modulus = ref 1; (*keep every nth proof line*)
|
paulson@22044
|
46 |
|
paulson@21978
|
47 |
(**** PARSING OF TSTP FORMAT ****)
|
paulson@21978
|
48 |
|
paulson@21978
|
49 |
(*Syntax trees, either termlist or formulae*)
|
paulson@21978
|
50 |
datatype stree = Int of int | Br of string * stree list;
|
paulson@21978
|
51 |
|
paulson@21978
|
52 |
fun atom x = Br(x,[]);
|
paulson@21978
|
53 |
|
paulson@21978
|
54 |
fun scons (x,y) = Br("cons", [x,y]);
|
paulson@21978
|
55 |
val listof = foldl scons (atom "nil");
|
paulson@21978
|
56 |
|
paulson@21978
|
57 |
(*Strings enclosed in single quotes, e.g. filenames*)
|
paulson@21978
|
58 |
val quoted = $$"'" |-- Scan.repeat (~$$"'") --| $$"'" >> implode;
|
paulson@21978
|
59 |
|
paulson@21978
|
60 |
(*Intended for $true and $false*)
|
paulson@21978
|
61 |
fun tf s = "c_" ^ str (Char.toUpper (String.sub(s,0))) ^ String.extract(s,1,NONE);
|
paulson@21978
|
62 |
val truefalse = $$"$" |-- Symbol.scan_id >> (atom o tf);
|
paulson@21978
|
63 |
|
paulson@21978
|
64 |
(*Integer constants, typically proof line numbers*)
|
paulson@21978
|
65 |
fun is_digit s = Char.isDigit (String.sub(s,0));
|
paulson@21978
|
66 |
val integer = Scan.many1 is_digit >> (valOf o Int.fromString o implode);
|
paulson@21978
|
67 |
|
paulson@21978
|
68 |
(*Generalized FO terms, which include filenames, numbers, etc.*)
|
paulson@21978
|
69 |
fun termlist x = (term -- Scan.repeat ($$"," |-- term) >> op::) x
|
paulson@21978
|
70 |
and term x = (quoted >> atom || integer>>Int || truefalse ||
|
paulson@21978
|
71 |
Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br ||
|
paulson@21978
|
72 |
$$"(" |-- term --| $$")" ||
|
paulson@24547
|
73 |
$$"[" |-- Scan.optional termlist [] --| $$"]" >> listof) x;
|
paulson@21978
|
74 |
|
paulson@21978
|
75 |
fun negate t = Br("c_Not", [t]);
|
paulson@21978
|
76 |
fun equate (t1,t2) = Br("c_equal", [t1,t2]);
|
paulson@21978
|
77 |
|
paulson@21978
|
78 |
(*Apply equal or not-equal to a term*)
|
paulson@21978
|
79 |
fun syn_equal (t, NONE) = t
|
paulson@21978
|
80 |
| syn_equal (t1, SOME (NONE, t2)) = equate (t1,t2)
|
paulson@21978
|
81 |
| syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2));
|
paulson@21978
|
82 |
|
paulson@21978
|
83 |
(*Literals can involve negation, = and !=.*)
|
paulson@24547
|
84 |
fun literal x = ($$"~" |-- literal >> negate ||
|
paulson@24547
|
85 |
(term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal)) x;
|
paulson@21978
|
86 |
|
paulson@21978
|
87 |
val literals = literal -- Scan.repeat ($$"|" |-- literal) >> op:: ;
|
paulson@21978
|
88 |
|
paulson@21978
|
89 |
(*Clause: a list of literals separated by the disjunction sign*)
|
paulson@24547
|
90 |
val clause = $$"(" |-- literals --| $$")" || Scan.single literal;
|
paulson@21978
|
91 |
|
paulson@21978
|
92 |
val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist);
|
paulson@21978
|
93 |
|
paulson@21978
|
94 |
(*<cnf_annotated> ::=Ęcnf(<name>,<formula_role>,<cnf_formula><annotations>).
|
paulson@21978
|
95 |
The <name> could be an identifier, but we assume integers.*)
|
wenzelm@23139
|
96 |
val tstp_line = (Scan.this_string "cnf" -- $$"(") |--
|
wenzelm@23139
|
97 |
integer --| $$"," -- Symbol.scan_id --| $$"," --
|
paulson@21978
|
98 |
clause -- Scan.option annotations --| $$ ")";
|
paulson@21978
|
99 |
|
paulson@21978
|
100 |
|
paulson@21978
|
101 |
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
|
paulson@21978
|
102 |
|
paulson@21978
|
103 |
exception STREE of stree;
|
paulson@21978
|
104 |
|
paulson@21978
|
105 |
(*If string s has the prefix s1, return the result of deleting it.*)
|
wenzelm@23139
|
106 |
fun strip_prefix s1 s =
|
paulson@24182
|
107 |
if String.isPrefix s1 s
|
paulson@24182
|
108 |
then SOME (ResClause.undo_ascii_of (String.extract (s, size s1, NONE)))
|
paulson@21978
|
109 |
else NONE;
|
paulson@21978
|
110 |
|
paulson@21978
|
111 |
(*Invert the table of translations between Isabelle and ATPs*)
|
paulson@21978
|
112 |
val type_const_trans_table_inv =
|
paulson@21978
|
113 |
Symtab.make (map swap (Symtab.dest ResClause.type_const_trans_table));
|
paulson@21978
|
114 |
|
paulson@21978
|
115 |
fun invert_type_const c =
|
paulson@21978
|
116 |
case Symtab.lookup type_const_trans_table_inv c of
|
paulson@21978
|
117 |
SOME c' => c'
|
paulson@21978
|
118 |
| NONE => c;
|
paulson@21978
|
119 |
|
paulson@21978
|
120 |
fun make_tvar b = TVar(("'" ^ b, 0), HOLogic.typeS);
|
paulson@21978
|
121 |
fun make_var (b,T) = Var((b,0),T);
|
paulson@21978
|
122 |
|
paulson@21978
|
123 |
(*Type variables are given the basic sort, HOL.type. Some will later be constrained
|
paulson@21978
|
124 |
by information from type literals, or by type inference.*)
|
paulson@21978
|
125 |
fun type_of_stree t =
|
paulson@21978
|
126 |
case t of
|
paulson@21978
|
127 |
Int _ => raise STREE t
|
wenzelm@23139
|
128 |
| Br (a,ts) =>
|
paulson@21978
|
129 |
let val Ts = map type_of_stree ts
|
wenzelm@23139
|
130 |
in
|
paulson@21978
|
131 |
case strip_prefix ResClause.tconst_prefix a of
|
paulson@21978
|
132 |
SOME b => Type(invert_type_const b, Ts)
|
wenzelm@23139
|
133 |
| NONE =>
|
paulson@21978
|
134 |
if not (null ts) then raise STREE t (*only tconsts have type arguments*)
|
wenzelm@23139
|
135 |
else
|
paulson@21978
|
136 |
case strip_prefix ResClause.tfree_prefix a of
|
paulson@21978
|
137 |
SOME b => TFree("'" ^ b, HOLogic.typeS)
|
wenzelm@23139
|
138 |
| NONE =>
|
paulson@21978
|
139 |
case strip_prefix ResClause.tvar_prefix a of
|
paulson@21978
|
140 |
SOME b => make_tvar b
|
paulson@21978
|
141 |
| NONE => make_tvar a (*Variable from the ATP, say X1*)
|
paulson@21978
|
142 |
end;
|
paulson@21978
|
143 |
|
paulson@21978
|
144 |
(*Invert the table of translations between Isabelle and ATPs*)
|
paulson@21978
|
145 |
val const_trans_table_inv =
|
wenzelm@23139
|
146 |
Symtab.update ("fequal", "op =")
|
paulson@22731
|
147 |
(Symtab.make (map swap (Symtab.dest ResClause.const_trans_table)));
|
paulson@21978
|
148 |
|
paulson@21978
|
149 |
fun invert_const c =
|
paulson@21978
|
150 |
case Symtab.lookup const_trans_table_inv c of
|
paulson@21978
|
151 |
SOME c' => c'
|
paulson@21978
|
152 |
| NONE => c;
|
paulson@21978
|
153 |
|
paulson@21978
|
154 |
(*The number of type arguments of a constant, zero if it's monomorphic*)
|
paulson@21978
|
155 |
fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s));
|
paulson@21978
|
156 |
|
paulson@21978
|
157 |
(*Generates a constant, given its type arguments*)
|
paulson@21978
|
158 |
fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts));
|
paulson@21978
|
159 |
|
paulson@21978
|
160 |
(*First-order translation. No types are known for variables. HOLogic.typeT should allow
|
paulson@21978
|
161 |
them to be inferred.*)
|
paulson@22428
|
162 |
fun term_of_stree args thy t =
|
paulson@21978
|
163 |
case t of
|
paulson@21978
|
164 |
Int _ => raise STREE t
|
paulson@22428
|
165 |
| Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*)
|
paulson@22428
|
166 |
| Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
|
wenzelm@23139
|
167 |
| Br (a,ts) =>
|
paulson@21978
|
168 |
case strip_prefix ResClause.const_prefix a of
|
wenzelm@23139
|
169 |
SOME "equal" =>
|
paulson@22731
|
170 |
list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
|
wenzelm@23139
|
171 |
| SOME b =>
|
paulson@21978
|
172 |
let val c = invert_const b
|
paulson@21978
|
173 |
val nterms = length ts - num_typargs thy c
|
paulson@22428
|
174 |
val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args)
|
paulson@22428
|
175 |
(*Extra args from hAPP come AFTER any arguments given directly to the
|
paulson@22428
|
176 |
constant.*)
|
paulson@21978
|
177 |
val Ts = List.map type_of_stree (List.drop(ts,nterms))
|
paulson@21978
|
178 |
in list_comb(const_of thy (c, Ts), us) end
|
paulson@21978
|
179 |
| NONE => (*a variable, not a constant*)
|
paulson@21978
|
180 |
let val T = HOLogic.typeT
|
paulson@21978
|
181 |
val opr = (*a Free variable is typically a Skolem function*)
|
paulson@21978
|
182 |
case strip_prefix ResClause.fixed_var_prefix a of
|
paulson@21978
|
183 |
SOME b => Free(b,T)
|
wenzelm@23139
|
184 |
| NONE =>
|
paulson@21978
|
185 |
case strip_prefix ResClause.schematic_var_prefix a of
|
paulson@21978
|
186 |
SOME b => make_var (b,T)
|
paulson@21978
|
187 |
| NONE => make_var (a,T) (*Variable from the ATP, say X1*)
|
paulson@23519
|
188 |
in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
|
paulson@21978
|
189 |
|
wenzelm@23139
|
190 |
(*Type class literal applied to a type. Returns triple of polarity, class, type.*)
|
paulson@21978
|
191 |
fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t
|
paulson@21978
|
192 |
| constraint_of_stree pol t = case t of
|
paulson@21978
|
193 |
Int _ => raise STREE t
|
wenzelm@23139
|
194 |
| Br (a,ts) =>
|
paulson@21978
|
195 |
(case (strip_prefix ResClause.class_prefix a, map type_of_stree ts) of
|
paulson@21978
|
196 |
(SOME b, [T]) => (pol, b, T)
|
paulson@21978
|
197 |
| _ => raise STREE t);
|
paulson@21978
|
198 |
|
paulson@21978
|
199 |
(** Accumulate type constraints in a clause: negative type literals **)
|
paulson@21978
|
200 |
|
paulson@21978
|
201 |
fun addix (key,z) = Vartab.map_default (key,[]) (cons z);
|
paulson@21978
|
202 |
|
paulson@21978
|
203 |
fun add_constraint ((false, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt
|
paulson@21978
|
204 |
| add_constraint ((false, cl, TVar(ix,_)), vt) = addix (ix,cl) vt
|
paulson@21978
|
205 |
| add_constraint (_, vt) = vt;
|
paulson@21978
|
206 |
|
paulson@21978
|
207 |
(*False literals (which E includes in its proofs) are deleted*)
|
paulson@21978
|
208 |
val nofalses = filter (not o equal HOLogic.false_const);
|
paulson@21978
|
209 |
|
paulson@22491
|
210 |
(*Final treatment of the list of "real" literals from a clause.*)
|
paulson@22491
|
211 |
fun finish [] = HOLogic.true_const (*No "real" literals means only type information*)
|
wenzelm@23139
|
212 |
| finish lits =
|
paulson@22491
|
213 |
case nofalses lits of
|
paulson@22491
|
214 |
[] => HOLogic.false_const (*The empty clause, since we started with real literals*)
|
paulson@22491
|
215 |
| xs => foldr1 HOLogic.mk_disj (rev xs);
|
paulson@22491
|
216 |
|
paulson@21978
|
217 |
(*Accumulate sort constraints in vt, with "real" literals in lits.*)
|
paulson@22491
|
218 |
fun lits_of_strees ctxt (vt, lits) [] = (vt, finish lits)
|
wenzelm@23139
|
219 |
| lits_of_strees ctxt (vt, lits) (t::ts) =
|
paulson@22012
|
220 |
lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts
|
wenzelm@23139
|
221 |
handle STREE _ =>
|
paulson@22428
|
222 |
lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts;
|
paulson@21978
|
223 |
|
paulson@21978
|
224 |
(*Update TVars/TFrees with detected sort constraints.*)
|
paulson@21978
|
225 |
fun fix_sorts vt =
|
paulson@21978
|
226 |
let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
|
paulson@21978
|
227 |
| tysubst (TVar (xi, s)) = TVar (xi, getOpt (Vartab.lookup vt xi, s))
|
paulson@21978
|
228 |
| tysubst (TFree (x, s)) = TFree (x, getOpt (Vartab.lookup vt (x,~1), s))
|
paulson@21978
|
229 |
fun tmsubst (Const (a, T)) = Const (a, tysubst T)
|
paulson@21978
|
230 |
| tmsubst (Free (a, T)) = Free (a, tysubst T)
|
paulson@21978
|
231 |
| tmsubst (Var (xi, T)) = Var (xi, tysubst T)
|
paulson@21978
|
232 |
| tmsubst (t as Bound _) = t
|
paulson@21978
|
233 |
| tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
|
paulson@21978
|
234 |
| tmsubst (t $ u) = tmsubst t $ tmsubst u;
|
paulson@21978
|
235 |
in fn t => if Vartab.is_empty vt then t else tmsubst t end;
|
paulson@21978
|
236 |
|
paulson@21978
|
237 |
(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
|
paulson@21978
|
238 |
vt0 holds the initial sort constraints, from the conjecture clauses.*)
|
paulson@23519
|
239 |
fun clause_of_strees ctxt vt0 ts =
|
wenzelm@22728
|
240 |
let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
|
wenzelm@24680
|
241 |
singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
|
wenzelm@22728
|
242 |
end;
|
paulson@21978
|
243 |
|
paulson@23519
|
244 |
(*Quantification over a list of Vars. FIXME: for term.ML??*)
|
paulson@21978
|
245 |
fun list_all_var ([], t: term) = t
|
paulson@21978
|
246 |
| list_all_var ((v as Var(ix,T)) :: vars, t) =
|
paulson@21979
|
247 |
(all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t)));
|
paulson@21978
|
248 |
|
paulson@21978
|
249 |
fun gen_all_vars t = list_all_var (term_vars t, t);
|
paulson@21978
|
250 |
|
paulson@21978
|
251 |
fun ints_of_stree_aux (Int n, ns) = n::ns
|
paulson@21978
|
252 |
| ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
|
paulson@21978
|
253 |
|
paulson@21978
|
254 |
fun ints_of_stree t = ints_of_stree_aux (t, []);
|
paulson@21978
|
255 |
|
paulson@22012
|
256 |
fun decode_tstp ctxt vt0 (name, role, ts, annots) =
|
paulson@21978
|
257 |
let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source
|
paulson@22012
|
258 |
in (name, role, clause_of_strees ctxt vt0 ts, deps) end;
|
paulson@21978
|
259 |
|
paulson@21978
|
260 |
fun dest_tstp ((((name, role), ts), annots), chs) =
|
paulson@21978
|
261 |
case chs of
|
paulson@21978
|
262 |
"."::_ => (name, role, ts, annots)
|
paulson@21978
|
263 |
| _ => error ("TSTP line not terminated by \".\": " ^ implode chs);
|
paulson@21978
|
264 |
|
paulson@21978
|
265 |
|
paulson@21978
|
266 |
(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **)
|
paulson@21978
|
267 |
|
paulson@21978
|
268 |
fun add_tfree_constraint ((true, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt
|
paulson@21978
|
269 |
| add_tfree_constraint (_, vt) = vt;
|
paulson@21978
|
270 |
|
paulson@21978
|
271 |
fun tfree_constraints_of_clauses vt [] = vt
|
wenzelm@23139
|
272 |
| tfree_constraints_of_clauses vt ([lit]::tss) =
|
paulson@21978
|
273 |
(tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss
|
paulson@21978
|
274 |
handle STREE _ => (*not a positive type constraint: ignore*)
|
paulson@21978
|
275 |
tfree_constraints_of_clauses vt tss)
|
paulson@21978
|
276 |
| tfree_constraints_of_clauses vt (_::tss) = tfree_constraints_of_clauses vt tss;
|
paulson@21978
|
277 |
|
paulson@21978
|
278 |
|
paulson@21978
|
279 |
(**** Translation of TSTP files to Isar Proofs ****)
|
paulson@21978
|
280 |
|
paulson@22012
|
281 |
fun decode_tstp_list ctxt tuples =
|
paulson@21978
|
282 |
let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
|
paulson@22012
|
283 |
in map (decode_tstp ctxt vt0) tuples end;
|
paulson@21978
|
284 |
|
paulson@21999
|
285 |
(*FIXME: simmilar function in res_atp. Move to HOLogic?*)
|
paulson@21999
|
286 |
fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
|
paulson@21999
|
287 |
| dest_disj_aux t disjs = t::disjs;
|
paulson@21999
|
288 |
|
paulson@21999
|
289 |
fun dest_disj t = dest_disj_aux t [];
|
paulson@21999
|
290 |
|
paulson@23519
|
291 |
(** Finding a matching assumption. The literals may be permuted, and variable names
|
paulson@23519
|
292 |
may disagree. We have to try all combinations of literals (quadratic!) and
|
paulson@23519
|
293 |
match up the variable names consistently. **)
|
paulson@22012
|
294 |
|
paulson@23519
|
295 |
fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) =
|
paulson@23519
|
296 |
strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
|
paulson@23519
|
297 |
| strip_alls_aux _ t = t;
|
paulson@23519
|
298 |
|
paulson@23519
|
299 |
val strip_alls = strip_alls_aux 0;
|
paulson@23519
|
300 |
|
paulson@23519
|
301 |
exception MATCH_LITERAL;
|
paulson@23519
|
302 |
|
paulson@23519
|
303 |
(*Ignore types: they are not to be trusted...*)
|
paulson@23519
|
304 |
fun match_literal (t1$u1) (t2$u2) env =
|
paulson@23519
|
305 |
match_literal t1 t2 (match_literal u1 u2 env)
|
paulson@23519
|
306 |
| match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env =
|
paulson@23519
|
307 |
match_literal t1 t2 env
|
paulson@23519
|
308 |
| match_literal (Bound i1) (Bound i2) env =
|
paulson@23519
|
309 |
if i1=i2 then env else raise MATCH_LITERAL
|
paulson@23519
|
310 |
| match_literal (Const(a1,_)) (Const(a2,_)) env =
|
paulson@23519
|
311 |
if a1=a2 then env else raise MATCH_LITERAL
|
paulson@23519
|
312 |
| match_literal (Free(a1,_)) (Free(a2,_)) env =
|
paulson@23519
|
313 |
if a1=a2 then env else raise MATCH_LITERAL
|
paulson@23519
|
314 |
| match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env
|
paulson@23519
|
315 |
| match_literal _ _ env = raise MATCH_LITERAL;
|
paulson@23519
|
316 |
|
paulson@23519
|
317 |
(*Checking that all variable associations are unique. The list env contains no
|
paulson@23519
|
318 |
repetitions, but does it contain say (x,y) and (y,y)? *)
|
paulson@23519
|
319 |
fun good env =
|
paulson@23519
|
320 |
let val (xs,ys) = ListPair.unzip env
|
paulson@23519
|
321 |
in not (has_duplicates (op=) xs orelse has_duplicates (op=) ys) end;
|
paulson@23519
|
322 |
|
paulson@23519
|
323 |
(*Match one list of literals against another, ignoring types and the order of
|
paulson@23519
|
324 |
literals. Sorting is unreliable because we don't have types or variable names.*)
|
paulson@23519
|
325 |
fun matches_aux _ [] [] = true
|
paulson@23519
|
326 |
| matches_aux env (lit::lits) ts =
|
paulson@23519
|
327 |
let fun match1 us [] = false
|
paulson@23519
|
328 |
| match1 us (t::ts) =
|
paulson@23519
|
329 |
let val env' = match_literal lit t env
|
paulson@23519
|
330 |
in (good env' andalso matches_aux env' lits (us@ts)) orelse
|
paulson@23519
|
331 |
match1 (t::us) ts
|
paulson@23519
|
332 |
end
|
paulson@23519
|
333 |
handle MATCH_LITERAL => match1 (t::us) ts
|
paulson@23519
|
334 |
in match1 [] ts end;
|
paulson@23519
|
335 |
|
paulson@23519
|
336 |
(*Is this length test useful?*)
|
paulson@23519
|
337 |
fun matches (lits1,lits2) =
|
paulson@23519
|
338 |
length lits1 = length lits2 andalso
|
paulson@23519
|
339 |
matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2);
|
paulson@21999
|
340 |
|
paulson@21999
|
341 |
fun permuted_clause t =
|
paulson@23519
|
342 |
let val lits = dest_disj t
|
paulson@21999
|
343 |
fun perm [] = NONE
|
wenzelm@23139
|
344 |
| perm (ctm::ctms) =
|
paulson@23519
|
345 |
if matches (lits, dest_disj (HOLogic.dest_Trueprop (strip_alls ctm)))
|
paulson@23519
|
346 |
then SOME ctm else perm ctms
|
paulson@21999
|
347 |
in perm end;
|
paulson@21999
|
348 |
|
paulson@22470
|
349 |
fun have_or_show "show " lname = "show \""
|
paulson@22470
|
350 |
| have_or_show have lname = have ^ lname ^ ": \""
|
paulson@22470
|
351 |
|
paulson@21999
|
352 |
(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
|
paulson@21999
|
353 |
ATP may have their literals reordered.*)
|
paulson@21999
|
354 |
fun isar_lines ctxt ctms =
|
wenzelm@24920
|
355 |
let val string_of = Syntax.string_of_term ctxt
|
paulson@22470
|
356 |
fun doline have (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
|
paulson@21999
|
357 |
(case permuted_clause t ctms of
|
paulson@21999
|
358 |
SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
|
paulson@21999
|
359 |
| NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*)
|
paulson@22470
|
360 |
| doline have (lname, t, deps) =
|
paulson@23519
|
361 |
have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^
|
paulson@22372
|
362 |
"\"\n by (metis " ^ space_implode " " deps ^ ")\n"
|
paulson@21978
|
363 |
fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
|
paulson@21978
|
364 |
| dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
|
paulson@22491
|
365 |
in setmp show_sorts (!recon_sorts) dolines end;
|
paulson@21978
|
366 |
|
paulson@21978
|
367 |
fun notequal t (_,t',_) = not (t aconv t');
|
paulson@21978
|
368 |
|
paulson@22491
|
369 |
(*No "real" literals means only type information*)
|
paulson@23519
|
370 |
fun eq_types t = t aconv HOLogic.true_const;
|
paulson@21978
|
371 |
|
paulson@22731
|
372 |
fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
|
paulson@21978
|
373 |
|
wenzelm@23139
|
374 |
fun replace_deps (old:int, new) (lno, t, deps) =
|
paulson@22731
|
375 |
(lno, t, foldl (op union_int) [] (map (replace_dep (old, new)) deps));
|
paulson@21978
|
376 |
|
paulson@22491
|
377 |
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
|
paulson@22491
|
378 |
only in type information.*)
|
paulson@21978
|
379 |
fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*)
|
paulson@22491
|
380 |
if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
|
wenzelm@23139
|
381 |
then map (replace_deps (lno, [])) lines
|
paulson@22470
|
382 |
else
|
paulson@22470
|
383 |
(case take_prefix (notequal t) lines of
|
paulson@22470
|
384 |
(_,[]) => lines (*no repetition of proof line*)
|
paulson@22470
|
385 |
| (pre, (lno',t',deps')::post) => (*repetition: replace later line by earlier one*)
|
paulson@22470
|
386 |
pre @ map (replace_deps (lno', [lno])) post)
|
paulson@21978
|
387 |
| add_prfline ((lno, role, t, []), lines) = (*no deps: conjecture clause*)
|
paulson@22470
|
388 |
(lno, t, []) :: lines
|
paulson@21978
|
389 |
| add_prfline ((lno, role, t, deps), lines) =
|
paulson@22491
|
390 |
if eq_types t then (lno, t, deps) :: lines
|
paulson@22491
|
391 |
(*Type information will be deleted later; skip repetition test.*)
|
paulson@22491
|
392 |
else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
|
paulson@22044
|
393 |
case take_prefix (notequal t) lines of
|
paulson@22044
|
394 |
(_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*)
|
wenzelm@23139
|
395 |
| (pre, (lno',t',deps')::post) =>
|
paulson@22044
|
396 |
(lno, t', deps) :: (*repetition: replace later line by earlier one*)
|
paulson@22044
|
397 |
(pre @ map (replace_deps (lno', [lno])) post);
|
paulson@22044
|
398 |
|
paulson@22470
|
399 |
(*Recursively delete empty lines (type information) from the proof.*)
|
paulson@22470
|
400 |
fun add_nonnull_prfline ((lno, t, []), lines) = (*no dependencies, so a conjecture clause*)
|
paulson@22491
|
401 |
if eq_types t (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*)
|
wenzelm@23139
|
402 |
then delete_dep lno lines
|
wenzelm@23139
|
403 |
else (lno, t, []) :: lines
|
paulson@22470
|
404 |
| add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
|
paulson@22470
|
405 |
and delete_dep lno lines = foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
|
paulson@22470
|
406 |
|
paulson@22731
|
407 |
fun bad_free (Free (a,_)) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
|
paulson@22731
|
408 |
| bad_free _ = false;
|
paulson@22731
|
409 |
|
wenzelm@23139
|
410 |
(*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
|
paulson@22491
|
411 |
To further compress proofs, setting modulus:=n deletes every nth line, and nlines
|
paulson@22491
|
412 |
counts the number of proof lines processed so far.
|
paulson@22491
|
413 |
Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline"
|
paulson@22044
|
414 |
phase may delete some dependencies, hence this phase comes later.*)
|
paulson@22491
|
415 |
fun add_wanted_prfline ((lno, t, []), (nlines, lines)) =
|
paulson@22491
|
416 |
(nlines, (lno, t, []) :: lines) (*conjecture clauses must be kept*)
|
paulson@22491
|
417 |
| add_wanted_prfline (line, (nlines, [])) = (nlines, [line]) (*final line must be kept*)
|
paulson@22491
|
418 |
| add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
|
paulson@22545
|
419 |
if eq_types t orelse not (null (term_tvars t)) orelse
|
wenzelm@23139
|
420 |
length deps < 2 orelse nlines mod !modulus <> 0 orelse
|
paulson@22731
|
421 |
exists bad_free (term_frees t)
|
paulson@22491
|
422 |
then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
|
paulson@22491
|
423 |
else (nlines+1, (lno, t, deps) :: lines);
|
paulson@21978
|
424 |
|
paulson@21999
|
425 |
(*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*)
|
paulson@21978
|
426 |
fun stringify_deps thm_names deps_map [] = []
|
paulson@21978
|
427 |
| stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
|
paulson@21978
|
428 |
if lno <= Vector.length thm_names (*axiom*)
|
wenzelm@23139
|
429 |
then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines
|
paulson@21979
|
430 |
else let val lname = Int.toString (length deps_map)
|
wenzelm@23139
|
431 |
fun fix lno = if lno <= Vector.length thm_names
|
paulson@21978
|
432 |
then SOME(Vector.sub(thm_names,lno-1))
|
paulson@21978
|
433 |
else AList.lookup op= deps_map lno;
|
paulson@22731
|
434 |
in (lname, t, List.mapPartial fix (distinct (op=) deps)) ::
|
paulson@21978
|
435 |
stringify_deps thm_names ((lno,lname)::deps_map) lines
|
paulson@21978
|
436 |
end;
|
paulson@21978
|
437 |
|
paulson@24547
|
438 |
val proofstart = "proof (neg_clausify)\n";
|
paulson@21979
|
439 |
|
paulson@21979
|
440 |
fun isar_header [] = proofstart
|
paulson@21999
|
441 |
| isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
|
paulson@21979
|
442 |
|
paulson@22012
|
443 |
fun decode_tstp_file cnfs ctxt th sgno thm_names =
|
paulson@21978
|
444 |
let val tuples = map (dest_tstp o tstp_line o explode) cnfs
|
paulson@24552
|
445 |
val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
|
wenzelm@23139
|
446 |
val nonnull_lines =
|
wenzelm@23139
|
447 |
foldr add_nonnull_prfline []
|
paulson@22491
|
448 |
(foldr add_prfline [] (decode_tstp_list ctxt tuples))
|
paulson@22491
|
449 |
val (_,lines) = foldr add_wanted_prfline (0,[]) nonnull_lines
|
paulson@21999
|
450 |
val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
|
paulson@21999
|
451 |
val ccls = map forall_intr_vars ccls
|
wenzelm@23139
|
452 |
in
|
wenzelm@22130
|
453 |
app (fn th => Output.debug (fn () => string_of_thm th)) ccls;
|
wenzelm@23139
|
454 |
isar_header (map #1 fixes) ^
|
wenzelm@22130
|
455 |
String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
|
paulson@24547
|
456 |
end
|
paulson@24547
|
457 |
handle e => (*FIXME: exn handler is too general!*)
|
paulson@24547
|
458 |
"Translation of TSTP raised an exception: " ^ Toplevel.exn_message e;
|
paulson@21978
|
459 |
|
paulson@21978
|
460 |
(*Could use split_lines, but it can return blank lines...*)
|
paulson@21978
|
461 |
val lines = String.tokens (equal #"\n");
|
paulson@21978
|
462 |
|
paulson@21978
|
463 |
val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
|
paulson@21978
|
464 |
|
paulson@23519
|
465 |
val txt_path = Path.ext "txt" o Path.explode o nospaces;
|
paulson@21978
|
466 |
|
wenzelm@23139
|
467 |
fun signal_success probfile toParent ppid msg =
|
paulson@23519
|
468 |
let val _ = trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg)
|
paulson@23519
|
469 |
in
|
paulson@23519
|
470 |
(*We write the proof to a file because sending very long lines may fail...*)
|
paulson@23519
|
471 |
File.write (txt_path probfile) msg;
|
paulson@23519
|
472 |
TextIO.output (toParent, "Success.\n");
|
paulson@23519
|
473 |
TextIO.output (toParent, probfile ^ "\n");
|
paulson@23519
|
474 |
TextIO.flushOut toParent;
|
paulson@23833
|
475 |
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
|
paulson@23833
|
476 |
(*Give the parent time to respond before possibly sending another signal*)
|
paulson@23833
|
477 |
OS.Process.sleep (Time.fromMilliseconds 600)
|
paulson@23519
|
478 |
end;
|
paulson@21978
|
479 |
|
paulson@21978
|
480 |
|
paulson@21978
|
481 |
(**** retrieve the axioms that were used in the proof ****)
|
paulson@21978
|
482 |
|
paulson@24547
|
483 |
(*PureThy.get_name_hint returns "??.unknown" if no name is available.*)
|
paulson@24547
|
484 |
fun goodhint x = (x <> "??.unknown");
|
paulson@24547
|
485 |
|
paulson@21978
|
486 |
(*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
|
wenzelm@23139
|
487 |
fun get_axiom_names (thm_names: string vector) step_nums =
|
wenzelm@23139
|
488 |
let fun is_axiom n = n <= Vector.length thm_names
|
paulson@24547
|
489 |
fun getname i = Vector.sub(thm_names, i-1)
|
paulson@21978
|
490 |
in
|
paulson@24547
|
491 |
sort_distinct string_ord (filter goodhint (map getname (filter is_axiom step_nums)))
|
paulson@24547
|
492 |
end;
|
paulson@21978
|
493 |
|
wenzelm@23139
|
494 |
(*String contains multiple lines. We want those of the form
|
paulson@21978
|
495 |
"253[0:Inp] et cetera..."
|
paulson@21978
|
496 |
A list consisting of the first number in each line is returned. *)
|
paulson@24425
|
497 |
fun get_spass_linenums proofextract =
|
paulson@21978
|
498 |
let val toks = String.tokens (not o Char.isAlphaNum)
|
paulson@21978
|
499 |
fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
|
paulson@21978
|
500 |
| inputno _ = NONE
|
paulson@24425
|
501 |
val lines = String.tokens (fn c => c = #"\n") proofextract
|
paulson@21978
|
502 |
in List.mapPartial (inputno o toks) lines end
|
paulson@21978
|
503 |
|
paulson@24425
|
504 |
fun get_axiom_names_spass proofextract thm_names =
|
paulson@24425
|
505 |
get_axiom_names thm_names (get_spass_linenums proofextract);
|
wenzelm@23139
|
506 |
|
paulson@21978
|
507 |
fun not_comma c = c <> #",";
|
paulson@21978
|
508 |
|
paulson@21978
|
509 |
(*A valid TSTP axiom line has the form cnf(NNN,axiom,...) where NNN is a positive integer.*)
|
paulson@21978
|
510 |
fun parse_tstp_line s =
|
paulson@21978
|
511 |
let val ss = Substring.full (unprefix "cnf(" (nospaces s))
|
paulson@21978
|
512 |
val (intf,rest) = Substring.splitl not_comma ss
|
paulson@21978
|
513 |
val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
|
paulson@21978
|
514 |
(*We only allow negated_conjecture because the line number will be removed in
|
paulson@21978
|
515 |
get_axiom_names above, while suppressing the UNSOUND warning*)
|
paulson@21978
|
516 |
val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
|
wenzelm@23139
|
517 |
then Substring.string intf
|
wenzelm@23139
|
518 |
else "error"
|
paulson@21978
|
519 |
in Int.fromString ints end
|
wenzelm@23139
|
520 |
handle Fail _ => NONE;
|
paulson@21978
|
521 |
|
paulson@24425
|
522 |
fun get_axiom_names_tstp proofextract thm_names =
|
paulson@24425
|
523 |
get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofextract));
|
wenzelm@23139
|
524 |
|
wenzelm@23139
|
525 |
(*String contains multiple lines. We want those of the form
|
paulson@24632
|
526 |
"*********** [448, input] ***********"
|
paulson@24632
|
527 |
or possibly those of the form
|
paulson@24632
|
528 |
"cnf(108, axiom, ..."
|
paulson@21978
|
529 |
A list consisting of the first number in each line is returned. *)
|
paulson@24425
|
530 |
fun get_vamp_linenums proofextract =
|
paulson@21978
|
531 |
let val toks = String.tokens (not o Char.isAlphaNum)
|
paulson@21978
|
532 |
fun inputno [ntok,"input"] = Int.fromString ntok
|
paulson@24632
|
533 |
| inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
|
paulson@21978
|
534 |
| inputno _ = NONE
|
paulson@24425
|
535 |
val lines = String.tokens (fn c => c = #"\n") proofextract
|
paulson@21978
|
536 |
in List.mapPartial (inputno o toks) lines end
|
paulson@21978
|
537 |
|
paulson@24425
|
538 |
fun get_axiom_names_vamp proofextract thm_names =
|
paulson@24425
|
539 |
get_axiom_names thm_names (get_vamp_linenums proofextract);
|
paulson@24425
|
540 |
|
paulson@24547
|
541 |
fun get_axiom_names_for E = get_axiom_names_tstp
|
paulson@24547
|
542 |
| get_axiom_names_for SPASS = get_axiom_names_spass
|
paulson@24547
|
543 |
| get_axiom_names_for Vampire = get_axiom_names_vamp;
|
wenzelm@23139
|
544 |
|
paulson@24547
|
545 |
fun metis_line [] = "apply metis"
|
paulson@24547
|
546 |
| metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
|
paulson@21978
|
547 |
|
paulson@21978
|
548 |
(*The signal handler in watcher.ML must be able to read the output of this.*)
|
paulson@24425
|
549 |
fun lemma_list atp proofextract thm_names probfile toParent ppid =
|
paulson@24547
|
550 |
signal_success probfile toParent ppid
|
paulson@24547
|
551 |
(metis_line (get_axiom_names_for atp proofextract thm_names));
|
paulson@21978
|
552 |
|
paulson@24547
|
553 |
fun tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno =
|
paulson@24425
|
554 |
let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
|
paulson@24547
|
555 |
val line1 = metis_line (get_axiom_names_tstp proofextract thm_names)
|
paulson@24425
|
556 |
in
|
paulson@24425
|
557 |
signal_success probfile toParent ppid
|
paulson@24425
|
558 |
(line1 ^ "\n" ^ decode_tstp_file cnfs ctxt th sgno thm_names)
|
paulson@24425
|
559 |
end;
|
paulson@21978
|
560 |
|
paulson@21978
|
561 |
(**** Extracting proofs from an ATP's output ****)
|
paulson@21978
|
562 |
|
paulson@24547
|
563 |
val start_TSTP = "SZS output start CNFRefutation"
|
paulson@24547
|
564 |
val end_TSTP = "SZS output end CNFRefutation"
|
paulson@21978
|
565 |
val start_E = "# Proof object starts here."
|
paulson@21978
|
566 |
val end_E = "# Proof object ends here."
|
paulson@21978
|
567 |
val start_V8 = "=========== Refutation =========="
|
paulson@21978
|
568 |
val end_V8 = "======= End of refutation ======="
|
paulson@24547
|
569 |
val start_SPASS = "Here is a proof"
|
paulson@21978
|
570 |
val end_SPASS = "Formulae used in the proof"
|
paulson@21978
|
571 |
|
paulson@24547
|
572 |
fun any_substring ss ln = exists (fn s => String.isSubstring s ln) ss;
|
paulson@24547
|
573 |
|
paulson@21978
|
574 |
(*********************************************************************************)
|
paulson@21978
|
575 |
(* Inspect the output of an ATP process to see if it has found a proof, *)
|
paulson@21978
|
576 |
(* and if so, transfer output to the input pipe of the main Isabelle process *)
|
paulson@21978
|
577 |
(*********************************************************************************)
|
paulson@21978
|
578 |
|
paulson@21978
|
579 |
(*Returns "true" if it successfully returns a lemma list, otherwise "false", but this
|
paulson@21978
|
580 |
return value is currently never used!*)
|
paulson@22012
|
581 |
fun startTransfer endS (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names) =
|
paulson@24547
|
582 |
let val atp = if endS = end_V8 then Vampire
|
paulson@24547
|
583 |
else if endS = end_SPASS then SPASS
|
paulson@24547
|
584 |
else E
|
paulson@24547
|
585 |
fun transferInput proofextract =
|
paulson@24547
|
586 |
case TextIO.inputLine fromChild of
|
paulson@24547
|
587 |
NONE => (*end of file?*)
|
paulson@24547
|
588 |
(trace ("\n extraction_failed. End bracket: " ^ endS ^
|
paulson@24547
|
589 |
"\naccumulated text: " ^ proofextract);
|
paulson@24547
|
590 |
false)
|
paulson@24547
|
591 |
| SOME thisLine =>
|
paulson@24547
|
592 |
if any_substring [endS,end_TSTP] thisLine
|
paulson@24547
|
593 |
then
|
paulson@24547
|
594 |
(trace ("\nExtracted proof:\n" ^ proofextract);
|
paulson@24425
|
595 |
if String.isPrefix "cnf(" proofextract
|
paulson@24547
|
596 |
then tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno
|
paulson@24425
|
597 |
else lemma_list atp proofextract thm_names probfile toParent ppid;
|
paulson@24425
|
598 |
true)
|
paulson@24547
|
599 |
else transferInput (proofextract ^ thisLine)
|
paulson@21978
|
600 |
in
|
paulson@21978
|
601 |
transferInput ""
|
wenzelm@23139
|
602 |
end
|
paulson@21978
|
603 |
|
paulson@21978
|
604 |
|
paulson@21978
|
605 |
(*The signal handler in watcher.ML must be able to read the output of this.*)
|
paulson@21978
|
606 |
fun signal_parent (toParent, ppid, msg, probfile) =
|
paulson@21978
|
607 |
(TextIO.output (toParent, msg);
|
paulson@21978
|
608 |
TextIO.output (toParent, probfile ^ "\n");
|
paulson@21978
|
609 |
TextIO.flushOut toParent;
|
paulson@21978
|
610 |
trace ("\nSignalled parent: " ^ msg ^ probfile);
|
paulson@21978
|
611 |
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
|
paulson@21978
|
612 |
(*Give the parent time to respond before possibly sending another signal*)
|
paulson@21978
|
613 |
OS.Process.sleep (Time.fromMilliseconds 600));
|
paulson@21978
|
614 |
|
paulson@22012
|
615 |
(*FIXME: once TSTP output is produced by all ATPs, these three functions can be combined.*)
|
paulson@22012
|
616 |
|
paulson@21978
|
617 |
(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
|
paulson@22012
|
618 |
fun checkVampProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
|
wenzelm@23139
|
619 |
(case TextIO.inputLine fromChild of
|
wenzelm@23139
|
620 |
NONE => (trace "\nNo proof output seen"; false)
|
wenzelm@23139
|
621 |
| SOME thisLine =>
|
paulson@24547
|
622 |
if any_substring [start_V8,start_TSTP] thisLine
|
paulson@22012
|
623 |
then startTransfer end_V8 arg
|
paulson@24547
|
624 |
else if (String.isSubstring "Satisfiability detected" thisLine) orelse
|
paulson@24547
|
625 |
(String.isSubstring "Refutation not found" thisLine)
|
paulson@21978
|
626 |
then (signal_parent (toParent, ppid, "Failure\n", probfile);
|
paulson@21978
|
627 |
true)
|
wenzelm@23139
|
628 |
else checkVampProofFound arg);
|
paulson@21978
|
629 |
|
paulson@21978
|
630 |
(*Called from watcher. Returns true if the E process has returned a verdict.*)
|
wenzelm@23139
|
631 |
fun checkEProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
|
wenzelm@23139
|
632 |
(case TextIO.inputLine fromChild of
|
wenzelm@23139
|
633 |
NONE => (trace "\nNo proof output seen"; false)
|
wenzelm@23139
|
634 |
| SOME thisLine =>
|
paulson@24547
|
635 |
if any_substring [start_E,start_TSTP] thisLine
|
paulson@22012
|
636 |
then startTransfer end_E arg
|
paulson@24547
|
637 |
else if String.isSubstring "SZS status: Satisfiable" thisLine
|
paulson@21978
|
638 |
then (signal_parent (toParent, ppid, "Invalid\n", probfile);
|
paulson@21978
|
639 |
true)
|
paulson@24547
|
640 |
else if String.isSubstring "SZS status: ResourceOut" thisLine
|
paulson@21978
|
641 |
then (signal_parent (toParent, ppid, "Failure\n", probfile);
|
paulson@21978
|
642 |
true)
|
wenzelm@23139
|
643 |
else checkEProofFound arg);
|
paulson@21978
|
644 |
|
paulson@21978
|
645 |
(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
|
wenzelm@23139
|
646 |
fun checkSpassProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
|
wenzelm@23139
|
647 |
(case TextIO.inputLine fromChild of
|
wenzelm@23139
|
648 |
NONE => (trace "\nNo proof output seen"; false)
|
wenzelm@23139
|
649 |
| SOME thisLine =>
|
paulson@24547
|
650 |
if any_substring [start_SPASS,start_TSTP] thisLine
|
paulson@22012
|
651 |
then startTransfer end_SPASS arg
|
paulson@21978
|
652 |
else if thisLine = "SPASS beiseite: Completion found.\n"
|
paulson@21978
|
653 |
then (signal_parent (toParent, ppid, "Invalid\n", probfile);
|
paulson@21978
|
654 |
true)
|
paulson@21978
|
655 |
else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
|
paulson@21978
|
656 |
thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
|
paulson@21978
|
657 |
then (signal_parent (toParent, ppid, "Failure\n", probfile);
|
paulson@21978
|
658 |
true)
|
wenzelm@23139
|
659 |
else checkSpassProofFound arg);
|
paulson@21978
|
660 |
|
paulson@21978
|
661 |
end;
|