------------------------------------------------------------------------
-- The Agda standard library
--
-- The Pair type which calls out to Haskell via the FFI
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible #-}
 
module Foreign.Haskell.Pair where
 
open import Level
open import Data.Product.Base using (_×_; _,_)
 
private
  variable
    a b : Level
    A : Set a
    B : Set b
 
------------------------------------------------------------------------
-- Definition
 
record Pair (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field  fst : A
         snd : B
infixr  _,_
open Pair public
 
{-# FOREIGN GHC type AgdaPair l1 l2 a b = (a , b) #-}
{-# COMPILE GHC Pair = data MAlonzo.Code.Foreign.Haskell.Pair.AgdaPair ((,)) #-}
 
------------------------------------------------------------------------
-- Conversion
 
toForeign : A × B → Pair A B
toForeign (a , b) = (a , b)
{-# WARNING_ON_USAGE toForeign
"Warning: toForeign was deprecated in 2.0.
Please use Foreign.Haskell.Coerce.coerce instead."
#-}
 
fromForeign : Pair A B → A × B
fromForeign (a , b) = (a , b)
{-# WARNING_ON_USAGE fromForeign
"Warning: fromForeign was deprecated in 2.0.
Please use Foreign.Haskell.Coerce.coerce instead."
#-}