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 *)