SIGNATURE Array [data]

-- version 1.5

-- monolithic arrays with O(1) access and occassionaly O(1) update
-- NOTE: indices of arrays range from 0 upto the length - 1

-- Parameter
SORT data

IMPORT Nat ONLY nat

-- the type itself
SORT array

-- constructing new arrays

FUN init: nat**data->array                      
    init: nat**(nat->data)->array               
        -- init (n,d) === init (n,\\ _ .d)
        -- generate array of size n and initial 
        -- data f (i) for  i = 0 .. n-1
        -- informally:
        -- init (n,f) = [f(0)...f(n-1)]
        --		 ^0     ^n-1
        -- init (0, f) is the empty array

FUN empty: array
        -- the empty array

-- combining arrays

FUN ++ : array ** array -> array
        -- a1 ++ a2
        -- concatentation of two arrays

-- working on an array

FUN upd : nat**data**array->array               
    :=  : array**nat**data->array
        -- upd (i,d,a) === (a,i) := d
        -- update i-th element of array a with value d
        -- where i ranges from 0 upto #(a)-1

FUN upd : nat**(data->data)**array->array       
        -- upd (i,f,a) 
        -- update i-th element of array a with value f(a!i)
        -- where i ranges from 0 upto #(a)-1
 
FUN swap: array**nat**nat->array                
        -- swap(a,i,j)
        -- swap elements i and j of array a
        -- undefined, if either i >= #(a) or j >= #(a)

FUN delete: array ** nat ** nat  -> array
        -- delete (a, i, j)
        -- delete from position i upto j in d
        -- function is total; indices are occasionally truncated

FUN insert: array ** nat ** array -> array
        -- insert (d1, i, d2)
        -- insert denotation d2 in d1 at position i
        -- function is total; indices are occasionally truncated

FUN extend: array ** nat ** data -> array
    extend: array ** nat ** (nat -> data) -> array
        -- extend(a,n,d) === extend(a,n,\\ _ . d)
        -- extend array by n entrys at the end
        -- informally:
        -- extend(a,n,f) == a ++ init(n,f)

-- accessing elements of an array
FUN !   : array**nat->data                      
        -- a ! i  
        -- select i-th element of array a
        -- where i ranges from 0 upto #(a)-1

-- information about an array

FUN #   : array->nat    
        -- # (a)			
        -- size of array a
        -- example: # (init (0,d)) = 0

FUN empty? : array -> bool
        -- is the array empty?