------------------------------------------------------------------------
-- The Agda standard library
--
-- The Either type which calls out to Haskell via the FFI
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible #-}
 
module Foreign.Haskell.Either where
 
open import Level
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 
private
  variable
    a b : Level
    A : Set a
    B : Set b
 
------------------------------------------------------------------------
-- Definition
 
data Either (A : Set a) (B : Set b) : Set (a ⊔ b) where
  left  : A → Either A B
  right : B → Either A B
 
{-# FOREIGN GHC type AgdaEither l1 l2 a b = Either a b #-}
{-# COMPILE GHC Either = data MAlonzo.Code.Foreign.Haskell.Either.AgdaEither (Left | Right) #-}
 
------------------------------------------------------------------------
-- Conversion
 
toForeign : A ⊎ B → Either A B
toForeign (inj₁ a) = left a
toForeign (inj₂ b) = right b
{-# WARNING_ON_USAGE toForeign
"Warning: toForeign was deprecated in 2.0.
Please use Foreign.Haskell.Coerce.coerce instead."
#-}
 
fromForeign : Either A B → A ⊎ B
fromForeign (left a)  = inj₁ a
fromForeign (right b) = inj₂ b
{-# WARNING_ON_USAGE fromForeign
"Warning: fromForeign was deprecated in 2.0.
Please use Foreign.Haskell.Coerce.coerce instead."
#-}