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