Set
Module
signature SET
structure Set
:> SET
This module implements an abstract type of finite sets.
type 'a set
val memb : 'a Sort.total_ordering -> 'a * 'a set -> bool
val fromList : 'a Sort.total_ordering -> 'a list -> 'a set
val toList : 'a set -> 'a list
val isEmpty : 'a set -> bool
val isNonEmpty : 'a set -> bool
val size : 'a set -> int
val hd : 'a set -> 'a
val tl : 'a set -> 'a set
val compare : 'a Sort.total_ordering -> 'a set * 'a set -> order
val subset : 'a Sort.total_ordering -> 'a set * 'a set -> bool
val equal : 'a Sort.total_ordering -> 'a set * 'a set -> bool
val all : ('a -> bool) -> 'a set -> bool
val exists : ('a -> bool) -> 'a set -> bool
val empty : 'a set
val sing : 'a -> 'a set
val filter : ('a -> bool) -> 'a set -> 'a set
val partition : ('a -> bool) -> 'a set -> 'a set * 'a set
val position : ('a -> bool) -> 'a set -> int option
val map : 'b Sort.total_ordering -> ('a -> 'b) -> 'a set -> 'b set
val mapFromList : 'b Sort.total_ordering -> ('a -> 'b) -> 'a list -> 'b set
val mapToList : ('a -> 'b) -> 'a set -> 'b list
val union : 'a Sort.total_ordering -> 'a set * 'a set -> 'a set
val genUnion : 'a Sort.total_ordering -> 'a set list -> 'a set
val inter : 'a Sort.total_ordering -> 'a set * 'a set -> 'a set
val genInter : 'a Sort.total_ordering -> 'a set list -> 'a set
val minus : 'a Sort.total_ordering -> 'a set * 'a set -> 'a set
val comparePair : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a * 'b) Sort.total_ordering
val times : 'a set * 'b set -> ('a * 'b) set
val compareTriple : 'a Sort.total_ordering
* 'b Sort.total_ordering
* 'c Sort.total_ordering -> ('a * 'b * 'c) Sort.total_ordering
val times3 : 'a set * 'b set * 'c set -> ('a * 'b * 'c) set
val compareList : 'a Sort.total_ordering -> 'a list Sort.total_ordering
val genTimes : 'a set list -> 'a list set
type 'a set
'a
.
The module's values are specified with the help of the abstract proposition saying that a value xs
of type 'a set
is compatible with a value cmp
of type 'a Sort.total_ordering
.
memb cmp (x, ys)
ys
is compatible with cmp
, then memb
tests whether x
is a member (element) of ys
. Formally, memb
must be understood in relationship to the specifications of the module's other values.
In a context where we know that a value xs
of type 'a set
is compatible with a value cmp
of type 'a Sort.total_ordering
, when we say that x
is an element of xs
, this means that x
is a value of type 'a
such that memb cmp (x, xs)
.
fromList cmp xs
cmp
and whose elements are the elements of xs
, i.e., the set ys
such that:
1 <= i <= length xs
, memb cmp (List.sub(xs, i), ys)
;
y
of type 'a
, if memb cmp (y, ys)
, then there is an 1 <= i <= length xs
such that Sort.equal cmp (y, List.sub(xs, i))
.
toList xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then toList
returns the list consisting of the elements of xs
, listed in strictly ascending order according to cmp
, i.e., the list ys
such that:
Sort.sorted (false, cmp) ys
;
x
of type 'a
, if memb cmp (x, xs)
, then there is an 1 <= i <= length ys
such that Sort.equal cmp (x, List.sub(ys, i))
;
1 <= i <= length ys
, memb cmp (List.sub(ys, i), xs)
.
isEmpty xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then isEmpty
tests whether xs
is empty, i.e., whether there is no value x
of type 'a
such that memb cmp (x, xs)
.
isNonEmpty xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then isNonEmpty
tests whether xs
is nonempty, i.e., whether there is a value x
of type 'a
such that memb cmp (x, xs)
.
size xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then size
returns the size of xs
, i.e., the length of toList xs
.
hd xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then hd
returns the head of xs
, i.e., the first element of toList xs
. It raises Empty
if this list is empty.
tl xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then tl
returns the tail of xs
, i.e., fromList cmp (tl(toList xs))
. It raises Empty
if toList xs
is the empty list.
compare cmp (xs, ys)
xs
and ys
are compatible with cmp
, then compare
first compares size xs
and size ys
, returning LESS
if the former is less than the latter, and GREATER
if the former is greater than the latter. If the sizes are equal, it works through the corresponding elements of toList xs
and toList ys
, using cmp
to compare those elements, until a result of LESS
or GREATER
is found, in which case that result in returned. If all comparisons result in EQUAL
, then compare
returns EQUAL
.
Unfortunately, compare cmp
isn't an 'a Sort.total_ordering
. But does satisfy the formulas of the definition of 'a set Sort.total_ordering
for all values xs
, ys
and zs
of type 'a set
that are compatible with cmp
. In addition, we have that compare cmp (xs, ys) = EQUAL
iff equal cmp (xs, ys)
, where the function equal
is specified below.
subset cmp (xs, ys)
xs
and ys
are compatible with cmp
, then subset
tests whether xs
is a subset of ys
, i.e., whether, for all values z
of type 'a
, if memb cmp (z, xs)
, then memb cmp (z, ys)
.
equal cmp (xs, ys)
xs
and ys
are compatible with cmp
, then equal
tests whether xs
is equal to ys
, i.e., whether, for all values z
of type 'a
, memb cmp (z, xs)
iff memb cmp (z, ys)
.
all f xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then all
tests whether, for all elements x
of xs
, f x
, i.e., whether, for all values x
of type 'a
, if memb cmp (x,
xs)
, then f x
.
exists f xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then exists
tests whether, there is an element x
of xs
such that f x
, i.e., whether there is a value x
of type 'a
such that memb cmp (x,
xs)
and f x
.
empty
cmp
is a value of type 'a Sort.total_ordering
, then empty
is the set that is compatible with cmp
and has no elements, i.e., the set xs
such that there is no value x
of 'a
such that memb cmp (x,
xs)
.
sing x
cmp
is a value of type 'a Sort.total_ordering
, then sing
returns the set that is compatible with cmp
and whose only element is x
, i.e., the set ys
such that, for all values y
of type 'a
, memb cmp (y, ys)
iff Sort.equal cmp (y, x)
.
filter f xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then filter
returns the set that is compatible with cmp
and consists of the elements of xs
on which f
returns true
, i.e., the set ys
such that, for all values y
of type 'a
, memb cmp (y, ys)
iff memb cmp (y, xs)
and f y
.
partition f xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then filter
returns the pair of sets (ys, zs)
such that ys
and zs
are compatible with cmp
, ys
consists of the elements of xs
on which f
returns true
, and zs
consists of the elements of xs
on which f
returns false
, i.e., such that
y
of type 'a
, memb cmp (y, ys)
iff memb cmp (y, xs)
and f y
;
z
of type 'a
, memb cmp (z, zs)
iff memb cmp (z, xs)
and not(f z)
.
position f xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then position
behaves the same as ListAux.position f (toList xs)
.
map cmp' f xs
cmp
is a value of type 'a Sort.total_ordering
, cmp'
is a value of type 'b Sort.total_ordering
, and xs
is compatible with cmp
, then map
returns the set that is compatible with cmp'
and consists of the set of all f x
such that x
is in xs
, i.e., the set ys
such that, for all values y
of type 'b
, memb
cmp' (y, ys)
iff Sort.equal
cmp' (y, f x)
, for some value x
of type 'a
such that memb
cmp (x, xs)
.
mapFromList cmp f xs
cmp
is a value of type 'b total_ordering
, then mapFromList
returns fromList cmp (map f xs)
.
mapToList f xs
xs
is compatible with a value cmp
of type 'a Sort.total_ordering
, then mapToList
returns map f (toList xs)
.
union cmp (xs, ys)
xs
and ys
are compatible with cmp
, then union
returns the set that is compatible with cmp
and is the union of xs
and ys
, i.e., the set zs
such that, for all values z
of type 'a
, memb cmp (z, zs)
iff memb cmp (z, xs)
or memb cmp (z, ys)
.
genUnion cmp xss
xss
are compatible with cmp
, then genUnion
returns the set that is compatible with cmp
and is the generalized union of the elements of xss
, i.e., the set ys
such that, for all values y
of type 'a
, memb cmp (y, ys)
iff there is an element xs
of xss
such that memb cmp (y, xs)
.
inter cmp (xs, ys)
xs
and ys
are compatible with cmp
, then inter
returns the set that is compatible with cmp
and is the intersection of xs
and ys
, i.e., the set zs
such that, for all values z
of type 'a
, memb cmp (z, zs)
iff memb cmp (z, xs)
and memb cmp (z, ys)
.
genInter cmp xss
xss
are compatible with cmp
, then genInter
returns the set that is compatible with cmp
and is the generalized intersection of the elements of xss
, i.e., the set ys
such that, for all values y
of type 'a
, memb cmp (y, ys)
iff for all elements xs
of xss
, memb cmp (y, xs)
. An error message is issued when xss
is the empty list.
minus cmp (xs, ys)
xs
and ys
are compatible with cmp
, then minus
returns the set that is compatible with cmp
and is the difference of xs
and ys
, i.e., the set zs such that, for all values z
of type 'a
, memb cmp (z, zs)
iff memb cmp (z, xs)
and not(memb cmp (z, ys))
.
comparePair (cmp1, cmp2) ((x, y), (x', y'))
cmp1
on (x, x')
, and then using cmp2
on (y, y')
. I.e., it returns
case cmp1(x, x') of LESS => LESS | EQUAL => cmp2(y, y') | GREATER => GREATER
times(xs, ys)
xs
is compatible with a value cmp1
of type 'a Sort.total_ordering
, and ys
is compatible with a value cmp2
of type 'b Sort.total_ordering
, then times
returns the set that is compatible with comparePair(cmp1, cmp2)
and is the product of xs
and ys
, i.e., the set zs
such that, for all values p
of type 'a * 'b
, memb (compairPair(cmp1, cmp2)) (p, zs)
iff memb cmp1 (#1 p, xs)
and memb cmp2 (#2 p, ys)
.
compareTriple
comparePair
, but for triples.
times3
times
, but for triples, ordered using compareTriple
.
compareList cmp (xs, ys)
xs
and ys
, returning LESS
, if xs
is shorter than ys
, and GREATER
, if xs
is longer than ys
. When the lengths are equal, it works lexicographically, using cmp
to compare corresponding elements of xs
and ys
, and yielding the first non-EQUAL
result. If all comparisons result in EQUAL
, then compareList
returns EQUAL
.
genTimes xss
xss
are compatible with a value cmp
of type 'a Sort.total_ordering
, then genTimes
returns the set that is compatible with compareList cmp
and is the generalized product of the elements of xss
, i.e., the set yss
such that, for all values ys
of type 'a list
, memb (compareList cmp) (ys, yss)
iff length ys = length xss
and, for all 1 <= i <= length xss
, memb cmp (ListAux.sub(ys, i), ListAux.sub(xss, i))
.
Forlan Version 4.12
Copyright © 2019 Alley Stoughton