Sort disjoint sublist: Difference between revisions
→{{header|ATS}}
m (→{{header|ATS}}) |
|||
Line 576:
let
typedef index = [i : nat | i < m] int i
prval () = lemma_list_vt_param values
Line 594 ⟶ 592:
val () = array_quicksort<index> (ix, num_indices)
nodes. The pointers will be in ascending index order. *)
val @(pf_refs, pfgc_refs | p_refs) =
array_ptr_alloc<ptr> num_indices
macdef refs = !p_refs▼
init_refs {j : nat | j <= m}
{i : nat | i <= n}
▲ (* Initialize the "refs" array with pointers to the relevant list
.<m - j>.
(pf_refs : !array_v (ptr?, p_refs + (i * sizeof ptr),
n - i)
let▼
ix : &array (index, n),
i : size_t i,
:<!wrt> void =
if i
| list_vt_nil () => $effmask_exn assertloc (false)
▲ in
| @ list_vt_cons (head, tail) =>
end▼
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)
(* Sort through the "refs" pointers. Here we will do that by
Line 647 ⟶ 670:
fun
write_back_values
{i : nat | i <= n}
vals : &array (a, n),
i : size_t i)
: void =
if i <> num_indices then
let
▲ macdef refs = !p_refs
val @(pf1, fpf1 | p1) = $UN.ptr_vtake{List1_vt a} (refs[i])
val+ @ list_vt_cons (head, tail) = !p1
Line 660 ⟶ 686:
prval () = fpf1 pf1
in
write_back_values (
end
val () = write_back_values (
in
array_ptr_free (pf_ix, pfgc_ix | p_ix);
| |||