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

Safe Haskell | None
Language | Haskell2010

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

- class HasTag a where
  - type Tag a
  - tag :: a -> Maybe (Tag a)
- tagInjectiveFor :: (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
- data BiMap k v = BiMap {
  - biMapThere :: !(Map k v)
  - biMapBack :: !(Map (Tag v) k)
  }
- biMapInvariant :: (Eq k, Eq v, Ord (Tag v), HasTag v) => BiMap k v -> Bool
- source :: Ord k => k -> BiMap k v -> Bool
- target :: Ord (Tag v) => Tag v -> BiMap k v -> Bool
- lookup :: Ord k => k -> BiMap k v -> Maybe v
- invLookup :: Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
- singleton :: HasTag v => k -> v -> BiMap k v
- insert :: (Ord k, HasTag v, Ord (Tag v)) => k -> v -> BiMap k v -> BiMap k v
- insertPrecondition :: (Eq k, Eq v, Eq (Tag v), HasTag v) => k -> v -> BiMap k v -> Bool
- alterM :: (Ord k, Ord (Tag v), HasTag v, Monad m) => (Maybe v -> m (Maybe v)) -> k -> BiMap k v -> m (BiMap k v)
- alter :: (Ord k, Ord (Tag v), HasTag v) => (Maybe v -> Maybe v) -> k -> BiMap k v -> BiMap k v
- alterPrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => (Maybe v -> Maybe v) -> k -> BiMap k v -> Bool
- update :: (Ord k, Ord (Tag v), HasTag v) => (v -> Maybe v) -> k -> BiMap k v -> BiMap k v
- updatePrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => (v -> Maybe v) -> k -> BiMap k v -> Bool
- adjust :: (Ord k, Ord (Tag v), HasTag v) => (v -> v) -> k -> BiMap k v -> BiMap k v
- adjustPrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => (v -> v) -> k -> BiMap k v -> Bool
- insertLookupWithKey :: (Ord k, Ord (Tag v), HasTag v) => (k -> v -> v -> v) -> k -> v -> BiMap k v -> (Maybe v, BiMap k v)
- insertLookupWithKeyPrecondition :: (Ord k, Eq v, Eq (Tag v), HasTag v) => (k -> v -> v -> v) -> k -> v -> BiMap k v -> Bool
- mapWithKey :: (Ord k, Ord (Tag v), HasTag v) => (k -> v -> v) -> BiMap k v -> BiMap k v
- mapWithKeyPrecondition :: (Eq k, Eq v, Eq (Tag v), HasTag v) => (k -> v -> v) -> BiMap k v -> Bool
- mapWithKeyFixedTags :: (k -> v -> v) -> BiMap k v -> BiMap k v
- mapWithKeyFixedTagsPrecondition :: (Eq v, Eq (Tag v), HasTag v) => (k -> v -> v) -> BiMap k v -> Bool
- union :: (Ord k, Ord (Tag v)) => BiMap k v -> BiMap k v -> BiMap k v
- 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
- fromListPrecondition :: (Eq k, Eq v, Eq (Tag v), HasTag v) => [(k, v)] -> Bool
- toList :: BiMap k v -> [(k, v)]
- keys :: BiMap k v -> [k]
- elems :: BiMap k v -> [v]
- fromDistinctAscendingLists :: ([(k, v)], [(Tag v, k)]) -> BiMap k v
- 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)])

# 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 type Tag ModuleNameHash = ModuleNameHash

Methods

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

HasTag InteractionPoint Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Associated Types

type Tag InteractionPoint |
Instance details Defined in Agda.TypeChecking.Monad.Base type Tag InteractionPoint = MetaId

Methods

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

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 type Tag (TopLevelModuleName' range) = ModuleNameHash

Methods

tag :: TopLevelModuleName' range -> Maybe (Tag (TopLevelModuleName' range)) Source #

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

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

#### Instances

Instances details

NFData InteractionPoints Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: InteractionPoints -> () Source #
(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 Word32 Source # icod_ :: BiMap k v -> S Word32 Source # value :: Word32 -> 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) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

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

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

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

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

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

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

max :: BiMap k v -> BiMap k v -> BiMap k v Source #

min :: BiMap k v -> BiMap k v -> BiMap k v Source #

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.8.0-DJrTbcOFazJDzri4fKrI2F" '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).