src/Pure/General/socket_io.ML
author wenzelm
Wed Sep 21 22:18:17 2011 +0200 (2011-09-21)
changeset 45028 d608dd8cd409
parent 45026 5c0b0d67f9b1
permissions -rw-r--r--
alternative Socket_Channel;
use BinIO for fifos uniformly;
     1 (*  Title:      Pure/General/socket_io.ML
     2     Author:     Timothy Bourke, NICTA
     3     Author:     Makarius
     4 
     5 Stream IO over TCP sockets.  Following example 10.2 in "The Standard
     6 ML Basis Library" by Emden R. Gansner and John H. Reppy.
     7 *)
     8 
     9 signature SOCKET_IO =
    10 sig
    11   val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
    12   val open_streams: string -> BinIO.instream * BinIO.outstream
    13 end;
    14 
    15 structure Socket_IO: SOCKET_IO =
    16 struct
    17 
    18 fun make_streams socket =
    19   let
    20     val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
    21     val name = NetHostDB.toString host ^ ":" ^ string_of_int port;
    22 
    23     val rd =
    24       BinPrimIO.RD {
    25         name = name,
    26         chunkSize = Socket.Ctl.getRCVBUF socket,
    27         readVec = SOME (fn n => Socket.recvVec (socket, n)),
    28         readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
    29         readVecNB = NONE,
    30         readArrNB = NONE,
    31         block = NONE,
    32         canInput = NONE,
    33         avail = fn () => NONE,
    34         getPos = NONE,
    35         setPos = NONE,
    36         endPos = NONE,
    37         verifyPos = NONE,
    38         close = fn () => Socket.close socket,
    39         ioDesc = NONE
    40       };
    41 
    42     val wr =
    43       BinPrimIO.WR {
    44         name = name,
    45         chunkSize = Socket.Ctl.getSNDBUF socket,
    46         writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
    47         writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
    48         writeVecNB = NONE,
    49         writeArrNB = NONE,
    50         block = NONE,
    51         canOutput = NONE,
    52         getPos = NONE,
    53         setPos = NONE,
    54         endPos = NONE,
    55         verifyPos = NONE,
    56         close = fn () => Socket.close socket,
    57         ioDesc = NONE
    58       };
    59 
    60     val in_stream =
    61       BinIO.mkInstream
    62         (BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
    63 
    64     val out_stream =
    65       BinIO.mkOutstream
    66         (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
    67 
    68   in (in_stream, out_stream) end;
    69 
    70 
    71 fun open_streams socket_name =
    72   let
    73     fun err () = error ("Bad socket name: " ^ quote socket_name);
    74     val (host, port) =
    75       (case space_explode ":" socket_name of
    76         [h, p] =>
    77          (case NetHostDB.getByName h of SOME host => host | NONE => err (),
    78           case Int.fromString p of SOME port => port | NONE => err ())
    79       | _ => err ());
    80     val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
    81     val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
    82   in make_streams socket end;
    83 
    84 end;
    85