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

IMPORT  Nat          ONLY nat
        Seq[data]    ONLY seq
        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 set

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

-- constructing a set from datas 

FUN % : data -> set                     
FUN % : data ** data -> set
FUN % : data ** data ** data -> set
FUN % : data ** data ** data ** data -> set
FUN % : data ** data ** data ** data ** data -> set
FUN % : data ** data ** data ** data ** data ** data -> set
FUN % : data ** data ** data ** data ** data ** data ** data -> set
FUN % : data ** data ** data ** data ** data ** data ** data ** data -> set
      --  %(d1, ..., dn) = {d1, ..., dn}

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

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

FUN iter : data ** (data -> data) ** (data -> 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 datas in a set
FUN arb      : set -> data                      -- select arbitrary element
                                                -- undefined for empty set

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

FUN min max  : set -> data          

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

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

FUN forall?  : (data -> 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

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

-- representation 

IMPORT Seq[data] ONLY seq

FUN abs: seq -> set
    rep: set -> seq