Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.BiMap

Description

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.

Synopsis

Documentation

class HasTag a where Source #

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 Source #

Methods

tag :: a -> Maybe (Tag a) Source #

Instances

Instances details
HasTag ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Associated Types

type Tag ModuleNameHash 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

HasTag InteractionPoint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Associated Types

type Tag InteractionPoint 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasTag (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Associated Types

type Tag (TopLevelModuleName' range) 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

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

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

data BiMap k v Source #

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

Instances

Instances details
NFData InteractionPoints 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: InteractionPoints -> ()

(EmbPrj k, EmbPrj v, EmbPrj (Tag v)) => EmbPrj (BiMap k v) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BiMap k v -> S Int32 Source #

icod_ :: BiMap k v -> S Int32 Source #

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

Null (BiMap k v) Source # 
Instance details

Defined in Agda.Utils.BiMap

Methods

empty :: BiMap k v Source #

null :: BiMap k v -> Bool Source #

NFData (BiMap RawTopLevelModuleName ModuleNameHash) 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Generic (BiMap k v) Source # 
Instance details

Defined in Agda.Utils.BiMap

Associated Types

type Rep (BiMap k v) 
Instance details

Defined in Agda.Utils.BiMap

type Rep (BiMap k v) = D1 ('MetaData "BiMap" "Agda.Utils.BiMap" "Agda-2.6.20240714-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))))

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) Source # 
Instance details

Defined in Agda.Utils.BiMap

Methods

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

show :: BiMap k v -> String

showList :: [BiMap k v] -> ShowS

(Eq k, Eq v) => Eq (BiMap k v) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.Utils.BiMap

type Rep (BiMap k v) = D1 ('MetaData "BiMap" "Agda.Utils.BiMap" "Agda-2.6.20240714-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 Source #

The invariant for BiMap.

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

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

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

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

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

Lookup. O(log n).

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

Inverse lookup. O(log n).

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

Singleton map. O(1).

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

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 Source #

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

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

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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

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 Source #

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

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

keys :: BiMap k v -> [k] Source #

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

elems :: BiMap k v -> [v] Source #

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

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

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 Source #

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

Generates input suitable for fromDistinctAscendingLists. O(n).