src/Pure/General/socket_io.ML
author wenzelm
Wed, 21 Sep 2011 22:18:17 +0200
changeset 45028 d608dd8cd409
parent 45026 5c0b0d67f9b1
permissions -rw-r--r--
alternative Socket_Channel; use BinIO for fifos uniformly;
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
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    12
  val open_streams: string -> BinIO.instream * BinIO.outstream
45026
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
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    71
fun open_streams socket_name =
45026
5c0b0d67f9b1 slightly more general Socket_IO as part of Pure;
wenzelm
parents:
diff changeset
    72
  let
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    73
    fun err () = error ("Bad socket name: " ^ quote socket_name);
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    74
    val (host, port) =
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    75
      (case space_explode ":" socket_name of
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    76
        [h, p] =>
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    77
         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    78
          case Int.fromString p of SOME port => port | NONE => err ())
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    79
      | _ => err ());
45026
5c0b0d67f9b1 slightly more general Socket_IO as part of Pure;
wenzelm
parents:
diff changeset
    80
    val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45026
diff changeset
    81
    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
45026
5c0b0d67f9b1 slightly more general Socket_IO as part of Pure;
wenzelm
parents:
diff changeset
    82
  in make_streams socket end;
5c0b0d67f9b1 slightly more general Socket_IO as part of Pure;
wenzelm
parents:
diff changeset
    83
5c0b0d67f9b1 slightly more general Socket_IO as part of Pure;
wenzelm
parents:
diff changeset
    84
end;
5c0b0d67f9b1 slightly more general Socket_IO as part of Pure;
wenzelm
parents:
diff changeset
    85