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