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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.BiMap

Description

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

Synopsis

- data BiMap a b = BiMap {
  - biMapThere :: Map a b
  - biMapBack :: Map b a
  }
- lookup :: Ord a => a -> BiMap a b -> Maybe b
- invLookup :: Ord b => b -> BiMap a b -> Maybe a
- empty :: BiMap a b
- singleton :: a -> b -> BiMap a b
- insert :: (Ord a, Ord b) => a -> b -> BiMap a b -> BiMap a b
- union :: (Ord a, Ord b) => BiMap a b -> BiMap a b -> BiMap a b
- fromList :: (Ord a, Ord b) => [(a, b)] -> BiMap a b
- toList :: BiMap a b -> [(a, b)]

# Documentation

data BiMap a b Source #

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) Source # |
Instance details Defined in Agda.Utils.BiMap Methods (==) :: BiMap a b -> BiMap a b -> Bool Source # (/=) :: BiMap a b -> BiMap a b -> Bool Source #
(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 Source #

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

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

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

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

max :: BiMap a b -> BiMap a b -> BiMap a b Source #

min :: BiMap a b -> BiMap a b -> BiMap a b Source #

(Show a, Show b) => Show (BiMap a b) Source # |
Instance details Defined in Agda.Utils.BiMap Methods showsPrec :: Int -> BiMap a b -> ShowS Source # show :: BiMap a b -> String Source # showList :: [BiMap a b] -> ShowS Source #
(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).

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

Inverse lookup. O(log n).

empty :: BiMap a b Source #

Empty bimap. O(1).

singleton :: a -> b -> BiMap a b Source #

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)