Agda.Utils.BiMap

Partly invertible finite maps.

Time complexities are given under the assumption that all relevant instance functions, as well as arguments of function type, take constant time, and "n" is the number of keys involved in the operation.

Documentation

class HasTag a where

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.

Associated Types

type Tag a

Methods

tag :: a -> Maybe (Tag a)

Instances

HasTag ModuleNameHash

Defined in Agda.Syntax.Common

Associated Types

type Tag ModuleNameHash

Methods

tag :: ModuleNameHash -> Maybe (Tag ModuleNameHash)

HasTag TopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Associated Types

type Tag TopLevelModuleName

Methods

tag :: TopLevelModuleName -> Maybe (Tag TopLevelModuleName)

HasTag InteractionPoint

Defined in Agda.TypeChecking.Monad.Base

Associated Types

type Tag InteractionPoint

Methods

tag :: InteractionPoint -> Maybe (Tag InteractionPoint)

tagInjectiveFor :: (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool

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

data BiMap k v

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.

Constructors

BiMap

Fields

• biMapThere :: !(Map k v)
• biMapBack :: !(Map (Tag v) k)

Instances

NFData InteractionPoints

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: InteractionPoints -> ()

(EmbPrj k, EmbPrj v, EmbPrj (Tag v)) => EmbPrj (BiMap k v)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BiMap k v -> S Int32

icod_ :: BiMap k v -> S Int32

value :: Int32 -> R (BiMap k v)

Null (BiMap k v)

Defined in Agda.Utils.BiMap

Methods

empty :: BiMap k v

null :: BiMap k v -> Bool

Generic (BiMap k v)

Defined in Agda.Utils.BiMap

Associated Types

type Rep (BiMap k v) :: Type -> Type

Methods

from :: BiMap k v -> Rep (BiMap k v) x

to :: Rep (BiMap k v) x -> BiMap k v

(Show k, Show v) => Show (BiMap k v)

Defined in Agda.Utils.BiMap

Methods

showsPrec :: Int -> BiMap k v -> ShowS

show :: BiMap k v -> String

showList :: [BiMap k v] -> ShowS

NFData (BiMap RawTopLevelModuleName ModuleNameHash)

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> ()

(Eq k, Eq v) => Eq (BiMap k v)

Defined in Agda.Utils.BiMap

Methods

(==) :: BiMap k v -> BiMap k v -> Bool

(/=) :: BiMap k v -> BiMap k v -> Bool

(Ord k, Ord v) => Ord (BiMap k v)

Defined in Agda.Utils.BiMap

Methods

compare :: BiMap k v -> BiMap k v -> Ordering

(<) :: BiMap k v -> BiMap k v -> Bool

(<=) :: BiMap k v -> BiMap k v -> Bool

(>) :: BiMap k v -> BiMap k v -> Bool

(>=) :: BiMap k v -> BiMap k v -> Bool

max :: BiMap k v -> BiMap k v -> BiMap k v

min :: BiMap k v -> BiMap k v -> BiMap k v

type Rep (BiMap k v)

Defined in Agda.Utils.BiMap

type Rep (BiMap k v) = D1 ('MetaData "BiMap" "Agda.Utils.BiMap" "Agda-2.6.2.2.20221106-inplace" 'False) (C1 ('MetaCons "BiMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "biMapThere") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map k v)) :*: S1 ('MetaSel ('Just "biMapBack") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map (Tag v) k))))

biMapInvariant :: (Eq k, Eq v, Ord (Tag v), HasTag v) => BiMap k v -> Bool

The invariant for BiMap.

source :: Ord k => k -> BiMap k v -> Bool

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

target :: Ord (Tag v) => Tag v -> BiMap k v -> Bool

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

lookup :: Ord k => k -> BiMap k v -> Maybe v

Lookup. O(log n).

invLookup :: Ord (Tag v) => Tag v -> BiMap k v -> Maybe k

Inverse lookup. O(log n).

singleton :: HasTag v => k -> v -> BiMap k v

Singleton map. O(1).

insert :: (Ord k, HasTag v, Ord (Tag v)) => k -> v -> BiMap k v -> BiMap k v

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

Precondition: See insertPrecondition.

insertPrecondition :: (Eq k, Eq v, Eq (Tag v), HasTag v) => k -> v -> BiMap k v -> Bool

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'.

alterM :: forall k v m. (Ord k, Ord (Tag v), HasTag v, Monad m) => (Maybe v -> m (Maybe v)) -> k -> BiMap k v -> m (BiMap k 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.

alter :: forall k v. (Ord k, Ord (Tag v), HasTag v) => (Maybe v -> Maybe v) -> k -> BiMap k v -> BiMap k 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.

alterPrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => (Maybe v -> Maybe v) -> k -> BiMap k v -> Bool

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.

update :: (Ord k, Ord (Tag v), HasTag v) => (v -> Maybe v) -> k -> BiMap k v -> BiMap k 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.

updatePrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => (v -> Maybe v) -> k -> BiMap k v -> Bool

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.

adjust :: (Ord k, Ord (Tag v), HasTag v) => (v -> v) -> k -> BiMap k v -> BiMap k v

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

Precondition: See adjustPrecondition.

adjustPrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => (v -> v) -> k -> BiMap k v -> Bool

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.

insertLookupWithKey :: forall k v. (Ord k, Ord (Tag v), HasTag v) => (k -> v -> v -> v) -> k -> v -> BiMap k v -> (Maybe v, BiMap k 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.

insertLookupWithKeyPrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => (k -> v -> v -> v) -> k -> v -> BiMap k v -> Bool

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'.

mapWithKey :: (Ord k, Ord (Tag v), HasTag v) => (k -> v -> v) -> BiMap k v -> BiMap k v

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

Precondition: See mapWithKeyPrecondition.

mapWithKeyPrecondition :: (Eq k, Eq v, Eq (Tag v), HasTag v) => (k -> v -> v) -> BiMap k v -> Bool

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 }.

mapWithKeyFixedTags :: (k -> v -> v) -> BiMap k v -> BiMap k v

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.

mapWithKeyFixedTagsPrecondition :: (Eq v, Eq (Tag v), HasTag v) => (k -> v -> v) -> BiMap k v -> Bool

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

union :: (Ord k, Ord (Tag v)) => BiMap k v -> BiMap k v -> BiMap k v

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

Precondition: See unionPrecondition.

unionPrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => BiMap k v -> BiMap k v -> Bool

fromList :: (Ord k, Ord (Tag v), HasTag v) => [(k, v)] -> BiMap k v

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

Precondition: See fromListPrecondition.

fromListPrecondition :: (Eq k, Eq v, Eq (Tag v), HasTag v) => [(k, v)] -> Bool

toList :: BiMap k v -> [(k, v)]

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

keys :: BiMap k v -> [k]

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

elems :: BiMap k v -> [v]

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

fromDistinctAscendingLists :: ([(k, v)], [(Tag v, k)]) -> BiMap k v

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

Precondition: See fromDistinctAscendingListsPrecondition.

fromDistinctAscendingListsPrecondition :: (Ord k, Eq v, Ord (Tag v), HasTag v) => ([(k, v)], [(Tag v, k)]) -> Bool

toDistinctAscendingLists :: BiMap k v -> ([(k, v)], [(Tag v, k)])

Generates input suitable for fromDistinctAscendingLists. O(n).