SIGNATURE Bitset 

-- sets of natural numbers implemented as dynamically growing
-- monolithic bitmaps

IMPORT  Nat        ONLY nat
        Option[nat] ONLY option

-- the type itself 
SORT set

 
-- non free constructors
FUN {}       : set                              -- empty set
FUN incl     : nat ** set->set                  -- include

-- constructing a set from nats 

FUN % : nat -> set                      
FUN % : nat ** nat -> set
FUN % : nat ** nat ** nat -> set
FUN % : nat ** nat ** nat ** nat -> set
FUN % : nat ** nat ** nat ** nat ** nat -> set
FUN % : nat ** nat ** nat ** nat ** nat ** nat -> set
FUN % : nat ** nat ** nat ** nat ** nat ** nat ** nat -> set
FUN % : nat ** nat ** nat ** nat ** nat ** nat ** nat ** nat -> set
      

FUN incl excl: nat ** set -> set         -- include/exclude

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

FUN iter : nat ** (nat -> nat) ** (nat -> bool) -> set
                -- 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 sets
FUN + - *    : set ** set -> set                -- union/diff./intersection

-- accessing nats in a set
FUN arb      : set -> nat                       -- select arbitrary element
                                                -- undefined for empty set

-- information about a set
FUN {}?      : set -> bool                      -- test for empty set
FUN in       : nat ** set -> bool               -- membership
FUN #        : set -> nat                       -- cardinality

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

FUN find?       : (nat -> bool) ** set -> option[nat]
                -- find? (p, s)
                -- return some element of s fulfilling p

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

-- comparing sets
FUN = <= <   : set**set->bool           -- equality/subset/proper subset

FUN {<}      : set ** set -> bool       -- ordering on sets