SIGNATURE ArrayFilter[data]

--

-- Parameter
SORT data

IMPORT Array[data] ONLY array

FUN | : (data -> bool) ** array -> array
--  P | [e0,e1,...,en] == [e_i0, e_i1, ..., e_in] with P(e_ij)

FUN partition : (data -> bool) ** array -> array ** array
--  informally: partition(P, M) = (P |M, ~P |M)

FUN take        : (data -> bool) ** array -> array
                -- 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) ** array -> array      
                -- 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) ** array -> array ** array     
                -- 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.