Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.VarSet

Description

Manage sets of natural numbers (de Bruijn indices).

Synopsis

- type VarSet = IntSet
- empty :: IntSet
- insert :: Key -> IntSet -> IntSet
- singleton :: Key -> IntSet
- union :: IntSet -> IntSet -> IntSet
- unions :: Foldable f => f IntSet -> IntSet
- fromList :: [Key] -> IntSet
- toList :: IntSet -> [Key]
- toAscList :: IntSet -> [Key]
- toDescList :: IntSet -> [Key]
- disjoint :: IntSet -> IntSet -> Bool
- isSubsetOf :: IntSet -> IntSet -> Bool
- member :: Key -> IntSet -> Bool
- null :: IntSet -> Bool
- delete :: Key -> IntSet -> IntSet
- difference :: IntSet -> IntSet -> IntSet
- filter :: (Key -> Bool) -> IntSet -> IntSet
- filterGE :: Int -> VarSet -> VarSet
- intersection :: IntSet -> IntSet -> IntSet
- mapMonotonic :: (Key -> Key) -> IntSet -> IntSet
- subtract :: Int -> VarSet -> VarSet

# Documentation

type VarSet = IntSet Source #

empty :: IntSet Source #

\(O(1)\). The empty set.

insert :: Key -> IntSet -> IntSet Source #

\(O(\min(n,W))\). Add a value to the set. There is no left- or right bias for IntSets.

singleton :: Key -> IntSet Source #

\(O(1)\). A set of one element.

union :: IntSet -> IntSet -> IntSet Source #

\(O(n+m)\). The union of two sets.

unions :: Foldable f => f IntSet -> IntSet Source #

The union of a list of sets.

fromList :: [Key] -> IntSet Source #

\(O(n \min(n,W))\). Create a set from a list of integers.

toList :: IntSet -> [Key] Source #

\(O(n)\). Convert the set to a list of elements. Subject to list fusion.

toAscList :: IntSet -> [Key] Source #

\(O(n)\). Convert the set to an ascending list of elements. Subject to list fusion.

toDescList :: IntSet -> [Key] Source #

\(O(n)\). Convert the set to a descending list of elements. Subject to list fusion.

disjoint :: IntSet -> IntSet -> Bool Source #

\(O(n+m)\). Check whether two sets are disjoint (i.e. their intersection is empty).

    disjoint (fromList [2,4,6])   (fromList [1,3])     == True
    disjoint (fromList [2,4,6,8]) (fromList [2,3,5,7]) == False
    disjoint (fromList [1,2])     (fromList [1,2,3,4]) == False
    disjoint (fromList [])        (fromList [])        == True

Since: containers-0.5.11

isSubsetOf :: IntSet -> IntSet -> Bool Source #

\(O(n+m)\). Is this a subset? `(s1 `isSubsetOf` s2)` tells whether `s1` is a subset of `s2`.

member :: Key -> IntSet -> Bool Source #

\(O(\min(n,W))\). Is the value a member of the set?

null :: IntSet -> Bool Source #

\(O(1)\). Is the set empty?

delete :: Key -> IntSet -> IntSet Source #

\(O(\min(n,W))\). Delete a value in the set. Returns the original set when the value was not present.

difference :: IntSet -> IntSet -> IntSet Source #

\(O(n+m)\). Difference between two sets.

filter :: (Key -> Bool) -> IntSet -> IntSet Source #

\(O(n)\). Filter all elements that satisfy some predicate.

filterGE :: Int -> VarSet -> VarSet Source #

Keep only elements greater or equal to the given pivot.

intersection :: IntSet -> IntSet -> IntSet Source #

\(O(n+m)\). The intersection of two sets.

mapMonotonic :: (Key -> Key) -> IntSet -> IntSet Source #

\(O(n)\). The

``mapMonotonic` f s == `map` f s`, but works only when `f` is strictly increasing. The precondition is not checked. Semi-formally, we have:

    and [x < y ==> f x < f y | x <- ls, y <- ls]
                        ==> mapMonotonic f s == map f s
        where ls = toList s

Since: containers-0.6.3.1

subtract :: Int -> VarSet -> VarSet Source #

Subtract from each element.