# HG changeset patch # User paulson # Date 1117188725 -7200 # Node ID f80fc4bff9332e8db5b07865bfaee0e4e18c283b # Parent c5882ca551ddb3952ddb075082e3b8bc5e6d5df1 Now uses File.write and File.append diff -r c5882ca551dd -r f80fc4bff933 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Fri May 27 01:30:27 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Fri May 27 12:12:05 2005 +0200 @@ -153,21 +153,20 @@ (*****************************************************************************************) (* need to modify to send over hyps file too *) -fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n"); - TextIO.flushOut toWatcherStr) +fun callResProvers (toWatcherStr, []) = + (sendOutput (toWatcherStr, "End of calls\n"); + TextIO.flushOut toWatcherStr) | callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) = let val dfg_dir = File.tmp_path (Path.basic "dfg"); (*** need to check here if the directory exists and, if not, create it***) - val outfile = TextIO.openAppend(File.sysify_path - (File.tmp_path (Path.basic"thmstring_in_watcher"))); - val _ = TextIO.output (outfile, - (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")) - val _ = TextIO.closeOut outfile + val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher")) + (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n") (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) val probID = ReconOrderClauses.last(explode probfile) val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) (*** only include problem and clasimp for the moment, not sure how to refer to ***) (*** hyps/local axioms just now ***) + (*FIXME: find a way that works for SML/NJ too: it regards > as a filename!*) val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) val dfg_create = if File.exists dfg_dir then warning("dfg dir exists") @@ -235,26 +234,25 @@ getSettings rest (settings@[(implode set)]) end -fun separateFields str = let val (prover, rest) = takeUntil "*" str [] - val prover = implode prover - val (thmstring, rest) = takeUntil "*" rest [] - val thmstring = implode thmstring - val (goalstring, rest) = takeUntil "*" rest [] - val goalstring = implode goalstring - val (proverCmd, rest ) = takeUntil "*" rest [] - val proverCmd = implode proverCmd - - val (settings, rest) = takeUntil "*" rest [] - val settings = getSettings settings [] - val (file, rest) = takeUntil "*" rest [] - val file = implode file - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "sep_comms"))); - val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) ) - val _ = TextIO.closeOut outfile - - in - (prover,thmstring,goalstring, proverCmd, settings, file) - end +fun separateFields str = + let val (prover, rest) = takeUntil "*" str [] + val prover = implode prover + val (thmstring, rest) = takeUntil "*" rest [] + val thmstring = implode thmstring + val (goalstring, rest) = takeUntil "*" rest [] + val goalstring = implode goalstring + val (proverCmd, rest ) = takeUntil "*" rest [] + val proverCmd = implode proverCmd + + val (settings, rest) = takeUntil "*" rest [] + val settings = getSettings settings [] + val (file, rest) = takeUntil "*" rest [] + val file = implode file + val _ = File.write (File.tmp_path (Path.basic "sep_comms")) + (prover^thmstring^goalstring^proverCmd^file) + in + (prover,thmstring,goalstring, proverCmd, settings, file) + end @@ -277,26 +275,26 @@ (**************************************************************) fun getCmds (toParentStr,fromParentStr, cmdList) = - let val thisLine = TextIO.inputLine fromParentStr - in - (if (thisLine = "End of calls\n") - then - (cmdList) - else if (thisLine = "Kill children\n") - then - ( TextIO.output (toParentStr,thisLine ); - TextIO.flushOut toParentStr; - (("","","","Kill children",[],"")::cmdList) - ) - else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*) - in - (*TextIO.output (toParentStr, thisCmd); - TextIO.flushOut toParentStr;*) - getCmds (toParentStr,fromParentStr, (thisCmd::cmdList)) - end - ) - ) - end + let val thisLine = TextIO.inputLine fromParentStr + in + (if (thisLine = "End of calls\n") + then + (cmdList) + else if (thisLine = "Kill children\n") + then + ( TextIO.output (toParentStr,thisLine ); + TextIO.flushOut toParentStr; + (("","","","Kill children",[],"")::cmdList) + ) + else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*) + in + (*TextIO.output (toParentStr, thisCmd); + TextIO.flushOut toParentStr;*) + getCmds (toParentStr,fromParentStr, (thisCmd::cmdList)) + end + ) + ) + end (**************************************************************) @@ -448,20 +446,15 @@ val sign = sign_of_thm thm val prems = prems_of thm val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) - val _ = (warning ("subgoals forked to checkChildren: "^prems_string)); - val goalstring = cmdGoal childProc - - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms"))); - val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) ) - val _ = TextIO.closeOut outfile + val _ = warning("subgoals forked to checkChildren: "^prems_string) + val goalstring = cmdGoal childProc + val _ = File.write (File.tmp_path (Path.basic "child_comms")) + (prover^thmstring^goalstring^childCmd) in if (isSome childIncoming) then (* check here for prover label on child*) - - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); - val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) ) - val _ = TextIO.closeOut outfile + 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" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) in @@ -482,12 +475,8 @@ (childProc::(checkChildren (otherChildren, toParentStr))) end else - let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); - val _ = TextIO.output (outfile,"No child output " ) - val _ = TextIO.closeOut outfile - in - (childProc::(checkChildren (otherChildren, toParentStr))) - end + (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output "; + childProc::(checkChildren (otherChildren, toParentStr))) end @@ -502,38 +491,36 @@ (*** add subgoal id num to this *) fun execCmds [] procList = procList | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = - if (prover = "spass") - then - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) - val (instr, outstr)=Unix.streamsOf childhandle - val newProcList = (((CMDPROC{ - prover = prover, - cmd = file, - thmstring = thmstring, - goalstring = goalstring, - proc_handle = childhandle, - instr = instr, - outstr = outstr })::procList)) - val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child"))); - val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file ) - val _ = TextIO.closeOut outfile - in - execCmds cmds newProcList - end - else - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) - val (instr, outstr)=Unix.streamsOf childhandle - val newProcList = (((CMDPROC{ - prover = prover, - cmd = file, - thmstring = thmstring, - goalstring = goalstring, - proc_handle = childhandle, - instr = instr, - outstr = outstr })::procList)) - in - execCmds cmds newProcList - end + if (prover = "spass") + then + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) + val (instr, outstr)=Unix.streamsOf childhandle + val newProcList = (((CMDPROC{ + prover = prover, + cmd = file, + thmstring = thmstring, + goalstring = goalstring, + proc_handle = childhandle, + instr = instr, + outstr = outstr })::procList)) + val _ = File.append (File.tmp_path (Path.basic "exec_child")) ("executing command for goal:"^goalstring^proverCmd^(concat settings)^file) + in + execCmds cmds newProcList + end + else + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) + val (instr, outstr)=Unix.streamsOf childhandle + val newProcList = (((CMDPROC{ + prover = prover, + cmd = file, + thmstring = thmstring, + goalstring = goalstring, + proc_handle = childhandle, + instr = instr, + outstr = outstr })::procList)) + in + execCmds cmds newProcList + end @@ -713,103 +700,83 @@ 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 childin = fst streams - val childout = snd streams - val childpid = fst mychild - val sign = sign_of_thm thm - val prems = prems_of thm - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) - val _ = (warning ("subgoals forked to createWatcher: "^prems_string)); - fun vampire_proofHandler (n) = - (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() ) - - -fun spass_proofHandler (n) = ( - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1"))); - val _ = TextIO.output (outfile, ("In signal handler now\n")) - val _ = TextIO.closeOut outfile - val (reconstr, thmstring, goalstring) = getSpassInput childin - val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal"))); - - 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))= "[") - then +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 childin = fst streams + val childout = snd streams + val childpid = fst mychild + val sign = sign_of_thm thm + val prems = prems_of thm + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) + val _ = (warning ("subgoals forked to createWatcher: "^prems_string)); + fun vampire_proofHandler (n) = + (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); + getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() ) + - ( - 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) - then - (let val outfile = TextIO.openOut(File.sysify_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 - in - reapWatcher (childpid,childin, childout); () - end) - else - () - ) - (* if there's no proof, but a message from 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 (goalstring^reconstr)); - Pretty.writeln(Pretty.str (oct_char "361")); - if (!goals_being_watched = 0) - then - (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp"))); - val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) - val _ = TextIO.closeOut outfile - in - reapWatcher (childpid,childin, childout); () - end ) - else - () - ) - (* if proof translation failed *) - 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^reconstr)); - Pretty.writeln(Pretty.str (oct_char "361")); - if (!goals_being_watched = 0) - then - (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp"))); - val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) - val _ = TextIO.closeOut outfile - in - reapWatcher (childpid,childin, childout); () - end ) - else - () - ) + fun spass_proofHandler (n) = ( + let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n" + val (reconstr, thmstring, goalstring) = getSpassInput childin + val _ = File.append (File.tmp_path (Path.basic "foo_signal")) + ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))) + in (* if a proof has been found and sent back as a reconstruction proof *) + 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) + then + (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 + reapWatcher (childpid,childin, childout); () + end) + else () + ) + (* if there's no proof, but a message from 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 (goalstring^reconstr)); + 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"); + reapWatcher (childpid,childin, childout); ()) + else + () + ) + (* if proof translation failed *) + 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^reconstr)); + 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"); + reapWatcher (childpid,childin, childout); ()) + else ()) + else () (* add something here ?*) + end) - else (* add something here ?*) - () - - end) - + + in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler); + IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler); + (childin, childout, childpid) - - in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler); - IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler); - (childin, childout, childpid) - - end + end