Tab Module
signature TAB
structure Tab :> TAB
This module defines an abstract type of finite tables (maps).
type ('a,'b) tab
val lookup : 'a Sort.total_ordering -> ('a, 'b) tab * 'a -> 'b option
val isEmpty : ('a, 'b) tab -> bool
val empty : ('a, 'b) tab
val update : 'a Sort.total_ordering -> ('a, 'b) tab * ('a * 'b) list -> ('a, 'b) tab
val domain : 'a Sort.total_ordering -> ('a, 'b) tab -> 'a Set.set
val toList : ('a, 'b) tab -> ('a * 'b) list
val fromList : 'a Sort.total_ordering -> ('a * 'b) list -> ('a, 'b) tab
type ('a,'b) tab
'a to outputs of type 'b. A table of type ('a,
'b)tab can be understood as consisting of a finite set of bindings (x, y), for a value x of type 'a and a value y of type 'b, where, for a given value x, there is at most one binding with a left-hand side of x.
The module's values are specified with the help of the abstract proposition saying that a value tab of type ('a, 'b)tab is compatible with a value cmp of type 'a Sort.total_ordering.
lookup cmp (tab, x)
tab is compatible with cmp, then lookup returns NONE, if tab doesn't contain a binding whose left-hand side is x, and lookup returns SOME y, if tab contains the binding (x, y). Formally, the meaning of lookup must be understood in relation to the specifications of the other values of the module.
isEmpty tab
tab is compatible with a value cmp of type 'a Sort.total_ordering, then isEmpty tests whether tab is the table with no bindings, i.e., whether lookup cmp (tab, x) = NONE, for all values x of type 'a.
empty
cmp is a value of type 'a Sort.total_ordering, then empty is the table that is compatible with cmp and has no bindings, i.e., the table tab such that lookup cmp (tab, x) = NONE, for all values x of type 'a.
update cmp (tab, xs)
tab is compatible with cmp, then update returns a table that is compatible with cmp and consists of the union of the bindings of tab whose left-hand sides don't appear as left-hand sides in xs, and the bindings of xs whose left-hand sides don't appear as left-hand sides in subsequent bindings of xs, i.e., the table tab' that is compatible with cmp and such that, for all values x of type 'a:
1 <= i <= length xs such that Sort.equal cmp (#1(ListAux.sub(xs, i)), x), then lookup cmp (tab', x) =
lookup cmp (tab, x); and
1 <= i <= length xs, if Sort.equal cmp (#1(ListAux.sub(xs, i)), x), and there is no i < j <= length xs such that Sort.equal cmp (#1(ListAux.sub(xs, j)), x), then lookup cmp (tab', x) =
SOME(#2(ListAux.sub(xs, i))).
domain cmp tab
tab is compatible with cmp, then domain returns the set that is compatible with cmp and consists of the left-hand sides of the bindings of tab, i.e., the set xs such that, for all values x of type 'a, Set.memb cmp (xs, x) iff lookup cmp (tab, x) is not NONE.
toList tab
tab is compatible with a value cmp of type 'a Sort.total_ordering, then toList returns the list of bindings of tab, ordered according to their left-hand sides using cmp, i.e., the list xs such that:
1 <= i <= length xs - 1, Sort.less cmp (#1(ListAux.sub(xs, i)),
#1(ListAux.sub(xs, i + 1)));
y of type 'a and z of type 'b, if lookup cmp (tab, y) = SOME z, then there is an 1 <= i <= length xs such that ListAux.sub(xs, i) = (y, z); and
1 <= i <= length xs, lookup cmp (#1(ListAux.sub(xs, i))) =
SOME(#2(ListAux.sub(xs, i))).
fromList cmp xs
update cmp (empty, xs).
Forlan Version 4.15
Copyright © 2022 Alley Stoughton