{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  ./Common/InjMap.hs
Description :  injective maps
Copyright   :  (c) Uni Bremen 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Injective maps
-}

module Common.InjMap
    ( InjMap
    , unsafeConstructInjMap
    , getAToB
    , getBToA
    , empty
    , member
    , insert
    , delete
    , deleteA
    , deleteB
    , lookupWithA
    , lookupWithB
    , updateBWithA
    , updateAWithB
    ) where

import Data.Data
import qualified Data.Map as Map

import GHC.Generics (Generic)

-- | the data type of injective maps
data InjMap a b = InjMap
    { InjMap a b -> Map a b
getAToB :: Map.Map a b -- ^ the actual injective map
    , InjMap a b -> Map b a
getBToA :: Map.Map b a -- ^ the inverse map
    } deriving (Int -> InjMap a b -> ShowS
[InjMap a b] -> ShowS
InjMap a b -> String
(Int -> InjMap a b -> ShowS)
-> (InjMap a b -> String)
-> ([InjMap a b] -> ShowS)
-> Show (InjMap a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> InjMap a b -> ShowS
forall a b. (Show a, Show b) => [InjMap a b] -> ShowS
forall a b. (Show a, Show b) => InjMap a b -> String
showList :: [InjMap a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [InjMap a b] -> ShowS
show :: InjMap a b -> String
$cshow :: forall a b. (Show a, Show b) => InjMap a b -> String
showsPrec :: Int -> InjMap a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> InjMap a b -> ShowS
Show, InjMap a b -> InjMap a b -> Bool
(InjMap a b -> InjMap a b -> Bool)
-> (InjMap a b -> InjMap a b -> Bool) -> Eq (InjMap a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => InjMap a b -> InjMap a b -> Bool
/= :: InjMap a b -> InjMap a b -> Bool
$c/= :: forall a b. (Eq a, Eq b) => InjMap a b -> InjMap a b -> Bool
== :: InjMap a b -> InjMap a b -> Bool
$c== :: forall a b. (Eq a, Eq b) => InjMap a b -> InjMap a b -> Bool
Eq, Eq (InjMap a b)
Eq (InjMap a b) =>
(InjMap a b -> InjMap a b -> Ordering)
-> (InjMap a b -> InjMap a b -> Bool)
-> (InjMap a b -> InjMap a b -> Bool)
-> (InjMap a b -> InjMap a b -> Bool)
-> (InjMap a b -> InjMap a b -> Bool)
-> (InjMap a b -> InjMap a b -> InjMap a b)
-> (InjMap a b -> InjMap a b -> InjMap a b)
-> Ord (InjMap a b)
InjMap a b -> InjMap a b -> Bool
InjMap a b -> InjMap a b -> Ordering
InjMap a b -> InjMap a b -> InjMap a b
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a b. (Ord a, Ord b) => Eq (InjMap a b)
forall a b. (Ord a, Ord b) => InjMap a b -> InjMap a b -> Bool
forall a b. (Ord a, Ord b) => InjMap a b -> InjMap a b -> Ordering
forall a b.
(Ord a, Ord b) =>
InjMap a b -> InjMap a b -> InjMap a b
min :: InjMap a b -> InjMap a b -> InjMap a b
$cmin :: forall a b.
(Ord a, Ord b) =>
InjMap a b -> InjMap a b -> InjMap a b
max :: InjMap a b -> InjMap a b -> InjMap a b
$cmax :: forall a b.
(Ord a, Ord b) =>
InjMap a b -> InjMap a b -> InjMap a b
>= :: InjMap a b -> InjMap a b -> Bool
$c>= :: forall a b. (Ord a, Ord b) => InjMap a b -> InjMap a b -> Bool
> :: InjMap a b -> InjMap a b -> Bool
$c> :: forall a b. (Ord a, Ord b) => InjMap a b -> InjMap a b -> Bool
<= :: InjMap a b -> InjMap a b -> Bool
$c<= :: forall a b. (Ord a, Ord b) => InjMap a b -> InjMap a b -> Bool
< :: InjMap a b -> InjMap a b -> Bool
$c< :: forall a b. (Ord a, Ord b) => InjMap a b -> InjMap a b -> Bool
compare :: InjMap a b -> InjMap a b -> Ordering
$ccompare :: forall a b. (Ord a, Ord b) => InjMap a b -> InjMap a b -> Ordering
$cp1Ord :: forall a b. (Ord a, Ord b) => Eq (InjMap a b)
Ord, Typeable, Typeable (InjMap a b)
Constr
DataType
Typeable (InjMap a b) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> InjMap a b -> c (InjMap a b))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (InjMap a b))
-> (InjMap a b -> Constr)
-> (InjMap a b -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (InjMap a b)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (InjMap a b)))
-> ((forall b. Data b => b -> b) -> InjMap a b -> InjMap a b)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> InjMap a b -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> InjMap a b -> r)
-> (forall u. (forall d. Data d => d -> u) -> InjMap a b -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> InjMap a b -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b))
-> Data (InjMap a b)
InjMap a b -> Constr
InjMap a b -> DataType
(forall b. Data b => b -> b) -> InjMap a b -> InjMap a b
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InjMap a b -> c (InjMap a b)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InjMap a b)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InjMap a b))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> InjMap a b -> u
forall u. (forall d. Data d => d -> u) -> InjMap a b -> [u]
forall a b. (Data a, Data b, Ord a, Ord b) => Typeable (InjMap a b)
forall a b. (Data a, Data b, Ord a, Ord b) => InjMap a b -> Constr
forall a b.
(Data a, Data b, Ord a, Ord b) =>
InjMap a b -> DataType
forall a b.
(Data a, Data b, Ord a, Ord b) =>
(forall b. Data b => b -> b) -> InjMap a b -> InjMap a b
forall a b u.
(Data a, Data b, Ord a, Ord b) =>
Int -> (forall d. Data d => d -> u) -> InjMap a b -> u
forall a b u.
(Data a, Data b, Ord a, Ord b) =>
(forall d. Data d => d -> u) -> InjMap a b -> [u]
forall a b r r'.
(Data a, Data b, Ord a, Ord b) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InjMap a b -> r
forall a b r r'.
(Data a, Data b, Ord a, Ord b) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InjMap a b -> r
forall a b (m :: * -> *).
(Data a, Data b, Ord a, Ord b, Monad m) =>
(forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
forall a b (m :: * -> *).
(Data a, Data b, Ord a, Ord b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
forall a b (c :: * -> *).
(Data a, Data b, Ord a, Ord b) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InjMap a b)
forall a b (c :: * -> *).
(Data a, Data b, Ord a, Ord b) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InjMap a b -> c (InjMap a b)
forall a b (t :: * -> *) (c :: * -> *).
(Data a, Data b, Ord a, Ord b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (InjMap a b))
forall a b (t :: * -> * -> *) (c :: * -> *).
(Data a, Data b, Ord a, Ord b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InjMap a b))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InjMap a b -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InjMap a b -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InjMap a b)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InjMap a b -> c (InjMap a b)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (InjMap a b))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InjMap a b))
$cInjMap :: Constr
$tInjMap :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
$cgmapMo :: forall a b (m :: * -> *).
(Data a, Data b, Ord a, Ord b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
gmapMp :: (forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
$cgmapMp :: forall a b (m :: * -> *).
(Data a, Data b, Ord a, Ord b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
gmapM :: (forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
$cgmapM :: forall a b (m :: * -> *).
(Data a, Data b, Ord a, Ord b, Monad m) =>
(forall d. Data d => d -> m d) -> InjMap a b -> m (InjMap a b)
gmapQi :: Int -> (forall d. Data d => d -> u) -> InjMap a b -> u
$cgmapQi :: forall a b u.
(Data a, Data b, Ord a, Ord b) =>
Int -> (forall d. Data d => d -> u) -> InjMap a b -> u
gmapQ :: (forall d. Data d => d -> u) -> InjMap a b -> [u]
$cgmapQ :: forall a b u.
(Data a, Data b, Ord a, Ord b) =>
(forall d. Data d => d -> u) -> InjMap a b -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InjMap a b -> r
$cgmapQr :: forall a b r r'.
(Data a, Data b, Ord a, Ord b) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InjMap a b -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InjMap a b -> r
$cgmapQl :: forall a b r r'.
(Data a, Data b, Ord a, Ord b) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InjMap a b -> r
gmapT :: (forall b. Data b => b -> b) -> InjMap a b -> InjMap a b
$cgmapT :: forall a b.
(Data a, Data b, Ord a, Ord b) =>
(forall b. Data b => b -> b) -> InjMap a b -> InjMap a b
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InjMap a b))
$cdataCast2 :: forall a b (t :: * -> * -> *) (c :: * -> *).
(Data a, Data b, Ord a, Ord b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InjMap a b))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (InjMap a b))
$cdataCast1 :: forall a b (t :: * -> *) (c :: * -> *).
(Data a, Data b, Ord a, Ord b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (InjMap a b))
dataTypeOf :: InjMap a b -> DataType
$cdataTypeOf :: forall a b.
(Data a, Data b, Ord a, Ord b) =>
InjMap a b -> DataType
toConstr :: InjMap a b -> Constr
$ctoConstr :: forall a b. (Data a, Data b, Ord a, Ord b) => InjMap a b -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InjMap a b)
$cgunfold :: forall a b (c :: * -> *).
(Data a, Data b, Ord a, Ord b) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InjMap a b)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InjMap a b -> c (InjMap a b)
$cgfoldl :: forall a b (c :: * -> *).
(Data a, Data b, Ord a, Ord b) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InjMap a b -> c (InjMap a b)
$cp1Data :: forall a b. (Data a, Data b, Ord a, Ord b) => Typeable (InjMap a b)
Data, (forall x. InjMap a b -> Rep (InjMap a b) x)
-> (forall x. Rep (InjMap a b) x -> InjMap a b)
-> Generic (InjMap a b)
forall x. Rep (InjMap a b) x -> InjMap a b
forall x. InjMap a b -> Rep (InjMap a b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (InjMap a b) x -> InjMap a b
forall a b x. InjMap a b -> Rep (InjMap a b) x
$cto :: forall a b x. Rep (InjMap a b) x -> InjMap a b
$cfrom :: forall a b x. InjMap a b -> Rep (InjMap a b) x
Generic)

