Agda.Utils.BiMap

Finite bijections (implemented as a pair of maps).

Documentation

data BiMap a b

Finite bijective map from a to b. There, and back again.

Constructors

BiMap

Fields

• biMapThere :: Map a b
• biMapBack :: Map b a

Instances

(Ord a, Ord b) => Eq (BiMap a b)

Methods

(==) :: BiMap a b -> BiMap a b -> Bool

(/=) :: BiMap a b -> BiMap a b -> Bool

(Ord a, Ord b) => Ord (BiMap a b)

Methods

compare :: BiMap a b -> BiMap a b -> Ordering

(<) :: BiMap a b -> BiMap a b -> Bool

(<=) :: BiMap a b -> BiMap a b -> Bool

(>) :: BiMap a b -> BiMap a b -> Bool

(>=) :: BiMap a b -> BiMap a b -> Bool

max :: BiMap a b -> BiMap a b -> BiMap a b

min :: BiMap a b -> BiMap a b -> BiMap a b

(Show a, Show b) => Show (BiMap a b)

Methods

showsPrec :: Int -> BiMap a b -> ShowS

show :: BiMap a b -> String

showList :: [BiMap a b] -> ShowS

(Ord a, Ord b, Arbitrary a, Arbitrary b) => Arbitrary (BiMap a b)

Methods

arbitrary :: Gen (BiMap a b)

shrink :: BiMap a b -> [BiMap a b]

lookup :: Ord a => a -> BiMap a b -> Maybe b

Lookup. O(log n).

invLookup :: Ord b => b -> BiMap a b -> Maybe a

Inverse lookup. O(log n).

empty :: BiMap a b

Empty bimap. O(1).

singleton :: a -> b -> BiMap a b

Singleton bimap. O(1).

insert :: (Ord a, Ord b) => a -> b -> BiMap a b -> BiMap a b

Insert. Overwrites existing value if present.

union :: (Ord a, Ord b) => BiMap a b -> BiMap a b -> BiMap a b

Left-biased Union. O(Map.union).

fromList :: (Ord a, Ord b) => [(a, b)] -> BiMap a b

Construct from a list of pairs.

Does not check for actual bijectivity of constructed finite map.

toList :: BiMap a b -> [(a, b)]

Turn into list, sorted ascendingly by first value.

Instances

Properties

prop_BiMap_invariant :: (Ord a, Ord b) => BiMap a b -> Bool

All tests

tests :: IO Bool