1 (* The type of FIFO queues. *)
 2 
 3 abstract fifo +(a : type) : type
 4 fact exclusive (fifo a)
 5 
 6 (* Elements are normally inserted at the end of the queue, and retrieved
 7    at the beginning. However, insertion at the beginning of the queue is
 8    also supported. *)
 9 
10 (* [create()] creates a new, empty queue. *)
11 val create: [a] () -> fifo a
12 
13 (* [insert (x, q)] inserts the element [x] at the end of the queue [q]. The
14    queue claims the ownership of the element. *)
15 val insert: [a] (consumes a, fifo a) -> ()
16 
17 (* [retrieve q] extracts the element found at the beginning of the queue [q],
18    if there is one. The caller recovers the ownership of the element. *)
19 val retrieve: [a] fifo a -> option a
20 
21 (* [peek q] returns the element found at the beginning of the queue [q],
22    if there is one. The element remains in the queue. This function is
23    available only if the elements are duplicable. *)
24 val peek: [a] duplicable a => fifo a -> option a
25 
26 (* [length q] returns the number of elements in the queue [q]. *)
27 val length: [a] fifo a -> int
28 
29 (* [clear q] empties the queue [q]. *)
30 val clear: [a] fifo a -> ()
31 
32 (* [insert_at_head (x, q)] inserts the element [x] at the beginning of the
33    queue [q]. *)
34 val insert_at_head: [a] (consumes a, fifo a) -> ()
35 
36 (* [rotate q] moves the first element of [q] to the end of the queue. If [q]
37    is empty, [rotate] has no effect. *)
38 val rotate: [a] fifo a -> ()
39 
40 (* [fold] applies the function [f], in turn, to every element of [q].
41    An accumulator is threaded through the iteration. *)
42 val fold : [a, b] (
43   q: fifo a,
44   consumes accu: b,
45   f: (a, consumes b) -> b
46 ) -> b
47 
48 (* [iter] applies the function [f], in turn, to every element of [q]. *)
49 val iter : [a, p : perm] (
50   q: fifo a,
51   f: (a | p) -> ()
52 | p
53 ) -> ()
54 
55 (* [map (q, f)] is a new queue obtained by applying [f] to every element of
56    the queue [q]. *)
57 val map: [a, b, p : perm] (
58   q: fifo a,
59   f: (a | p) -> b
60 | p
61 ) -> fifo b
62 
63 (* [copy q] is a new queue whose elements are the elements of [q]. *)
64 val copy  : [a] duplicable a => fifo a -> fifo a
65 
66 (* [work (q, f)] extracts an element [x] out of the queue [q] and
67    executes [f x]. The function [f] has access to the queue, and may
68    insert new elements into it. This process is repeated until the
69    queue becomes empty. *)
70 val work : [a, p : perm] (q: fifo a, f: (a | q @ fifo a * p) -> () | p) -> ()
71 
72 (*
73   Local Variables:
74   compile-command: "../mezzo queue.mzi"
75   End:
76 *)