SIGNATURE ISeqIndex[data]

-- functions which use an "index" for accessing arbitary elements of an
-- infinite sequence
-- note, that some of these functions are quite expensive and therefore
-- should be avoided, if possible

-- Parameter
SORT data

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

FUN !           : iseq ** nat -> data           
                -- s ! i
                -- select component at position i in s
                -- (positions of components in sequences are counted beginning
                -- from 0!)
                -- informally:
                -- <...,e_i,...> ! i = e_i
                --      ^i	

FUN pos         : (data -> bool) ** iseq -> nat
FUN pos         : (data -> bool) ** iseq -> option[nat]
                -- pos(P, s)
                -- return avail(n), for first component of s which fulfills
                -- predicate P

FUN slice       : iseq ** nat ** nat -> seq             
                -- slice (s, i, j)
                -- subsequence of s from position i upto j where i <= j 
                -- informally:
                -- slice (<...,e_i,...,e_i+n,...>, i, i+n) = <e_i,...,e_i+n>
                --	   ^0  ^i      ^i+n

FUN upd         : nat ** data ** iseq -> iseq
                -- upd(i, d, <e_0, ..., e_i, ..., e_n>) = 
                --		   <e_0, ..., d, ..., e_n>

FUN upd         : nat ** (data -> data) ** iseq -> iseq
                -- upd(i, f, <e_0, ..., e_i, ..., e_n>) = 
                --		   <e_0, ..., f(e_i), ..., e_n>

FUN swap        : nat ** nat ** iseq -> iseq
                -- swap(i, j, <e_0, ..., e_i, ..., e_j, ..., e_n>) =
                --	   <e_0, ..., e_j, ..., e_i, ..., e_n>
                
FUN repl        : iseq ** nat ** seq -> iseq
                -- repl(<e_0, e_1, ... >, k, <d_0, d_1, ..., d_m>) = r
                -- replace elements e_k, e_k+1, ... e_k+m by 
                --				d_0, d_1, ..., d_m

FUN insert      : iseq ** nat ** seq -> iseq
                -- insert(e, k, d) = take(k, e) ++ d ++ drop(k, e)

FUN delete      : iseq ** nat ** nat -> iseq
                -- delete (s, i, j) 
                -- delete subsequence from position i upto j in s
                -- where i <= j 
                -- informally:
                -- delete ('...ab...cd...', i, i+n) 	= '...ad...'
                --		^i  ^i+n	
                -- has no effect, if i > j