Agda.Utils.BiMap

Partial injections from a type to some tag type.

The idea is that tag should be injective on its domain: if tag x = tag y = Just i, then x = y. However, this property does not need to hold globally. The preconditions of the BiMap operations below specify for which sets of values tag must be injective.

Checks if the function tag is injective for the values in the given list for which the function is defined.

Finite maps from k to v, with a way to quickly get from v to k for certain values of type v (those for which tag is defined).

Every value of this type must satisfy biMapInvariant.

The invariant for BiMap.

Is the value a source key? O(log n).

Is the value a target key? O(log n).

Lookup. O(log n).

Inverse lookup. O(log n).

Singleton map. O(1).

Insertion. Overwrites existing values. O(log n).

Precondition: See insertPrecondition.

The precondition for insert k v m: If v has a tag (tag v ≠ Nothing), then m must not contain any mapping k' ↦ v' for which k ≠ k' and tag v = tag v'.

Modifies the value at the given position, if any. If the function returns Nothing, then the value is removed. O(log n).

The precondition for alterM f k m is that, if the value v is inserted into m, and tag v is defined, then no key other than k may map to a value v' for which tag v' = tag v.

Modifies the value at the given position, if any. If the function returns Nothing, then the value is removed. O(log n).

Precondition: See alterPrecondition.

The precondition for alter f k m is that, if the value v is inserted into m, and tag v is defined, then no key other than k may map to a value v' for which tag v' = tag v.

Modifies the value at the given position, if any. If the function returns Nothing, then the value is removed. O(log n).

Precondition: See updatePrecondition.

The precondition for update f k m is that, if the value v is inserted into m, and tag v is defined, then no key other than k may map to a value v' for which tag v' = tag v.

Modifies the value at the given position, if any. O(log n).

Precondition: See adjustPrecondition.

The precondition for adjust f k m is that, if the value v is inserted into m, and tag v is defined, then no key other than k may map to a value v' for which tag v' = tag v.

Inserts a binding into the map. If a binding for the key already exists, then the value obtained by applying the function to the key, the new value and the old value is inserted, and the old value is returned.

Precondition: See insertLookupWithKeyPrecondition.

The precondition for insertLookupWithKey f k v m is that, if the value v' is inserted into m, and tag v' is defined, then no key other than k may map to a value v'' for which tag v'' = tag v'.

Changes all the values using the given function, which is also given access to keys. O(n log n).

Precondition: See mapWithKeyPrecondition.

The precondition for mapWithKey f m: For any two distinct mappings k₁ ↦ v₁, k₂ ↦ v₂ in m for which the tags of f k₁ v₁ and f k₂ v₂ are defined the values of f must be distinct (f k₁ v₁ ≠ f k₂ v₂). Furthermore tag must be injective for { f k v | (k, v) ∈ m }.

Changes all the values using the given function, which is also given access to keys. O(n).

Precondition: See mapWithKeyFixedTagsPrecondition. Note that tags must not change.

The precondition for mapWithKeyFixedTags f m is that, if m maps k to v, then tag (f k v) == tag v.

Left-biased union. For the time complexity, see union.

Precondition: See unionPrecondition.

Conversion from lists of pairs. Later entries take precedence over earlier ones. O(n log n).

Precondition: See fromListPrecondition.

Conversion to lists of pairs, with the keys in ascending order. O(n).

The keys, in ascending order. O(n).

The values, ordered according to the corresponding keys. O(n).

Conversion from two lists that contain distinct keys/tags, with the keys/tags in ascending order. O(n).

Precondition: See fromDistinctAscendingListsPrecondition.

Generates input suitable for fromDistinctAscendingLists. O(n).