# HG changeset patch # User wenzelm # Date 1119296071 -7200 # Node ID abf475cf11f2625b3b38c5dad0e87d92d859d7e8 # Parent cf872f3e16d917ba15db8bad8a13cff29e3f235c improved formatting; diff -r cf872f3e16d9 -r abf475cf11f2 src/HOL/Tools/ATP/VampCommunication.ML --- a/src/HOL/Tools/ATP/VampCommunication.ML Mon Jun 20 21:33:27 2005 +0200 +++ b/src/HOL/Tools/ATP/VampCommunication.ML Mon Jun 20 21:34:31 2005 +0200 @@ -11,9 +11,9 @@ sig val reconstruct : bool ref val getVampInput : TextIO.instream -> string * string * string - val checkVampProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string * + val checkVampProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string * string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array * int -> bool - + end; structure VampComm :VAMP_COMM = @@ -26,12 +26,13 @@ (* Write Vamp output to a file *) (***********************************) -fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr - in if (thisLine = "%============== End of proof. ==================\n" ) - then TextIO.output (fd, thisLine) - else ( - TextIO.output (fd, thisLine); logVampInput (instr,fd)) - end; +fun logVampInput (instr, fd) = + let val thisLine = TextIO.inputLine instr + in if (thisLine = "%============== End of proof. ==================\n" ) + then TextIO.output (fd, thisLine) + else ( + TextIO.output (fd, thisLine); logVampInput (instr,fd)) + end; (**********************************************************************) (* Reconstruct the Vamp proof w.r.t. thmstring (string version of *) @@ -43,49 +44,51 @@ val atomize_tac = SUBGOAL (fn (prop,_) => - let val ts = Logic.strip_assums_hyp prop - in EVERY1 - [METAHYPS - (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), - REPEAT_DETERM_N (length ts) o (etac thin_rl)] + let val ts = Logic.strip_assums_hyp prop + in EVERY1 + [METAHYPS + (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), + REPEAT_DETERM_N (length ts) o (etac thin_rl)] end); -fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr (num_of_clauses:int ) = - let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3"))); - in -SELECT_GOAL - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, - METAHYPS(fn negs => ((*if !reconstruct - then - Recon_Transfer.vampString_to_reconString proofextract thmstring goalstring - toParent ppid negs clause_arr num_of_clauses - else*) - Recon_Transfer.vampString_to_lemmaString proofextract thmstring goalstring - toParent ppid negs clause_arr num_of_clauses ))]) sg_num - end ; +fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr (num_of_clauses:int ) = + let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3"))); + in + SELECT_GOAL + (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, + METAHYPS(fn negs => + ((*if !reconstruct + then + Recon_Transfer.vampString_to_reconString proofextract thmstring goalstring + toParent ppid negs clause_arr num_of_clauses + else*) + Recon_Transfer.vampString_to_lemmaString proofextract thmstring goalstring + toParent ppid negs clause_arr num_of_clauses ))]) sg_num + end ; -fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = let - val thisLine = TextIO.inputLine fromChild - in - if (thisLine = "%============== End of proof. ==================\n" ) - then ( - let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) - val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2"))); - - in +fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = + let + val thisLine = TextIO.inputLine fromChild + in + if (thisLine = "%============== End of proof. ==================\n" ) + then ( + let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) + val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2"))); + + in - TextIO.output(foo,(proofextract));TextIO.closeOut foo; - reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr num_of_clauses thm - - end - ) - else ( - - transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr, num_of_clauses) - ) - end; + TextIO.output(foo,(proofextract));TextIO.closeOut foo; + reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr num_of_clauses thm + + end + ) + else ( + + transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr, num_of_clauses) + ) + end; @@ -95,187 +98,184 @@ (* and if so, transfer output to the input pipe of the main Isabelle process *) (*********************************************************************************) - -fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = - (*let val _ = Posix.Process.wait () - in*) - - if (isSome (TextIO.canInput(fromChild, 5))) - then - ( - let val thisLine = TextIO.inputLine fromChild - in - if (thisLine = "%================== Proof: ======================\n") - then - ( - let - val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer"))); - val _= TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm)); - val _ = TextIO.closeOut outfile; - in - transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr, num_of_clauses); - true - end) - - else - ( - startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses) - ) - end - ) - else (false) - (* end*) + +fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = + (*let val _ = Posix.Process.wait () + in*) + + if (isSome (TextIO.canInput(fromChild, 5))) + then + ( + let val thisLine = TextIO.inputLine fromChild + in + if (thisLine = "%================== Proof: ======================\n") + then + ( + let + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer"))); + val _= TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm)); + val _ = TextIO.closeOut outfile; + in + transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr, num_of_clauses); + true + end) + + else + ( + startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses) + ) + end + ) + else (false) +(* end*) -fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) = - let val vamp_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof"))) - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkvamp"))); - val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm)) - - val _ = TextIO.closeOut outfile - in - if (isSome (TextIO.canInput(fromChild, 5))) - then - ( - let val thisLine = TextIO.inputLine fromChild - in if (thisLine = "% Proof found. Thanks to Tanya!\n" ) - then - ( - let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) - val _ = TextIO.output (outfile, (thisLine)) - - val _ = TextIO.closeOut outfile - in - startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) - end - ) - else if (thisLine = "% Unprovable.\n" ) - then +fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) = + let val vamp_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof"))) + val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkvamp"))); + val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm)) + + val _ = TextIO.closeOut outfile + in + if (isSome (TextIO.canInput(fromChild, 5))) + then + ( + let val thisLine = TextIO.inputLine fromChild + in if (thisLine = "% Proof found. Thanks to Tanya!\n" ) + then + ( + let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + val _ = TextIO.output (outfile, (thisLine)) + + val _ = TextIO.closeOut outfile + in + startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) + end + ) + else if (thisLine = "% Unprovable.\n" ) + then + + ( + let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + val _ = TextIO.output (outfile, (thisLine)) + + val _ = TextIO.closeOut outfile + in - ( - let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) - val _ = TextIO.output (outfile, (thisLine)) - - val _ = TextIO.closeOut outfile - in - - TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (vamp_proof_file, (thisLine)); - TextIO.flushOut vamp_proof_file; - TextIO.closeOut vamp_proof_file; - (*TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; - TextIO.output (toParent, "bar\n"); - TextIO.flushOut toParent;*) + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (vamp_proof_file, (thisLine)); + TextIO.flushOut vamp_proof_file; + TextIO.closeOut vamp_proof_file; + (*TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + TextIO.output (toParent, "bar\n"); + TextIO.flushOut toParent;*) - TextIO.output (toParent, thisLine^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, thmstring^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); - true - end) - else if (thisLine = "% Proof not found.\n") - then - ( - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; + TextIO.output (toParent, thisLine^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, thmstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, goalstring^"\n"); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + (* Attempt to prevent several signals from turning up simultaneously *) + Posix.Process.sleep(Time.fromSeconds 1); + true + end) + else if (thisLine = "% Proof not found.\n") + then + ( + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; - true) - - else - (TextIO.output (vamp_proof_file, (thisLine)); - TextIO.flushOut vamp_proof_file; - checkVampProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)) + true) + + else + (TextIO.output (vamp_proof_file, (thisLine)); + TextIO.flushOut vamp_proof_file; + checkVampProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)) - end - ) - else - (TextIO.output (vamp_proof_file, ("No proof output seen \n"));TextIO.closeOut vamp_proof_file;false) - end + end + ) + else + (TextIO.output (vamp_proof_file, ("No proof output seen \n"));TextIO.closeOut vamp_proof_file;false) + end - + (***********************************************************************) (* Function used by the Isabelle process to read in a vamp proof *) (***********************************************************************) - +fun getVampInput instr = + if (isSome (TextIO.canInput(instr, 2))) + then + let val thisLine = TextIO.inputLine instr + val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine)) -fun getVampInput instr = if (isSome (TextIO.canInput(instr, 2))) - then - let val thisLine = TextIO.inputLine instr - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine)) - - val _ = TextIO.closeOut outfile - in (* reconstructed proof string *) - if ( (substring (thisLine, 0,1))= "[") - then - (*Pretty.writeln(Pretty.str (thisLine))*) - let val reconstr = thisLine - val thmstring = TextIO.inputLine instr - val goalstring = TextIO.inputLine instr - in - (reconstr, thmstring, goalstring) - end - else if (thisLine = "% Unprovable.\n" ) - then - ( - let val reconstr = thisLine - val thmstring = TextIO.inputLine instr - val goalstring = TextIO.inputLine instr - in - (reconstr, thmstring, goalstring) - end - ) - else if (thisLine = "% Proof not found.\n") - then - ( - let val reconstr = thisLine - val thmstring = TextIO.inputLine instr - val goalstring = TextIO.inputLine instr - in - (reconstr, thmstring, goalstring) - end - ) - else if (String.isPrefix "Rules from" thisLine) - then - ( - let val reconstr = thisLine - val thmstring = TextIO.inputLine instr - val goalstring = TextIO.inputLine instr - in - (reconstr, thmstring, goalstring) - end - ) + val _ = TextIO.closeOut outfile + in (* reconstructed proof string *) + if ( (substring (thisLine, 0,1))= "[") + then + (*Pretty.writeln(Pretty.str (thisLine))*) + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + else if (thisLine = "% Unprovable.\n" ) + then + ( + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + ) + else if (thisLine = "% Proof not found.\n") + then + ( + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + ) + else if (String.isPrefix "Rules from" thisLine) + then + ( + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + (reconstr, thmstring, goalstring) + end + ) - else if (thisLine = "Proof found but translation failed!") - then - ( - let val reconstr = thisLine - val thmstring = TextIO.inputLine instr - val goalstring = TextIO.inputLine instr - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getVamp"))); - val _ = TextIO.output (outfile, (thisLine)) - val _ = TextIO.closeOut outfile - in - (reconstr, thmstring, goalstring) - end - ) - else - getVampInput instr - - end - else - ("No output from reconstruction process.\n","","") + else if (thisLine = "Proof found but translation failed!") + then + ( + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getVamp"))); + val _ = TextIO.output (outfile, (thisLine)) + val _ = TextIO.closeOut outfile + in + (reconstr, thmstring, goalstring) + end + ) + else + getVampInput instr - + end + else + ("No output from reconstruction process.\n","","") end; diff -r cf872f3e16d9 -r abf475cf11f2 src/HOL/Tools/ATP/VampireCommunication.ML --- a/src/HOL/Tools/ATP/VampireCommunication.ML Mon Jun 20 21:33:27 2005 +0200 +++ b/src/HOL/Tools/ATP/VampireCommunication.ML Mon Jun 20 21:34:31 2005 +0200 @@ -4,6 +4,8 @@ Copyright 2004 University of Cambridge *) +(* FIXME proper structure definition *) + (***************************************************************************) (* Code to deal with the transfer of proofs from a Vampire process *) (***************************************************************************) @@ -12,32 +14,34 @@ (* Write vampire output to a file *) (***********************************) -fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr - in if thisLine = "%============== End of proof. ==================\n" - then TextIO.output (fd, thisLine) - else ( - TextIO.output (fd, thisLine); logVampInput (instr,fd)) - end; +fun logVampInput (instr, fd) = + let val thisLine = TextIO.inputLine instr + in if thisLine = "%============== End of proof. ==================\n" + then TextIO.output (fd, thisLine) + else ( + TextIO.output (fd, thisLine); logVampInput (instr,fd)) + end; (**********************************************************************) (* Transfer the vampire output from the watcher to the input pipe of *) (* the main Isabelle process *) (**********************************************************************) -fun transferVampInput (fromChild, toParent, ppid) = let - val thisLine = TextIO.inputLine fromChild - in - if (thisLine = "%============== End of proof. ==================\n" ) - then ( - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent - ) - else ( - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; - transferVampInput (fromChild, toParent, ppid) - ) - end; +fun transferVampInput (fromChild, toParent, ppid) = + let + val thisLine = TextIO.inputLine fromChild + in + if (thisLine = "%============== End of proof. ==================\n" ) + then ( + TextIO.output (toParent, thisLine); + TextIO.flushOut toParent + ) + else ( + TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + transferVampInput (fromChild, toParent, ppid) + ) + end; (*********************************************************************************) @@ -45,74 +49,63 @@ (* and if so, transfer output to the input pipe of the main Isabelle process *) (*********************************************************************************) -fun startVampireTransfer (fromChild, toParent, ppid, childCmd) = - if (isSome (TextIO.canInput(fromChild, 5))) - then - ( - let val thisLine = TextIO.inputLine fromChild - in - if (thisLine = "% Proof found. Thanks to Tanya!\n" ) - then - ( - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1); - TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; +fun startVampireTransfer (fromChild, toParent, ppid, childCmd) = + if (isSome (TextIO.canInput(fromChild, 5))) + then + ( + let val thisLine = TextIO.inputLine fromChild + in + if (thisLine = "% Proof found. Thanks to Tanya!\n" ) + then + ( + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1); + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; - transferVampInput (fromChild, toParent, ppid); - true) - else if (thisLine = "% Unprovable.\n" ) - then - ( - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1); - TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; + transferVampInput (fromChild, toParent, ppid); + true) + else if (thisLine = "% Unprovable.\n" ) + then + ( + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1); + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; - true) - else if (thisLine = "% Proof not found.\n") - then - (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1); TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; - true) - else - ( - startVampireTransfer (fromChild, toParent, ppid, childCmd) - ) - end - ) - else (false) + true) + else if (thisLine = "% Proof not found.\n") + then + (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1); + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + true) + else + ( + startVampireTransfer (fromChild, toParent, ppid, childCmd) + ) + end + ) + else (false) (***********************************************************************) (* Function used by the Isabelle process to read in a vampire proof *) (***********************************************************************) -fun getVampInput instr = let val thisLine = TextIO.inputLine instr - in - if (thisLine = "%============== End of proof. ==================\n" ) - then - ( - (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));() - ) - else if (thisLine = "% Unprovable.\n" ) - then - ( - (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));() - ) - else if (thisLine = "% Proof not found.\n") - then - ( - Pretty.writeln(Pretty.str (concat["vampire", thisLine]));() - ) - - - else - ( - Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr - ) - end; +fun getVampInput instr = + let val thisLine = TextIO.inputLine instr + in + if thisLine = "%============== End of proof. ==================\n" then + Pretty.writeln (Pretty.str (concat ["vampire", thisLine])) + else if thisLine = "% Unprovable.\n" then + Pretty.writeln (Pretty.str (concat ["vampire", thisLine])) + else if thisLine = "% Proof not found.\n" then + Pretty.writeln (Pretty.str (concat ["vampire", thisLine])) + else + (Pretty.writeln (Pretty.str (concat ["vampire", thisLine])); getVampInput instr) + end;