Forlan Manual

The `Sort` Module

Synopsis

signature SORT structure Sort :> SORT

This module defines functions for testing orderedness of lists, inserting elements into ordered lists, merging ordered lists, and sorting lists, as well as the total ordering type on which they are based.

In the following specifications, if xs and yz are lists, then:

xs is a permuation of ys iff xs can be formed by reordering the elements of ys;
xs is a sub-permutation of ys iff xs can be formed from ys by first removing some (possibly none) of the elements of ys, and then reordering the remaining elements.

For example, [2, 1, 3, 1] is a permutation of [1, 3, 2, 1], and [6, 5, 4, 1] is a sub-permutation of [1, 4, 5, 2, 6, 4].

Interface

type 'a total_ordering = 'a * 'a -> order val equal : 'a total_ordering -> 'a * 'a -> bool val less : 'a total_ordering -> 'a * 'a -> bool val lessEqual : 'a total_ordering -> 'a * 'a -> bool val sorted : bool * 'a total_ordering -> 'a list -> bool val insert : bool * 'a total_ordering -> 'a * 'a list -> 'a list val merge : bool * 'a total_ordering -> 'a list * 'a list -> 'a list val sort : bool * 'a total_ordering -> 'a list -> 'a list

Description

type 'a total_ordering = 'a * 'a -> order

The type of total orderings. A value cmp (for "compare") of type 'a total_ordering must satisfy the following formulas, for all values x, y and z of type 'a:

cmp(x, y) = EQUAL iff x and y are indistinguishable;
cmp(x, y) = LESS iff cmp(y, x) = GREATER;
if cmp(x, y) = LESS and cmp(y, z) = LESS, then cmp(x, z) = LESS.

Note that the first formula implies these five formulas:

cmp(x, x);
cmp(x, y) = EQUAL iff cmp(y, x) = EQUAL;
if cmp(x, y) = EQUAL and cmp(y, z) = EQUAL, then cmp(x, z) = EQUAL;
if cmp(x, y) = EQUAL and cmp(y, z) = LESS, then cmp(x, z) = LESS;
if cmp(x, y) = LESS and cmp(y, z) = EQUAL, then cmp(x, z) = LESS.

equal cmp (x, y)

tests whether cmp(x, y) = EQUAL.

less cmp (x, y)

tests whether cmp(x, y) = LESS.

lessEqual cmp (x, y)

tests whether cmp(x, y) returns LESS or EQUAL.

sorted (true, cmp) xs

tests whether

lessEqual cmp (ListAux.sub(xs, i),
ListAux.sub(xs, i + 1))

, for all 1 <= i <= length xs - 1.

sorted (false, cmp) xs

tests whether

less cmp (ListAux.sub(xs, i),
ListAux.sub(xs, i + 1))

, for all 1 <= i <= length xs - 1.

insert (true, cmp) (x, ys)

If sorted (true, cmp) ys, then insert returns a permutation zs of x :: ys such that sorted (true, cmp) zs.

insert (false, cmp) (x, ys)

If sorted (false, cmp) ys, then insert returns a sub-permutation zs off x :: ys such that sorted (false, cmp) zs and, for all elements w of x :: ys, there is an element z of zs such that equal cmp (w, z).

merge (true, cmp) (xs, ys)

If sorted (true, cmp) xs and sorted (true, cmp) ys, then merge returns a permuation zs of xs @ ys such that sorted (true, cmp) zs.

merge (false, cmp) (xs, ys)

If sorted (false, cmp) xs and sorted (false, cmp) ys, then merge returns a sub-permutation zs of xs @ ys such that sorted (false, cmp) zs and, for all elements w of xs @ ys, there is an element z of zs such that

equal
cmp (w, z)

sort (true, cmp) xs

returns a permutation ys of xs such that sorted (true, cmp) ys.

sort (false, cmp) xs

returns a sub-permutation ys of xs such that sorted (false, cmp) ys and, for all elements x of xs, there is an element y of ys such that equal cmp (x, y).

Discussion

sort (dups, cmp) xs begins by checking whether sorted (dups, cmp) xs, in a computation taking at most length xs - 1 calls to cmp. If sorted returns true, then xs is returned. Otherwise, xs is sorted using merge sort.