src/HOL/Tools/ATP/VampCommunication.ML

use AList operations;

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