Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
- 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
- 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 :: 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)
- alter :: forall k v. (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 :: forall k v. (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
Partial injections from a type to some tag type.
The idea is that tag
should be injective on its domain: if
, then tag
x = tag
y = Just
ix = 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.
Instances
HasTag InteractionPoint Source # | |
Defined in Agda.TypeChecking.Monad.Base type Tag InteractionPoint Source # tag :: InteractionPoint -> Maybe (Tag InteractionPoint) 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.
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
.
Instances
NFData InteractionPoints Source # | |
Defined in Agda.TypeChecking.Monad.Base rnf :: InteractionPoints -> () # | |
(EmbPrj k, EmbPrj v, EmbPrj (Tag v)) => EmbPrj (BiMap k v) Source # | |
Null (BiMap k v) Source # | |
Generic (BiMap k v) Source # | |
(Show k, Show v) => Show (BiMap k v) Source # | |
(Eq k, Eq v) => Eq (BiMap k v) Source # | |
(Ord k, Ord v) => Ord (BiMap k v) Source # | |
Defined in Agda.Utils.BiMap | |
type Rep (BiMap k v) Source # | |
Defined in Agda.Utils.BiMap type Rep (BiMap k v) = D1 ('MetaData "BiMap" "Agda.Utils.BiMap" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "BiMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "biMapThere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map k v)) :*: S1 ('MetaSel ('Just "biMapBack") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map (Tag v) k)))) |
biMapInvariant :: (Eq k, Eq v, Ord (Tag v), HasTag v) => BiMap k v -> Bool Source #
The invariant for BiMap
.
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
.
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) Source #
alter :: forall k v. (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 #
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 #
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 #
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) 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
is that, if
the value insertLookupWithKey
f k v mv'
is inserted into m
, and
is defined,
then no key other than tag
v'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
: For any two distinct
mappings mapWithKey
f mk₁ ↦ 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
is that, if mapWithKeyFixedTags
f mm
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
.
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
.
toList :: BiMap k v -> [(k, v)] Source #
Conversion to lists of pairs, with the keys in ascending order. 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).