-- | for serialization only
unsafeConstructInjMap :: Map.Map a b -> Map.Map b a -> InjMap a b
unsafeConstructInjMap :: Map a b -> Map b a -> InjMap a b
unsafeConstructInjMap = Map a b -> Map b a -> InjMap a b
forall a b. Map a b -> Map b a -> InjMap a b
InjMap

-- * the visible interface

-- | get an empty injective map
empty :: InjMap a b
empty :: InjMap a b
empty = Map a b -> Map b a -> InjMap a b
forall a b. Map a b -> Map b a -> InjMap a b
InjMap Map a b
forall k a. Map k a
Map.empty Map b a
forall k a. Map k a
Map.empty

{- | insert a pair into the given injective map. An existing key and the
corresponding content will be overridden. -}
insert :: (Ord a, Ord b) => a -> b -> InjMap a b -> InjMap a b
insert :: a -> b -> InjMap a b -> InjMap a b
insert a :: a
a b :: b
b i :: InjMap a b
i = let InjMap m :: Map a b
m n :: Map b a
n = a -> b -> InjMap a b -> InjMap a b
forall a b. (Ord a, Ord b) => a -> b -> InjMap a b -> InjMap a b
delete a
a b
b InjMap a b
i in
    Map a b -> Map b a -> InjMap a b
