NatMapConv

Converting natMaps to/from sequences and to strings/denotations

Signature of NatMapConv

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

SIGNATURE NatMapConv[codom]

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

IMPORT NatMap[codom] ONLY natMap
       Seq[pair[nat, codom]] ONLY seq
       Pair[nat, codom] ONLY pair
       String ONLY string
       Nat ONLY nat

Parameter

nat and codom are the types of the map domain and codomain resp.

SORT codom

Converting to and from sequences

Transform natMap m into a sequence of pairs, each pair consisting of domain element and its associated codomain element. Informally, asSeq({d1 -> c1, ..., dn -> cn) = <&(d1, c1), ..., &(dn, cn)>}

FUN asSeq: natMap -> seq[pair]

Transform a sequence of pairs into a natMap; each pair has to consist of a nat and a codomain element. Informally, asNatMap(<&(d1, c1), ...,&(dn, cn)>) = {d1 -> c1, ..., dn -> cn}. If di = dj with i |= j, then asMap(..)!di may be either ci or cj.

FUN asNatMap: seq[pair] -> natMap

Converting to textual representation

`(d,c)({d1 -> c1, d2 -> c2, ..., dn -> cn}) == "{" d(d1) " -> " c(c1) "," d(d2) " -> " c(c2) "," ... "," d(dn) " -> " c(cn) "}"

FUN ` : (nat -> denotation) ** (codom -> denotation) -> natMap -> denotation
FUN ` : (nat -> string)     ** (codom -> string)     -> natMap -> string    

Here, you can replace "->", "{", "," "}" by your favourite denotations:
`(d,c)(m) == `("->")("{",",","}")(d,c)(m)

FUN ` : denotation -> denotation ** denotation ** denotation ->
        (nat -> denotation) ** (codom -> denotation) -> natMap -> denotation
FUN ` : denotation -> denotation ** denotation ** denotation ->
        (nat -> string)     ** (codom -> string)     -> natMap -> string

next node: NatMapFilter,
prev node: NatMapNotForUserPurpose,
up to node: Subsystem Mapping Natural Numbers