Maps

[
Type   maps
Funcon map
Funcon map-elements
Funcon map-lookup    Alias lookup
Funcon map-domain    Alias dom
Funcon map-override
Funcon map-unite
Funcon map-delete
]
Meta-variables
GT <: ground-values
T? <: values?
Built-in Type
maps(GT, T?)

maps(GT, T?) is the type of possibly-empty finite maps from values of type GT to optional values of type T?.

Built-in Funcon
map(_:(tuples(GT, T?))*) : =>(maps(GT, T?))?

map(tuple(K_1, V_1?), ..., tuple(K_n, V_n?)) constructs a map from K_1 to V_1?, …, K_n to V_n?, provided that K_1, …, K_n are distinct, otherwise the result is ( ).

Note that map(...) is not a constructor operation.

The built-in notation {K_1|->V_1?, ..., K_n|->V_n?} is equivalent to map(tuple(K_1, V_1?), ..., tuple(K_n, V_n?)). Note however that in general, maps cannot be identified with sets of tuples, since the values V_i? are not restricted to ground-values.

When T? <: types, maps(GT, T?) <: types. The type MT:maps(GT, T?) represents the set of value-maps MV:maps(GT, values?) such that dom(MV) is a subset of dom(MT) and for all K in dom(MV), map-lookup(MV, K) : map-lookup(MT, K).

Built-in Funcon
map-elements(_:maps(GT, T?)) : =>(tuples(GT, T?))*

The sequence of tuples (tuple(K_1, V_1?), ..., tuple(K_n, V_n?)) given by map-elements(M) contains each mapped value K_i just once. The order of the elements is unspecified, and may vary between maps.

Assert
map(map-elements(M)) == M
Built-in Funcon
map-lookup(_:maps(GT, T?), K:GT) : =>(T?)?
Alias
lookup = map-lookup

map-lookup(M,K) gives the optional value to which K is mapped by M, if any, and otherwise ( ).

Built-in Funcon
map-domain(_:maps(GT, T?)) : =>sets(GT)
Alias
dom = map-domain

map-domain(M) gives the set of values mapped by M.

map-lookup(M, K) is always ( ) when K is not in map-domain(M).

Built-in Funcon
map-override(_:(maps(GT, T?))*) : =>maps(GT,T?)

map-override(...) takes a sequence of maps. It returns the map whose domain is the union of their domains, and which maps each of those values to the same optional value as the first map in the sequence in whose domain it occurs . When the domains of the M* are disjoint, map-override(M*) is equivalent to map-unite(M*).

Built-in Funcon
map-unite(_:(maps(GT, T?))*) : =>(maps(GT, T?))?

map-unite(...) takes a sequence of maps. It returns the map whose domain is the union of their domains, and which maps each of those values to the same optional value as the map in the sequence in whose domain it occurs, provided that those domains are disjoint - otherwise the result is ( ).

Built-in Funcon
map-delete(_:maps(GT, T?), _:sets(GT)) : =>maps(GT, T?)

map-delete(M, S) takes a map M and a set of values S, and returns the map obtained from M by removing S from its domain.

Assert
map-domain(map-delete(M, S)) == set-difference(map-domain(M), S)

 From the PLanCompS Project CBS-beta issues… Suggest an improvement…