Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
POTTIER Francois
menhir
Commits
81871f0c
Commit
81871f0c
authored
Jul 10, 2015
by
POTTIER Francois
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Added [LowIntegerPriorityQueue], extracted out of [Astar] (and simplified).
parent
14e9e620
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
85 additions
and
0 deletions
+85
0
src/LowIntegerPriorityQueue.ml
src/LowIntegerPriorityQueue.ml
+65
0
src/LowIntegerPriorityQueue.mli
src/LowIntegerPriorityQueue.mli
+20
0
No files found.
src/LowIntegerPriorityQueue.ml
0 → 100644
View file @
81871f0c
(* This module implements a simpleminded priority queue, under the assumption
that priorities are low nonnegative integers. *)
module
InfiniteArray
=
MenhirLib
.
InfiniteArray
type
'
a
t
=
{
(* A priority queue is represented as an array of lists, indexed by
priorities. There is no a priori bound on the size of this array  its
size is increased if needed. It is up to the user to use priorities of
reasonable magnitude. *)
a
:
'
a
list
InfiniteArray
.
t
;
(* Index of lowest nonempty list, if there is one; or lower (suboptimal,
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
()
=
{
a
=
InfiniteArray
.
make
[]
;
best
=
0
;
cardinal
=
0
;
}
let
add
q
x
priority
=
assert
(
0
<=
priority
);
q
.
cardinal
<
q
.
cardinal
+
1
;
let
xs
=
InfiniteArray
.
get
q
.
a
priority
in
InfiniteArray
.
set
q
.
a
priority
(
x
::
xs
);
(* 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. *)
match
InfiniteArray
.
get
q
.
a
q
.
best
with

[]
>
q
.
best
<
q
.
best
+
1
;
remove_nonempty
q

x
::
xs
>
q
.
cardinal
<
q
.
cardinal

1
;
InfiniteArray
.
set
q
.
a
q
.
best
xs
;
Some
x
let
remove
q
=
if
q
.
cardinal
=
0
then
None
else
remove_nonempty
q
src/LowIntegerPriorityQueue.mli
0 → 100644
View file @
81871f0c
(** This module implements a simpleminded priority queue, under the
assumption that priorities are low nonnegative integers. *)
(** The type of priority queues. *)
type
'
a
t
(** [create()] creates an empty priority queue. *)
val
create
:
unit
>
'
a
t
(** [add q x p] inserts the element [x], with priority [p], into the queue [q]. *)
val
add
:
'
a
t
>
'
a
>
int
>
unit
(** [remove q] extracts out of [q] and returns an element with minimum priority. *)
val
remove
:
'
a
t
>
'
a
option
(** [is_empty q] tests whether the queue [q] is empty. *)
val
is_empty
:
'
a
t
>
bool
(** [cardinal q] returns the number of elements in the queue [q]. *)
val
cardinal
:
'
a
t
>
int
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment