(* Title: SpassCommunication.ml
ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
(***************************************************************************)
(* Code to deal with the transfer of proofs from a E process *)
(***************************************************************************)
signature E_COMM =
sig
val reconstruct : bool ref
val E: bool ref
val getEInput : TextIO.instream -> string * string * string
val checkEProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array * int -> bool
end;
structure EComm :E_COMM =
struct
(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
val reconstruct = ref true;
val E = ref false;
(***********************************)
(* Write E output to a file *)
(***********************************)
fun logEInput (instr, fd) =
let val thisLine = TextIO.inputLine instr
in if thisLine = "# Proof object ends here.\n"
then TextIO.output (fd, thisLine)
else (TextIO.output (fd, thisLine); logEInput (instr,fd))
end;
(**********************************************************************)
(* Reconstruct the E proof w.r.t. thmstring (string version of *)
(* Isabelle goal to be proved), then transfer the reconstruction *)
(* 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);
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 =>
( Recon_Transfer.EString_to_lemmaString proofextract thmstring goalstring
toParent ppid negs clause_arr num_of_clauses ))]) sg_num
end ;
fun transferEInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr, num_of_clauses) =
let val thisLine = TextIO.inputLine fromChild
in
if thisLine = "# Proof object ends here.\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 transferEInput (fromChild, toParent, ppid,thmstring, goalstring,
(currentString^thisLine), thm, sg_num, clause_arr,
num_of_clauses)
end;
(*********************************************************************************)
(* Inspect the output of a E process to see if it has found a proof, *)
(* and if so, transfer output to the input pipe of the main Isabelle process *)
(*********************************************************************************)
fun startETransfer (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 String.isPrefix "# Proof object starts" 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
transferEInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine,
thm, sg_num,clause_arr, num_of_clauses);
true
end
else startETransfer (fromChild, toParent, ppid, thmstring, goalstring,
childCmd, thm, sg_num,clause_arr, num_of_clauses)
end
else false
(* end*)
fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) =
let val E_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "E_proof")))
val _ = File.write(File.tmp_path (Path.basic "foo_checkE"))
("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 = "# Problem is unsatisfiable (or provable), constructing proof object\n"*)
thisLine = "# # TSTP exit status: Unsatisfiable\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
startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses)
end
else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\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
TextIO.output (toParent,childCmd^"\n" );
TextIO.flushOut toParent;
TextIO.output (E_proof_file, thisLine);
TextIO.flushOut E_proof_file;
TextIO.closeOut E_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 = "# Failure: Resource limit exceeded (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 = "# Failure: Resource limit exceeded (memory)\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 (E_proof_file, thisLine);
TextIO.flushOut E_proof_file;
checkEProofFound (fromChild, toParent, ppid, thmstring,goalstring,
childCmd, thm, sg_num, clause_arr, num_of_clauses))
end
else
(TextIO.output (E_proof_file, ("No proof output seen \n"));
TextIO.closeOut E_proof_file;
false)
end
(***********************************************************************)
(* Function used by the Isabelle process to read in a E proof *)
(***********************************************************************)
fun getEInput 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 "# No proof" 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 "# Failure" 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 getEInput instr
end
else
("No output from reconstruction process.\n","","")
end;