author | wenzelm |
Thu, 26 Jul 2012 19:41:05 +0200 | |
changeset 48527 | 4ee8d70cd5a3 |
parent 45158 | db4bf4fb5492 |
child 50800 | c0fb2839d1a9 |
permissions | -rw-r--r-- |
45029 | 1 |
(* Title: Pure/System/system_channel.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Portable system channel for inter-process communication, based on |
|
5 |
named pipes or sockets. |
|
6 |
*) |
|
7 |
||
8 |
signature SYSTEM_CHANNEL = |
|
9 |
sig |
|
10 |
type T |
|
11 |
val input_line: T -> string option |
|
12 |
val inputN: T -> int -> string |
|
13 |
val output: T -> string -> unit |
|
14 |
val flush: T -> unit |
|
15 |
val fifo_rendezvous: string -> string -> T |
|
16 |
val socket_rendezvous: string -> T |
|
17 |
end; |
|
18 |
||
19 |
structure System_Channel: SYSTEM_CHANNEL = |
|
20 |
struct |
|
21 |
||
22 |
datatype T = System_Channel of |
|
23 |
{input_line: unit -> string option, |
|
24 |
inputN: int -> string, |
|
25 |
output: string -> unit, |
|
26 |
flush: unit -> unit}; |
|
27 |
||
28 |
fun input_line (System_Channel {input_line = f, ...}) = f (); |
|
29 |
fun inputN (System_Channel {inputN = f, ...}) n = f n; |
|
30 |
fun output (System_Channel {output = f, ...}) s = f s; |
|
31 |
fun flush (System_Channel {flush = f, ...}) = f (); |
|
32 |
||
33 |
||
34 |
(* named pipes *) |
|
35 |
||
36 |
fun fifo_rendezvous fifo1 fifo2 = |
|
37 |
let |
|
38 |
val in_stream = TextIO.openIn fifo1; |
|
39 |
val out_stream = TextIO.openOut fifo2; |
|
40 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream out_stream, IO.BLOCK_BUF); |
|
41 |
in |
|
42 |
System_Channel |
|
43 |
{input_line = fn () => TextIO.inputLine in_stream, |
|
44 |
inputN = fn n => TextIO.inputN (in_stream, n), |
|
45 |
output = fn s => TextIO.output (out_stream, s), |
|
46 |
flush = fn () => TextIO.flushOut out_stream} |
|
47 |
end; |
|
48 |
||
49 |
||
45158 | 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 | 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 | 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 | 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 | 73 |
in read [] end; |
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 | 89 |
fun socket_rendezvous name = |
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 | 100 |
in |
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 | 106 |
end; |
107 |
||
108 |
end; |
|
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 |