Map

This structure defines the data type of mappings from a domain to a codomain.

The implementation currently is based on balanced search trees, which gives good performance on single element operations such as def, undef and ! (select), but not on operations on whole maps, such as <+.

The implementation may change in future revisions. If you want to make sure that you use maps based on balanced search trees, you can use the MapByBST family of structures.

Signature of Map

List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
See Pair
See Seq
See Set

SIGNATURE Map [dom:SORT,< : dom ** dom -> bool,codom: SORT]

$Date: 2011-12-07 16:04:45 +0100 (Mi, 07. Dez 2011) $ ($Revision: 788 $)

IMPORT Nat              ONLY nat
       Option[codom]    ONLY option
       Set[dom,<]       ONLY set
       Seq[dom]         ONLY seq
       Seq[codom]       ONLY seq
       Pair[dom, codom] ONLY pair
       Option[pair]     ONLY option

Parameter

dom is the type of the domain, codom the type of the codomain. < is a total strict order: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold.

SORT dom codom
FUN <   : dom ** dom -> bool

The Type Itself

SORT map

Nonfree Constructors

The empty map.

FUN {}          : map   

(Re)define map at point.

FUN def         : dom ** codom ** map -> map

Constructing a Map From Datas

(Re)define resp. undefine map at point.

FUN def         : dom ** codom ** map -> map
    undef       : dom ** map -> map

In upd (d, f, m), redefine m at d by f(m!d)

FUN upd         : dom ** (codom -> codom) ** map -> map 

Best explained informally: extend (M, <d1, ..., dn>, <c1, ..., cn>) results def(d1,c1, def(..., def(dn,cn,M)...)).

FUN extend      : map ** seq[dom] ** seq[codom]->map

Constructing a Map From a Function

(n1 .. n2)(f,g) == {f(n1) -> g(f(n1)), ... , f(n2) -> g(f(n2))}

FUN ..          : nat ** nat -> (nat -> dom) ** (dom -> codom) -> map

Generate elements of the domain from start upto (excluding) the first element, for which P(it^x(start)) does not hold. The function f assigns to each element of the domain the associated codom element.

FUN iter        : dom ** (dom -> dom) ** (dom -> bool) -> (dom -> codom) -> map

Add for every element d of the set the maplet d -> f(d) to the map

FUN init        : set[dom, <] ** (dom -> codom) -> map

Combining Maps

Lifting of def to maps. Informally, M <+ {d1->c1,...,dn -> cn} = def(d1, c1, def( ..., def(dn, cn, M)...))

FUN <+          : map ** map -> map                     

Lifting of undef to sets. Informally, M <- {d1,...,dn} = undef(d1, undef( ..., undef(dn, M)...))

FUN <-          : map ** set[dom,<] -> map

Accessing Codom - Elements

m!d: give associated value to d in m which must exist

FUN !           : map ** dom -> codom     

!(default)(m!d): return default, if not d in dom(m). Otherwise like ordinary !.

FUN !           : codom -> map ** dom -> codom      

m !? d: give associated value to d in m, if it exists, else nil

FUN !?          : map ** dom -> option[codom]

Information About a Map

test for empty map

FUN {}?         : map -> bool

test for definedness

FUN def?        : dom ** map -> bool

domain of the map. Informally, dom ( {d1->c1,...,dn -> cn} ) = {d1, ..., dn}

FUN dom         : map -> set[dom,<]   

Codomain of the map. Note that this is a sequence and not a set!

FUN codom       : map -> seq[codom]

cardinality of dom(m)

FUN #           : map -> nat                    

exist?(P, M): is there d in dom(M) with P(d, M!d) ?

FUN exist?      : (dom ** codom -> bool) ** map -> bool

find?(P, M): return avail(c, d) for some c->d in M for which P holds

FUN find?       : (dom ** codom -> bool) ** map -> option[pair]

forall?(P, M): does P hold for every (d, r) in M ?

FUN forall?     : (dom ** codom -> bool) ** map -> bool

not for user purpose

see structure MapNotForUSerPurpose

next node: MapNotForUserPurpose,
prev node: Subsystem Maps Proper,
up to node: Subsystem Maps Proper