recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
authorwenzelm
Thu Jan 10 12:41:53 2013 +0100 (2013-01-10)
changeset 50800c0fb2839d1a9
parent 50799 5a2f5834ccb4
child 50801 b8ff6d1ee56c
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
src/Pure/General/socket_io.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/system_channel.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/socket_io.ML	Thu Jan 10 12:41:53 2013 +0100
     1.3 @@ -0,0 +1,87 @@
     1.4 +(*  Title:      Pure/General/socket_io.ML
     1.5 +    Author:     Timothy Bourke, NICTA
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Stream IO over TCP sockets.  Following example 10.2 in "The Standard
     1.9 +ML Basis Library" by Emden R. Gansner and John H. Reppy.
    1.10 +
    1.11 +Note: BinIO requires Poly/ML 5.5.x to work reliably.
    1.12 +*)
    1.13 +
    1.14 +signature SOCKET_IO =
    1.15 +sig
    1.16 +  val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
    1.17 +  val open_streams: string -> BinIO.instream * BinIO.outstream
    1.18 +end;
    1.19 +
    1.20 +structure Socket_IO: SOCKET_IO =
    1.21 +struct
    1.22 +
    1.23 +fun make_streams socket =
    1.24 +  let
    1.25 +    val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
    1.26 +    val name = NetHostDB.toString host ^ ":" ^ string_of_int port;
    1.27 +
    1.28 +    val rd =
    1.29 +      BinPrimIO.RD {
    1.30 +        name = name,
    1.31 +        chunkSize = Socket.Ctl.getRCVBUF socket,
    1.32 +        readVec = SOME (fn n => Socket.recvVec (socket, n)),
    1.33 +        readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
    1.34 +        readVecNB = NONE,
    1.35 +        readArrNB = NONE,
    1.36 +        block = NONE,
    1.37 +        canInput = NONE,
    1.38 +        avail = fn () => NONE,
    1.39 +        getPos = NONE,
    1.40 +        setPos = NONE,
    1.41 +        endPos = NONE,
    1.42 +        verifyPos = NONE,
    1.43 +        close = fn () => Socket.close socket,
    1.44 +        ioDesc = NONE
    1.45 +      };
    1.46 +
    1.47 +    val wr =
    1.48 +      BinPrimIO.WR {
    1.49 +        name = name,
    1.50 +        chunkSize = Socket.Ctl.getSNDBUF socket,
    1.51 +        writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
    1.52 +        writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
    1.53 +        writeVecNB = NONE,
    1.54 +        writeArrNB = NONE,
    1.55 +        block = NONE,
    1.56 +        canOutput = NONE,
    1.57 +        getPos = NONE,
    1.58 +        setPos = NONE,
    1.59 +        endPos = NONE,
    1.60 +        verifyPos = NONE,
    1.61 +        close = fn () => Socket.close socket,
    1.62 +        ioDesc = NONE
    1.63 +      };
    1.64 +
    1.65 +    val in_stream =
    1.66 +      BinIO.mkInstream
    1.67 +        (BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
    1.68 +
    1.69 +    val out_stream =
    1.70 +      BinIO.mkOutstream
    1.71 +        (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
    1.72 +
    1.73 +  in (in_stream, out_stream) end;
    1.74 +
    1.75 +
    1.76 +fun open_streams socket_name =
    1.77 +  let
    1.78 +    fun err () = error ("Bad socket name: " ^ quote socket_name);
    1.79 +    val (host, port) =
    1.80 +      (case space_explode ":" socket_name of
    1.81 +        [h, p] =>
    1.82 +         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
    1.83 +          case Int.fromString p of SOME port => port | NONE => err ())
    1.84 +      | _ => err ());
    1.85 +    val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
    1.86 +    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
    1.87 +  in make_streams socket end;
    1.88 +
    1.89 +end;
    1.90 +
     2.1 --- a/src/Pure/ROOT	Wed Jan 09 22:38:21 2013 +0100
     2.2 +++ b/src/Pure/ROOT	Thu Jan 10 12:41:53 2013 +0100
     2.3 @@ -87,6 +87,7 @@
     2.4      "General/seq.ML"
     2.5      "General/sha1.ML"
     2.6      "General/sha1_polyml.ML"
     2.7 +    "General/socket_io.ML"
     2.8      "General/source.ML"
     2.9      "General/stack.ML"
    2.10      "General/symbol.ML"
     3.1 --- a/src/Pure/ROOT.ML	Wed Jan 09 22:38:21 2013 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Thu Jan 10 12:41:53 2013 +0100
     3.3 @@ -57,6 +57,7 @@
     3.4  use "General/file.ML";
     3.5  use "General/long_name.ML";
     3.6  use "General/binding.ML";
     3.7 +use "General/socket_io.ML";
     3.8  
     3.9  use "General/sha1.ML";
    3.10  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
     4.1 --- a/src/Pure/System/system_channel.ML	Wed Jan 09 22:38:21 2013 +0100
     4.2 +++ b/src/Pure/System/system_channel.ML	Thu Jan 10 12:41:53 2013 +0100
     4.3 @@ -47,65 +47,31 @@
     4.4    end;
     4.5  
     4.6  
     4.7 -(* sockets *)  (* FIXME proper buffering via BinIO (after Poly/ML 5.4.1) *)
     4.8 +(* sockets *)
     4.9  
    4.10 -local
    4.11 -
    4.12 -fun readN socket n =
    4.13 +fun read_line in_stream =
    4.14    let
    4.15 -    fun read i buf =
    4.16 -      let
    4.17 -        val s = Byte.bytesToString (Socket.recvVec (socket, n - i));
    4.18 -        val m = size s;
    4.19 -        val i' = i + m;
    4.20 -        val buf' = Buffer.add s buf;
    4.21 -      in if m > 0 andalso n > i' then read i' buf' else Buffer.content buf' end;
    4.22 -  in read 0 Buffer.empty end;
    4.23 -
    4.24 -fun read_line socket =
    4.25 -  let
    4.26 -    fun result cs = implode (rev ("\n" :: cs));
    4.27 +    fun result cs = String.implode (rev (#"\n" :: cs));
    4.28      fun read cs =
    4.29 -      (case readN socket 1 of
    4.30 -        "" => if null cs then NONE else SOME (result cs)
    4.31 -      | "\n" => SOME (result cs)
    4.32 -      | c => read (c :: cs));
    4.33 +      (case BinIO.input1 in_stream of
    4.34 +        NONE => if null cs then NONE else SOME (result cs)
    4.35 +      | SOME b =>
    4.36 +          (case Byte.byteToChar b of
    4.37 +            #"\n" => SOME (result cs)
    4.38 +          | c => read (c :: cs)));
    4.39    in read [] end;
    4.40  
    4.41 -fun write socket =
    4.42 -  let
    4.43 -    fun send buf =
    4.44 -      if Word8VectorSlice.isEmpty buf then ()
    4.45 -      else
    4.46 -        let
    4.47 -          val n = Int.min (Word8VectorSlice.length buf, 4096);
    4.48 -          val m = Socket.sendVec (socket, Word8VectorSlice.subslice (buf, 0, SOME n));
    4.49 -          val buf' = Word8VectorSlice.subslice (buf, m, NONE);
    4.50 -        in send buf' end;
    4.51 -  in fn s => send (Word8VectorSlice.full (Byte.stringToBytes s)) end;
    4.52 -
    4.53 -in
    4.54 -
    4.55  fun socket_rendezvous name =
    4.56    let
    4.57 -    fun err () = error ("Bad socket name: " ^ quote name);
    4.58 -    val (host, port) =
    4.59 -      (case space_explode ":" name of
    4.60 -        [h, p] =>
    4.61 -         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
    4.62 -          case Int.fromString p of SOME port => port | NONE => err ())
    4.63 -      | _ => err ());
    4.64 -    val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
    4.65 -    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
    4.66 +    val (in_stream, out_stream) = Socket_IO.open_streams name;
    4.67 +    val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
    4.68    in
    4.69      System_Channel
    4.70 -     {input_line = fn () => read_line socket,
    4.71 -      inputN = fn n => readN socket n,
    4.72 -      output = fn s => write socket s,
    4.73 -      flush = fn () => ()}
    4.74 +     {input_line = fn () => read_line in_stream,
    4.75 +      inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)),
    4.76 +      output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
    4.77 +      flush = fn () => BinIO.flushOut out_stream}
    4.78    end;
    4.79  
    4.80  end;
    4.81  
    4.82 -end;
    4.83 -