{-|
Copyright        : (c) Galois, Inc 2017

This module defines a 2-tuple where both elements are parameterized over the
same existentially quantified parameter.

-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Data.Parameterized.Pair
  ( Pair(..)
  , fstPair
  , sndPair
  , viewPair
  ) where

import Data.Parameterized.Classes
import Data.Parameterized.Some
import Data.Parameterized.TraversableF

-- | Like a 2-tuple, but with an existentially quantified parameter that both of
-- the elements share.
data Pair (a :: k -> *) (b :: k -> *) where
  Pair :: !(a tp) -> !(b tp) -> Pair a b

instance (TestEquality a, EqF b) => Eq (Pair a b) where
  Pair xa xb == Pair ya yb =
    case testEquality xa ya of
      Just Refl -> eqF xb yb
      Nothing -> False

instance FunctorF (Pair a) where
  fmapF f (Pair x y) = Pair x (f y)

instance FoldableF (Pair a) where
  foldMapF f (Pair _ y) = f y
  foldrF f z (Pair _ y) = f y z

-- | Extract the first element of a pair.
fstPair :: Pair a b -> Some a
fstPair (Pair x _) = Some x

-- | Extract the second element of a pair.
sndPair :: Pair a b -> Some b
sndPair (Pair _ y) = Some y

-- | Project out of Pair.
viewPair :: (forall tp. a tp -> b tp -> c) -> Pair a b -> c
viewPair f (Pair x y) = f x y