add Maybe type for Haskell interop (#700)

Author: Zambonifofex

CHANGELOG.md

@@ -155,6 +155,9 @@ New modules
   Data.Vec.Bounded.Base
   Data.Vec.Bounded
 
+  Foreign.Haskell.Pair
+  Foreign.Haskell.Maybe
+
   Relation.Binary.Construct.Closure.Reflexive.Properties
   Relation.Binary.Construct.Closure.Reflexive.Properties.WithK
   Relation.Binary.Construct.Closure.Equivalence.Properties

GenerateEverything.hs

@@ -38,6 +38,8 @@ unsafeModules = map toAgdaFilePath
   , "Data.Word.Unsafe"
   , "Debug.Trace"
   , "Foreign.Haskell"
+  , "Foreign.Haskell.Maybe"
+  , "Foreign.Haskell.Pair"
   , "IO"
   , "IO.Primitive"
   , "Reflection"

src/Foreign/Haskell.agda

@@ -10,17 +10,23 @@ module Foreign.Haskell where
 
 open import Level
 
--- A pair type
+------------------------------------------------------------------------
+-- Pairs
 
-record Pair {ℓ ℓ′ : Level} (A : Set ℓ) (B : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
-  constructor _,_
-  field  fst : A
-         snd : B
-open Pair public
+open import Foreign.Haskell.Pair public
+  renaming
+  ( toForeign   to toForeignPair
+  ; fromForeign to fromForeignPair
+  )
 
-{-# FOREIGN GHC type AgdaPair l1 l2 a b = (a , b) #-}
-{-# COMPILE GHC Pair = data MAlonzo.Code.Foreign.Haskell.AgdaPair ((,)) #-}
+------------------------------------------------------------------------
+-- Maybe
 
+open import Foreign.Haskell.Maybe public
+  renaming
+  ( toForeign   to toForeignMaybe
+  ; fromForeign to fromForeignMaybe
+  )
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Foreign/Haskell/Maybe.agda

@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Which Maybe type which calls out to Haskell via the FFI
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K #-}
+
+module Foreign.Haskell.Maybe where
+
+open import Level
+import Data.Maybe as Data
+
+private
+  variable
+    a : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- Definition
+
+abstract
+
+  Maybe : Set a → Set a
+  Maybe = Data.Maybe
+
+{-# FOREIGN GHC type AgdaMaybe l a = Maybe a #-}
+{-# COMPILE GHC Maybe = data AgdaMaybe (Just | Nothing) #-}
+
+------------------------------------------------------------------------
+-- Conversion
+
+abstract
+
+  toForeign : Data.Maybe A → Maybe A
+  toForeign x = x
+
+  fromForeign : Maybe A → Data.Maybe A
+  fromForeign x = x

src/Foreign/Haskell/Pair.agda

@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The Pair type which calls out to Haskell via the FFI
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K #-}
+
+module Foreign.Haskell.Pair where
+
+open import Level
+open import Data.Product using (_×_; _,_)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+------------------------------------------------------------------------
+-- Definition
+
+abstract
+
+  Pair : Set a → Set b → Set (a ⊔ b)
+  Pair = _×_
+
+{-# FOREIGN GHC type AgdaPair l1 l2 a b = (a , b) #-}
+{-# COMPILE GHC Pair = data MAlonzo.Code.Foreign.Haskell.AgdaPair ((,)) #-}
+
+------------------------------------------------------------------------
+-- Conversion
+
+abstract
+
+  toForeign : A × B → Pair A B
+  toForeign x = x
+
+  fromForeign : Pair A B → A × B
+  fromForeign x = x