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