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