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