(* Title: VampCommunication.ml
ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
(***************************************************************************)
(* Code to deal with the transfer of proofs from a Vamp process *)
(***************************************************************************)
signature VAMP_COMM =
sig
val reconstruct : bool ref
val getVampInput : TextIO.instream -> string * string * 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 =
struct
(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
val reconstruct = ref true;
(***********************************)
(* 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;
(**********************************************************************)
(* Reconstruct the Vamp 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 ) =
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
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;
(*********************************************************************************)
(* Inspect the output of a Vamp process to see if it has found a proof, *)
(* 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 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
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. Time limit expired.\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
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
(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
(***********************************************************************)
(* 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))
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. Time limit expired.\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","","")
end;