SIGNATURE BagConv[data, <]

-- converting bags

-- Parameter
SORT data
FUN <   : data ** data -> bool  
        -- total strict-order; in 
        --   ~(x < y) AND ~(y < x) => x = y
        -- should = represent semantic equality

IMPORT Bag[data, <]   ONLY bag
       Nat            ONLY nat
       Seq[data]      ONLY seq
       Pair[data,nat] ONLY pair
       Seq[pair]      ONLY seq
       String         ONLY string

FUN asSeq       : bag -> seq[data]      
                -- transform bag into sequence, 
                -- informally:
                -- explode ({{e1, ..., en}}) = <e1, ..., en>

FUN asBag       : seq[data] -> bag
                -- transform sequence into bag
                -- informally:
                -- implode (<e1, ..., en>) = {{e1, ..., en}}

FUN asSeqPair   : bag -> seq[pair]      
                -- transform bag into sequence of pairs under consideration
                -- of occurences; each pair consists of the element and its
                -- number of occurences
                -- informally:
                -- explode ({{e}} + b) = &(e, ct (e, b)) :: explode(exclAll(b))
                -- explode ({})      = <>

FUN asBag       : seq[pair] -> bag      
                -- transform sequence of pairs into bag under consideration 
                -- of occurences; each pair has to consist of an element and
                -- its number of occurences
                -- informally:
                -- implode (<(e1, i), ... (en, j)>) 
                --		= {{ e1, ..., e1, ..., en, ...en}}
                --		     ^^^^^^^^^^ i      ^^^^^^^^^ j occurences

FUN ` : (data -> denotation) -> bag -> denotation
FUN ` : (data -> string)     -> bag -> string

-- `(f)({{e1, e2, ..., en}}) == "{{" f(e1) "," f(e2) "," ... "," f(en) "}}"

-- old fashioned

FUN explode: bag -> seq[data]     -- explode == asSeq
FUN explodeCt: bag -> seq[pair]   -- eplodeCt == asSeqPair

FUN implode: seq[data] -> bag     -- implode == asBag
FUN implodeCt: seq[pair] -> bag