Dijkstra's algorithm: Difference between revisions
→{{header|ATS}}
Line 973:
the "goto". Nevertheless, because the code "jumped to" is small, I
simply use a macro to duplicate it. *)
dataprop PQUEUE_N_MAX (n_max : int) =
| {0 <= n_max}
PQUEUE_N_MAX (n_max)
typedef pqueue (priority_t : t@ype+,
Line 980 ⟶ 984:
[n <= n_max]
@{
(* An earlier version of this structure stored a copy of n_max,
but the following use of the PQUEUE_N_MAX prop eliminates the
need for that. Instead the information is kept only at
typechecking time. *)
pf = PQUEUE_N_MAX (n_max) |
arr = arrayref (@(priority_t, value_t), n_max + 1),
n = size_t n
}
Line 1,031 ⟶ 1,039:
(succ n_max, arbitrary_entry)
in
@{
end
Line 1,046 ⟶ 1,054:
:<!wrt> void =
let
prval PQUEUE_N_MAX () =
in
pq := @{
end
Line 1,127 ⟶ 1,135:
arr[n1] := entry;
_upheap {n_max} {n + 1} (arr, n1);
pq := @{
end
Line 1,210 ⟶ 1,218:
:<!refwrt> void =
let
val @{
in
if i2sz 0 < pred n then
Line 1,219 ⟶ 1,227:
_downheap {n_max} {n - 1} (arr, pred n)
end;
pq := @{
end
| |||