TrieSet.md

TrieSet

Functional set

Sets are partial maps from element type to unit type, i.e., the partial map represents the set with its domain.

LIMITATIONS: This data structure allows at most MAX_LEAF_SIZE=8 hash collisions: attempts to insert more than MAX_LEAF_SIZE elements (whether directly via put or indirectly via other operations) with the same hash value will trap. This limitation is inherited from the underlying Trie data structure.

Type Hash

type Hash = Hash.Hash

Type Set

type Set<T> = Trie.Trie<T, ()>

Function empty

func empty<T>() : Set<T>

Empty set.

Function put

func put<T>(s : Set<T>, x : T, xh : Hash, eq : (T, T) -> Bool) : Set<T>

Put an element into the set.

Function delete

func delete<T>(s : Set<T>, x : T, xh : Hash, eq : (T, T) -> Bool) : Set<T>

Delete an element from the set.

Function equal

func equal<T>(s1 : Set<T>, s2 : Set<T>, eq : (T, T) -> Bool) : Bool

Test if two sets are equal.

Function size

func size<T>(s : Set<T>) : Nat

The number of set elements, set's cardinality.

Function isEmpty

func isEmpty<T>(s : Set<T>) : Bool

Test if s is the empty set.

Function isSubset

func isSubset<T>(s1 : Set<T>, s2 : Set<T>, eq : (T, T) -> Bool) : Bool

Test if s1 is a subset of s2.

Function mem

func mem<T>(s : Set<T>, x : T, xh : Hash, eq : (T, T) -> Bool) : Bool

@deprecated: use TrieSet.contains()

Test if a set contains a given element.

Function contains

func contains<T>(s : Set<T>, x : T, xh : Hash, eq : (T, T) -> Bool) : Bool

Test if a set contains a given element.

Function union

func union<T>(s1 : Set<T>, s2 : Set<T>, eq : (T, T) -> Bool) : Set<T>

Set union.

Function diff

func diff<T>(s1 : Set<T>, s2 : Set<T>, eq : (T, T) -> Bool) : Set<T>

Set difference.

Function intersect

func intersect<T>(s1 : Set<T>, s2 : Set<T>, eq : (T, T) -> Bool) : Set<T>

Set intersection.

Function fromArray

func fromArray<T>(arr : [T], elemHash : T -> Hash, eq : (T, T) -> Bool) : Set<T>

Function toArray

func toArray<T>(s : Set<T>) : [T]