1(*  Title:      Pure/General/byte_message.ML
2    Author:     Makarius
3
4Byte-oriented messages.
5*)
6
7signature BYTE_MESSAGE =
8sig
9  val write: BinIO.outstream -> string list -> unit
10  val flush: BinIO.outstream -> unit
11  val write_line: BinIO.outstream -> string -> unit
12  val read: BinIO.instream -> int -> string
13  val read_block: BinIO.instream -> int -> string option * int
14  val read_line: BinIO.instream -> string option
15  val write_message: BinIO.outstream -> string list -> unit
16  val read_message: BinIO.instream -> string list option
17  val write_line_message: BinIO.outstream -> string -> unit
18  val read_line_message: BinIO.instream -> string option
19end;
20
21structure Byte_Message: BYTE_MESSAGE =
22struct
23
24(* output operations *)
25
26fun write stream = List.app (File.output stream);
27
28fun flush stream = ignore (try BinIO.flushOut stream);
29
30fun write_line stream s = (write stream [s, "\n"]; flush stream);
31
32
33(* input operations *)
34
35fun read stream n = Byte.bytesToString (BinIO.inputN (stream, n));
36
37fun read_block stream n =
38  let
39    val msg = read stream n;
40    val len = size msg;
41  in (if len = n then SOME msg else NONE, len) end;
42
43fun read_line stream =
44  let
45    val result = trim_line o String.implode o rev;
46    fun read_body cs =
47      (case BinIO.input1 stream of
48        NONE => if null cs then NONE else SOME (result cs)
49      | SOME b =>
50          (case Byte.byteToChar b of
51            #"\n" => SOME (result cs)
52          | c => read_body (c :: cs)));
53  in read_body [] end;
54
55
56(* messages with multiple chunks (arbitrary content) *)
57
58fun make_header ns =
59  [space_implode "," (map Value.print_int ns), "\n"];
60
61fun write_message stream chunks =
62  (write stream (make_header (map size chunks) @ chunks); flush stream);
63
64fun parse_header line =
65  map Value.parse_nat (space_explode "," line)
66    handle Fail _ => error ("Malformed message header: " ^ quote line);
67
68fun read_chunk stream n =
69  (case read_block stream n of
70    (SOME chunk, _) => chunk
71  | (NONE, len) =>
72      error ("Malformed message chunk: unexpected EOF after " ^
73        string_of_int len ^ " of " ^ string_of_int n ^ " bytes"));
74
75fun read_message stream =
76  read_line stream |> Option.map (parse_header #> map (read_chunk stream));
77
78
79(* hybrid messages: line or length+block (with content restriction) *)
80
81fun is_length msg =
82  msg <> "" andalso forall_string Symbol.is_ascii_digit msg;
83
84fun is_terminated msg =
85  let val len = size msg
86  in len > 0 andalso Symbol.is_ascii_line_terminator (str (String.sub (msg, len - 1))) end;
87
88fun write_line_message stream msg =
89  if is_length msg orelse is_terminated msg then
90    error ("Bad content for line message:\n" ^ implode (take 100 (Symbol.explode msg)))
91  else
92    let val n = size msg in
93      write stream
94        ((if n > 100 orelse exists_string (fn s => s = "\n") msg
95          then make_header [n + 1] else []) @ [msg, "\n"]);
96      flush stream
97    end;
98
99fun read_line_message stream =
100  (case read_line stream of
101    NONE => NONE
102  | SOME line =>
103      (case try Value.parse_nat line of
104        NONE => SOME line
105      | SOME n => Option.map trim_line (#1 (read_block stream n))));
106
107end;
108