# HG changeset patch # User paulson # Date 1125667544 -7200 # Node ID f42bc4f7afdfe4b43dcf603a21b818d05dea9cd1 # Parent 77e93bf303a5ba87643b310c88e8e02a57a9b7e9 tidying up the Isabelle/ATP interface diff -r 77e93bf303a5 -r f42bc4f7afdf src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Fri Sep 02 15:25:27 2005 +0200 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Fri Sep 02 15:25:44 2005 +0200 @@ -28,12 +28,12 @@ (* Write Spass output to a file *) (***********************************) -fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr - in if thisLine = "--------------------------SPASS-STOP------------------------------\n" - then TextIO.output (fd, thisLine) - else ( - TextIO.output (fd, thisLine); logSpassInput (instr,fd)) - end; +fun logSpassInput (instr, fd) = + let val thisLine = TextIO.inputLine instr + in if thisLine = "--------------------------SPASS-STOP------------------------------\n" + then TextIO.output (fd, thisLine) + else (TextIO.output (fd, thisLine); logSpassInput (instr,fd)) + end; (**********************************************************************) (* Reconstruct the Spass proof w.r.t. thmstring (string version of *) @@ -41,54 +41,47 @@ (* steps as a string to the input pipe of the main Isabelle process *) (**********************************************************************) - -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)] - end); +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)] + 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"))); +fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num + clause_arr (num_of_clauses:int ) = + (*FIXME: foo is never used!*) + 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.spassString_to_reconString proofextract thmstring goalstring - toParent ppid negs clause_arr num_of_clauses - else - Recon_Transfer.spassString_to_lemmaString proofextract thmstring goalstring - toParent ppid negs clause_arr num_of_clauses ))]) sg_num + SELECT_GOAL + (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, + METAHYPS(fn negs => + (if !reconstruct + then Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring + toParent ppid negs clause_arr num_of_clauses + else Recon_Transfer.spassString_to_lemmaString proofextract thmstring goalstring + toParent ppid negs clause_arr num_of_clauses ))]) sg_num end ; -fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = let - val thisLine = TextIO.inputLine fromChild - in - if (thisLine = "--------------------------SPASS-STOP------------------------------\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 ( - - transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr, num_of_clauses) - ) - end; - - +fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) = + let val thisLine = TextIO.inputLine fromChild + in + if thisLine = "--------------------------SPASS-STOP------------------------------\n" + then + let val proofextract = Recon_Parse.extract_proof (currentString^thisLine) + in + File.write (File.tmp_path (Path.basic"foobar2")) proofextract; + reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num + clause_arr num_of_clauses thm + end + else transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring, + (currentString^thisLine), thm, sg_num, clause_arr, + num_of_clauses) + end; (*********************************************************************************) @@ -98,210 +91,171 @@ fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = - (*let val _ = Posix.Process.wait () - in*) +(*let val _ = Posix.Process.wait () +in*) - if (isSome (TextIO.canInput(fromChild, 5))) - then - ( - let val thisLine = TextIO.inputLine fromChild - in - if (String.isPrefix "Here is a proof" thisLine ) - 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 - transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr, num_of_clauses); - true - end) - - else - ( - startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses) - ) - end - ) - else (false) - (* end*) + if (isSome (TextIO.canInput(fromChild, 5))) + then + let val thisLine = TextIO.inputLine fromChild + in + if String.isPrefix "Here is a proof" thisLine 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 + transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, + thm, sg_num,clause_arr, num_of_clauses); + true + end + else startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring, + childCmd, thm, sg_num,clause_arr, num_of_clauses) + end + else false + (* end*) fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) = - let val spass_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "spass_proof"))) - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkspass"))); - 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 = "SPASS beiseite: Proof found.\n" ) - then - ( - let val outfile = TextIO.openAppend(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 - startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) - end - ) - else if (thisLine= "SPASS beiseite: Completion found.\n" ) - then + let val spass_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "spass_proof"))) + val _ = File.write(File.tmp_path (Path.basic "foo_checkspass")) + ("checking if proof found, thm is: "^(string_of_thm thm)) + in + if (isSome (TextIO.canInput(fromChild, 5))) + then + let val thisLine = TextIO.inputLine fromChild + in if thisLine = "SPASS beiseite: Proof found.\n" + then + let val outfile = TextIO.openAppend(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 + startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses) + end + else if thisLine= "SPASS beiseite: Completion found.\n" + then + let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + val _ = TextIO.output (outfile, thisLine) - ( - let val outfile = TextIO.openAppend(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 (spass_proof_file, (thisLine)); - TextIO.flushOut spass_proof_file; - TextIO.closeOut spass_proof_file; - (*TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; - TextIO.output (toParent, "bar\n"); - TextIO.flushOut toParent;*) + val _ = TextIO.closeOut outfile + in + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (spass_proof_file, thisLine); + TextIO.flushOut spass_proof_file; + TextIO.closeOut spass_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 = "SPASS beiseite: Ran out of time.\n" ) - then - ( let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) - val _ = TextIO.output (outfile, (thisLine)) - - - in 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); - TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile; - - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); - true - end) - - - - else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\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 (spass_proof_file, (thisLine)); - TextIO.flushOut spass_proof_file; - checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)) - - end - ) - else - (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false) - end + 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 = "SPASS beiseite: Ran out of time.\n" + then + let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + val _ = TextIO.output (outfile, thisLine) + in 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); + TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile; + (* Attempt to prevent several signals from turning up simultaneously *) + Posix.Process.sleep(Time.fromSeconds 1); + true + end + else if thisLine = "SPASS beiseite: Maximal number of loops exceeded.\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 (spass_proof_file, thisLine); + TextIO.flushOut spass_proof_file; + checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring, + childCmd, thm, sg_num, clause_arr, num_of_clauses)) + end + else + (TextIO.output (spass_proof_file, ("No proof output seen \n")); + TextIO.closeOut spass_proof_file; + false) + end (***********************************************************************) (* Function used by the Isabelle process to read in a spass proof *) (***********************************************************************) - - -fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2))) - then - let val thisLine = TextIO.inputLine instr - val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine)) - - - val _ = TextIO.closeOut outfile - in - 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 (String.isPrefix "SPASS beiseite:" thisLine ) - 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 ((substring (thisLine, 0,5)) = "Proof") - 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_getSpass"))); - val _ = TextIO.output (outfile, (thisLine)) - val _ = TextIO.closeOut outfile - in - (reconstr, thmstring, goalstring) - end - ) - else if ((substring (thisLine, 0,1)) = "%") - 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_getSpass"))); - val _ = TextIO.output (outfile, (thisLine)) - val _ = TextIO.closeOut outfile - in - (reconstr, thmstring, goalstring) - end - ) - else - getSpassInput instr - - end - else - ("No output from reconstruction process.\n","","") +fun getSpassInput instr = + if isSome (TextIO.canInput(instr, 2)) + then + let val thisLine = TextIO.inputLine instr + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); + val _ = TextIO.output (outfile, thisLine) + val _ = TextIO.closeOut outfile + in + 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 String.isPrefix "SPASS beiseite:" thisLine + 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 substring (thisLine, 0,5) = "Proof" + then + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine; + (reconstr, thmstring, goalstring) + end + else if substring (thisLine, 0,1) = "%" + then + let val reconstr = thisLine + val thmstring = TextIO.inputLine instr + val goalstring = TextIO.inputLine instr + in + File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine; + (reconstr, thmstring, goalstring) + end + else getSpassInput instr + end + else + ("No output from reconstruction process.\n","","") end; diff -r 77e93bf303a5 -r f42bc4f7afdf src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Fri Sep 02 15:25:27 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Sep 02 15:25:44 2005 +0200 @@ -143,8 +143,9 @@ (* Send request to Watcher for a vampire to be called for filename in arg *) (********************************************************************************) -fun callResProver (toWatcherStr, arg) = (sendOutput (toWatcherStr, arg^"\n"); - TextIO.flushOut toWatcherStr) +fun callResProver (toWatcherStr, arg) = + (sendOutput (toWatcherStr, arg^"\n"); + TextIO.flushOut toWatcherStr) (*****************************************************************************************) (* Send request to Watcher for multiple provers to be called for filenames in arg *) @@ -267,34 +268,12 @@ (*** only include problem and clasimp for the moment, not sure how to refer to ***) (*** hyps/local axioms just now ***) val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile, ">", (File.platform_path wholefile)]) - (*** check if the directory exists and, if not, create it***) - (* val _ = - if !SpassComm.spass - then - if File.exists dfg_dir then warning("dfg dir exists") - else File.mkdir dfg_dir - else - warning("not converting to dfg") - - val _ = if !SpassComm.spass then - system (ResLib.helper_path "TPTP2X_HOME" "tptp2X" ^ - " -fdfg -d " ^ dfg_path ^ " " ^ - File.platform_path wholefile) - else 7 - val newfile = if !SpassComm.spass - then - dfg_path^"/ax_prob"^"_"^(probID)^".dfg" - - else - (File.platform_path wholefile)*) (* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*) (* from clasimpset onto problem file *) val newfile = if !SpassComm.spass - then - probfile - else - (File.platform_path wholefile) + then probfile + else (File.platform_path wholefile) val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher")) (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n") @@ -366,7 +345,6 @@ (* Get Io-descriptor for polling of an input stream *) (**************************************************************) - fun getInIoDesc someInstr = let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr) val _ = TextIO.output (TextIO.stdOut, buf) @@ -385,8 +363,6 @@ (* Set up a Watcher Process *) (*************************************) - - fun setupWatcher (thm,clause_arr, num_of_clauses) = let (** pipes for communication between parent and watcher **) @@ -451,13 +427,10 @@ then NONE else if (OS.IO.isIn (hd pdl)) - then - (SOME ( getCmds (toParentStr, fromParentStr, []))) - else - NONE + then SOME (getCmds (toParentStr, fromParentStr, [])) + else NONE end - else - NONE + else NONE end fun pollChildInput (fromStr) = @@ -472,7 +445,6 @@ if (isSome pd ) then let val pd' = OS.IO.pollIn (valOf pd) val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) - in if null pdl then @@ -534,7 +506,9 @@ if (isSome childIncoming) then (* check here for prover label on child*) - let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) + let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) + ("subgoals forked to checkChildren:"^ + prems_string^prover^thmstring^goalstring^childCmd) val childDone = (case prover of "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) @@ -709,13 +683,10 @@ (* start the watcher loop *) (***************************) keepWatching (toParentStr, fromParentStr, procList); - - (****************************************************************************) - (* fake return value - actually want the watcher to loop until killed *) + (* fake return value - actually want the watcher to loop until killed *) (****************************************************************************) Posix.Process.wordToPid 0w0 - end); (* end case *) @@ -770,11 +741,9 @@ status end - - fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses)) - val streams =snd mychild + val streams = snd mychild val childin = fst streams val childout = snd streams val childpid = fst mychild @@ -795,24 +764,24 @@ val _ = TextIO.output (outfile, ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))) val _ = TextIO.closeOut outfile in (* if a proof has been found and sent back as a reconstruction proof *) - if ( (substring (reconstr, 0,1))= "[") + if substring (reconstr, 0,1) = "[" then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); Recon_Transfer.apply_res_thm reconstr goalstring; Pretty.writeln(Pretty.str (oct_char "361")); goals_being_watched := ((!goals_being_watched) - 1); - if ((!goals_being_watched) = 0) + if (!goals_being_watched) = 0 then - (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found"))); - val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) - val _ = TextIO.closeOut outfile + let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found")) + ("Reaping a watcher, goals watched is: "^ + (string_of_int (!goals_being_watched))^"\n") in killWatcher (childpid); reapWatcher (childpid,childin, childout); () - end) + end else () ) (* if there's no proof, but a message from Spass *) - else if ((substring (reconstr, 0,5))= "SPASS") + else if substring (reconstr, 0,5) = "SPASS" then (goals_being_watched := (!goals_being_watched) -1; Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr)); @@ -824,7 +793,7 @@ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()) else () ) (* print out a list of rules used from clasimpset*) - else if ((substring (reconstr, 0,5))= "Rules") + else if substring (reconstr, 0,5) = "Rules" then (goals_being_watched := (!goals_being_watched) -1; Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); Pretty.writeln(Pretty.str (goalstring^reconstr)); @@ -837,7 +806,7 @@ ) else () ) (* if proof translation failed *) - else if ((substring (reconstr, 0,5)) = "Proof") + else if substring (reconstr, 0,5) = "Proof" then (goals_being_watched := (!goals_being_watched) -1; Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); @@ -850,7 +819,7 @@ ) else () ) - else if ((substring (reconstr, 0,1)) = "%") + else if substring (reconstr, 0,1) = "%" then (goals_being_watched := (!goals_being_watched) -1; Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); @@ -866,15 +835,15 @@ else (* add something here ?*) (goals_being_watched := (!goals_being_watched) -1; Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str ("Ran out of options in handler")); - Pretty.writeln(Pretty.str (oct_char "361")); - if (!goals_being_watched = 0) - then (File.write (File.tmp_path (Path.basic "foo_reap_comp")) - ("Reaping a watcher, goals watched is: " ^ - (string_of_int (!goals_being_watched))^"\n"); - killWatcher (childpid); reapWatcher (childpid,childin, childout);() - ) - else () ) + Pretty.writeln(Pretty.str ("Ran out of options in handler")); + Pretty.writeln(Pretty.str (oct_char "361")); + if (!goals_being_watched = 0) + then (File.write (File.tmp_path (Path.basic "foo_reap_comp")) + ("Reaping a watcher, goals watched is: " ^ + (string_of_int (!goals_being_watched))^"\n"); + killWatcher (childpid); reapWatcher (childpid,childin, childout);() + ) + else () ) end) in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler); diff -r 77e93bf303a5 -r f42bc4f7afdf src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Sep 02 15:25:27 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Sep 02 15:25:44 2005 +0200 @@ -143,28 +143,18 @@ (* where N is the number of this subgoal *) (*********************************************************************) -(*fun dfg_inputs_tfrees thms n tfrees axclauses= - let val clss = map (ResClause.make_conjecture_clause_thm) thms - val _ = (debug ("in dfg_inputs_tfrees 1")) - val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss) - val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) - val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) - val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] tfrees - val out = TextIO.openOut(probfile) - in - (ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; debug probfile) - end; -*) fun dfg_inputs_tfrees thms n tfrees axclauses = let val clss = map (ResClause.make_conjecture_clause_thm) thms val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) - val _ = warning ("about to write out dfg prob file "^probfile) + val _ = debug ("about to write out dfg prob file " ^ probfile) (*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss) val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *) - val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] tfrees + val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) + axclauses [] [] [] tfrees val out = TextIO.openOut(probfile) in (ResLib.writeln_strs out [filestr]; TextIO.closeOut out; debug probfile ) +(* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *) end; @@ -238,11 +228,13 @@ ( SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, - METAHYPS(fn negs => (if !SpassComm.spass then - dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses - else - tptp_inputs_tfrees (make_clauses negs) n tfrees; - get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n -1) (negs::sko_thms) axclauses; dummy_tac))]) n thm ) + METAHYPS(fn negs => + (if !SpassComm.spass + then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses + else tptp_inputs_tfrees (make_clauses negs) n tfrees; + get_sko_thms tfrees sign sg_terms (childin, childout, pid) + thm (n -1) (negs::sko_thms) axclauses; + dummy_tac))]) n thm ) @@ -277,7 +269,7 @@ (* write to file "hyps" *) (**************************************************) -fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) axclauses= +fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) axclauses = let val tfree_lits = isar_atp_h thms in debug ("in isar_atp_aux");