Module Gospelstdlib.Sequence

Gospel declaration:
    type 'a t = 'a sequence 

An alias for sequence

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

length s is the length of the sequence s.

Gospel declaration:
    function empty : 'a t 

empty is the empty sequence.

Gospel declaration:
    function singleton (x: 'a) : 'a t 

singleton is an alias for return.

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

init n f is the sequence containing f 0, f 1, ... , f n.

Gospel declaration:
    function cons (x: 'a) (s: 'a t): 'a t 

cons x s is the sequence containing x followed by the elements of s.

Gospel declaration:
    function snoc (s: 'a t) (x: 'a): 'a t 

snoc s x is the sequence containing the elements of s followed by x.

Gospel declaration:
    function hd (s: 'a t) : 'a 

When s contains one or more elements, hd s is the first element of s.

Gospel declaration:
    function tl (s: 'a t) : 'a t 

When s contains one or more elements, tl s is the sequence of the elements of s, starting at position 2.

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

append s s' is s ++ s'.

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

mem s x holds iff x is in s.

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

map f s is a sequence whose elements are the elements of s, transformed by f.

Gospel declaration:
    function filter (f: 'a -> bool) (s: 'a t) : 'a t 

filter f s is a sequence whose elements are the elements of s, that satisfy f.

Gospel declaration:
    function filter_map (f: 'a -> 'b option) (s: 'a t) : 'b t 

filter_map f s is a sequence whose elements are the elements of s, transformed by f. An element x is dropped whenever f x is None.

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

get s i is s[i].

Gospel declaration:
    function set (s: 'a t) (i: integer) (x: 'a): 'a t 

set s i x is the sequence s where the ith element is x.

Gospel declaration:
    function rev (s: 'a t) : 'a t 

rev s is the sequence containing the same elements as s, in reverse order.

Gospel declaration:
    function rec fold_left (f: 'a -> 'b -> 'a) (acc: 'a) (s: 'b sequence) : 'a 

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

Gospel declaration:
    function rec fold_right (f: 'a -> 'b -> 'b) (s: 'a t) (acc: 'b) : 'b 

fold_right f s acc is f s[1] (f s[2] (... (f s[n] acc) ...)) where n is the length of s.