Dijkstra's algorithm: Difference between revisions
→{{header|ATS}}
m (→{{header|ATS}}) |
|||
Line 757:
[https://en.wikipedia.org/w/index.php?title=Dijkstra%27s_algorithm&oldid=1117533081#Using_a_priority_queue a Wikipedia article about Dijkstra's algorithm].
''Note: Currently I do not prove termination of
<syntaxhighlight lang="ats">
Line 1,042:
source : size_t source)
(* Returns total-costs and previous-hops arrays. *)
:<!refwrt,!ntm> @(arrayref (flt, n),
arrayref ([i : nat | i <= n] size_t i, n)) =
let
prval () = lemma_matrixref_param adj_matrix
Line 1,062:
val active = arrayref_make_elt<bool> (n, true)
var num_active : [i : nat | i <= n] size_t i = n
fun
Line 1,076 ⟶ 1,077:
fun
main_loop
:<!refwrt,!ntm> void =▼
num_active : size_t num_active)▼
▲ :<!refwrt> void =
if (num_active <> i2sz 0) * (~pqueue_is_empty pq) then
let
val @(priority, u) =
pqueue_extract_min<flt><defined_index_t> pq
val () = active[u] := false▼
in
(* Ignore any queue entries that might raise the cost. *)
if
main_loop (pq, num_active)
else
let
▲ val () = active[u] := false
fun
loop_over_neighbors
Line 1,123 ⟶ 1,126:
end;
main_loop (pq,
end
val () = fill_pq (pq, i2sz 0)
val () = main_loop (pq,
in
@(cost, prev)
| |||