SIGNATURE ISeq[data]

-- inifinite sequences

-- Parameter
SORT data

IMPORT Nat ONLY nat
       Option[data] ONLY option
       Seq[data] ONLY seq       

-- the type itself
SORT iseq

-- constructing a seq from datas

FUN gen: data -> iseq   -- gen(d) == <d, d, d, ... >

FUN repeat: seq -> iseq -- repeat(s) == s ++ s ++ s ++ ...

FUN ::  : data ** iseq -> iseq -- prepend
FUN cons: data ** iseq -> iseq -- prepend (alternate name)
FUN +%  : iseq ** data -> iseq -- append at end

-- constructing a seq from a function
FUN ..         : nat -> (nat -> data) -> iseq
               -- (n .. )(f) = <f(n), f(n+1), ... >

FUN iter : data ** (data -> data)  -> iseq
                -- iter(start, it) == 
                --    <start,  it(start), ... >

-- combining sequences
FUN ++  :  seq ** iseq -> iseq 
FUN ++  : iseq ** iseq -> iseq  -- concat

FUN +/+ : data -> seq ** iseq -> iseq 
FUN +/+ : seq -> seq ** iseq -> iseq 

FUN +%+ : data -> seq ** iseq -> iseq 
FUN +%+ : seq -> seq ** iseq -> iseq 

-- working on a sequence

FUN take        : nat ** iseq -> seq                    
                -- take (k, s)
                -- take first k components of s
                -- informally:
                -- take (k, <e_0, ..., e_k-1, ...>) = <e_0, ..., e_k-1>

FUN drop        : nat ** iseq -> iseq                   
                -- drop (k, s)
                -- drop first k components of s
                -- informally:
                -- drop (k, <e_0, ..., e_k-1, e_k, ... >) 
                --				= <e_k, ..., e_n>

FUN split       : nat ** iseq -> seq ** iseq            
                -- split (n, s) = (take (n,s), drop (n,s))
                -- split s after n elements

FUN rt          : iseq -> iseq
                -- rt(<e_0, ..., e_n>) = <e_1, ..., e_n>

-- accessing datas in a sequence
FUN ft          : iseq -> data   
    
-- information about a sequence

FUN find?       : (data -> bool) ** iseq -> data
                -- find? (p, s)
                -- return some component of s fulfilling p

-- for compatibility reasons to finite sequences
-- though find?(p,s) can never return nil
FUN find?       : (data -> bool) ** iseq -> option[data]

-- not for user purpose (oder doch?)

FUN :: : (() -> data) ** (() -> iseq) -> iseq