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