--- 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;
--- 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);