{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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 (on)
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
$cfrom :: forall k v x. BiMap k v -> Rep (BiMap k v) x
from :: forall x. BiMap k v -> Rep (BiMap k v) x
$cto :: forall k v x. Rep (BiMap k v) x -> BiMap k v
to :: forall x. Rep (BiMap k v) x -> BiMap k v
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

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

source :: Ord k => k -> BiMap k v -> Bool
source :: forall k v. Ord k => k -> BiMap k v -> Bool
source k
k = k -> Map k v -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member k
k (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

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

target :: Ord (Tag v) => Tag v -> BiMap k v -> Bool
target :: forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Bool
target Tag v
k = Tag v -> Map (Tag v) k -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Tag v
k (Map (Tag v) k -> Bool)
-> (BiMap k v -> Map (Tag v) k) -> BiMap k v -> Bool
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

-- | 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 a. a -> m a
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 (m :: * -> *) a.
Monad m =>
m a -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m a
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 a. a -> StateT (Maybe (Maybe (Tag v), Maybe (Tag v))) m a
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 a. a -> StateT (Maybe v) Identity a
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 a. a -> StateT (Maybe v) Identity a
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 a. Eq a => a -> [a] -> 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 a b. (a -> b -> b) -> b -> [a] -> b
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)