(******************************************************************************)
(* *)
(* Menhir *)
(* *)
(* François Pottier, Inria Paris *)
(* Yann Régis-Gianas, PPS, Université Paris Diderot *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU General Public License version 2, as described in the *)
(* file LICENSE. *)
(* *)
(******************************************************************************)
(* This module implements a simple-minded priority queue, under the assumption
that priorities are low nonnegative integers. *)
module MyArray = ResizableArray
module MyStack = ResizableArray
type 'a t = {
(* A priority queue is represented as a resizable array, indexed by
priorities, of stacks (implemented as resizable arrays). There is no a
priori bound on the size of the main array -- its size is increased if
needed. It is up to the user to use priorities of reasonable
magnitude. *)
a: 'a MyStack.t MyArray.t;
(* Index of lowest nonempty stack, if there is one; or lower (sub-optimal,
but safe). If the queue is empty, [best] is arbitrary. *)
mutable best: int;
(* Current number of elements in the queue. Used in [remove] to stop the
search for a nonempty bucket. *)
mutable cardinal: int;
}
let create default =
(* Set up the main array so that it initially has 16 priority levels and, whenever
new levels are added, each of them is initialized with a fresh empty stack. The
dummy stack is never accessed; it is used to fill empty physical slots in the
main array. *)
let dummy = MyStack.make_ 0 default in
let a = MyArray.make 16 dummy (fun _ -> MyStack.make_ 1024 default) in
{ a; best = 0; cardinal = 0 }
let add q x priority =
assert (0 <= priority);
q.cardinal <- q.cardinal + 1;
(* Grow the main array if necessary. *)
if MyArray.length q.a <= priority then
MyArray.resize q.a (priority + 1);
(* Find out which stack we should push into. *)
let xs = MyArray.get q.a priority in
(* assert (xs != MyArray.default q.a); *)
(* Push. *)
MyStack.push xs x;
(* Decrease [q.best], if necessary, so as not to miss the new element. In
the special case of Dijkstra's algorithm or A*, this never happens. *)
if priority < q.best then
q.best <- priority
let is_empty q =
q.cardinal = 0
let cardinal q =
q.cardinal
let rec remove_nonempty q =
(* Look for the next nonempty bucket. We know there is one. This may seem
inefficient, because it is a linear search. However, in applications
where [q.best] never decreases, the cumulated cost of this loop is the
maximum priority ever used, which is good. *)
let xs = MyArray.get q.a q.best in
if MyStack.length xs = 0 then begin
(* As noted below, [MyStack.pop] does not physically shrink the stack.
When we find that a priority level has become empty, we physically
empty it, so as to free the (possibly large) space that it takes up.
This strategy is good when the client is Dijkstra's algorithm or A*. *)
let dummy = MyArray.default q.a in
MyArray.set q.a q.best dummy;
q.best <- q.best + 1;
remove_nonempty q
end
else begin
q.cardinal <- q.cardinal - 1;
Some (MyStack.pop xs)
(* Note: [MyStack.pop] does not shrink the physical array underlying the
stack. This is good, because we are likely to push new elements into
this stack. *)
end
let remove q =
if q.cardinal = 0 then
None
else
remove_nonempty q
let rec repeat q f =
match remove q with
| None ->
()
| Some x ->
f x;
repeat q f