Natural sorting: Difference between revisions
→{{header|C}}
Thundergnat (talk | contribs) m (syntax highlighting fixup automation) |
|||
Line 332:
"Start with an " & (character id 223) & ": 8-3", "Start with an s: 8-4", "Start with an ss: 8-5"})
--> {"Start with an ʒ: 8-1", "Start with an ſ: 8-2", "Start with an s: 8-4", "Start with an ß: 8-3", "Start with an ss: 8-5"}</syntaxhighlight>
=={{header|ATS}}==
<syntaxhighlight lang="ats">
(*------------------------------------------------------------------*)
(* Natural sorting. *)
(*------------------------------------------------------------------*)
(* I deal only with ASCII here and solve only the first four
problems. For Unicode, I would most likely use GNU libunistring (or
Gnulib) and UTF-32. Handling Unicode properly is complicated.
There are other matters that make "natural sorting" a tricky
thing. For instance, which "accented letters" are actually
"accented"--rather than distinct letters in their own
right--depends on the language and the purpose. In Esperanto, for
example, 'ĉ' is a distinct letter that goes just after the letter
'c'. *)
#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"
#define NIL list_nil ()
#define :: list_cons
(*------------------------------------------------------------------*)
(* Types and interfaces. *)
typedef char_skipper =
{n : int}
{i : nat | i <= n}
(string n,
size_t n,
size_t i) -<cloref>
[j : int | i <= j; j <= n]
size_t j
typedef char_skipper_backwards =
{n : int}
{i : nat | i <= n}
(string n,
size_t n,
size_t i) -<cloref>
[j : int | 0 <= j; j <= i]
size_t j
typedef char_translator =
{n : int}
string n -<cloref,!wrt> string n
extern fn
make_char_skipper :
(char -<cloref> bool) -<> char_skipper
extern fn
make_char_skipper_backwards :
(char -<cloref> bool) -<> char_skipper_backwards
extern fn
make_char_translator :
(char -<cloref> bool,
char -<cloref> [c : int | 1 <= c; c <= 127] char c) -<>
char_translator
extern fn
remove_leading_spaces :
{n : int}
string n -< !wrt >
[m : nat | m <= n]
string m
extern fn
remove_trailing_spaces :
{n : int}
string n -< !wrt >
[m : nat | m <= n]
string m
extern fn
combine_adjacent_spaces :
{n : int}
string n -< !wrt >
[m : nat | m <= n]
string m
extern fn
compare_strings_containing_numbers :
{m, n : int}
(string m, string n) -<> int
extern fn
evaluate_natural :
{m : int}
{i, n : nat | i + n <= m}
(string m, size_t i, size_t n) -<> ullint
extern fn
compare_strings_naturally :
{m, n : int}
(string m, string n) -< !wrt > int
extern fn
list_sort_strings_naturally :
{n : int}
list (String, n) -< !wrt > list (String, n)
(*------------------------------------------------------------------*)
(* Global closures. *)
val skip_spaces =
make_char_skipper (lam c => c = ' ')
val skip_spaces_backwards =
make_char_skipper_backwards (lam c => c = ' ')
val skip_digits =
make_char_skipper (lam c => isdigit c)
val translate_whitespace_to_spaces =
make_char_translator (lam c => isspace c, lam c => ' ')
(* A little unit test. *)
val- "1 2 3 " = translate_whitespace_to_spaces "1\t2\v3\n"
val string_tolower =
make_char_translator
(lam c => isupper c,
lam c =>
let
typedef ascii_lowercase =
[c : int | 'a' <= c; c <= 'z'] char c
val c = tolower c
in
$UN.cast{ascii_lowercase} c
end)
(* A little unit test. *)
val- "abcdef" = string_tolower "ABCdef"
(*------------------------------------------------------------------*)
(* Implementations. *)
implement
make_char_skipper match =
let
fun
skipper {n : int}
{i : nat | i <= n}
.<n - i>.
(s : string n,
n : size_t n,
i : size_t i)
:<cloref> [j : int | i <= j; j <= n]
size_t j =
if i = n then
i
else if ~match s[i] then
i
else
skipper (s, n, succ i)
in
skipper
end
implement
make_char_skipper_backwards match =
let
fun
skipper {n : int}
{i : nat | i <= n}
.<i>.
(s : string n,
n : size_t n,
i : size_t i)
:<cloref> [j : int | 0 <= j; j <= i]
size_t j =
if i = i2sz 0 then
i
else if ~match s[pred i] then
i
else
skipper (s, n, pred i)
in
skipper
end
implement
make_char_translator (match, replace) =
let
fn
translator {n : int}
(s : string n)
:<cloref,!wrt> string n =
let
prval () = lemma_string_param s
val n = strlen s
fun
loop {i : nat | i <= n}
.<n - i>.
(t : strnptr n, (* strnptr so it is mutable. *)
i : size_t i)
:<!wrt> strnptr n =
if i = n then
t
else
let
val c = t[i]
in
if match c then
t[i] := replace c;
loop (t, succ i)
end
in
strnptr2string (loop (string1_copy s, i2sz 0))
end
in
translator
end
implement
remove_leading_spaces s =
let
prval () = lemma_string_param s
val n = strlen s
val j = skip_spaces (s, n, i2sz 0)
in
strnptr2string (string_make_substring (s, j, n - j))
end
(* A little unit test. *)
val- "1 " = remove_leading_spaces " 1 "
implement
remove_trailing_spaces s =
let
prval () = lemma_string_param s
val n = strlen s
val j = skip_spaces_backwards (s, n, n)
in
strnptr2string (string_make_substring (s, i2sz 0, j))
end
(* A little unit test. *)
val- " 1" = remove_trailing_spaces " 1 "
fn
_combine_adjacent_spaces
{n : int}
(s : string n)
:<!refwrt> [m : nat | m <= n]
string m =
let
prval () = lemma_string_param s
val n = strlen s
in
if n = i2sz 0 then
s
else
let
val buf = arrayref_make_elt<char> (succ n, '\0')
val () = buf[0] := s[0]
fun
loop {i : pos | i <= n}
{j : pos | j <= i}
.<n - i>.
(i : size_t i,
j : size_t j)
:<!refwrt> [k : pos | k <= n]
size_t k =
if i = n then
j
else
begin
if (s[i] = ' ') * (s[pred i] = ' ') then
loop (succ i, j)
else
begin
buf[j] := s[i];
loop (succ i, succ j)
end
end
val [k : int] k = loop (i2sz 1, i2sz 1)
val s1 = $UN.cast{string k} (ptrcast buf)
in
strnptr2string (string_make_substring (s1, i2sz 0, k))
end
end
implement
combine_adjacent_spaces s =
$effmask_ref _combine_adjacent_spaces s
(* A little unit test. *)
val- " 1 2 3 4 " = combine_adjacent_spaces " 1 2 3 4 "
implement
compare_strings_containing_numbers {m, n} (sm, sn) =
let
prval () = lemma_string_param sm
prval () = lemma_string_param sn
val m = strlen sm
and n = strlen sn
fun
compare_them
{i, j : nat | i <= m; j <= n}
.<m - i, n - j>.
(i : size_t i,
j : size_t j)
:<> int =
if i = m then
(if j = n then 0 else ~1)
else if j = n then
1
else if (isdigit sm[i]) * (isdigit sn[j]) then
let
val i1 = skip_digits (sm, m, succ i)
and j1 = skip_digits (sn, n, succ j)
val vm = evaluate_natural (sm, i, i1 - i)
and vn = evaluate_natural (sn, j, j1 - j)
in
if vm = vn then
compare_them (i1, j1)
else if vm < vn then
~1
else
1
end
else
let
val cmp = compare (sm[i], sn[j])
in
if cmp = 0 then
compare_them (succ i, succ j)
else
cmp
end
in
compare_them (i2sz 0, i2sz 0)
end
implement
evaluate_natural {m} {i, n} (s, i, n) =
let
fun
loop {k : int | i <= k; k <= i + n}
.<(i + n) - k>.
(k : size_t k,
accum : ullint)
:<> ullint =
if k = i + n then
accum
else
let
val digit = (char2int0 s[k] - char2int0 '0')
val accum = (10ULL * accum) + g0i2u digit
in
loop (succ k, accum)
end
in
loop (i, 0ULL)
end
(* A little unit test. *)
val- 1234ULL = evaluate_natural ("xy1234z", i2sz 2, i2sz 4)
implement
compare_strings_naturally (sm, sn) =
let
prval () = lemma_string_param sm
prval () = lemma_string_param sn
fn
adjust_string (s : String0)
:<!wrt> String0 =
let
val s = translate_whitespace_to_spaces s
val s = string_tolower s
val s = remove_leading_spaces s
val s = remove_trailing_spaces s
val s = combine_adjacent_spaces s
in
s
end
in
compare_strings_containing_numbers (adjust_string sm,
adjust_string sn)
end
implement
list_sort_strings_naturally lst =
let
implement
list_mergesort$cmp<String> (x, y) =
$effmask_wrt compare_strings_naturally (x, y)
in
list_vt2t (list_mergesort<String> lst)
end
(*------------------------------------------------------------------*)
(* Now see if we pass the required tests. *)
implement
gequal_val_val<String> (x, y) =
g0ofg1 x = g0ofg1 y
fn
nicefy_string (s : string)
: string =
let
val s = g1ofg0 s
prval () = lemma_string_param s
val n = strlen s
prval [n : int] EQINT () = eqint_make_guint n
var t : string = ""
var i : [i : nat | i <= n] size_t i
in
for (i := i2sz 0; i <> n; i := succ i)
let
val c = char2int0 s[i]
in
if c < 32 then
let
val numstr = strptr2string (g0int2string c)
val u =
strptr2string (string0_append4 (t, "[", numstr, "]"))
in
t := u
end
else
let
val chrstr = strnptr2string (string_sing s[i])
val u = strptr2string (string0_append (t, chrstr))
in
t := u
end
end;
t
end
fn
make_list_printable {n : int}
(lst : list (String, n))
: list (string, n) =
let
prval () = lemma_list_param lst
fun
loop {i : nat | i <= n}
.<n - i>.
(lst : list (String, n - i),
accum : list (string, i))
: list (string, n) =
case+ lst of
| NIL => list_vt2t (list_reverse accum)
| head :: tail =>
let
val s = strptr2string (string0_append3 ("|", head, "|"))
in
loop (tail, nicefy_string s :: accum)
end
in
loop (lst, NIL)
end
fn
test_ignoring_leading_spaces () : void =
let
val givenlst = $list ("ignore leading spaces: 2-2",
" ignore leading spaces: 2-1",
" ignore leading spaces: 2+0",
" ignore leading spaces: 2+1")
val expected = $list (" ignore leading spaces: 2+0",
" ignore leading spaces: 2+1",
" ignore leading spaces: 2-1",
"ignore leading spaces: 2-2")
val sortedlst = list_sort_strings_naturally givenlst
in
assertloc (sortedlst = expected);
println! ("Ignoring leading spaces:");
println! (" given: ", make_list_printable givenlst);
println! (" result: ", make_list_printable sortedlst)
end
fn
test_ignoring_trailing_spaces () : void =
(* I added this test, myself. *)
let
val givenlst = $list ("ignore trailing spaces: 2b2",
"ignore trailing spaces: 2b1 ",
"ignore trailing spaces: 2b+0 ",
"ignore trailing spaces: 2b+1 ")
val expected = $list ("ignore trailing spaces: 2b+0 ",
"ignore trailing spaces: 2b+1 ",
"ignore trailing spaces: 2b1 ",
"ignore trailing spaces: 2b2")
val sortedlst = list_sort_strings_naturally givenlst
in
assertloc (sortedlst = expected);
println! ("Ignoring trailing spaces:");
println! (" given: ", make_list_printable givenlst);
println! (" result: ", make_list_printable sortedlst)
end
fn
test_combining_adjacent_spaces () : void =
let
val givenlst = $list ("ignore m.a.s spaces: 2-2",
"ignore m.a.s spaces: 2-1",
"ignore m.a.s spaces: 2+0",
"ignore m.a.s spaces: 2+1")
val expected = $list ("ignore m.a.s spaces: 2+0",
"ignore m.a.s spaces: 2+1",
"ignore m.a.s spaces: 2-1",
"ignore m.a.s spaces: 2-2")
val sortedlst = list_sort_strings_naturally givenlst
in
assertloc (sortedlst = expected);
println! ("Combining adjacent spaces:");
println! (" given: ", make_list_printable givenlst);
println! (" result: ", make_list_printable sortedlst)
end
fn
test_whitespace_equivalence () : void =
let
val givenlst = $list ("Equiv. spaces: 3-3",
"Equiv.\rspaces: 3-2",
"Equiv.\x0cspaces: 3-1",
"Equiv.\x0bspaces: 3+0",
"Equiv.\nspaces: 3+1",
"Equiv.\tspaces: 3+2")
val expected = $list ("Equiv.\x0bspaces: 3+0",
"Equiv.\nspaces: 3+1",
"Equiv.\tspaces: 3+2",
"Equiv.\x0cspaces: 3-1",
"Equiv.\rspaces: 3-2",
"Equiv. spaces: 3-3")
val sortedlst = list_sort_strings_naturally givenlst
in
assertloc (sortedlst = expected);
println! ("All whitespace characters equivalent:");
println! (" given: ", make_list_printable givenlst);
println! (" result: ", make_list_printable sortedlst)
end
fn
test_case_independence () : void =
let
val givenlst = $list ("cASE INDEPENENT: 3-2",
"caSE INDEPENENT: 3-1",
"casE INDEPENENT: 3+0",
"case INDEPENENT: 3+1")
val expected = $list ("casE INDEPENENT: 3+0",
"case INDEPENENT: 3+1",
"caSE INDEPENENT: 3-1",
"cASE INDEPENENT: 3-2")
val sortedlst = list_sort_strings_naturally givenlst
in
assertloc (sortedlst = expected);
println! ("Case independence:");
println! (" given: ", make_list_printable givenlst);
println! (" result: ", make_list_printable sortedlst)
end
fn
test_numeric_fields () : void =
let
val givenlst = $list ("foo100bar99baz0.txt",
"foo100bar10baz0.txt",
"foo1000bar99baz10.txt",
"foo1000bar99baz9.txt")
val expected = $list ("foo100bar10baz0.txt",
"foo100bar99baz0.txt",
"foo1000bar99baz9.txt",
"foo1000bar99baz10.txt")
val sortedlst = list_sort_strings_naturally givenlst
in
assertloc (sortedlst = expected);
println! ("Numeric fields:");
println! (" given: ", make_list_printable givenlst);
println! (" result: ", make_list_printable sortedlst)
end
implement
main0 () =
begin
test_ignoring_leading_spaces ();
test_ignoring_trailing_spaces ();
test_combining_adjacent_spaces ();
test_whitespace_equivalence ();
test_case_independence ();
test_numeric_fields ();
println! ("success")
end
(*------------------------------------------------------------------*)
</syntaxhighlight>
{{out}}
<pre>
Ignoring leading spaces:
given: |ignore leading spaces: 2-2|, | ignore leading spaces: 2-1|, | ignore leading spaces: 2+0|, | ignore leading spaces: 2+1|
result: | ignore leading spaces: 2+0|, | ignore leading spaces: 2+1|, | ignore leading spaces: 2-1|, |ignore leading spaces: 2-2|
Ignoring trailing spaces:
given: |ignore trailing spaces: 2b2|, |ignore trailing spaces: 2b1 |, |ignore trailing spaces: 2b+0 |, |ignore trailing spaces: 2b+1 |
result: |ignore trailing spaces: 2b+0 |, |ignore trailing spaces: 2b+1 |, |ignore trailing spaces: 2b1 |, |ignore trailing spaces: 2b2|
Combining adjacent spaces:
given: |ignore m.a.s spaces: 2-2|, |ignore m.a.s spaces: 2-1|, |ignore m.a.s spaces: 2+0|, |ignore m.a.s spaces: 2+1|
result: |ignore m.a.s spaces: 2+0|, |ignore m.a.s spaces: 2+1|, |ignore m.a.s spaces: 2-1|, |ignore m.a.s spaces: 2-2|
All whitespace characters equivalent:
given: |Equiv. spaces: 3-3|, |Equiv.[13]spaces: 3-2|, |Equiv.[12]spaces: 3-1|, |Equiv.[11]spaces: 3+0|, |Equiv [10]spaces: 3+1|, |Equiv.[9]spaces: 3+2|
result: |Equiv.[11]spaces: 3+0|, |Equiv.[10]spaces: 3+1|, |Equiv.[9]spaces: 3+2|, |Equiv.[12]spaces: 3-1|, |Equiv.[13]spaces: 3-2|, |Equiv. spaces: 3-3|
Case independence:
given: |cASE INDEPENENT: 3-2|, |caSE INDEPENENT: 3-1|, |casE INDEPENENT: 3+0|, |case INDEPENENT: 3+1|
result: |casE INDEPENENT: 3+0|, |case INDEPENENT: 3+1|, |caSE INDEPENENT: 3-1|, |cASE INDEPENENT: 3-2|
Numeric fields:
given: |foo100bar99baz0.txt|, |foo100bar10baz0.txt|, |foo1000bar99baz10.txt|, |foo1000bar99baz9.txt|
result: |foo100bar10baz0.txt|, |foo100bar99baz0.txt|, |foo1000bar99baz9.txt|, |foo1000bar99baz10.txt|
success
</pre>
=={{header|C}}==
| |||