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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.Bag

Contents

- Query
- Construction
- Destruction
- Traversal

Description

A simple overlay over Data.Map to manage unordered sets with duplicates.

Synopsis

- newtype Bag a = Bag {
  - bag :: Map a [a]
  }
- null :: Bag a -> Bool
- size :: Bag a -> Int
- (!) :: Ord a => Bag a -> a -> [a]
- member :: Ord a => a -> Bag a -> Bool
- notMember :: Ord a => a -> Bag a -> Bool
- count :: Ord a => a -> Bag a -> Int
- empty :: Bag a
- singleton :: a -> Bag a
- union :: Ord a => Bag a -> Bag a -> Bag a
- unions :: Ord a => [Bag a] -> Bag a
- insert :: Ord a => a -> Bag a -> Bag a
- fromList :: Ord a => [a] -> Bag a
- groups :: Bag a -> [[a]]
- toList :: Bag a -> [a]
- keys :: Bag a -> [a]
- elems :: Bag a -> [a]
- toAscList :: Bag a -> [a]
- map :: Ord b => (a -> b) -> Bag a -> Bag b
- traverse' :: forall a b m. (Applicative m, Ord b) => (a -> m b) -> Bag a -> m (Bag b)

# Documentation

newtype Bag a Source #

A set with duplicates. Faithfully stores elements which are equal with regard to (==).

Constructors

Bag |

Fields

- bag :: Map a [a]

  The list contains all occurrences of `a` (not just the duplicates!). Hence, the invariant: the list is never empty.

#### Instances

Instances details

Foldable Bag Source # |

Instance details

Defined in Agda.Utils.Bag

Methods

fold :: Monoid m => Bag m -> m Source #

foldMap :: Monoid m => (a -> m) -> Bag a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Bag a -> m Source #

foldr :: (a -> b -> b) -> b -> Bag a -> b Source #

foldr' :: (a -> b -> b) -> b -> Bag a -> b Source #

foldl :: (b -> a -> b) -> b -> Bag a -> b Source #

foldl' :: (b -> a -> b) -> b -> Bag a -> b Source #

foldr1 :: (a -> a -> a) -> Bag a -> a Source #

foldl1 :: (a -> a -> a) -> Bag a -> a Source #

toList :: Bag a -> [a] Source #

null :: Bag a -> Bool Source #

length :: Bag a -> Int Source #

elem :: Eq a => a -> Bag a -> Bool Source #

maximum :: Ord a => Bag a -> a Source #

minimum :: Ord a => Bag a -> a Source #

sum :: Num a => Bag a -> a Source #

product :: Num a => Bag a -> a Source #

Null (Bag a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: Bag a Source # null :: Bag a -> Bool Source #
Ord a => Monoid (Bag a) Source # |
Instance details Defined in Agda.Utils.Bag Methods mempty :: Bag a Source # mappend :: Bag a -> Bag a -> Bag a Source # mconcat :: [Bag a] -> Bag a Source #
Ord a => Semigroup (Bag a) Source # |
Instance details Defined in Agda.Utils.Bag Methods (<>) :: Bag a -> Bag a -> Bag a Source # sconcat :: NonEmpty (Bag a) -> Bag a Source # stimes :: Integral b => b -> Bag a -> Bag a Source #
Show a => Show (Bag a) Source # |
Instance details Defined in Agda.Utils.Bag Methods showsPrec :: Int -> Bag a -> ShowS Source # show :: Bag a -> String Source # showList :: [Bag a] -> ShowS Source #
Eq a => Eq (Bag a) Source # |
Instance details Defined in Agda.Utils.Bag Methods (==) :: Bag a -> Bag a -> Bool Source # (/=) :: Bag a -> Bag a -> Bool Source #
Ord a => Ord (Bag a) Source # |
Instance details Defined in Agda.Utils.Bag Methods compare :: Bag a -> Bag a -> Ordering Source # (<) :: Bag a -> Bag a -> Bool Source # (<=) :: Bag a -> Bag a -> Bool Source # (>) :: Bag a -> Bag a -> Bool Source # (>=) :: Bag a -> Bag a -> Bool Source # max :: Bag a -> Bag a -> Bag a Source # min :: Bag a -> Bag a -> Bag a Source #

# Query

null :: Bag a -> Bool Source #

Is the bag empty?

size :: Bag a -> Int Source #

Number of elements in the bag. Duplicates count. O(n).

(!) :: Ord a => Bag a -> a -> [a] Source #

`(bag ! a)` finds all elements equal to `a`. O(log n). Total function, returns `[]` if none are.

member :: Ord a => a -> Bag a -> Bool Source #

O(log n).

notMember :: Ord a => a -> Bag a -> Bool Source #

O(log n).

count :: Ord a => a -> Bag a -> Int Source #

Return the multiplicity of the given element. O(log n + count _ _).

# Construction

empty :: Bag a Source #

O(1)

singleton :: a -> Bag a Source #

O(1)

union :: Ord a => Bag a -> Bag a -> Bag a Source #

unions :: Ord a => [Bag a] -> Bag a Source #

insert :: Ord a => a -> Bag a -> Bag a Source #

    insert a b = union b (singleton a)

fromList :: Ord a => [a] -> Bag a Source #

    fromList = unions . map singleton

# Destruction

groups :: Bag a -> [[a]] Source #

Returns the elements of the bag, grouped by equality (==).

toList :: Bag a -> [a] Source #

Returns the bag, with duplicates.

keys :: Bag a -> [a] Source #

Returns the bag without duplicates.

elems :: Bag a -> [a] Source #

Returns the bag, with duplicates.

toAscList :: Bag a -> [a] Source #

# Traversal

map :: Ord b => (a -> b) -> Bag a -> Bag b Source #

traverse' :: forall a b m. (Applicative m, Ord b) => (a -> m b) -> Bag a -> m (Bag b) Source #