MapByOS

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

This implementation is based on ordered sequences, which in general has good performance on operations on whole maps. Use this family of structures, if you absolutely want to rely on this implementation; otherwise you are advised to use the standard implementation of maps.

Signature of MapByOS

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

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

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

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(...def(M,d1,c1)...,dn,cn).

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(...def(M,d1,c1)...,dn,cn)}

FUN <+          : map ** map -> map                     

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

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

Accessing Codom - Elements

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

FUN !           : 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

-- representation 
IMPORT Pair[dom, codom] ONLY pair
       Set[pair[dom, codom], less] ONLY set

FUN less : pair ** pair -> bool
FUN abs: set[pair, less] -> map
FUN rep: map -> set[pair, less]

next node: MapByOSConv,
prev node: Subsystem Maps By Ordered Sequences,
up to node: Subsystem Maps By Ordered Sequences