Module Gospelstdlib.Array

Gospel declaration:
    type 'a t = 'a array 

An alias for the type of arrays.

Gospel declaration:
    function length (a: 'a t) : integer 

length a is the number of elements of a.

Gospel declaration:
    function get (a: 'a t) (i: integer) : 'a 

get a i is the element number i of array a.

Gospel declaration:
    function make (n: integer) (x: 'a) : 'a t 

make n x is an array of length n, initialized with x.

Gospel declaration:
    function init (n: integer) (f: integer -> 'a) : 'a t 

init n f is an array of length n, with element number i initialized to the result of f i.

Gospel declaration:
    function append (a b: 'a t) : 'a t 

append v1 v2 returns an array containing the concatenation of v1 and v2.

Gospel declaration:
    function concat (a: 'a t list) : 'a t 

Same as append, but concatenates a list of arrays.

Gospel declaration:
    function sub (a: 'a t) (i len: integer) : 'a t 

sub a pos len is the array of length len, containing the elements number pos to pos + len - 1 of array a.

Gospel declaration:
    function map (f: 'a -> 'b) (a: 'a t) : 'b t 

map f a applies function f to all the elements of a, and builds an array with the results returned by f

Gospel declaration:
    function mapi (f: integer -> 'a -> 'b) (a: 'a t) : 'b t 

Same as map, but the function is applied to the index of the element as first argument, and the element itself as second argument.

Gospel declaration:
    function fold_left (f: 'a -> 'b -> 'a) (init: 'a) (a: 'b t) : 'a 

fold_left f init a is f (... (f (f init a[0]) a[1]) ...) a[n-1], where n is the length of a.

Gospel declaration:
    function fold_right (f: 'b -> 'a -> 'a) (a: 'b t) (init: 'a) : 'a 

fold_right f a init is f a[0] (f a[1] ( ... (f a[n-1] init) ...)), where n is the length of a.

Gospel declaration:
    function map2 (f: 'a -> 'b -> 'c) (a: 'a t) (b: 'b t) : 'c t 

map2 f a b applies function f to all the elements of a and b, and builds an array with the results returned by f.

Gospel declaration:
    predicate for_all (f: 'a -> bool) (a: 'a t) 

for_all f a holds iff all elements of a satisfy the predicate f.

Gospel declaration:
    predicate _exists (f: 'a -> bool) (a: 'a t) 

_exists f a holds iff at least one element of a satisfies f.

Gospel declaration:
    predicate for_all2 (f: 'a -> 'b -> bool) (a: 'a t) (b: 'b t) 

Same as for_all, but for a two-argument predicate.

Gospel declaration:
    predicate _exists2 (f: 'a -> 'b -> bool) (a: 'a t) (b: 'b t) 

Same as _exists, but for a two-argument predicate.

Gospel declaration:
    predicate mem (x: 'a) (a: 'a t) 

mem x a holds iff x is equal to an element of a

Gospel declaration:
    function to_list (a: 'a t) : 'a list 

Gospel declaration:
    function of_list (l: 'a list) : 'a t 

Gospel declaration:
    function to_seq (a: 'a t) : 'a Sequence.t 
    coercion 

Gospel declaration:
    function of_seq (s: 'a Sequence.t) : 'a t 

Gospel declaration:
    function to_bag (a: 'a t) : 'a bag 

Gospel declaration:
    predicate permut (a b: 'a array) 

permut a b is true iff a and b contain the same elements with the same number of occurrences

Gospel declaration:
    predicate permut_sub (a b: 'a array) (lo hi: integer) 

permut_sub a b lo hi is true iff the segment `a1.(lo..hi-1)` is a permutation of the segment `a2.(lo..hi-1)` and values outside of the interval are equal.