src/Pure/Concurrent/mailbox.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 57417 29fe9bac501b
permissions -rw-r--r--
prefer infix operations;
wenzelm@28135
     1
(*  Title:      Pure/Concurrent/mailbox.ML
wenzelm@28140
     2
    Author:     Makarius
wenzelm@28135
     3
wenzelm@57417
     4
Message exchange via mailbox, with multiple senders (non-blocking,
wenzelm@57417
     5
unbounded buffering) and single receiver (bulk messages).
wenzelm@28135
     6
*)
wenzelm@28135
     7
wenzelm@28135
     8
signature MAILBOX =
wenzelm@28135
     9
sig
wenzelm@28135
    10
  type 'a T
wenzelm@28135
    11
  val create: unit -> 'a T
wenzelm@28170
    12
  val send: 'a T -> 'a -> unit
wenzelm@57417
    13
  val receive: Time.time option -> 'a T -> 'a list
wenzelm@52583
    14
  val await_empty: 'a T -> unit
wenzelm@28135
    15
end;
wenzelm@28135
    16
wenzelm@28135
    17
structure Mailbox: MAILBOX =
wenzelm@28135
    18
struct
wenzelm@28135
    19
wenzelm@57417
    20
datatype 'a T = Mailbox of 'a list Synchronized.var;
wenzelm@28579
    21
wenzelm@57417
    22
fun create () = Mailbox (Synchronized.var "mailbox" []);
wenzelm@28135
    23
wenzelm@57417
    24
fun send (Mailbox mailbox) msg = Synchronized.change mailbox (cons msg);
wenzelm@28139
    25
wenzelm@57417
    26
fun receive timeout (Mailbox mailbox) =
wenzelm@28579
    27
  Synchronized.timed_access mailbox
wenzelm@62826
    28
    (fn _ => Option.map (fn t => Time.now () + t) timeout)
wenzelm@57417
    29
    (fn [] => NONE | msgs => SOME (msgs, []))
wenzelm@57417
    30
  |> these |> rev;
wenzelm@28135
    31
wenzelm@52583
    32
fun await_empty (Mailbox mailbox) =
wenzelm@57417
    33
  Synchronized.guarded_access mailbox (fn [] => SOME ((), []) | _ => NONE);
wenzelm@52583
    34
wenzelm@28135
    35
end;