--- a/src/HOL/Tools/ATP/modUnix.ML Thu May 26 10:05:28 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,280 +0,0 @@
-(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-(****************************************************************)
-(****** Slightly modified version of sml Unix structure *********)
-(****************************************************************)
-
-
-structure modUnix: MODUNIX =
- struct
-
-type signal = Posix.Signal.signal
-datatype exit_status = datatype Posix.Process.exit_status
-
-val fromStatus = Posix.Process.fromStatus
-
-
-fun reap(pid, instr, outstr) =
- let
- val u = TextIO.closeIn instr;
- val u = TextIO.closeOut outstr;
-
- val (_, status) =
- Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
- in
- status
- end
-
-fun fdReader (name : string, fd : Posix.IO.file_desc) =
- Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
-
-fun fdWriter (name, fd) =
- Posix.IO.mkTextWriter {
- appendMode = false,
- initBlkMode = true,
- name = name,
- chunkSize=4096,
- fd = fd
- };
-
-fun openOutFD (name, fd) =
- TextIO.mkOutstream (
- TextIO.StreamIO.mkOutstream (
- fdWriter (name, fd), IO.BLOCK_BUF));
-
-fun openInFD (name, fd) =
- TextIO.mkInstream (
- TextIO.StreamIO.mkInstream (
- fdReader (name, fd), ""));
-
-
-
-
-
-(*****************************************)
-(* The result of calling createWatcher *)
-(*****************************************)
-
-datatype proc = PROC of {
- pid : Posix.Process.pid,
- instr : TextIO.instream,
- outstr : TextIO.outstream
- };
-
-
-
-(*****************************************)
-(* The result of calling executeToList *)
-(*****************************************)
-
-datatype cmdproc = CMDPROC of {
- prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *)
- cmd: string, (* The file containing the goal for res prover to prove *)
- thmstring: string, (* string representation of subgoal after negation, skolemization*)
- goalstring: string, (* string representation of subgoal*)
- pid : Posix.Process.pid,
- instr : TextIO.instream, (* Input stream to child process *)
- outstr : TextIO.outstream (* Output stream from child process *)
- };
-
-
-
-fun killChild pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
-
-fun childInfo (PROC{pid,instr,outstr}) = ((pid, (instr,outstr)));
-
-fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
-
-fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
-
-fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover,(cmd,(pid, (instr,outstr))));
-
-fun cmdchildPid (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (pid);
-
-fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover);
-
-fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (thmstring);
-
-fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (goalstring);
-(***************************************************************************)
-(* Takes a command - e.g. 'vampire', a list of arguments for the command, *)
-(* and a list of currently running processes. Creates a new process for *)
-(* cmd and argv and adds it to procList *)
-(***************************************************************************)
-
-
-
-
-fun mySshExecuteToList (cmd, argv, procList) = let
- val p1 = Posix.IO.pipe ()
- val p2 = Posix.IO.pipe ()
- val prover = hd argv
- val thmstring = hd(tl argv)
- val goalstring = hd(tl(tl argv))
- val argv = tl (tl argv)
-
- (* Turn the arguments into a single string. Perhaps we should quote the
- arguments. *)
- fun convArgs [] = []
- | convArgs [s] = [s]
- | convArgs (hd::tl) = hd :: " " :: convArgs tl
- val cmd_args = concat(convArgs(cmd :: argv))
-
- fun closep () = (
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p1);
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p2)
- )
- fun startChild () =(case Posix.Process.fork()
- of SOME pid => pid (* parent *)
- | NONE => let
- val oldchildin = #infd p1
- val newchildin = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val newchildout = Posix.FileSys.wordToFD 0w1
- (*val args = (["shep"]@([cmd]@argv))
- val newcmd = "/usr/bin/ssh"*)
-
- in
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = newchildin};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = newchildout};
- Posix.IO.close oldchildout;
- (* Run the command. *)
- (* Run this as a shell command. The command and arguments have
- to be a single argument. *)
- Posix.Process.exec("/bin/sh", ["sh", "-c", cmd_args])
- (*Posix.Process.exec(newcmd, args)*)
- end
- (* end case *))
- val _ = TextIO.flushOut TextIO.stdOut
- val pid = (startChild ()) handle ex => (closep(); raise ex)
- val instr = openInFD ("_exec_in", #infd p2)
- val outstr = openOutFD ("_exec_out", #outfd p1)
- val cmd = hd (rev argv)
- in
- (* close the child-side fds *)
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p1);
- (* set the fds close on exec *)
- Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- (((CMDPROC{
- prover = prover,
- cmd = cmd,
- thmstring = thmstring,
- goalstring = goalstring,
- pid = pid,
- instr = instr,
- outstr = outstr
- })::procList))
- end;
-
-
-fun myexecuteInEnv (cmd, argv, env) = let
- val p1 = Posix.IO.pipe ()
- val p2 = Posix.IO.pipe ()
- fun closep () = (
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p1);
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p2)
- )
- fun startChild () =(case Posix.Process.fork()
- of SOME pid => pid (* parent *)
- | NONE => let
- val oldchildin = #infd p1
- val newchildin = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val newchildout = Posix.FileSys.wordToFD 0w1
- in
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = newchildin};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = newchildout};
- Posix.IO.close oldchildout;
- Posix.Process.exece(cmd, argv, env)
- end
- (* end case *))
- val _ = TextIO.flushOut TextIO.stdOut
- val pid = (startChild ()) handle ex => (closep(); raise ex)
- val instr = openInFD ("_exec_in", #infd p2)
- val outstr = openOutFD ("_exec_out", #outfd p1)
- in
- (* close the child-side fds *)
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p1);
- (* set the fds close on exec *)
- Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- PROC{pid = pid,
- instr = instr,
- outstr = outstr
- }
- end;
-
-
-
-
-fun myexecuteToList (cmd, argv, procList) = let
- val p1 = Posix.IO.pipe ()
- val p2 = Posix.IO.pipe ()
- val prover = hd argv
- val thmstring = hd(tl argv)
- val goalstring = hd(tl(tl argv))
- val argv = tl (tl (tl(argv)))
-
- fun closep () = (
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p1);
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p2)
- )
- fun startChild () =(case Posix.Process.fork()
- of SOME pid => pid (* parent *)
- | NONE => let
- val oldchildin = #infd p1
- val newchildin = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val newchildout = Posix.FileSys.wordToFD 0w1
- in
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = newchildin};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = newchildout};
- Posix.IO.close oldchildout;
- Posix.Process.exec(cmd, argv)
- end
- (* end case *))
- val _ = TextIO.flushOut TextIO.stdOut
- val pid = (startChild ()) handle ex => (closep(); raise ex)
- val instr = openInFD ("_exec_in", #infd p2)
- val outstr = openOutFD ("_exec_out", #outfd p1)
- val cmd = hd (rev argv)
- in
- (* close the child-side fds *)
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p1);
- (* set the fds close on exec *)
- Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- (((CMDPROC{
- prover = prover,
- cmd = cmd,
- thmstring = thmstring,
- goalstring = goalstring,
- pid = pid,
- instr = instr,
- outstr = outstr
- })::procList))
- end;
-
-end;