Module Gospelstdlib.Bag

Gospel declaration:
    type 'a t = 'a bag 

An alias for 'a bag.

Gospel declaration:
    function occurrences (x: 'a) (b: 'a t): integer 

occurrences x b is the number of occurrences of x in s.

Gospel declaration:
    function empty : 'a t 

empty is the empty bag.

Gospel declaration:
    predicate is_empty (b: 'a t) 

is_empty b is b = empty.

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

mem x b holds iff b contains x at least once.

Gospel declaration:
    function add (x: 'a) (b: 'a t) : 'a t 

add x b is b when an occurence of x was added.

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

singleton x is a bag containing one occurence of x.

Gospel declaration:
    function remove (x: 'a) (b: 'a t) : 'a t 

remove x b is b where an occurence of x was removed.

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

union b b' is a bag br where for all element x, occurences x br = max (occurences x b) (occurences x b').

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

sum b b' is a bag br where for all element x, occurences x br = (occurences x b) + (occurences x b').

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

inter b b' is a bag br where for all element x, occurences x br = min (occurences x b) (occurences x b').

Gospel declaration:
    predicate disjoint (b b': 'a t) 

disjoint b b' holds iff b and b' have no element in common.

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

diff b b' is a bag br where for all element x, occurences x br = max 0 (occurences x b - occurences x b').

Gospel declaration:
    predicate subset (b b': 'a t) 

subset b b' holds iff for all element x, occurences x b <= occurences x b'.

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

choose b is an arbitrary element of b.

Gospel declaration:
    function choose_opt (b: 'a t) : 'a option 

choose_opt b is an arbitrary element of b or None if b is empty.

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

map f b is a fresh bag which elements are f x1 ... f xN, where x1 ... xN are the elements of b.

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

fold f b a is (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of b.

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

for_all f b holds iff f x is true for all elements in b.

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

for_all f b holds iff f x is true for at least one element in b.

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

filter f b is the bag of all elements in b that satisfy f.

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

filter_map f b is the bag of all v such that f x = Some v for some element x of b.

Gospel declaration:
    function partition (f: 'a -> bool) (b: 'a t) : ('a t * 'a t) 

partition f b is the pair of bags (b1, b2), where b1 is the bag of all the elements of b that satisfy f, and b2 is the bag of all the elements of b that do not satisfy f.

Gospel declaration:
    function cardinal (b: 'a t) : integer 

cardinal b is the total number of elements in b, all occurrences being counted.

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

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

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

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