# HG changeset patch # User paulson # Date 1168000592 -3600 # Node ID adf68479ae1b86b5396452c6a91ebba79cd6dda5 # Parent 3d4ea1819cb76116e1e24340ee4d11dda1f6bed0 Proof.context now sent to watcher and used in type inference step of proof reconstruction diff -r 3d4ea1819cb7 -r adf68479ae1b src/HOL/Tools/ATP/watcher.ML --- 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 diff -r 3d4ea1819cb7 -r adf68479ae1b src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Jan 04 21:58:46 2007 +0100 +++ b/src/HOL/Tools/res_atp.ML Fri Jan 05 13:36:32 2007 +0100 @@ -895,7 +895,7 @@ let val _ = kill_last_watcher() val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th) - val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list) + val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list) in last_watcher_pid := SOME (childin, childout, pid, files); Output.debug ("problem files: " ^ space_implode ", " files); diff -r 3d4ea1819cb7 -r adf68479ae1b src/HOL/Tools/res_reconstruct.ML --- 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;