/usr/share/doc/ats-lang-anairiats-examples/examples/KernighanRitchie/Chapter04/qsort.dats is in ats-lang-anairiats-examples 0.2.5-0ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 | //
// K&R, 2nd edition, page 87
//
(* ****** ****** *)
fn swap {n:nat} {i,j:nat | i < n; j < n}
(v: &(@[int][n]), i: int i, j: int j):<> void = let
val tmp = v.[i]
in
v.[i] := v.[j]; v.[j] := tmp
end // end of [swap]
(* ****** ****** *)
fun qsort {n:nat} {left,right:int}
{0 <= left; left <= right+1; right+1 <= n}
.<right+1-left>. (
v: &(@[int][n]), left: int left, right: int right
) :<> void =
if (left >= right) then () else let
val () = swap (v, left, (left + right) / 2)
val piv = v.[left]; val left1 = left + 1
val last = loop (v, left1, left1) where {
fun loop {last,i:nat}
{left < last; last <= i; i <= right+1}
.<right+1-i>.
(v: &(@[int][n]), last: int last, i: int i)
:<cloref> intBtw (left, right+1) =
if i <= right then begin
if v.[i] < piv then begin
swap (v, last, i); loop (v, last+1, i+1)
end else begin
loop (v, last, i+1)
end // end of [if]
end else begin
last - 1 // loop exits
end // end of [if]
} // end of [val]
in
swap (v, left, last); qsort (v, left, last-1); qsort (v, last+1, right)
end // end of [if]
// end of [qsort]
(* ****** ****** *)
implement main () = let
fn pr {n:nat}
(v: &(@[int][n]), n: int n): void = loop (v, n, 0) where {
fun loop {i:nat | i <= n} .<n-i>.
(v: &(@[int][n]), n: int n, i: int i): void =
if i < n then
(if i > 0 then print ", "; print v.[i]; loop (v, n, i+1))
// end of [if]
}
var !p_arr with pf_arr = @[int](8, 7, 1, 3, 9, 4, 2, 0, 6, 5)
val () = (print "bef: "; pr (!p_arr, 10); print_newline ())
val () = qsort (!p_arr, 0, 9)
val () = (print "aft: "; pr (!p_arr, 10); print_newline ())
in
// empty
end // end of [main]
(* ****** ****** *)
(* end of [qsort.dats] *)
|