-- | 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 = forall (t :: * -> *). Foldable t => t Bool -> Bool
and
  [ v
v1 forall a. Eq a => a -> a -> Bool
== v
v2
  | v
v1 <- [v]
vs
  , v
v2 <- [v]
vs
  , forall a. Maybe a -> Bool
isJust (forall a. HasTag a => a -> Maybe (Tag a)
tag v
v1)
  , forall a. HasTag a => a -> Maybe (Tag a)
tag v
v1 forall a. Eq a => a -> a -> Bool
== 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 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 forall a. Eq a => a -> a -> Bool
==
  forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (Tag v
k', k
k)
    | (k
k, v
v) <- forall k a. Map k a -> [(k, a)]
Map.toList Map k v
t
    , Just Tag v
k' <- [forall a. HasTag a => a -> Maybe (Tag a)
tag v
v]
    ]
    Bool -> Bool -> Bool
&&
  forall v. (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
tagInjectiveFor (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall k v. BiMap k v -> [(k, v)]
toList BiMap k v
m)

instance Null (BiMap k v) where
  empty :: BiMap k v
empty = forall k v. Map k v -> Map (Tag v) k -> BiMap k v
BiMap forall k a. Map k a
Map.empty forall k a. Map k a
Map.empty
  null :: BiMap k v -> Bool
null  = forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Ord k => k -> Map k a -> Bool
Map.member k
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Ord k => k -> Map k a -> Bool
Map.member Tag v
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Tag v
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
  forall k v. Map k v -> Map (Tag v) k -> BiMap k v
BiMap
    (forall k a. k -> a -> Map k a
Map.singleton k
k v
v)
    (case forall a. HasTag a => a -> Maybe (Tag a)
tag v
v of
       Maybe (Tag v)
Nothing -> forall k a. Map k a
Map.empty
       Just 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) =
  forall k v. Map k v -> Map (Tag v) k -> BiMap k v
BiMap
    (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k v
v Map k v
t)
    (case 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' -> 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 forall a. HasTag a => a -> Maybe (Tag a)
tag forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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' -> 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 forall a. HasTag a => a -> Maybe (Tag a)
tag v
v of
    Maybe (Tag v)
Nothing -> Bool
True
    Just Tag v
_  ->
      Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(k
k', v
v') -> k
k' forall a. Eq a => a -> a -> Bool
/= k
k Bool -> Bool -> Bool
&& forall a. HasTag a => a -> Maybe (Tag a)
tag v
v forall a. Eq a => a -> a -> Bool
== forall a. HasTag a => a -> Maybe (Tag a)
tag v
v') forall a b. (a -> b) -> a -> b
$ 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) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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) forall a. Maybe a
Nothing
  forall (m :: * -> *) a. Monad m => a -> m a
return 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  -> 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe v -> m (Maybe v)
f Maybe v
v)
    forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall a. HasTag a => a -> Maybe (Tag a)
tag forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe v
v, forall a. HasTag a => a -> Maybe (Tag a)
tag forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe v
r)
    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 forall a. Eq a => a -> a -> Bool
== Maybe (Tag v)
k'2
    then forall a. a -> a
id
    else forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k) Maybe (Tag v)
k'2 forall b c a. (b -> c) -> (a -> b) -> a -> c
.
         forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id 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 = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ 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 a. a -> Identity a
