MapByBSTConv

Converting maps to/from sequences and to strings/denotations

Signature of MapByBSTConv

List of Import References :
See BOOL
See BSTree
See Char
See DENOTATION
See MapByBST
See Nat
See Option
See Pair
See Seq
See SetByBST
See String
See Tree

SIGNATURE MapByBSTConv[dom, <, codom]

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

IMPORT MapByBST[dom, <, codom] ONLY map
       Seq[pair[dom, codom]] ONLY seq
       Pair[dom, codom] ONLY pair
       String ONLY string

Parameter

dom and codom are the types of the map domain and codomain resp. < 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

Converting to and from Sequences

Transform map 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: map -> seq[pair]

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

FUN asMap: seq[pair] -> map

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 ` : (dom -> denotation) ** (codom -> denotation) -> map -> denotation
FUN ` : (dom -> string)     ** (codom -> string)     -> map -> string    

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

FUN ` : denotation -> denotation ** denotation ** denotation ->
        (dom -> denotation) ** (codom -> denotation) -> map -> denotation
FUN ` : denotation -> denotation ** denotation ** denotation ->
        (dom -> string)     ** (codom -> string)     -> map -> string

next node: MapByBSTFilter,
prev node: MapByBST,
up to node: Subsystem Maps By Binary Search Trees