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