src/HOL/Tools/ATP/modUnix.ML
author quigley
Wed Apr 20 18:01:50 2005 +0200 (2005-04-20)
changeset 15782 a1863ea9052b
parent 15700 970e0293dfb3
child 15789 4cb16144c81b
permissions -rw-r--r--
Corrected the problem with the ATP directory.
     1 
     2 (****************************************************************)
     3 (****** Slightly modified version of sml Unix structure *********)
     4 (****************************************************************)
     5 
     6 type signal = Posix.Signal.signal
     7 datatype exit_status = datatype Posix.Process.exit_status
     8 
     9 val fromStatus = Posix.Process.fromStatus
    10 
    11 
    12 fun reap(pid, instr, outstr) =
    13         let
    14 		val u = TextIO.closeIn instr;
    15 	        val u = TextIO.closeOut outstr;
    16 	
    17 		val (_, status) =
    18 			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    19 	in
    20 		status
    21 	end
    22 
    23 fun fdReader (name : string, fd : Posix.IO.file_desc) =
    24 	  Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
    25 
    26 fun fdWriter (name, fd) =
    27           Posix.IO.mkWriter {
    28 	      appendMode = false,
    29               initBlkMode = true,
    30               name = name,  
    31               chunkSize=4096,
    32               fd = fd
    33             };
    34 
    35 fun openOutFD (name, fd) =
    36 	  TextIO.mkOutstream (
    37 	    TextIO.StreamIO.mkOutstream (
    38 	      fdWriter (name, fd), IO.BLOCK_BUF));
    39 
    40 fun openInFD (name, fd) =
    41 	  TextIO.mkInstream (
    42 	    TextIO.StreamIO.mkInstream (
    43 	      fdReader (name, fd), ""));
    44 
    45 
    46 
    47 
    48 
    49 (*****************************************)
    50 (*  The result of calling createWatcher  *)
    51 (*****************************************)
    52 
    53 datatype proc = PROC of {
    54         pid : Posix.Process.pid,
    55         instr : TextIO.instream,
    56         outstr : TextIO.outstream
    57       };
    58 
    59 
    60 
    61 (*****************************************)
    62 (*  The result of calling executeToList  *)
    63 (*****************************************)
    64 
    65 datatype cmdproc = CMDPROC of {
    66         prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
    67         cmd:  string,              (* The file containing the goal for res prover to prove *)     
    68         thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
    69         goalstring: string,         (* string representation of subgoal*) 
    70         pid : Posix.Process.pid,
    71         instr : TextIO.instream,   (*  Input stream to child process *)
    72         outstr : TextIO.outstream  (*  Output stream from child process *)
    73       };
    74 
    75 
    76 
    77 fun killChild pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
    78 
    79 fun childInfo (PROC{pid,instr,outstr}) = ((pid, (instr,outstr)));
    80 
    81 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
    82 
    83 fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
    84 
    85 fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover,(cmd,(pid, (instr,outstr))));
    86 
    87 fun cmdchildPid (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr})  = (pid);
    88 
    89 fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr})  = (prover);
    90 
    91 fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr})  = (thmstring);
    92 
    93 fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr})  = (goalstring);
    94 (***************************************************************************)
    95 (*  Takes a command - e.g. 'vampire', a list of arguments for the command, *)
    96 (*  and a list of currently running processes.  Creates a new process for  *)
    97 (*  cmd and argv and adds it to procList                                   *)
    98 (***************************************************************************)
    99 
   100 
   101 
   102 
   103 fun mySshExecuteToList (cmd, argv, procList) = let
   104           val p1 = Posix.IO.pipe ()
   105           val p2 = Posix.IO.pipe ()
   106           val prover = hd argv
   107           val thmstring = hd(tl argv)
   108           val goalstring = hd(tl(tl argv))
   109           val argv = tl (tl argv)
   110           
   111           (* Turn the arguments into a single string.  Perhaps we should quote the
   112                    arguments.  *)
   113                 fun convArgs [] = []
   114                   | convArgs [s] = [s]
   115                   | convArgs (hd::tl) = hd :: " " :: convArgs tl
   116                 val cmd_args = concat(convArgs(cmd :: argv))
   117 
   118 	  fun closep () = (
   119                 Posix.IO.close (#outfd p1); 
   120                 Posix.IO.close (#infd p1);
   121                 Posix.IO.close (#outfd p2); 
   122                 Posix.IO.close (#infd p2)
   123               )
   124           fun startChild () =(case  Posix.Process.fork()
   125 		 of SOME pid =>  pid           (* parent *)
   126                   | NONE => let                 
   127 		      val oldchildin = #infd p1
   128 		      val newchildin = Posix.FileSys.wordToFD 0w0
   129 		      val oldchildout = #outfd p2
   130 		      val newchildout = Posix.FileSys.wordToFD 0w1
   131                       (*val args = (["shep"]@([cmd]@argv))
   132                       val newcmd = "/usr/bin/ssh"*)
   133                       
   134                       in
   135 			Posix.IO.close (#outfd p1);
   136 			Posix.IO.close (#infd p2);
   137 			Posix.IO.dup2{old = oldchildin, new = newchildin};
   138                         Posix.IO.close oldchildin;
   139 			Posix.IO.dup2{old = oldchildout, new = newchildout};
   140                         Posix.IO.close oldchildout;
   141                        (* Run the command. *)
   142                        (* Run this as a shell command.  The command and arguments have
   143                           to be a single argument. *)
   144                        Posix.Process.exec("/bin/sh", ["sh", "-c", cmd_args])
   145 			(*Posix.Process.exec(newcmd, args)*)
   146 		      end
   147 		(* end case *))
   148           val _ = TextIO.flushOut TextIO.stdOut
   149           val pid = (startChild ()) handle ex => (closep(); raise ex)
   150 	  val instr = openInFD ("_exec_in", #infd p2)
   151           val outstr = openOutFD ("_exec_out", #outfd p1)
   152           val cmd = hd (rev argv)
   153           in
   154               (* close the child-side fds *)
   155             Posix.IO.close (#outfd p2);
   156             Posix.IO.close (#infd p1);
   157               (* set the fds close on exec *)
   158             Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   159             Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   160             (((CMDPROC{
   161               prover = prover,
   162               cmd = cmd,
   163               thmstring = thmstring,
   164               goalstring = goalstring,
   165               pid = pid,
   166               instr = instr,
   167               outstr = outstr
   168             })::procList))
   169           end;
   170 
   171 
   172 fun myexecuteInEnv (cmd, argv, env) = let
   173           val p1 = Posix.IO.pipe ()
   174           val p2 = Posix.IO.pipe ()
   175           fun closep () = (
   176                 Posix.IO.close (#outfd p1); 
   177                 Posix.IO.close (#infd p1);
   178                 Posix.IO.close (#outfd p2); 
   179                 Posix.IO.close (#infd p2)
   180               )
   181           fun startChild () =(case  Posix.Process.fork()
   182                  of SOME pid =>  pid           (* parent *)
   183                   | NONE => let
   184                       val oldchildin = #infd p1
   185                       val newchildin = Posix.FileSys.wordToFD 0w0
   186                       val oldchildout = #outfd p2
   187                       val newchildout = Posix.FileSys.wordToFD 0w1
   188                       in
   189                         Posix.IO.close (#outfd p1);
   190                         Posix.IO.close (#infd p2);
   191                         Posix.IO.dup2{old = oldchildin, new = newchildin};
   192                         Posix.IO.close oldchildin;
   193                         Posix.IO.dup2{old = oldchildout, new = newchildout};
   194                         Posix.IO.close oldchildout;
   195                         Posix.Process.exece(cmd, argv, env)
   196                       end
   197                 (* end case *))
   198           val _ = TextIO.flushOut TextIO.stdOut
   199           val pid = (startChild ()) handle ex => (closep(); raise ex)
   200           val instr = openInFD ("_exec_in", #infd p2)
   201           val outstr = openOutFD ("_exec_out", #outfd p1)
   202           in
   203               (* close the child-side fds *)
   204             Posix.IO.close (#outfd p2);
   205             Posix.IO.close (#infd p1);
   206               (* set the fds close on exec *)
   207             Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   208             Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   209             PROC{pid = pid,
   210               instr = instr,
   211               outstr = outstr
   212             }
   213           end;
   214 
   215 
   216 
   217 
   218 fun myexecuteToList (cmd, argv, procList) = let
   219           val p1 = Posix.IO.pipe ()
   220           val p2 = Posix.IO.pipe ()
   221           val prover = hd argv
   222           val thmstring = hd(tl argv)
   223           val goalstring = hd(tl(tl argv))
   224           val argv = tl (tl (tl(argv)))
   225           
   226 	  fun closep () = (
   227                 Posix.IO.close (#outfd p1); 
   228                 Posix.IO.close (#infd p1);
   229                 Posix.IO.close (#outfd p2); 
   230                 Posix.IO.close (#infd p2)
   231               )
   232           fun startChild () =(case  Posix.Process.fork()
   233 		 of SOME pid =>  pid           (* parent *)
   234                   | NONE => let
   235 		      val oldchildin = #infd p1
   236 		      val newchildin = Posix.FileSys.wordToFD 0w0
   237 		      val oldchildout = #outfd p2
   238 		      val newchildout = Posix.FileSys.wordToFD 0w1
   239                       in
   240 			Posix.IO.close (#outfd p1);
   241 			Posix.IO.close (#infd p2);
   242 			Posix.IO.dup2{old = oldchildin, new = newchildin};
   243                         Posix.IO.close oldchildin;
   244 			Posix.IO.dup2{old = oldchildout, new = newchildout};
   245                         Posix.IO.close oldchildout;
   246 			Posix.Process.exec(cmd, argv)
   247 		      end
   248 		(* end case *))
   249           val _ = TextIO.flushOut TextIO.stdOut
   250           val pid = (startChild ()) handle ex => (closep(); raise ex)
   251 	  val instr = openInFD ("_exec_in", #infd p2)
   252           val outstr = openOutFD ("_exec_out", #outfd p1)
   253           val cmd = hd (rev argv)
   254           in
   255               (* close the child-side fds *)
   256             Posix.IO.close (#outfd p2);
   257             Posix.IO.close (#infd p1);
   258               (* set the fds close on exec *)
   259             Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   260             Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   261             (((CMDPROC{
   262               prover = prover,
   263               cmd = cmd,
   264               thmstring = thmstring,
   265               goalstring = goalstring,
   266               pid = pid,
   267               instr = instr,
   268               outstr = outstr
   269             })::procList))
   270           end;