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