SIGNATURE ISeqFilter[data]

-- functions for removing elements of an infinite sequence by 
-- a predicate on data
-- ** take care, that an infinite sequence is returned **

-- Parameter
SORT data

IMPORT ISeq[data] ONLY iseq
        Seq[data] ONLY seq

FUN |           : (data -> bool) ** iseq -> iseq        
                -- p | s
                -- filter: select all elements of b fulfilling predicate p

FUN partition   : (data -> bool) ** iseq -> iseq ** iseq
                -- partition (p, s) = (p | s, (\\x. ~(p(x))) | s)

FUN take        : (data -> bool) ** iseq -> seq 
                -- take (p, s1) = s2
                -- take all components of s1 (from left to right) fulfilling 
                -- predicate p just upto the first component, which does not
                -- fulfill p.

FUN drop        : (data -> bool) ** iseq -> iseq        
                -- drop (p, s1) = s2
                -- drop all components of s1 (from left to right) fulfilling
                -- predicate p just upto the first component, which does not
                -- fulfill p.
                
FUN split       : (data -> bool) ** iseq -> seq ** iseq 
                -- split (p, s) = (take (p,s), drop (p, s))
                -- split s before the first component (operating from left to 
                -- right) which does not fulfill predicate p.