Dijkstra's algorithm: Difference between revisions

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,077 ⟶ 1,076:
 
fun
main_loop (pq : &pqueue_t >> _,)
num_active : &([i : nat | i <= n] size_t i) >> _)
:<!refwrt,!ntm> void =
if (num_active <> i2sz 0) * (~pqueue_is_empty pq) then
let
val @(priority, u) =
Line 1,087 ⟶ 1,085:
(* Ignore any queue entries that might raise the cost. *)
if priority > cost[u] then
main_loop (pq, num_active)
else
let
val () = active[u] := false
and () = num_active := pred num_active
 
fun
Line 1,126 ⟶ 1,123:
end;
 
main_loop (pq, num_active)
end
 
val () = fill_pq (pq, i2sz 0)
val () = main_loop (pq, num_active)
in
@(cost, prev)
1,448

edits