Sort disjoint sublist: Difference between revisions

(* Initialize a "refs" array with pointers to the relevant list

nodes. The pointers will be in ascending index order. *)

fun

init_refs {j : nat | j <= m}

{i : nat | i <= n}

{p_refs : addr}

.<m - j>.

(pf_refs : !array_v (ptr?, p_refs + (i * sizeof ptr),

n - i)

>> array_v (ptr, p_refs + (i * sizeof ptr),

n - i) |

ix : &array (index, n),

p_refs : ptr p_refs,

i : size_t i,

values : &list_vt (a, m - j),

j : size_t j)

:<!wrt> void =

if i < num_indices then

case+ values of

| list_vt_nil () => $effmask_exn assertloc (false)

| @ list_vt_cons (head, tail) =>

if j = ix[i] then

let

prval @(pf_elem, pf_rest) = array_v_uncons pf_refs

val p = ptr_add<ptr> (p_refs, i)

val () = ptr_set<ptr> (pf_elem | p, addr@ values)

val () = init_refs (pf_rest | ix, p_refs, succ i,

tail, succ j)

prval () = pf_refs := array_v_cons (pf_elem, pf_rest)

prval () = fold@ values

in

end

else

let

val () = init_refs (pf_refs | ix, p_refs, i,

tail, succ j)

prval () = fold@ values

in

end

else

let

prval () = pf_refs := array_v_unnil_nil{ptr?, ptr} pf_refs

in

end

val () = init_refs (pf_refs | ix, p_refs, i2sz 0, values, i2sz 0)

{i : nat | i <= n}

{p_refs : addr}

(pf_refs : !array_v (ptr, p_refs, n) |

p_refs : ptr p_refs,

vals : &array (a, n),

i : size_t i)

macdef refs = !p_refs

write_back_values (pf_refs | p_refs, vals, succ i)

val () = write_back_values (pf_refs | p_refs, vals, i2sz 0)