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

    module Agda.Utils.BiMap where

    import Prelude hiding (null, lookup)

    import Control.Monad.Identity
    import Control.Monad.State

    import Data.Function
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Maybe
    import Data.Ord
    import Data.Tuple

    import GHC.Generics (Generic)

    import Agda.Utils.List
    import Agda.Utils.Null

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

    class HasTag a where
      type Tag a
      tag :: a -> Maybe (Tag a)

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

    tagInjectiveFor ::
      (Eq v, Eq (Tag v), HasTag v) =>
      [v] -> Bool
    tagInjectiveFor :: forall v. (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
    tagInjectiveFor [v]
    vs = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
      [ v
    v1 v -> v -> Bool
    forall a. Eq a => a -> a -> Bool
    == v
    v2
      | v
    v1 <- [v]
    vs
      , v
    v2 <- [v]
    vs
      , Maybe (Tag v) -> Bool
    forall a. Maybe a -> Bool
    isJust (v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v1)
      , v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v1 Maybe (Tag v) -> Maybe (Tag v) -> Bool
    forall a. Eq a => a -> a -> Bool
    == v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v2
      ]

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

    data BiMap k v = BiMap
      { forall k v. BiMap k v -> Map k v
    biMapThere :: Map k v
      , forall k v. BiMap k v -> Map (Tag v) k
    biMapBack  :: Map (Tag v) k
      }
      deriving (forall x. BiMap k v -> Rep (BiMap k v) x)
    -> (forall x. Rep (BiMap k v) x -> BiMap k v)
    -> Generic (BiMap k v)
    forall x. Rep (BiMap k v) x -> BiMap k v
    forall x. BiMap k v -> Rep (BiMap k v) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall k v x. Rep (BiMap k v) x -> BiMap k v
    forall k v x. BiMap k v -> Rep (BiMap k v) x
    $cto :: forall k v x. Rep (BiMap k v) x -> BiMap k v
    $cfrom :: forall k v x. BiMap k v -> Rep (BiMap k v) x
    Generic

    -- | The invariant for 'BiMap'.

    biMapInvariant ::
      (Eq k, Eq v, Ord (Tag v), HasTag v) =>
      BiMap k v -> Bool
    biMapInvariant :: forall k v.
    (Eq k, Eq v, Ord (Tag v), HasTag v) =>
    BiMap k v -> Bool
    biMapInvariant m :: BiMap k v
    m@(BiMap Map k v
    t Map (Tag v) k
    u) =
      Map (Tag v) k
    u Map (Tag v) k -> Map (Tag v) k -> Bool
    forall a. Eq a => a -> a -> Bool
    ==
      [(Tag v, k)] -> Map (Tag v) k
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList
        [ (Tag v
    k', k
    k)
        | (k
    k, v
    v) <- Map k v -> [(k, v)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map k v
    t
        , Just Tag v
    k' <- [v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v]
        ]
        Bool -> Bool -> Bool
    &&
      [v] -> Bool
    forall v. (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
    tagInjectiveFor (((k, v) -> v) -> [(k, v)] -> [v]
    forall a b. (a -> b) -> [a] -> [b]
    map (k, v) -> v
    forall a b. (a, b) -> b
    snd ([(k, v)] -> [v]) -> [(k, v)] -> [v]
    forall a b. (a -> b) -> a -> b
    $ BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m)

    instance Null (BiMap k v) where
      empty :: BiMap k v
    empty = Map k v -> Map (Tag v) k -> BiMap k v
    forall k v. Map k v -> Map (Tag v) k -> BiMap k v
    BiMap Map k v
    forall k a. Map k a
    Map.empty Map (Tag v) k
    forall k a. Map k a
    Map.empty
      null :: BiMap k v -> Bool
    null  = Map k v -> Bool
    forall a. Null a => a -> Bool
    null (Map k v -> Bool) -> (BiMap k v -> Map k v) -> BiMap k v -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap k v -> Map k v
    forall k v. BiMap k v -> Map k v
    biMapThere

    -- | Lookup. O(log n).

    lookup :: Ord k => k -> BiMap k v -> Maybe v
    lookup :: forall k v. Ord k => k -> BiMap k v -> Maybe v
    lookup k
    a = k -> Map k v -> Maybe v
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup k
    a (Map k v -> Maybe v)
    -> (BiMap k v -> Map k v) -> BiMap k v -> Maybe v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap k v -> Map k v
    forall k v. BiMap k v -> Map k v
    biMapThere

    -- | Inverse lookup. O(log n).

    invLookup :: Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
    invLookup :: forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
    invLookup Tag v
    k = Tag v -> Map (Tag v) k -> Maybe k
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Tag v
    k (Map (Tag v) k -> Maybe k)
    -> (BiMap k v -> Map (Tag v) k) -> BiMap k v -> Maybe k
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap k v -> Map (Tag v) k
    forall k v. BiMap k v -> Map (Tag v) k
    biMapBack

    -- | Singleton map. O(1).

    singleton :: HasTag v => k -> v -> BiMap k v
    singleton :: forall v k. HasTag v => k -> v -> BiMap k v
    singleton k
    k v
    v =
      Map k v -> Map (Tag v) k -> BiMap k v
    forall k v. Map k v -> Map (Tag v) k -> BiMap k v
    BiMap
        (k -> v -> Map k v
    forall k a. k -> a -> Map k a
    Map.singleton k
    k v
    v)
        (case v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v of
           Maybe (Tag v)
    Nothing -> Map (Tag v) k
    forall k a. Map k a
    Map.empty
           Just Tag v
    k' -> Tag v -> k -> Map (Tag v) k
    forall k a. k -> a -> Map k a
    Map.singleton Tag v
    k' k
    k)

    -- | Insertion. Overwrites existing values. O(log n).
    --
    -- Precondition: See 'insertPrecondition'.

    insert ::
      (Ord k, HasTag v, Ord (Tag v)) =>
      k -> v -> BiMap k v -> BiMap k v
    insert :: forall k v.
    (Ord k, HasTag v, Ord (Tag v)) =>
    k -> v -> BiMap k v -> BiMap k v
    insert k
    k v
    v (BiMap Map k v
    t Map (Tag v) k
    b) =
      Map k v -> Map (Tag v) k -> BiMap k v
    forall k v. Map k v -> Map (Tag v) k -> BiMap k v
    BiMap
        (k -> v -> Map k v -> Map k v
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert k
    k v
    v Map k v
    t)
        (case v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v of
           Maybe (Tag v)
    Nothing -> Map (Tag v) k
    b'
           Just Tag v
    k' -> Tag v -> k -> Map (Tag v) k -> Map (Tag v) k
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Tag v
    k' k
    k Map (Tag v) k
    b')
      where
      b' :: Map (Tag v) k
    b' = case v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag (v -> Maybe (Tag v)) -> Maybe v -> Maybe (Tag v)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< k -> Map k v -> Maybe v
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup k
    k Map k v
    t of
        Maybe (Tag v)
    Nothing -> Map (Tag v) k
    b
        Just Tag v
    k' -> Tag v -> Map (Tag v) k -> Map (Tag v) k
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete Tag v
    k' Map (Tag v) k
    b

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

    insertPrecondition ::
      (Eq k, Eq v, Eq (Tag v), HasTag v) =>
      k -> v -> BiMap k v -> Bool
    insertPrecondition :: forall k v.
    (Eq k, Eq v, Eq (Tag v), HasTag v) =>
    k -> v -> BiMap k v -> Bool
    insertPrecondition k
    k v
    v BiMap k v
    m =
      case v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v of
        Maybe (Tag v)
    Nothing -> Bool
    True
        Just Tag v
    _  ->
          Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ ((k, v) -> Bool) -> [(k, v)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (\(k
    k', v
    v') -> k
    k' k -> k -> Bool
    forall a. Eq a => a -> a -> Bool
    /= k
    k Bool -> Bool -> Bool
    && v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v Maybe (Tag v) -> Maybe (Tag v) -> Bool
    forall a. Eq a => a -> a -> Bool
    == v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v') ([(k, v)] -> Bool) -> [(k, v)] -> Bool
    forall a b. (a -> b) -> a -> b
    $ BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m

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

    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)
    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)
    alterM Maybe v -> m (Maybe v)
    f k
    k m :: BiMap k v
    m@(BiMap Map k v
    t Map (Tag v) k
    b) = do
      (Map k v
    t', Maybe (Maybe (Tag v), Maybe (Tag v))
    r) <- StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m (Map k v)
    -> Maybe (Maybe (Tag v), Maybe (Tag v))
    -> m (Map k v, Maybe (Maybe (Tag v), Maybe (Tag v)))
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT ((Maybe v
     -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m (Maybe v))
    -> k
    -> Map k v
    -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m (Map k v)
    forall (f :: * -> *) k a.
    (Functor f, Ord k) =>
    (Maybe a -> f (Maybe a)) -> k -> Map k a -> f (Map k a)
    Map.alterF Maybe v
    -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m (Maybe v)
    f' k
    k Map k v
    t) Maybe (Maybe (Tag v), Maybe (Tag v))
    forall a. Maybe a
    Nothing
      BiMap k v -> m (BiMap k v)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (BiMap k v -> m (BiMap k v)) -> BiMap k v -> m (BiMap k v)
    forall a b. (a -> b) -> a -> b
    $ case Maybe (Maybe (Tag v), Maybe (Tag v))
    r of
        Maybe (Maybe (Tag v), Maybe (Tag v))
    Nothing -> BiMap k v
    m
        Just (Maybe (Tag v), Maybe (Tag v))
    r  -> Map k v -> Map (Tag v) k -> BiMap k v
    forall k v. Map k v -> Map (Tag v) k -> BiMap k v
    BiMap Map k v
    t' ((Maybe (Tag v), Maybe (Tag v)) -> Map (Tag v) k -> Map (Tag v) k
    updateBack (Maybe (Tag v), Maybe (Tag v))
    r Map (Tag v) k
    b)
      where
      f' ::
        Maybe v ->
        StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m (Maybe v)
      f' :: Maybe v
    -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m (Maybe v)
    f' Maybe v
    v = do
        Maybe v
    r <- m (Maybe v)
    -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m (Maybe v)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Maybe v -> m (Maybe v)
    f Maybe v
    v)
        Maybe (Maybe (Tag v), Maybe (Tag v))
    -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Maybe (Maybe (Tag v), Maybe (Tag v))
     -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m ())
    -> Maybe (Maybe (Tag v), Maybe (Tag v))
    -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m ()
    forall a b. (a -> b) -> a -> b
    $ (Maybe (Tag v), Maybe (Tag v))
    -> Maybe (Maybe (Tag v), Maybe (Tag v))
    forall a. a -> Maybe a
    Just (v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag (v -> Maybe (Tag v)) -> Maybe v -> Maybe (Tag v)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe v
    v, v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag (v -> Maybe (Tag v)) -> Maybe v -> Maybe (Tag v)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe v
    r)
        Maybe v
    -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m (Maybe v)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe v
    r

      updateBack :: (Maybe (Tag v), Maybe (Tag v)) -> Map (Tag v) k -> Map (Tag v) k
    updateBack (Maybe (Tag v)
    k'1, Maybe (Tag v)
    k'2) =
        if Maybe (Tag v)
    k'1 Maybe (Tag v) -> Maybe (Tag v) -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe (Tag v)
    k'2
        then Map (Tag v) k -> Map (Tag v) k
    forall a. a -> a
    id
        else (Map (Tag v) k -> Map (Tag v) k)
    -> (Tag v -> Map (Tag v) k -> Map (Tag v) k)
    -> Maybe (Tag v)
    -> Map (Tag v) k
    -> Map (Tag v) k
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Map (Tag v) k -> Map (Tag v) k
    forall a. a -> a
    id ((Tag v -> k -> Map (Tag v) k -> Map (Tag v) k)
    -> k -> Tag v -> Map (Tag v) k -> Map (Tag v) k
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Tag v -> k -> Map (Tag v) k -> Map (Tag v) k
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert k
    k) Maybe (Tag v)
    k'2 (Map (Tag v) k -> Map (Tag v) k)
    -> (Map (Tag v) k -> Map (Tag v) k)
    -> Map (Tag v) k
    -> Map (Tag v) k
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
             (Map (Tag v) k -> Map (Tag v) k)
    -> (Tag v -> Map (Tag v) k -> Map (Tag v) k)
    -> Maybe (Tag v)
    -> Map (Tag v) k
    -> Map (Tag v) k
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Map (Tag v) k -> Map (Tag v) k
    forall a. a -> a
    id Tag v -> Map (Tag v) k -> Map (Tag v) k
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete Maybe (Tag v)
    k'1

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

    alter ::
      forall k v. (Ord k, Ord (Tag v), HasTag v) =>
      (Maybe v -> Maybe v) -> k -> BiMap k v -> 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
    alter Maybe v -> Maybe v
    f k
    k BiMap k v
    m = Identity (BiMap k v) -> BiMap k v
    forall a. Identity a -> a
    runIdentity (Identity (BiMap k v) -> BiMap k v)
    -> Identity (BiMap k v) -> BiMap k v
    forall a b. (a -> b) -> a -> b
    $ (Maybe v -> Identity (Maybe v))
    -> k -> BiMap k v -> Identity (BiMap k v)
    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)
    alterM (Maybe v -> Identity (Maybe v)
    forall a. a -> Identity a
    Identity (Maybe v -> Identity (Maybe v))
    -> (Maybe v -> Maybe v) -> Maybe v -> Identity (Maybe v)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe v -> Maybe v
    f) k
    k BiMap k v
    m

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

    alterPrecondition ::
      (Ord k, Eq v, Eq (Tag v), HasTag v) =>
      (Maybe v -> Maybe v) -> k -> BiMap k v -> Bool
    alterPrecondition :: forall k v.
    (Ord k, Eq v, Eq (Tag v), HasTag v) =>
    (Maybe v -> Maybe v) -> k -> BiMap k v -> Bool
    alterPrecondition Maybe v -> Maybe v
    f k
    k BiMap k v
    m =
      case v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag (v -> Maybe (Tag v)) -> Maybe v -> Maybe (Tag v)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe v -> Maybe v
    f (k -> BiMap k v -> Maybe v
    forall k v. Ord k => k -> BiMap k v -> Maybe v
    lookup k
    k BiMap k v
    m) of
        Maybe (Tag v)
    Nothing -> Bool
    True
        Just Tag v
    k' -> [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
          [ Tag v -> Maybe (Tag v)
    forall a. a -> Maybe a
    Just Tag v
    k' Maybe (Tag v) -> Maybe (Tag v) -> Bool
    forall a. Eq a => a -> a -> Bool
    /= v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v
          | (k
    k'', v
    v) <- BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m
          , k
    k'' k -> k -> Bool
    forall a. Eq a => a -> a -> Bool
    /= k
    k
          ]

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

    update ::
      (Ord k, Ord (Tag v), HasTag v) =>
      (v -> Maybe v) -> k -> BiMap k v -> BiMap k v
    update :: forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (v -> Maybe v) -> k -> BiMap k v -> BiMap k v
    update v -> Maybe v
    f = (Maybe v -> Maybe v) -> k -> BiMap k v -> BiMap k v
    forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (Maybe v -> Maybe v) -> k -> BiMap k v -> BiMap k v
    alter (v -> Maybe v
    f (v -> Maybe v) -> Maybe v -> Maybe v
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<)

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

    updatePrecondition ::
      (Ord k, Eq v, Eq (Tag v), HasTag v) =>
      (v -> Maybe v) -> k -> BiMap k v -> Bool
    updatePrecondition :: forall k v.
    (Ord k, Eq v, Eq (Tag v), HasTag v) =>
    (v -> Maybe v) -> k -> BiMap k v -> Bool
    updatePrecondition v -> Maybe v
    f = (Maybe v -> Maybe v) -> k -> BiMap k v -> Bool
    forall k v.
    (Ord k, Eq v, Eq (Tag v), HasTag v) =>
    (Maybe v -> Maybe v) -> k -> BiMap k v -> Bool
    alterPrecondition (v -> Maybe v
    f (v -> Maybe v) -> Maybe v -> Maybe v
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<)

    -- | Modifies the value at the given position, if any. O(log n).
    --
    -- Precondition: See 'adjustPrecondition'.

    adjust ::
      (Ord k, Ord (Tag v), HasTag v) =>
      (v -> v) -> k -> BiMap k v -> BiMap k v
    adjust :: forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (v -> v) -> k -> BiMap k v -> BiMap k v
    adjust v -> v
    f = (v -> Maybe v) -> k -> BiMap k v -> BiMap k v
    forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (v -> Maybe v) -> k -> BiMap k v -> BiMap k v
    update (v -> Maybe v
    forall a. a -> Maybe a
    Just (v -> Maybe v) -> (v -> v) -> v -> Maybe v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . v -> v
    f)

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

    adjustPrecondition ::
      (Ord k, Eq v, Eq (Tag v), HasTag v) =>
      (v -> v) -> k -> BiMap k v -> Bool
    adjustPrecondition :: forall k v.
    (Ord k, Eq v, Eq (Tag v), HasTag v) =>
    (v -> v) -> k -> BiMap k v -> Bool
    adjustPrecondition v -> v
    f = (v -> Maybe v) -> k -> BiMap k v -> Bool
    forall k v.
    (Ord k, Eq v, Eq (Tag v), HasTag v) =>
    (v -> Maybe v) -> k -> BiMap k v -> Bool
    updatePrecondition (v -> Maybe v
    forall a. a -> Maybe a
    Just (v -> Maybe v) -> (v -> v) -> v -> Maybe v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . v -> v
    f)

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

    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)
    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)
    insertLookupWithKey k -> v -> v -> v
    f k
    k v
    v BiMap k v
    m = (BiMap k v, Maybe v) -> (Maybe v, BiMap k v)
    forall a b. (a, b) -> (b, a)
    swap ((BiMap k v, Maybe v) -> (Maybe v, BiMap k v))
    -> (BiMap k v, Maybe v) -> (Maybe v, BiMap k v)
    forall a b. (a -> b) -> a -> b
    $ State (Maybe v) (BiMap k v) -> Maybe v -> (BiMap k v, Maybe v)
    forall s a. State s a -> s -> (a, s)
    runState ((Maybe v -> StateT (Maybe v) Identity (Maybe v))
    -> k -> BiMap k v -> State (Maybe v) (BiMap k v)
    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)
    alterM Maybe v -> StateT (Maybe v) Identity (Maybe v)
    f' k
    k BiMap k v
    m) Maybe v
    forall a. Maybe a
    Nothing
      where
      f' :: Maybe v -> State (Maybe v) (Maybe v)
      f' :: Maybe v -> StateT (Maybe v) Identity (Maybe v)
    f' Maybe v
    Nothing     = Maybe v -> StateT (Maybe v) Identity (Maybe v)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe v -> StateT (Maybe v) Identity (Maybe v))
    -> Maybe v -> StateT (Maybe v) Identity (Maybe v)
    forall a b. (a -> b) -> a -> b
    $ v -> Maybe v
    forall a. a -> Maybe a
    Just v
    v
      f' r :: Maybe v
    r@(Just v
    v') = do
        Maybe v -> StateT (Maybe v) Identity ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put Maybe v
    r
        Maybe v -> StateT (Maybe v) Identity (Maybe v)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe v -> StateT (Maybe v) Identity (Maybe v))
    -> Maybe v -> StateT (Maybe v) Identity (Maybe v)
    forall a b. (a -> b) -> a -> b
    $ v -> Maybe v
    forall a. a -> Maybe a
    Just (k -> v -> v -> v
    f k
    k v
    v v
    v')

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

    insertLookupWithKeyPrecondition ::
      (Ord k, Eq v, Eq (Tag v), HasTag v) =>
      (k -> v -> v -> v) -> k -> v -> BiMap k v -> Bool
    insertLookupWithKeyPrecondition :: forall k v.
    (Ord k, Eq v, Eq (Tag v), HasTag v) =>
    (k -> v -> v -> v) -> k -> v -> BiMap k v -> Bool
    insertLookupWithKeyPrecondition k -> v -> v -> v
    f k
    k v
    v =
      (Maybe v -> Maybe v) -> k -> BiMap k v -> Bool
    forall k v.
    (Ord k, Eq v, Eq (Tag v), HasTag v) =>
    (Maybe v -> Maybe v) -> k -> BiMap k v -> Bool
    alterPrecondition (v -> Maybe v
    forall a. a -> Maybe a
    Just (v -> Maybe v) -> (Maybe v -> v) -> Maybe v -> Maybe v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . v -> (v -> v) -> Maybe v -> v
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe v
    v (k -> v -> v -> v
    f k
    k v
    v)) k
    k

    -- | Changes all the values using the given function, which is also
    -- given access to keys. O(n log n).
    --
    -- Precondition: See 'mapWithKeyPrecondition'.

    mapWithKey ::
      (Ord k, Ord (Tag v), HasTag v) =>
      (k -> v -> v) -> BiMap k v -> BiMap k v
    mapWithKey :: forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (k -> v -> v) -> BiMap k v -> BiMap k v
    mapWithKey k -> v -> v
    f = [(k, v)] -> BiMap k v
    forall k v. (Ord k, Ord (Tag v), HasTag v) => [(k, v)] -> BiMap k v
    fromList ([(k, v)] -> BiMap k v)
    -> (BiMap k v -> [(k, v)]) -> BiMap k v -> BiMap k v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((k, v) -> (k, v)) -> [(k, v)] -> [(k, v)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(k
    k, v
    v) -> (k
    k, k -> v -> v
    f k
    k v
    v)) ([(k, v)] -> [(k, v)])
    -> (BiMap k v -> [(k, v)]) -> BiMap k v -> [(k, v)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList

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

    mapWithKeyPrecondition ::
      (Eq k, Eq v, Eq (Tag v), HasTag v) =>
      (k -> v -> v) -> BiMap k v -> Bool
    mapWithKeyPrecondition :: forall k v.
    (Eq k, Eq v, Eq (Tag v), HasTag v) =>
    (k -> v -> v) -> BiMap k v -> Bool
    mapWithKeyPrecondition k -> v -> v
    f =
      [(k, v)] -> Bool
    forall k v. (Eq k, Eq v, Eq (Tag v), HasTag v) => [(k, v)] -> Bool
    fromListPrecondition ([(k, v)] -> Bool) -> (BiMap k v -> [(k, v)]) -> BiMap k v -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((k, v) -> (k, v)) -> [(k, v)] -> [(k, v)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(k
    k, v
    v) -> (k
    k, k -> v -> v
    f k
    k v
    v)) ([(k, v)] -> [(k, v)])
    -> (BiMap k v -> [(k, v)]) -> BiMap k v -> [(k, v)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList

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

    mapWithKeyFixedTags :: (k -> v -> v) -> BiMap k v -> BiMap k v
    mapWithKeyFixedTags :: forall k v. (k -> v -> v) -> BiMap k v -> BiMap k v
    mapWithKeyFixedTags k -> v -> v
    f (BiMap Map k v
    t Map (Tag v) k
    b) = Map k v -> Map (Tag v) k -> BiMap k v
    forall k v. Map k v -> Map (Tag v) k -> BiMap k v
    BiMap ((k -> v -> v) -> Map k v -> Map k v
    forall k a b. (k -> a -> b) -> Map k a -> Map k b
    Map.mapWithKey k -> v -> v
    f Map k v
    t) Map (Tag v) k
    b

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

    mapWithKeyFixedTagsPrecondition ::
      (Eq v, Eq (Tag v), HasTag v) =>
      (k -> v -> v) -> BiMap k v -> Bool
    mapWithKeyFixedTagsPrecondition :: forall v k.
    (Eq v, Eq (Tag v), HasTag v) =>
    (k -> v -> v) -> BiMap k v -> Bool
    mapWithKeyFixedTagsPrecondition k -> v -> v
    f BiMap k v
    m = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
      [ v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag (k -> v -> v
    f k
    k v
    v) Maybe (Tag v) -> Maybe (Tag v) -> Bool
    forall a. Eq a => a -> a -> Bool
    == v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v
      | (k
    k, v
    v) <- BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m
      ]

    -- | Left-biased union. For the time complexity, see 'Map.union'.
    --
    -- Precondition: See 'unionPrecondition'.

    union :: (Ord k, Ord (Tag v)) => BiMap k v -> BiMap k v -> BiMap k v
    union :: forall k v.
    (Ord k, Ord (Tag v)) =>
    BiMap k v -> BiMap k v -> BiMap k v
    union (BiMap Map k v
    t1 Map (Tag v) k
    b1) (BiMap Map k v
    t2 Map (Tag v) k
    b2) =
      Map k v -> Map (Tag v) k -> BiMap k v
    forall k v. Map k v -> Map (Tag v) k -> BiMap k v
    BiMap (Map k v -> Map k v -> Map k v
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map k v
    t1 Map k v
    t2) (Map (Tag v) k -> Map (Tag v) k -> Map (Tag v) k
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map (Tag v) k
    b1 Map (Tag v) k
    b2)

    -- The precondition for @'union' m₁ m₂@: If @k@ is mapped to @v₁@ in
    -- @m₁@ and @v₂@ in @m₂@, then @'tag' v₂ = 'Nothing'@ or @'tag' v₁ =
    -- 'tag' v₂@. Furthermore, if @k₁@ is mapped to @v₁@ in @m₁@ and @k₂@
    -- is mapped to @v₂@ in @m₂@, where @'tag' v₁ = 'tag' v₂ = 'Just' k@,
    -- then @k₁ = k₂@. Finally 'tag' must be injective for
    -- @{v₁ | (k₁, v₁) ∈ m₁} ∪ {v₂ | (k₂, v₂) ∈ m₂, k₂ ∉ m₁}@.

    unionPrecondition ::
      (Ord k, Eq v, Eq (Tag v), HasTag v) =>
      BiMap k v -> BiMap k v -> Bool
    unionPrecondition :: forall k v.
    (Ord k, Eq v, Eq (Tag v), HasTag v) =>
    BiMap k v -> BiMap k v -> Bool
    unionPrecondition m1 :: BiMap k v
    m1@(BiMap Map k v
    t1 Map (Tag v) k
    _) m2 :: BiMap k v
    m2@(BiMap Map k v
    t2 Map (Tag v) k
    _) =
      [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
        [ v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v2 Maybe (Tag v) -> Maybe (Tag v) -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe (Tag v)
    forall a. Maybe a
    Nothing Bool -> Bool -> Bool
    || v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v1 Maybe (Tag v) -> Maybe (Tag v) -> Bool
    forall a. Eq a => a -> a -> Bool
    == v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v2
        | (v
    v1, v
    v2) <- Map k (v, v) -> [(v, v)]
    forall k a. Map k a -> [a]
    Map.elems (Map k (v, v) -> [(v, v)]) -> Map k (v, v) -> [(v, v)]
    forall a b. (a -> b) -> a -> b
    $ (v -> v -> (v, v)) -> Map k v -> Map k v -> Map k (v, v)
    forall k a b c.
    Ord k =>
    (a -> b -> c) -> Map k a -> Map k b -> Map k c
    Map.intersectionWith (,) Map k v
    t1 Map k v
    t2
        ] Bool -> Bool -> Bool
    &&
      [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
        [ k
    k1 k -> k -> Bool
    forall a. Eq a => a -> a -> Bool
    == k
    k2
        | (k
    k1, v
    v1) <- BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m1
        , (k
    k2, v
    v2) <- BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m2
        , v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v1 Maybe (Tag v) -> Maybe (Tag v) -> Bool
    forall a. Eq a => a -> a -> Bool
    == v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v2
        , Maybe (Tag v) -> Bool
    forall a. Maybe a -> Bool
    isJust (v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v1)
        ]
        Bool -> Bool -> Bool
    &&
      [v] -> Bool
    forall v. (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
    tagInjectiveFor
        ([ v
    v1
         | (k
    _, v
    v1) <- BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m1
         ] [v] -> [v] -> [v]
    forall a. [a] -> [a] -> [a]
    ++
         [ v
    v2
         | (k
    k2, v
    v2) <- BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m2
         , Bool -> Bool
    not (k
    k2 k -> [k] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [k]
    ks1)
         ])
      where
      ks1 :: [k]
    ks1 = ((k, v) -> k) -> [(k, v)] -> [k]
    forall a b. (a -> b) -> [a] -> [b]
    map (k, v) -> k
    forall a b. (a, b) -> a
    fst (BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    m1)

    -- | Conversion from lists of pairs. Later entries take precedence
    -- over earlier ones. O(n log n).
    --
    -- Precondition: See 'fromListPrecondition'.

    fromList ::
      (Ord k, Ord (Tag v), HasTag v) =>
      [(k, v)] -> BiMap k v
    fromList :: forall k v. (Ord k, Ord (Tag v), HasTag v) => [(k, v)] -> BiMap k v
    fromList = ((k, v) -> BiMap k v -> BiMap k v)
    -> BiMap k v -> [(k, v)] -> BiMap k v
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    List.foldr ((k -> v -> BiMap k v -> BiMap k v)
    -> (k, v) -> BiMap k v -> BiMap k v
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry k -> v -> BiMap k v -> BiMap k v
    forall k v.
    (Ord k, HasTag v, Ord (Tag v)) =>
    k -> v -> BiMap k v -> BiMap k v
    insert) BiMap k v
    forall a. Null a => a
    empty

    -- The precondition for @'fromList' kvs@: For all pairs @(k₁, v₁)@,
    -- @(k₂, v₂)@ in @kvs@ for which the tags of @v₁@ and @v₂@ are
    -- defined, if @v₁ = v₂@ then @k₁ = k₂@. Furthermore 'tag' must be
    -- injective for the values in the list.

    fromListPrecondition ::
      (Eq k, Eq v, Eq (Tag v), HasTag v) =>
      [(k, v)] -> Bool
    fromListPrecondition :: forall k v. (Eq k, Eq v, Eq (Tag v), HasTag v) => [(k, v)] -> Bool
    fromListPrecondition [(k, v)]
    kvs =
      [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
        [ k
    k1 k -> k -> Bool
    forall a. Eq a => a -> a -> Bool
    == k
    k2
        | (k
    k1, v
    v1) <- [(k, v)]
    kvs
        , (k
    k2, v
    v2) <- [(k, v)]
    kvs
        , Maybe (Tag v) -> Bool
    forall a. Maybe a -> Bool
    isJust (v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v1)
        , Maybe (Tag v) -> Bool
    forall a. Maybe a -> Bool
    isJust (v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v2)
        , v
    v1 v -> v -> Bool
    forall a. Eq a => a -> a -> Bool
    == v
    v2
        ]
        Bool -> Bool -> Bool
    &&
      [v] -> Bool
    forall v. (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
    tagInjectiveFor (((k, v) -> v) -> [(k, v)] -> [v]
    forall a b. (a -> b) -> [a] -> [b]
    map (k, v) -> v
    forall a b. (a, b) -> b
    snd [(k, v)]
    kvs)

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

    toList :: BiMap k v -> [(k, v)]
    toList :: forall k v. BiMap k v -> [(k, v)]
    toList = Map k v -> [(k, v)]
    forall k a. Map k a -> [(k, a)]
    Map.toAscList (Map k v -> [(k, v)])
    -> (BiMap k v -> Map k v) -> BiMap k v -> [(k, v)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap k v -> Map k v
    forall k v. BiMap k v -> Map k v
    biMapThere

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

    keys :: BiMap k v -> [k]
    keys :: forall k v. BiMap k v -> [k]
    keys = Map k v -> [k]
    forall k a. Map k a -> [k]
    Map.keys (Map k v -> [k]) -> (BiMap k v -> Map k v) -> BiMap k v -> [k]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap k v -> Map k v
    forall k v. BiMap k v -> Map k v
    biMapThere

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

    elems :: BiMap k v -> [v]
    elems :: forall k v. BiMap k v -> [v]
    elems = Map k v -> [v]
    forall k a. Map k a -> [a]
    Map.elems (Map k v -> [v]) -> (BiMap k v -> Map k v) -> BiMap k v -> [v]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap k v -> Map k v
    forall k v. BiMap k v -> Map k v
    biMapThere

    -- | Conversion from two lists that contain distinct keys/tags, with
    -- the keys/tags in ascending order. O(n).
    --
    -- Precondition: See 'fromDistinctAscendingListsPrecondition'.

    fromDistinctAscendingLists ::
      ([(k, v)], [(Tag v, k)]) -> BiMap k v
    fromDistinctAscendingLists :: forall k v. ([(k, v)], [(Tag v, k)]) -> BiMap k v
    fromDistinctAscendingLists ([(k, v)]
    t, [(Tag v, k)]
    b) =
      Map k v -> Map (Tag v) k -> BiMap k v
    forall k v. Map k v -> Map (Tag v) k -> BiMap k v
    BiMap ([(k, v)] -> Map k v
    forall k a. [(k, a)] -> Map k a
    Map.fromDistinctAscList [(k, v)]
    t) ([(Tag v, k)] -> Map (Tag v) k
    forall k a. [(k, a)] -> Map k a
    Map.fromDistinctAscList [(Tag v, k)]
    b)

    -- The precondition for @'fromDistinctAscendingLists' (kvs, kks)@: The
    -- lists must contain distinct keys/tags, and must be sorted according
    -- to the keys/tags. Furthermore, for every pair @(k, v)@ in the first
    -- list for which @'tag' v = 'Just' k'@ there must be a pair @(k', k)@
    -- in the second list, and there must not be any other pairs in that
    -- list. Finally 'tag' must be injective for @{v | (_, v) ∈ kvs }@.

    fromDistinctAscendingListsPrecondition ::
      (Ord k, Eq v, Ord (Tag v), HasTag v) =>
      ([(k, v)], [(Tag v, k)]) -> Bool
    fromDistinctAscendingListsPrecondition :: forall k v.
    (Ord k, Eq v, Ord (Tag v), HasTag v) =>
    ([(k, v)], [(Tag v, k)]) -> Bool
    fromDistinctAscendingListsPrecondition ([(k, v)]
    kvs, [(Tag v, k)]
    kks) =
      [k] -> Bool
    forall a. Ord a => [a] -> Bool
    fastDistinct (((k, v) -> k) -> [(k, v)] -> [k]
    forall a b. (a -> b) -> [a] -> [b]
    map (k, v) -> k
    forall a b. (a, b) -> a
    fst [(k, v)]
    kvs) Bool -> Bool -> Bool
    && [k] -> Bool
    forall a. Ord a => [a] -> Bool
    sorted (((k, v) -> k) -> [(k, v)] -> [k]
    forall a b. (a -> b) -> [a] -> [b]
    map (k, v) -> k
    forall a b. (a, b) -> a
    fst [(k, v)]
    kvs)
        Bool -> Bool -> Bool
    &&
      [Tag v] -> Bool
    forall a. Ord a => [a] -> Bool
    fastDistinct (((Tag v, k) -> Tag v) -> [(Tag v, k)] -> [Tag v]
    forall a b. (a -> b) -> [a] -> [b]
    map (Tag v, k) -> Tag v
    forall a b. (a, b) -> a
    fst [(Tag v, k)]
    kks) Bool -> Bool -> Bool
    && [Tag v] -> Bool
    forall a. Ord a => [a] -> Bool
    sorted (((Tag v, k) -> Tag v) -> [(Tag v, k)] -> [Tag v]
    forall a b. (a -> b) -> [a] -> [b]
    map (Tag v, k) -> Tag v
    forall a b. (a, b) -> a
    fst [(Tag v, k)]
    kks)
        Bool -> Bool -> Bool
    &&
      [(Tag v, k)]
    kks [(Tag v, k)] -> [(Tag v, k)] -> Bool
    forall a. Eq a => a -> a -> Bool
    ==
      ((Tag v, k) -> (Tag v, k) -> Ordering)
    -> [(Tag v, k)] -> [(Tag v, k)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (((Tag v, k) -> Tag v) -> (Tag v, k) -> (Tag v, k) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Tag v, k) -> Tag v
    forall a b. (a, b) -> a
    fst)
        [ (Tag v
    k', k
    k)
        | (k
    k, v
    v) <- [(k, v)]
    kvs
        , Just Tag v
    k' <- [v -> Maybe (Tag v)
    forall a. HasTag a => a -> Maybe (Tag a)
    tag v
    v]
        ]
        Bool -> Bool -> Bool
    &&
      [v] -> Bool
    forall v. (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
    tagInjectiveFor [ v
    v | (k
    _, v
    v) <- [(k, v)]
    kvs ]

    -- | Generates input suitable for 'fromDistinctAscendingLists'. O(n).

    toDistinctAscendingLists :: BiMap k v -> ([(k, v)], [(Tag v, k)])
    toDistinctAscendingLists :: forall k v. BiMap k v -> ([(k, v)], [(Tag v, k)])
    toDistinctAscendingLists (BiMap Map k v
    t Map (Tag v) k
    b) =
      (Map k v -> [(k, v)]
    forall k a. Map k a -> [(k, a)]
    Map.toAscList Map k v
    t, Map (Tag v) k -> [(Tag v, k)]
    forall k a. Map k a -> [(k, a)]
    Map.toAscList Map (Tag v) k
    b)

    ------------------------------------------------------------------------
    -- Instances
    ------------------------------------------------------------------------

    instance (Eq k, Eq v) => Eq (BiMap k v) where
      == :: BiMap k v -> BiMap k v -> Bool
    (==) = Map k v -> Map k v -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Map k v -> Map k v -> Bool)
    -> (BiMap k v -> Map k v) -> BiMap k v -> BiMap k v -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` BiMap k v -> Map k v
    forall k v. BiMap k v -> Map k v
    biMapThere

    instance (Ord k, Ord v) => Ord (BiMap k v) where
      compare :: BiMap k v -> BiMap k v -> Ordering
    compare = Map k v -> Map k v -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Map k v -> Map k v -> Ordering)
    -> (BiMap k v -> Map k v) -> BiMap k v -> BiMap k v -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` BiMap k v -> Map k v
    forall k v. BiMap k v -> Map k v
    biMapThere

    instance (Show k, Show v) => Show (BiMap k v) where
      show :: BiMap k v -> String
    show BiMap k v
    bimap = String
    "Agda.Utils.BiMap.fromList " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [(k, v)] -> String
    forall a. Show a => a -> String
    show (BiMap k v -> [(k, v)]
    forall k v. BiMap k v -> [(k, v)]
    toList BiMap k v
    bimap)