Dijkstra's algorithm: Difference between revisions

Content added Content deleted
Line 973: Line 973:
the "goto". Nevertheless, because the code "jumped to" is small, I
the "goto". Nevertheless, because the code "jumped to" is small, I
simply use a macro to duplicate it. *)
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+,
typedef pqueue (priority_t : t@ype+,
Line 980: Line 984:
[n <= n_max]
[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),
arr = arrayref (@(priority_t, value_t), n_max + 1),
n = size_t n,
n = size_t n
n_max = size_t n_max
}
}


Line 1,031: Line 1,039:
(succ n_max, arbitrary_entry)
(succ n_max, arbitrary_entry)
in
in
@{arr = arr,
@{pf = PQUEUE_N_MAX {n_max} () |
n = i2sz 0,
arr = arr,
n_max = n_max}
n = i2sz 0}
end
end


Line 1,046: Line 1,054:
:<!wrt> void =
:<!wrt> void =
let
let
prval () = lemma_g1uint_param (pq.n_max)
prval PQUEUE_N_MAX () = pq.pf (* Proves 0 <= n_max. *)
in
in
pq := @{arr = pq.arr,
pq := @{pf = pq.pf |
n = i2sz 0,
arr = pq.arr,
n_max = pq.n_max}
n = i2sz 0}
end
end


Line 1,127: Line 1,135:
arr[n1] := entry;
arr[n1] := entry;
_upheap {n_max} {n + 1} (arr, n1);
_upheap {n_max} {n + 1} (arr, n1);
pq := @{arr = arr,
pq := @{pf = pq.pf |
n = n1,
arr = arr,
n_max = pq.n_max}
n = n1}
end
end


Line 1,210: Line 1,218:
:<!refwrt> void =
:<!refwrt> void =
let
let
val @{arr = arr,
val @{pf = pf |
n = n,
arr = arr,
n_max = n_max} = pq
n = n} = pq
in
in
if i2sz 0 < pred n then
if i2sz 0 < pred n then
Line 1,219: Line 1,227:
_downheap {n_max} {n - 1} (arr, pred n)
_downheap {n_max} {n - 1} (arr, pred n)
end;
end;
pq := @{arr = arr,
pq := @{pf = pf |
n = pred n,
arr = arr,
n_max = n_max}
n = pred n}
end
end


Retrieved from "https://rosettacode.org/wiki/Dijkstra%27s_algorithm"