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:

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: Note that the first formula implies these five formulas:

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.


[ Top | Parent | Root | Contents | Index ]

Forlan Version 4.12
Copyright © 2019 Alley Stoughton