SIGNATURE Bag [data,< : data**data->bool]

-- multisets 

IMPORT  Nat             ONLY nat
        Pair[data,nat]  ONLY pair
        Option[data]    ONLY option

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

-- The type itself 
SORT bag

 
-- non free constructors
FUN {}       : bag                              -- empty bag
FUN incl     : data ** bag->bag                 -- include

-- constructing a bag from datas 

FUN % : data -> bag                     
FUN % : data ** data -> bag
FUN % : data ** data ** data -> bag
FUN % : data ** data ** data ** data -> bag
FUN % : data ** data ** data ** data ** data -> bag
FUN % : data ** data ** data ** data ** data ** data -> bag
FUN % : data ** data ** data ** data ** data ** data ** data -> bag
FUN % : data ** data ** data ** data ** data ** data ** data ** data -> bag
      

FUN incl excl: data ** bag -> bag        -- include/exclude
FUN inclCt   : data ** nat ** bag -> bag -- include ct times
FUN exclAll  : data ** bag -> bag        -- exclude all occurrences

-- constructing a bag from a function
FUN .. : nat ** nat -> (nat -> data) -> bag
       -- (n1 .. n2)(f) = {{ f(n1), f(n1 + 1), ..., f(n2) }}

FUN iter : data ** (data -> data) ** (data -> bool) -> bag
                -- iter(start, it, P) == 
                --    {{start,  it(start), ... it^n(start)}}
                -- where P(it^i(start)) for 0 <= i <= n
                -- and ~(P(it^(n+1)(start)))

-- combining bags
FUN + - *    : bag ** bag -> bag                -- union/diff./intersection
FUN U        : bag**bag->bag            
                -- union taking maximal occurrences of all elements

-- accessing datas in a bag
FUN arb      : bag -> data                      -- select arbitrary element
                                                -- undefined for empty bag

-- information about a bag
FUN {}?      : bag -> bool                      -- test for empty bag
FUN in       : data ** bag -> bool              -- membership
FUN #        : bag -> nat                       -- cardinality
FUN ct       : data ** bag -> nat               -- number of occurrences

FUN exist?   : (data -> bool) ** bag->bool      
                -- exist? (p, s)
                -- is there any element of b fulfilling predicate p?

FUN find?       : (data -> bool) ** bag -> option[data]
                -- find? (p, s)
                -- return some component of s fulfilling p

FUN forall?  : (data -> bool) ** bag->bool  
                -- forall? (p, s) 
                -- do all elements of s fulfill predicate p?

-- comparing bags
FUN = <= <   : bag ** bag -> bool       -- equality/subbag/proper subbag

-- not for user purpose -----------------------------------------------

-- representation 

IMPORT  Seq[pair]       ONLY seq

FUN abs: seq -> bag
    rep: bag -> seq