SIGNATURE StringIndex

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

IMPORT String ONLY string
       Char ONLY char
       Nat ONLY nat
       Option[nat] ONLY option

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

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

FUN slice       : string ** nat ** nat -> string                
                -- slice (s, i, j)
                -- substring of s from position i upto j where i <= j < #(s)
                -- range from 0 upto #(s) - 1 and i <= j 
                -- informally:
                -- slice (<...,c_i,...,c_i+n,...>, i, i+n) = <c_i,...,c_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 ** char ** string -> string
                -- upd(i, d, <c_0, ..., c_i, ..., c_n>) = 
                --		   <c_0, ..., d, ..., c_n>
                -- if i >= #(s), do nothing

FUN upd         : nat ** (char -> char) ** string -> string
                -- upd(i, f, <c_0, ..., c_i, ..., c_n>) = 
                --		   <c_0, ..., f(c_i), ..., c_n>
                -- if i >= #(s), do nothing

FUN swap        : nat ** nat ** string -> string
                -- swap(i, j, <c_0, ..., c_i, ..., c_j, ..., c_n>) =
                --	   <c_0, ..., c_j, ..., c_i, ..., c_n>
                -- undefined, if either i >= #(s) or j >= #(s)
                
FUN repl        : string ** nat ** string -> string
                -- repl(e, k, d) = r
                -- replace elements c_k, c_k+1, ... c_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      : string ** nat ** string -> string
                -- insert(e, k, d) = take(k, e) ++ d ++ drop(k, e)

FUN delete      : string ** nat ** nat  -> string       
                -- delete (s, i, j) 
                -- delete substring 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