/* Shared buffer */ /* shallow interface to imperative queue */ /* derived from linear buffer, lbuffer.c1 */ #use choice buffer { Ins; Del; }; choice buffer_response { Some; <# ; ?choice buffer> None; }; typedef lbuffer; typedef <# ; ?choice buffer> sbuffer; sbuffer #b new_buffer(int capacity) { queue_t q = new_queue(capacity); while (true) { lbuffer $b = (lbuffer)#b; /* accept */ switch ($b) { case Ins: { /* $b : */ int x = recv($b); /* $b : buffer */ enq(q,x); #b = (sbuffer)$b; /* detach */ break; } case Del: { /* $b : !choice buffer_response */ if (is_empty(q)) { $b.None; #b = (sbuffer)$b; /* detach */ } else { int x = deq(q); $b.Some; send($b, x); /* detach */ #b = (sbuffer)$b; } break; } } } }