forall a b. Map a b -> Map b a -> InjMap a b
InjMap (a -> b -> Map a b -> Map a b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
a b
b Map a b
m) (b -> a -> Map b a -> Map b a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert b
b a
a Map b a
n)

{- | delete the pair with the given key in the injective
map. Possibly two pairs may be deleted if the pair is not a member. -}
delete :: (Ord a, Ord b) => a -> b -> InjMap a b -> InjMap a b
delete :: a -> b -> InjMap a b -> InjMap a b
delete a :: a
a b :: b
b (InjMap m :: Map a b
m n :: Map b a
n) =
       Map a b -> Map b a -> InjMap a b
forall a b. Map a b -> Map b a -> InjMap a b
InjMap (a -> Map a b -> Map a b
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (a -> b -> Map b a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault a
a b
b Map b a
n) (Map a b -> Map a b) -> Map a b -> Map a b
forall a b. (a -> b) -> a -> b
$ a -> Map a b -> Map a b
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete a
a Map a b
m)
              (b -> Map b a -> Map b a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (b -> a -> Map a b -> b
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault b
b a
a Map a b
m) (Map b a -> Map b a) -> Map b a -> Map b a
forall a b. (a -> b) -> a -> b
$ b -> Map b a -> Map b a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete b
b Map b a
n)

-- | delete domain entry
deleteA :: (Ord a, Ord b) => a -> InjMap a b -> InjMap a b
deleteA :: a -> InjMap a b -> InjMap a b
deleteA a :: a
a i :: InjMap a b
i@(InjMap m :: Map a b
m n :: Map b a
n) = case a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a Map a b
m of
  Just b :: b
b -> case b -> Map b a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup b
b Map b a
n of
    Just e :: a
e -> if a
e a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a then Map a b -> Map b a -> InjMap a b
forall a b. Map a b -> Map b a -> InjMap a b
InjMap (a -> Map a b -> Map a b
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete a
a Map a b
m) (Map b a -> InjMap a b) -> Map b a -> InjMap a b
forall a b. (a -> b) -> a -> b
$ b -> Map b a -> Map b a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete b
b Map b a
n
              else String -> InjMap a b
forall a. HasCallStack => String -> a
error "InjMap.deleteA1"
    Nothing -> String -> InjMap a b
forall a. HasCallStack => String -> a
error "InjMap.deleteA2"
  Nothing -> InjMap a b
i

