Sort disjoint sublist: Difference between revisions
→{{header|AutoHotkey}}
(Added XPL0 example.) |
|||
Line 548:
<pre>7 0 5 4 3 2 1 6</pre>
=={{header|ATS}}==
Much of the code here is proofs, necessary assertions, memory management enforced by the type system, etc. (Some might say I am somewhat lax in my handling of pointers, using the simplest type '''ptr''' instead of more elaborate types.)
<lang ATS>#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"
(* For simplicity, I implement this task only for sorting values of
non-linear type. That would include all the basic integer types,
garbage-collected strings, etc.
Also I freely create arrays as workspace, although the size of any
workspace array is equal only to the number of indices (not to the
number of values). *)
extern fn {a : t@ype}
sort_disjoint_sublist$cmp : (a, a) -<> int
fn {a : t@ype}
sort_disjoint_sublist
{m : int}
{n : int}
(values : &list_vt (a, m) >> _,
indices : list ([i : nat | i < m] int i, n))
: void =
let
typedef index = [i : nat | i < m] int i
val p_values = addr@ values
prval () = lemma_list_vt_param values
prval () = lemma_list_param indices
val num_values : size_t m = i2sz (list_vt_length values)
and num_indices : size_t n = i2sz (list_length indices)
(* Put the indices in ascending order. *)
val @(pf_ix, pfgc_ix | p_ix) =
array_ptr_alloc<index> num_indices
macdef ix = !p_ix
val () = array_initize_list<index> (ix, sz2i num_indices, indices)
implement
array_quicksort$cmp<index> (x, y) =
if x < y then ~1 else 1
val () = array_quicksort<index> (ix, num_indices)
val @(pf_refs, pfgc_refs | p_refs) =
array_ptr_alloc<ptr> num_indices
macdef refs = !p_refs
(* Initialize the "refs" array with pointers to the relevant list
nodes. The pointers will be in ascending index order. *)
implement
array_initize$init<ptr> (i, x) =
let
val @(pf1, fpf1 | p1) = $UN.ptr_vtake{list_vt (a, m)} p_values
val i1 = g1ofg0 i
prval () = lemma_g1uint_param i1
val () = assertloc (i1 < num_indices)
val @(pf2, fpf2 | p2) = $UN.ptr_vtake{@[index][n]} p_ix
macdef ix = !p_ix
val () = x :=
$UN.castvwtp0{ptr} (list_vt_getref_at (!p1, ix[i1]))
prval () = fpf2 pf2
prval () = fpf1 pf1
in
end
val () = array_initize<ptr> (refs, num_indices)
(* Sort through the "refs" pointers. Here we will do that by
copying the values to an array, sorting the array, then writing
the sorted values back. One could also do the sort in place,
however. *)
val @(pf_vals, pfgc_vals | p_vals) =
array_ptr_alloc<a> num_indices
macdef vals = !p_vals
implement
array_initize$init<a> (i, x) =
let
val @(pf1, fpf1 | p1) = $UN.ptr_vtake{array (ptr, n)} p_refs
macdef refs = !p1
val i1 = g1ofg0 i
prval () = lemma_g1uint_param i1
val () = assertloc (i1 < num_indices)
val @(pf2, fpf2 | p2) = $UN.ptr_vtake{List1_vt a} (refs[i1])
val+ @ list_vt_cons (head, tail) = !p2
val () = x := head
prval () = fold@ (!p2)
prval () = fpf2 pf2
prval () = fpf1 pf1
in
end
val () = array_initize<a> (vals, num_indices)
implement
array_quicksort$cmp<a> (x, y) =
sort_disjoint_sublist$cmp<a> (x, y)
val () = array_quicksort<a> (vals, num_indices)
fun
write_back_values
{i : nat | i <= n}
(refs : &array (ptr, n),
vals : &array (a, n),
i : size_t i)
: void =
if i <> num_indices then
let
val @(pf1, fpf1 | p1) = $UN.ptr_vtake{List1_vt a} (refs[i])
val+ @ list_vt_cons (head, tail) = !p1
val () = head := vals[i]
prval () = fold@ (!p1)
prval () = fpf1 pf1
in
write_back_values (refs, vals, succ i)
end
val () = write_back_values (refs, vals, i2sz 0)
in
array_ptr_free (pf_ix, pfgc_ix | p_ix);
array_ptr_free (pf_refs, pfgc_refs | p_refs);
array_ptr_free (pf_vals, pfgc_vals | p_vals)
end
implement
sort_disjoint_sublist$cmp<int> (x, y) =
if x < y then
~1
else if y < x then
1
else
0
implement
main0 () =
let
var values = $list_vt{int} (7, 6, 5, 4, 3, 2, 1, 0)
val indices = $list{[i : nat | i < 8] int i} (6, 1, 7)
in
println! values;
sort_disjoint_sublist<int> (values, indices);
println! values;
free values
end</lang>
{{out}}
<pre>$ patscc -DATS_MEMALLOC_GCBDW -O3 sort_disjoint_sublist_task.dats -lgc && ./a.out
7, 6, 5, 4, 3, 2, 1, 0
7, 0, 5, 4, 3, 2, 1, 6</pre>
=={{header|AutoHotkey}}==
| |||