1 (* A FIFO queue implementation, adapted from OCaml's queue.ml. *)
  2 
  3 mutable data cell a =
  4   Cell { value: a; next: dynamic }
  5 
  6 (* The FIFO structure is implemented as a cyclic list. The
  7    [fifo] object contains a pointer to the last element of
  8    the queue, as well as the length of the queue. The length
  9    information is used in the OCaml version to test whether
 10    the queue is empty. Here, the tag, [Empty] or [NonEmpty],
 11    provides this information. The [tail] pointer is present
 12    only when the queue is nonempty. *)
 13 
 14 mutable data fifo a =
 15   Empty    { length: int; tail: ()      }
 16 | NonEmpty { length: int; tail: dynamic }
 17 adopts cell a
 18 
 19 val create [a] () : fifo a =
 20   Empty { length = 0; tail = () }
 21 
 22 val internal_insert [a] (consumes x: a, q: fifo a, insertAtEnd: bool): () =
 23   let c = Cell {
 24     value = x; next = ()
 25   } in
 26   match q with
 27   | Empty ->
 28       c.next <- c;
 29       give c to q;
 30       tag of q <- NonEmpty;
 31       q.length <- 1;
 32       q.tail <- c
 33   | NonEmpty { tail } ->
 34       taking tail from q begin
 35         c.next <- tail.next;
 36         tail.next <- c;
 37       end;
 38       give c to q;
 39       q.length <- q.length + 1;
 40       (* We have just inserted the cell [c] at the beginning of the
 41          queue. If the caller would like [c] to be inserted at the
 42          end of the queue, advance the [tail] pointer. *)
 43       if insertAtEnd then
 44         q.tail <- c
 45   end
 46 
 47 val insert [a] (consumes x: a, q: fifo a) : () =
 48   internal_insert (x, q, true)
 49 
 50 val insert_at_head [a] (consumes x: a, q: fifo a) : () =
 51   internal_insert (x, q, false)
 52 
 53 val retrieve [a] (q: fifo a) : option a =
 54   match q with
 55   | Empty ->
 56       None
 57   | NonEmpty { tail } ->
 58       take tail from q;
 59       let head = tail.next in
 60       if head == tail then begin
 61         tag of q <- Empty;
 62         q.length <- 0;
 63         q.tail <- ()
 64       end
 65       else begin
 66         q.length <- q.length - 1;
 67         take head from q;
 68         tail.next <- head.next;
 69         give tail to q
 70       end;
 71       (* At this point, we own the [head] cell. Note that this annotation
 72          is not required. *)
 73       assert head @ cell a;
 74       (* The head cell must not be given back to the queue. We need to assert
 75          the ownership of [head.value], whose type is not duplicable. *)
 76       some head.value
 77  end
 78 
 79 val peek [a] duplicable a => (q: fifo a) : option a =
 80   match q with
 81   | Empty ->
 82       none
 83   | NonEmpty { tail } ->
 84       let head =
 85         taking tail from q begin
 86           tail.next
 87         end
 88       in
 89       taking head from q begin
 90         some head.value
 91       end
 92   end
 93 
 94 val length [a] (q: fifo a) : int =
 95   match q with
 96   | Empty -> 0
 97   | NonEmpty -> q.length
 98   end
 99 
100 (* The function [clear] doesn't type-check without the [match]
101    construct. Mezzo does not allow setting an object's tag
102    unless its current tag is known. *)
103 
104 val clear [a] (q: fifo a) : () =
105   match q with
106   | Empty -> ()
107   | NonEmpty ->
108       tag of q <- Empty;
109       q.length <- 0;
110       q.tail   <- ()
111   end
112 
113 val rotate [a] (q: fifo a) : () =
114   match q with
115   | Empty ->
116       ()
117   | NonEmpty { tail } ->
118       (* Advance the tail pointer. *)
119       taking tail from q begin
120         q.tail <- tail.next
121       end
122   end
123 
124 (* In contrast with [list::fold], the function [queue::fold] cannot perform
125    a strong update on the queue elements. The queue [q] adopts elements of
126    type [cell a], and this cannot be changed. Thus, [queue::fold] must require
127    its argument [f] to preserve the type [a] of the list element. *)
128 
129 val fold [a, b] (
130   q: fifo a,
131   consumes accu: b,
132   f: (a, consumes b) -> b
133 ) : b =
134   match q with
135   | Empty ->
136       accu
137   | NonEmpty { tail } ->
138       let rec fold (consumes accu: b, c: dynamic | q @ fifo a) : b =
139         take c from q;
140         let Cell { next; value } = c in
141         let accu = f (value, accu) in
142         give c to q;
143         if tail == c then
144           accu
145         else
146           fold (accu, next)
147       in
148       (* Obtain the address of the first cell. *)
149       let head = taking tail from q begin tail.next end in
150       (* We're ready to launch the recursion. *)
151       fold (accu, head)
152   end
153 
154 val iter [a, p : perm] (
155   q: fifo a,
156   f: (a | p) -> ()
157 | p
158 ) : () =
159   fold [a, (| p)] (q, (), fun (x:a, (| p)) : () = f x)
160 
161 val map [a, b, p : perm] (
162   q: fifo a,
163   f: (a | p) -> b
164 | p
165 ) : fifo b =
166   let q' : fifo b = create () in
167   iter (q, fun (x: a | q' @ fifo b * p) : () =
168     insert (f x, q')
169   );
170   q'
171 
172 val copy [a] duplicable a => (q: fifo a): fifo a =
173   map (q, fun (x: a) : a = x)
174 
175 val rec work [a, p : perm] (q: fifo a, f: (a | q @ fifo a * p) -> () | p) : () =
176   match retrieve q with
177   | None ->
178       ()
179   | Some { contents = x } ->
180       f x;
181       work (q, f)
182   end
183 
184 (*
185 Local Variables:
186 compile-command: "../mezzo queue.mz"
187 End:
188 *)