src/Pure/System/system_channel.ML
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 45158 db4bf4fb5492
child 50800 c0fb2839d1a9
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45029
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/System/system_channel.ML
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     3
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     4
Portable system channel for inter-process communication, based on
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     5
named pipes or sockets.
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     6
*)
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     7
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     8
signature SYSTEM_CHANNEL =
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
     9
sig
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    10
  type T
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    11
  val input_line: T -> string option
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    12
  val inputN: T -> int -> string
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    13
  val output: T -> string -> unit
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    14
  val flush: T -> unit
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    15
  val fifo_rendezvous: string -> string -> T
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    16
  val socket_rendezvous: string -> T
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    17
end;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    18
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    19
structure System_Channel: SYSTEM_CHANNEL =
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    20
struct
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    21
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    22
datatype T = System_Channel of
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    23
 {input_line: unit -> string option,
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    24
  inputN: int -> string,
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    25
  output: string -> unit,
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    26
  flush: unit -> unit};
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    27
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    28
fun input_line (System_Channel {input_line = f, ...}) = f ();
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    29
fun inputN (System_Channel {inputN = f, ...}) n = f n;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    30
fun output (System_Channel {output = f, ...}) s = f s;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    31
fun flush (System_Channel {flush = f, ...}) = f ();
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    32
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    33
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    34
(* named pipes *)
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    35
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    36
fun fifo_rendezvous fifo1 fifo2 =
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    37
  let
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    38
    val in_stream = TextIO.openIn fifo1;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    39
    val out_stream = TextIO.openOut fifo2;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    40
    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream out_stream, IO.BLOCK_BUF);
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    41
  in
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    42
    System_Channel
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    43
     {input_line = fn () => TextIO.inputLine in_stream,
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    44
      inputN = fn n => TextIO.inputN (in_stream, n),
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    45
      output = fn s => TextIO.output (out_stream, s),
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    46
      flush = fn () => TextIO.flushOut out_stream}
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    47
  end;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    48
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    49
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45058
diff changeset
    50
(* sockets *)  (* FIXME proper buffering via BinIO (after Poly/ML 5.4.1) *)
45058
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    51
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    52
local
45029
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    53
45058
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    54
fun readN socket n =
45029
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    55
  let
45058
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    56
    fun read i buf =
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    57
      let
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    58
        val s = Byte.bytesToString (Socket.recvVec (socket, n - i));
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    59
        val m = size s;
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    60
        val i' = i + m;
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    61
        val buf' = Buffer.add s buf;
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    62
      in if m > 0 andalso n > i' then read i' buf' else Buffer.content buf' end;
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    63
  in read 0 Buffer.empty end;
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    64
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    65
fun read_line socket =
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    66
  let
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    67
    fun result cs = implode (rev ("\n" :: cs));
45029
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    68
    fun read cs =
45058
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    69
      (case readN socket 1 of
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    70
        "" => if null cs then NONE else SOME (result cs)
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    71
      | "\n" => SOME (result cs)
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    72
      | c => read (c :: cs));
45029
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    73
  in read [] end;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    74
45058
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    75
fun write socket =
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    76
  let
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    77
    fun send buf =
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    78
      if Word8VectorSlice.isEmpty buf then ()
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    79
      else
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    80
        let
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    81
          val n = Int.min (Word8VectorSlice.length buf, 4096);
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    82
          val m = Socket.sendVec (socket, Word8VectorSlice.subslice (buf, 0, SOME n));
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    83
          val buf' = Word8VectorSlice.subslice (buf, m, NONE);
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    84
        in send buf' end;
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    85
  in fn s => send (Word8VectorSlice.full (Byte.stringToBytes s)) end;
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    86
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    87
in
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    88
45029
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    89
fun socket_rendezvous name =
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
    90
  let
45058
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    91
    fun err () = error ("Bad socket name: " ^ quote name);
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    92
    val (host, port) =
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    93
      (case space_explode ":" name of
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    94
        [h, p] =>
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    95
         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    96
          case Int.fromString p of SOME port => port | NONE => err ())
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    97
      | _ => err ());
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    98
    val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
    99
    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
45029
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
   100
  in
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
   101
    System_Channel
45058
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
   102
     {input_line = fn () => read_line socket,
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
   103
      inputN = fn n => readN socket n,
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
   104
      output = fn s => write socket s,
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
   105
      flush = fn () => ()}
45029
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
   106
  end;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
   107
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
   108
end;
63144ea111f7 abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
diff changeset
   109
45058
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
   110
end;
8b20be429cf3 raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents: 45029
diff changeset
   111