Safe Haskell	None
Language	Haskell2010

Agda.Utils.BiMap

Description

Finite bijections (implemented as a pair of tree maps).

Synopsis

Documentation

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

Constructors

BiMap
Fields biMapThere :: Map a b biMapBack :: Map b a

Instances details

(Ord a, Ord b) => Eq (BiMap a b) Source #
Instance details Defined in Agda.Utils.BiMap Methods (==) :: BiMap a b -> BiMap a b -> Bool # (/=) :: BiMap a b -> BiMap a b -> Bool #
(Ord a, Ord b) => Ord (BiMap a b) Source #
Instance details Defined in Agda.Utils.BiMap 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) Source #
Instance details Defined in Agda.Utils.BiMap Methods showsPrec :: Int -> BiMap a b -> ShowS # show :: BiMap a b -> String # showList :: [BiMap a b] -> ShowS #
(Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BiMap a b -> S Int32 Source # icod_ :: BiMap a b -> S Int32 Source # value :: Int32 -> R (BiMap a b) Source #

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

Lookup. O(log n).

Inverse lookup. O(log n).

Empty bimap. O(1).

Singleton bimap. O(1).

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

Insert. Overwrites existing value if present. O(Map.insert).

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

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

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

Construct from a list of pairs.

Does not check for actual bijectivity of constructed finite map. O(n log n)

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

Turn into list, sorted ascendingly by first value. O(Map.toList)