--- a/src/HOL/Tools/ATP/watcher.ML Thu Jan 04 21:58:46 2007 +0100
+++ b/src/HOL/Tools/ATP/watcher.ML Fri Jan 05 13:36:32 2007 +0100
@@ -23,7 +23,7 @@
(* Start a watcher and set up signal handlers*)
val createWatcher :
- thm * string Vector.vector list ->
+ Proof.context * thm * string Vector.vector list ->
TextIO.instream * TextIO.outstream * Posix.Process.pid
val killWatcher : Posix.Process.pid -> unit
val killChild : ('a, 'b) Unix.proc -> OS.Process.status
@@ -213,7 +213,7 @@
Date.toString(Date.fromTimeLocal(Time.now())))
in execCmds cmds newProcList end
-fun checkChildren (th, thm_names_list, toParentStr, children) =
+fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
let fun check [] = [] (* no children to check *)
| check (child::children) =
let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
@@ -227,11 +227,11 @@
let val _ = trace ("\nInput available from child: " ^ file)
val childDone = (case prover of
"vampire" => ResReconstruct.checkVampProofFound
- (childIn, toParentStr, ppid, file, th, sgno, thm_names)
+ (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
| "E" => ResReconstruct.checkEProofFound
- (childIn, toParentStr, ppid, file, th, sgno, thm_names)
+ (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
| "spass" => ResReconstruct.checkSpassProofFound
- (childIn, toParentStr, ppid, file, th, sgno, thm_names)
+ (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
| _ => (trace ("\nBad prover! " ^ prover); true) )
in
if childDone (*ATP has reported back (with success OR failure)*)
@@ -248,8 +248,9 @@
end;
-fun setupWatcher (th,thm_names_list) =
+fun setupWatcher (ctxt, th, thm_names_list) =
let
+ val checkc = checkChildren (ctxt, th, thm_names_list)
val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*)
val p2 = Posix.IO.pipe()
(****** fork a watcher process and get it set up and going ******)
@@ -285,16 +286,14 @@
if length procList < 40 then (* Execute locally *)
let val _ = trace("\nCommands from parent: " ^
Int.toString(length cmds))
- val newProcList' = checkChildren(th, thm_names_list, toParentStr,
- execCmds cmds procList)
+ val newProcList' = checkc toParentStr (execCmds cmds procList)
in trace "\nCommands executed"; keepWatching newProcList' end
else (* Execute remotely [FIXME: NOT REALLY] *)
- let val newProcList' = checkChildren (th, thm_names_list, toParentStr,
- execCmds cmds procList)
+ let val newProcList' = checkc toParentStr (execCmds cmds procList)
in keepWatching newProcList' end
| NONE => (* No new input from Isabelle *)
(trace "\nNothing from parent...";
- keepWatching(checkChildren(th, thm_names_list, toParentStr, procList))))
+ keepWatching(checkc toParentStr procList)))
handle exn => (*FIXME: exn handler is too general!*)
(trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
keepWatching procList);
@@ -353,8 +352,8 @@
fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
-fun createWatcher (th, thm_names_list) =
- let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,thm_names_list)
+fun createWatcher (ctxt, th, thm_names_list) =
+ let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
fun decr_watched() =
(goals_being_watched := !goals_being_watched - 1;
if !goals_being_watched = 0
--- a/src/HOL/Tools/res_reconstruct.ML Thu Jan 04 21:58:46 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Fri Jan 05 13:36:32 2007 +0100
@@ -10,16 +10,15 @@
sig
val checkEProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * thm * int * string Vector.vector -> bool
+ string * Proof.context * thm * int * string Vector.vector -> bool
val checkVampProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * thm * int * string Vector.vector -> bool
+ string * Proof.context * thm * int * string Vector.vector -> bool
val checkSpassProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * thm * int * string Vector.vector -> bool
+ string * Proof.context * thm * int * string Vector.vector -> bool
val signal_parent:
TextIO.outstream * Posix.Process.pid * string * string -> unit
- val nospaces: string -> string
end;
@@ -245,11 +244,11 @@
val nofalses = filter (not o equal HOLogic.false_const);
(*Accumulate sort constraints in vt, with "real" literals in lits.*)
-fun lits_of_strees thy (vt, lits) [] = (vt, rev (nofalses lits))
- | lits_of_strees thy (vt, lits) (t::ts) =
- lits_of_strees thy (add_constraint (constraint_of_stree true t, vt), lits) ts
+fun lits_of_strees ctxt (vt, lits) [] = (vt, rev (nofalses lits))
+ | lits_of_strees ctxt (vt, lits) (t::ts) =
+ lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts
handle STREE _ =>
- lits_of_strees thy (vt, term_of_stree thy t :: lits) ts;
+ lits_of_strees ctxt (vt, term_of_stree (ProofContext.theory_of ctxt) t :: lits) ts;
(*Update TVars/TFrees with detected sort constraints.*)
fun fix_sorts vt =
@@ -266,14 +265,16 @@
(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
vt0 holds the initial sort constraints, from the conjecture clauses.*)
-fun clause_of_strees_aux thy vt0 ts =
- case lits_of_strees thy (vt0,[]) ts of
+fun clause_of_strees_aux ctxt vt0 ts =
+ case lits_of_strees ctxt (vt0,[]) ts of
(_, []) => HOLogic.false_const
| (vt, lits) =>
let val dt = fix_sorts vt (foldr1 HOLogic.mk_disj lits)
- val infer = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
+ val infer = Sign.infer_types (ProofContext.pp ctxt) (ProofContext.theory_of ctxt)
+ (ProofContext.consts_of ctxt) (Variable.def_type ctxt false)
+ (Variable.def_sort ctxt) (Variable.names_of ctxt) true
in
- #1(infer (K NONE) (K NONE) (Name.make_context []) true ([dt], HOLogic.boolT))
+ #1(infer ([dt], HOLogic.boolT))
end;
(*Quantification over a list of Vars. FUXNE: for term.ML??*)
@@ -291,9 +292,9 @@
fun ints_of_stree t = ints_of_stree_aux (t, []);
-fun decode_tstp thy vt0 (name, role, ts, annots) =
+fun decode_tstp ctxt vt0 (name, role, ts, annots) =
let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source
- in (name, role, clause_of_strees thy vt0 ts, deps) end;
+ in (name, role, clause_of_strees ctxt vt0 ts, deps) end;
fun dest_tstp ((((name, role), ts), annots), chs) =
case chs of
@@ -316,9 +317,9 @@
(**** Translation of TSTP files to Isar Proofs ****)
-fun decode_tstp_list thy tuples =
+fun decode_tstp_list ctxt tuples =
let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
- in map (decode_tstp thy vt0) tuples end;
+ in map (decode_tstp ctxt vt0) tuples end;
(*FIXME: simmilar function in res_atp. Move to HOLogic?*)
fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
@@ -326,7 +327,15 @@
fun dest_disj t = dest_disj_aux t [];
-val sort_lits = sort Term.fast_term_ord o dest_disj o HOLogic.dest_Trueprop o strip_all_body;
+(*Remove types from a term, to eliminate the randomness of type inference*)
+fun smash_types (Const(a,_)) = Const(a,dummyT)
+ | smash_types (Free(a,_)) = Free(a,dummyT)
+ | smash_types (Var(a,_)) = Var(a,dummyT)
+ | smash_types (f$t) = smash_types f $ smash_types t
+ | smash_types t = t;
+
+val sort_lits = sort Term.fast_term_ord o dest_disj o
+ smash_types o HOLogic.dest_Trueprop o strip_all_body;
fun permuted_clause t =
let val lits = sort_lits t
@@ -400,19 +409,17 @@
fun isar_header [] = proofstart
| isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
-fun decode_tstp_file cnfs th sgno thm_names =
+fun decode_tstp_file cnfs ctxt th sgno thm_names =
let val tuples = map (dest_tstp o tstp_line o explode) cnfs
- and ctxt = ProofContext.init (Thm.theory_of_thm th)
- (*The full context could be sent from ResAtp.isar_atp_body to Watcher.createWatcher,
- then to setupWatcher and checkChildren...but is it really needed?*)
- val decoded_tuples = decode_tstp_list (ProofContext.theory_of ctxt) tuples
+ val lines = foldr add_prfline [] (decode_tstp_list ctxt tuples)
val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
val ccls = map forall_intr_vars ccls
- val lines = foldr add_prfline [] decoded_tuples
- and clines = map (fn th => string_of_thm th ^ "\n") ccls
in
+ if !Output.show_debug_msgs
+ then app (Output.debug o string_of_thm) ccls
+ else ();
isar_header (map #1 fixes) ^
- String.concat (clines @ isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
+ String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
end;
(*Could use split_lines, but it can return blank lines...*)
@@ -431,11 +438,11 @@
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
-fun tstp_extract proofextract probfile toParent ppid th sgno thm_names =
+fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
in
signal_success probfile toParent ppid
- (decode_tstp_file cnfs th sgno thm_names)
+ (decode_tstp_file cnfs ctxt th sgno thm_names)
end;
@@ -545,7 +552,7 @@
(*Returns "true" if it successfully returns a lemma list, otherwise "false", but this
return value is currently never used!*)
-fun startTransfer (endS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
+fun startTransfer endS (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names) =
let fun transferInput currentString =
let val thisLine = TextIO.inputLine fromChild
in
@@ -561,7 +568,7 @@
in
trace ("\nExtracted proof:\n" ^ proofextract);
if !full andalso String.isPrefix "cnf(" proofextract
- then tstp_extract proofextract probfile toParent ppid th sgno thm_names
+ then tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names
else lemma_list proofextract probfile toParent ppid thm_names;
true
end
@@ -582,48 +589,49 @@
(*Give the parent time to respond before possibly sending another signal*)
OS.Process.sleep (Time.fromMilliseconds 600));
+(*FIXME: once TSTP output is produced by all ATPs, these three functions can be combined.*)
+
(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
-fun checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
+fun checkVampProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
if thisLine = ""
then (trace "\nNo proof output seen"; false)
else if String.isPrefix start_V8 thisLine
- then startTransfer (end_V8, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
+ then startTransfer end_V8 arg
else if (String.isPrefix "Satisfiability detected" thisLine) orelse
(String.isPrefix "Refutation not found" thisLine)
then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
- else checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
+ else checkVampProofFound arg
end
(*Called from watcher. Returns true if the E process has returned a verdict.*)
-fun checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
+fun checkEProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
if thisLine = "" then (trace "\nNo proof output seen"; false)
else if String.isPrefix start_E thisLine
- then startTransfer (end_E, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
+ then startTransfer end_E arg
else if String.isPrefix "# Problem is satisfiable" thisLine
then (signal_parent (toParent, ppid, "Invalid\n", probfile);
true)
else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
- else checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
+ else checkEProofFound arg
end;
(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
-fun checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
+fun checkSpassProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
if thisLine = "" then (trace "\nNo proof output seen"; false)
else if String.isPrefix "Here is a proof" thisLine
- then
- startTransfer (end_SPASS, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
+ then startTransfer end_SPASS arg
else if thisLine = "SPASS beiseite: Completion found.\n"
then (signal_parent (toParent, ppid, "Invalid\n", probfile);
true)
@@ -631,7 +639,7 @@
thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
- else checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
+ else checkSpassProofFound arg
end
end;