    module Agda.Utils.Tuple
      ( (-*-)
      , mapFst
      , mapSnd
      , (/\)
      , fst3
      , snd3
      , thd3
      , swap
      , uncurry3
      , uncurry4
      , mapPairM
      , mapFstM
      , mapSndM
      , Pair(..)
      ) where

    import Control.Arrow  ((&&&))
    import Data.Bifunctor (bimap, first, second)
    import Data.Tuple (swap)

    infix 2 -*-
    infix 3 /\ -- backslashes at EOL interact badly with CPP...

    -- | Bifunctoriality for pairs.
    (-*-) :: (a -> c) -> (b -> d) -> (a,b) -> (c,d)
    -*- :: forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
    (-*-) = (a -> c) -> (b -> d) -> (a, b) -> (c, d)
    forall (p :: * -> * -> *) a b c d.
    Bifunctor p =>
    (a -> b) -> (c -> d) -> p a c -> p b d
    bimap

    -- | @mapFst f = f -*- id@
    mapFst :: (a -> c) -> (a,b) -> (c,b)
    mapFst :: forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst = (a -> c) -> (a, b) -> (c, b)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first

    -- | @mapSnd g = id -*- g@
    mapSnd :: (b -> d) -> (a,b) -> (a,d)
    mapSnd :: forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd = (b -> d) -> (a, b) -> (a, d)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second

    -- | Lifted pairing.
    (/\) :: (a -> b) -> (a -> c) -> a -> (b,c)
    /\ :: forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
    (/\) = (a -> b) -> (a -> c) -> a -> (b, c)
    forall (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    (&&&)

    -- * Triple (stolen from Data.Tuple.HT)

    {-# INLINE fst3 #-}
    fst3 :: (a,b,c) -> a
    fst3 :: forall a b c. (a, b, c) -> a
    fst3 ~(a
    x,b
    _,c
    _) = a
    x

    {-# INLINE snd3 #-}
    snd3 :: (a,b,c) -> b
    snd3 :: forall a b c. (a, b, c) -> b
    snd3 ~(a
    _,b
    x,c
    _) = b
    x

    {-# INLINE thd3 #-}
    thd3 :: (a,b,c) -> c
    thd3 :: forall a b c. (a, b, c) -> c
    thd3 ~(a
    _,b
    _,c
    x) = c
    x

    {-# INLINE uncurry3 #-}
    uncurry3 :: (a -> b -> c -> d) -> (a,b,c) -> d
    uncurry3 :: forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
    uncurry3 a -> b -> c -> d
    f ~(a
    x,b
    y,c
    z) = a -> b -> c -> d
    f a
    x b
    y c
    z

    {-# INLINE uncurry4 #-}
    uncurry4 :: (a -> b -> c -> d -> e) -> (a,b,c,d) -> e
    uncurry4 :: forall a b c d e. (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
    uncurry4 a -> b -> c -> d -> e
    f ~(a
    w,b
    x,c
    y,d
    z) = a -> b -> c -> d -> e
    f a
    w b
    x c
    y d
    z

    -- | Monadic version of '-*-'.
    mapPairM :: (Applicative m) => (a -> m c) -> (b -> m d) -> (a,b) -> m (c,d)
    mapPairM :: forall (m :: * -> *) a c b d.
    Applicative m =>
    (a -> m c) -> (b -> m d) -> (a, b) -> m (c, d)
    mapPairM a -> m c
    f b -> m d
    g ~(a
    a,b
    b) = (,) (c -> d -> (c, d)) -> m c -> m (d -> (c, d))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m c
    f a
    a m (d -> (c, d)) -> m d -> m (c, d)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m d
    g b
    b

    -- | Monadic 'mapFst'.
    mapFstM :: (Applicative m) => (a -> m c) -> (a,b) -> m (c,b)
    mapFstM :: forall (m :: * -> *) a c b.
    Applicative m =>
    (a -> m c) -> (a, b) -> m (c, b)
    mapFstM a -> m c
    f ~(a
    a,b
    b) = (,b
    b) (c -> (c, b)) -> m c -> m (c, b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m c
    f a
    a

    -- | Monadic 'mapSnd'.
    mapSndM :: (Applicative m) => (b -> m d) -> (a,b) -> m (a,d)
    mapSndM :: forall (m :: * -> *) b d a.
    Applicative m =>
    (b -> m d) -> (a, b) -> m (a, d)
    mapSndM b -> m d
    f ~(a
    a,b
    b) = (a
    a,) (d -> (a, d)) -> m d -> m (a, d)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m d
    f b
    b

    data Pair a = Pair a a
      deriving (Pair a -> Pair a -> Bool
    (Pair a -> Pair a -> Bool)
    -> (Pair a -> Pair a -> Bool) -> Eq (Pair a)
    forall a. Eq a => Pair a -> Pair a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Pair a -> Pair a -> Bool
    $c/= :: forall a. Eq a => Pair a -> Pair a -> Bool
    == :: Pair a -> Pair a -> Bool
    $c== :: forall a. Eq a => Pair a -> Pair a -> Bool
    Eq, (forall a b. (a -> b) -> Pair a -> Pair b)
    -> (forall a b. a -> Pair b -> Pair a) -> Functor Pair
    forall a b. a -> Pair b -> Pair a
    forall a b. (a -> b) -> Pair a -> Pair b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Pair b -> Pair a
    $c<$ :: forall a b. a -> Pair b -> Pair a
    fmap :: forall a b. (a -> b) -> Pair a -> Pair b
    $cfmap :: forall a b. (a -> b) -> Pair a -> Pair b
    Functor, (forall m. Monoid m => Pair m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Pair a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Pair a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Pair a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Pair a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Pair a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Pair a -> b)
    -> (forall a. (a -> a -> a) -> Pair a -> a)
    -> (forall a. (a -> a -> a) -> Pair a -> a)
    -> (forall a. Pair a -> [a])
    -> (forall a. Pair a -> Bool)
    -> (forall a. Pair a -> Int)
    -> (forall a. Eq a => a -> Pair a -> Bool)
    -> (forall a. Ord a => Pair a -> a)
    -> (forall a. Ord a => Pair a -> a)
    -> (forall a. Num a => Pair a -> a)
    -> (forall a. Num a => Pair a -> a)
    -> Foldable Pair
    forall a. Eq a => a -> Pair a -> Bool
    forall a. Num a => Pair a -> a
    forall a. Ord a => Pair a -> a
    forall m. Monoid m => Pair m -> m
    forall a. Pair a -> Bool
    forall a. Pair a -> Int
    forall a. Pair a -> [a]
    forall a. (a -> a -> a) -> Pair a -> a
    forall m a. Monoid m => (a -> m) -> Pair a -> m
    forall b a. (b -> a -> b) -> b -> Pair a -> b
    forall a b. (a -> b -> b) -> b -> Pair a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    product :: forall a. Num a => Pair a -> a
    $cproduct :: forall a. Num a => Pair a -> a
    sum :: forall a. Num a => Pair a -> a
    $csum :: forall a. Num a => Pair a -> a
    minimum :: forall a. Ord a => Pair a -> a
    $cminimum :: forall a. Ord a => Pair a -> a
    maximum :: forall a. Ord a => Pair a -> a
    $cmaximum :: forall a. Ord a => Pair a -> a
    elem :: forall a. Eq a => a -> Pair a -> Bool
    $celem :: forall a. Eq a => a -> Pair a -> Bool
    length :: forall a. Pair a -> Int
    $clength :: forall a. Pair a -> Int
    null :: forall a. Pair a -> Bool
    $cnull :: forall a. Pair a -> Bool
    toList :: forall a. Pair a -> [a]
    $ctoList :: forall a. Pair a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> Pair a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Pair a -> a
    foldr1 :: forall a. (a -> a -> a) -> Pair a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> Pair a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> Pair a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Pair a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Pair a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Pair a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Pair a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Pair a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Pair a -> b
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Pair a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> Pair a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Pair a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Pair a -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Pair a -> m
    fold :: forall m. Monoid m => Pair m -> m
    $cfold :: forall m. Monoid m => Pair m -> m
    Foldable, Functor Pair
    Foldable Pair
    Functor Pair
    -> Foldable Pair
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> Pair a -> f (Pair b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Pair (f a) -> f (Pair a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Pair a -> m (Pair b))
    -> (forall (m :: * -> *) a. Monad m => Pair (m a) -> m (Pair a))
    -> Traversable Pair
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => Pair (m a) -> m (Pair a)
    forall (f :: * -> *) a. Applicative f => Pair (f a) -> f (Pair a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pair a -> m (Pair b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pair a -> f (Pair b)
    sequence :: forall (m :: * -> *) a. Monad m => Pair (m a) -> m (Pair a)
    $csequence :: forall (m :: * -> *) a. Monad m => Pair (m a) -> m (Pair a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pair a -> m (Pair b)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pair a -> m (Pair b)
    sequenceA :: forall (f :: * -> *) a. Applicative f => Pair (f a) -> f (Pair a)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => Pair (f a) -> f (Pair a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pair a -> f (Pair b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pair a -> f (Pair b)
    Traversable)

    instance Applicative Pair where
      pure :: forall a. a -> Pair a
    pure a
    a                  = a -> a -> Pair a
    forall a. a -> a -> Pair a
    Pair a
    a a
    a
      Pair a -> b
    f a -> b
    f' <*> :: forall a b. Pair (a -> b) -> Pair a -> Pair b
    <*> Pair a
    a a
    a' = b -> b -> Pair b
    forall a. a -> a -> Pair a
    Pair (a -> b
    f a
    a) (a -> b
    f' a
    a')