src/Tools/WWW_Find/socket_util.ML
author blanchet
Mon, 26 Nov 2012 13:35:05 +0100
changeset 50222 40e3c3be6bca
parent 45066 11f622794ad6
child 51930 52fd62618631
permissions -rw-r--r--
added file headers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45066
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/WWW_Find/socket_util.ML
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     2
    Author:     Timothy Bourke, NICTA
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     3
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     4
Routines for working with sockets.  Following example 10.2 in "The
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     5
Standard-ML Basis Library" by Emden R. Gansner and John H. Reppy.
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     6
*)
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     7
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     8
signature SOCKET_UTIL =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
     9
sig
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    10
  val init_server_socket: string option -> int -> Socket.passive INetSock.stream_sock
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    11
  val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    12
end;
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    13
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    14
structure Socket_Util: SOCKET_UTIL =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    15
struct
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    16
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    17
fun init_server_socket opt_host port =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    18
  let
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    19
    val sock = INetSock.TCP.socket ();
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    20
    val addr =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    21
      (case opt_host of
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    22
         NONE => INetSock.any port
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    23
       | SOME host =>
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    24
           NetHostDB.getByName host
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    25
           |> the
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    26
           |> NetHostDB.addr
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    27
           |> rpair port
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    28
           |> INetSock.toAddr
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    29
           handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    30
    val _ = Socket.bind (sock, addr);
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    31
    val _ = Socket.listen (sock, 5);
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    32
  in sock end;
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    33
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    34
fun make_streams sock =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    35
  let
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    36
    val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    37
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    38
    val sock_name =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    39
      implode [ NetHostDB.toString haddr, ":", string_of_int port ];
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    40
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    41
    val rd =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    42
      BinPrimIO.RD {
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    43
        name = sock_name,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    44
        chunkSize = Socket.Ctl.getRCVBUF sock,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    45
        readVec = SOME (fn sz => Socket.recvVec (sock, sz)),
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    46
        readArr = SOME (fn buffer => Socket.recvArr (sock, buffer)),
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    47
        readVecNB = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    48
        readArrNB = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    49
        block = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    50
        canInput = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    51
        avail = fn () => NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    52
        getPos = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    53
        setPos = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    54
        endPos = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    55
        verifyPos = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    56
        close = fn () => Socket.close sock,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    57
        ioDesc = NONE
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    58
      };
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    59
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    60
    val wr =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    61
      BinPrimIO.WR {
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    62
        name = sock_name,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    63
        chunkSize = Socket.Ctl.getSNDBUF sock,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    64
        writeVec = SOME (fn buffer => Socket.sendVec (sock, buffer)),
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    65
        writeArr = SOME (fn buffer => Socket.sendArr (sock, buffer)),
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    66
        writeVecNB = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    67
        writeArrNB = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    68
        block = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    69
        canOutput = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    70
        getPos = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    71
        setPos = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    72
        endPos = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    73
        verifyPos = NONE,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    74
        close = fn () => Socket.close sock,
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    75
        ioDesc = NONE
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    76
      };
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    77
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    78
    val in_strm =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    79
      BinIO.mkInstream (
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    80
        BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    81
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    82
    val out_strm =
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    83
      BinIO.mkOutstream (
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    84
        BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    85
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    86
    in (in_strm, out_strm) end;
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    87
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    88
end;
11f622794ad6 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
wenzelm
parents:
diff changeset
    89