-- | delete codomain entry
deleteB :: (Ord a, Ord b) => b -> InjMap a b -> InjMap a b
deleteB :: b -> InjMap a b -> InjMap a b
deleteB b :: b
b = InjMap b a -> InjMap a b
forall a b. InjMap a b -> InjMap b a
transpose (InjMap b a -> InjMap a b)
-> (InjMap a b -> InjMap b a) -> InjMap a b -> InjMap a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> InjMap b a -> InjMap b a
forall a b. (Ord a, Ord b) => a -> InjMap a b -> InjMap a b
deleteA b
b (InjMap b a -> InjMap b a)
-> (InjMap a b -> InjMap b a) -> InjMap a b -> InjMap b a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjMap a b -> InjMap b a
forall a b. InjMap a b -> InjMap b a
transpose

-- | check membership of an injective pair
member :: (Ord a, Ord b) => a -> b -> InjMap a b -> Bool
member :: a -> b -> InjMap a b -> Bool
member a :: a
a b :: b
b (InjMap m :: Map a b
m n :: Map b a
n) = case (a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a Map a b
m, b -> Map b a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup b
b Map b a
n) of
   (Just x :: b
x, Just y :: a
y) | b
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b Bool -> Bool -> Bool
&& a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a -> Bool
True
   _ -> Bool
False

-- | transpose to avoid duplicate code
transpose :: InjMap a b -> InjMap b a
transpose :: InjMap a b -> InjMap b a
transpose (InjMap m :: Map a b
m n :: Map b a
n) = Map b a -> Map a b -> InjMap b a
forall a b. Map a b -> Map b a -> InjMap a b
InjMap Map b a
n Map a b
m

-- | look up the content at domain
lookupWithA :: (Ord a, Ord b) => a -> InjMap a b -> Maybe b
lookupWithA :: a -> InjMap a b -> Maybe b
lookupWithA a :: a
a (InjMap m :: Map a b
m n :: Map b a
n) = case a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a Map a b
m of
    Just b :: b
b -> case b -> Map b a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup b
b Map b a
n of
        Just e :: a
e -> if a
e a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a then b -> Maybe b
forall a. a -> Maybe a
Just b
b
                     else String -> Maybe b
forall a. HasCallStack => String -> a
error "InjMap.lookupWith1"
        Nothing -> String -> Maybe b
forall a. HasCallStack => String -> a
error "InjMap.lookupWith2"
    Nothing -> Maybe b
forall a. Maybe a
Nothing
-- the errors indicate that the injectivity is destroyed

-- | look up the content at codomain
lookupWithB :: (Ord a, Ord b) => b -> InjMap a b -> Maybe a
lookupWithB :: b -> InjMap a b -> Maybe a
lookupWithB y :: b
y = b -> InjMap b a -> Maybe a
forall a b. (Ord a, Ord b) => a -> InjMap a b -> Maybe b
lookupWithA b
y (InjMap b a -> Maybe a)
-> (InjMap a b -> InjMap b a) -> InjMap a b -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjMap a b -> InjMap b a
forall a b. InjMap a b -> InjMap b a
transpose

-- | update codomain at domain value that must be defined
updateBWithA :: (Ord a, Ord b) => a -> b -> InjMap a b -> InjMap a b
updateBWithA :: a -> b -> InjMap a b -> InjMap a b
updateBWithA a :: a
a b :: b
b m :: InjMap a b
m = case a -> InjMap a b -> Maybe b
forall a b. (Ord a, Ord b) => a -> InjMap a b -> Maybe b
lookupWithA a
a InjMap a b
m of
    Nothing -> String -> InjMap a b
forall a. HasCallStack => String -> a
error "InjMap.updateBWithA"
    _ -> a -> b -> InjMap a b -> InjMap a b
forall a b. (Ord a, Ord b) => a -> b -> InjMap a b -> InjMap a b
insert a
a b
b InjMap a b
m

-- | update domain at codomain value that must be defined
updateAWithB :: (Ord a, Ord b) => b -> a -> InjMap a b -> InjMap a b
updateAWithB :: b -> a -> InjMap a b -> InjMap a b
updateAWithB b :: b
b newA :: a
newA = InjMap b a -> InjMap a b
forall a b. InjMap a b -> InjMap b a
transpose (InjMap b a -> InjMap a b)
-> (InjMap a b -> InjMap b a) -> InjMap a b -> InjMap a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a -> InjMap b a -> InjMap b a
forall a b. (Ord a, Ord b) => a -> b -> InjMap a b -> InjMap a b
updateBWithA b
b a
newA (InjMap b a -> InjMap b a)
-> (InjMap a b -> InjMap b a) -> InjMap a b -> InjMap b a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjMap a b -> InjMap b a
forall a b. InjMap a b -> InjMap b a
transpose