SIGNATURE SeqIndex[data]

-- functions which use an "index" for accessing arbitary elements of a
-- 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
       Option[nat] ONLY option

FUN !           : seq ** nat -> data            
                -- s ! i
                -- select component at position i in s, where i ranges from 
                -- 0 upto #(s)-1	
                -- (positions of components in sequences are counted beginning
                -- from 0!)
                -- informally:
                -- <...,e_i,...> ! i = e_i
                --      ^i	
                -- undefined, if i >= #(s)

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

FUN slice       : seq ** nat ** nat -> seq              
                -- slice (s, i, j)
                -- subsequence of s from position i upto j where i <= j < #(s)
                -- range from 0 upto #(s) - 1 and i <= j 
                -- informally:
                -- slice (<...,e_i,...,e_i+n,...>, i, i+n) = <e_i,...,e_i+n>
                --	   ^0  ^i      ^i+n
                -- function is total: if i >= #(s) or i > j then result <>
                -- if j > #(s), assume j = #(s) - 1

FUN upd         : nat ** data ** seq -> seq
                -- upd(i, d, <e_0, ..., e_i, ..., e_n>) = 
                --		   <e_0, ..., d, ..., e_n>
                -- if i >= #(s), do nothing

FUN upd         : nat ** (data -> data) ** seq -> seq
                -- upd(i, f, <e_0, ..., e_i, ..., e_n>) = 
                --		   <e_0, ..., f(e_i), ..., e_n>
                -- if j > #(s), assume j = #(s) - 1

FUN swap        : nat ** nat ** seq -> seq
                -- swap(i, j, <e_0, ..., e_i, ..., e_j, ..., e_n>) =
                --	   <e_0, ..., e_j, ..., e_i, ..., e_n>
                -- undefined, if either i >= #(s) or j >= #(s)
                
FUN repl        : seq ** nat ** seq -> seq
                -- repl(<e_0, e_1, ..., e_n>, 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
                -- does nothing, if k > n
                -- replaces only upto e_n, truncates d, if k+m > n

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

FUN delete      : seq ** nat ** nat -> seq
                -- delete (s, i, j) 
                -- delete subsequence from position i upto j in s
                -- where i <= j < #(s)
                -- informally:
                -- delete ('...ab...cd...', i, i+n) 	= '...ad...'
                --		^i  ^i+n	
                -- function is total: if i > j, returns s
                -- if j >= #(s), assume = #(s)-1