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