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