Identity 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 forall a. HasTag a => a -> Maybe (Tag a)
tag forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe v -> Maybe v
f (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' -> forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ forall a. a -> Maybe a
Just Tag v
k' forall a. Eq a => a -> a -> Bool
/= forall a. HasTag a => a -> Maybe (Tag a)
tag v
v
      | (k
k'', v
v) <- forall k v. BiMap k v -> [(k, v)]
toList BiMap k v
m
      , k
k'' 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 = 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 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 = 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 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 = forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> Maybe v) -> k -> BiMap k v -> BiMap k v
update (forall a. a -> Maybe a
Just 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 = forall k v.
(Ord k, Eq v, Eq (Tag v), HasTag v) =>
(v -> Maybe v) -> k -> BiMap k v -> Bool
updatePrecondition (forall a. a -> Maybe a
Just 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 = forall a b. (a, b) -> (b, a)
swap forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> (a, s)
runState (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 -> State (Maybe v) (Maybe v)
f' k
k BiMap k v
m) forall a. Maybe a
Nothing
  where
  f' :: Maybe v -> State (Maybe v) (Maybe v)
  f' :: Maybe v -> State (Maybe v) (Maybe v)
f' Maybe v
Nothing     = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just v
v
  f' r :: Maybe v
r@(Just v
v') = do
    forall s (m :: * -> *). MonadState s m => s -> m ()
put Maybe v
r
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 =
  forall k v.
(Ord k, Eq v, Eq (Tag v), HasTag v) =>
(Maybe v -> Maybe v) -> k -> BiMap k v -> Bool
alterPrecondition (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k v. (Ord k, Ord (Tag v), HasTag v) => [(k, v)] -> BiMap k v
fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\(k
k, v
v) -> (k
k, k -> v -> v
f k
k v
v)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
  forall k v. (Eq k, Eq v, Eq (Tag v), HasTag v) => [(k, v)] -> Bool
fromListPrecondition forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\(k
k, v
v) -> (k
k, k -> v -> v
f k
k v
v)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall k v. Map k v -> Map (Tag v) k -> BiMap k v
BiMap (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 = forall (t :: * -> *). Foldable t => t Bool -> Bool
and
  [ forall a. HasTag a => a -> Maybe (Tag a)
tag (k -> v -> v
f k
k v
v) forall a. Eq a => a -> a -> Bool
== forall a. HasTag a => a -> Maybe (Tag a)
tag v
v
  | (k
k, v
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) =
  forall k v. Map k v -> Map (Tag v) k -> BiMap k v
BiMap (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map k v
t1 Map k v
t2) (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
_) =
  forall (t :: * -> *). Foldable t => t Bool -> Bool
and
    [ forall a. HasTag a => a -> Maybe (Tag a)
tag v
v2 forall a. Eq a => a -> a -> Bool
== forall a. Maybe a
Nothing Bool -> Bool -> Bool
|| forall a. HasTag a => a -> Maybe (Tag a)
tag v
v1 forall a. Eq a => a -> a -> Bool
== forall a. HasTag a => a -> Maybe (Tag a)
tag v
v2
    | (v
v1, v
v2) <- forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ 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
&&
  forall (t :: * -> *). Foldable t => t Bool -> Bool
and
    [ k
k1 forall a. Eq a => a -> a -> Bool
== k
k2
    | (k
k1, v
v1) <- forall k v. BiMap k v -> [(k, v)]
toList BiMap k v
m1
    , (k
k2, v
v2) <- forall k v. BiMap k v -> [(k, v)]
toList BiMap k v
m2
    , forall a. HasTag a => a -> Maybe (Tag a)
tag v
v1 forall a. Eq a => a -> a -> Bool
== forall a. HasTag a => a -> Maybe (Tag a)
tag v
v2
    , forall a. Maybe a -> Bool
isJust (forall a. HasTag a => a -> Maybe (Tag a)
tag v
v1)
    ]
    Bool -> Bool -> Bool
&&
  forall v. (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
tagInjectiveFor
    ([ v
v1
     | (k
_, v
v1) <- forall k v. BiMap k v -> [(k, v)]
toList BiMap k v
m1
     ] forall a. [a] -> [a] -> [a]
++
     [ v
v2
     | (k
k2, v
v2) <- forall k v. BiMap k v -> [(k, v)]
toList BiMap k v
m2
     , Bool -> Bool
not (k
k2 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [k]
ks1)
     ])
  where
  ks1 :: [k]
ks1 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall k v.
(Ord k, HasTag v, Ord (Tag v)) =>
k -> v -> BiMap k v -> BiMap k v
insert) 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 =
  forall (t :: * -> *). Foldable t => t Bool -> Bool
and
    [ k
k1 forall a. Eq a => a -> a -> Bool
== k
k2
    | (k
k1, v
v1) <- [(k, v)]
kvs
    , (k
k2, v
v2) <- [(k, v)]
kvs
    , forall a. Maybe a -> Bool
isJust (forall a. HasTag a => a -> Maybe (Tag a)
tag v
v1)
    , forall a. Maybe a -> Bool
isJust (forall a. HasTag a => a -> Maybe (Tag a)
tag v
v2)
    , v
v1 forall a. Eq a => a -> a -> Bool
== v
v2
    ]
    Bool -> Bool -> Bool
&&
  forall v. (Eq v, Eq (Tag v), HasTag v) => [v] -> Bool
tagInjectiveFor (forall a b. (a -> b) -> [a] -> [b]
map 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 = forall k a. Map k a -> [(k, a)]
Map.toAscList forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Map k a -> [k]
Map.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Map k a -> [a]
Map.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) =
  forall k v. Map k v -> Map (Tag v) k -> BiMap k v
BiMap (forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(k, v)]
t) (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) =
  forall a. Ord a => [a] -> Bool
fastDistinct (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(k, v)]
kvs) Bool -> Bool -> Bool
&& forall a. Ord a => [a] -> Bool
sorted (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(k, v)]
kvs)
    Bool -> Bool -> Bool
&&
  forall a. Ord a => [a] -> Bool
fastDistinct (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Tag v, k)]
kks) Bool -> Bool -> Bool
&& forall a. Ord a => [a] -> Bool
sorted (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Tag v, k)]
kks)
    Bool -> Bool -> Bool
&&
  [(Tag v, k)]
kks forall a. Eq a => a -> a -> Bool
==
  forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> a
fst)
    [ (Tag v
k', k
k)
    | (k
k, v
v) <- [(k, v)]
kvs
    , Just Tag v
k' <- [forall a. HasTag a => a -> Maybe (Tag a)
tag v
v]
    ]
    Bool -> Bool -> 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) =
  (forall k a. Map k a -> [(k, a)]
Map.toAscList Map k v
t, 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
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 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 = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 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 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k v. BiMap k v -> [(k, v)]
toList BiMap k v
bimap)