[ fix agda#377 ] Add module Haskell.Data.Maybe with fromMaybe and more

lib/Haskell/Data/Maybe.agda

@@ -0,0 +1,34 @@
+module Haskell.Data.Maybe where
+
+open import Haskell.Prelude
+
+isJust : Maybe a → Bool
+isJust Nothing  = False
+isJust (Just _) = True
+
+isNothing : Maybe a → Bool
+isNothing Nothing  = True
+isNothing (Just _) = False
+
+fromJust : (x : Maybe a) → @0 {IsJust x} → a
+fromJust Nothing  = error "fromJust Nothing"
+fromJust (Just x) = x
+
+fromMaybe : {a : Set} → a → Maybe a → a
+fromMaybe d Nothing = d
+fromMaybe _ (Just x) = x
+
+listToMaybe : List a → Maybe a
+listToMaybe [] = Nothing
+listToMaybe (x ∷ _) = Just x
+
+maybeToList : Maybe a → List a
+maybeToList Nothing = []
+maybeToList (Just x) = x ∷ []
+
+mapMaybe : (a → Maybe b) → List a → List b
+mapMaybe f [] = []
+mapMaybe f (x ∷ xs) = maybe id _∷_ (f x) (mapMaybe f xs)
+
+catMaybes : List (Maybe a) → List a
+catMaybes = mapMaybe id

lib/Haskell/Extra/Delay.agda

@@ -5,8 +5,10 @@ module Haskell.Extra.Delay where
 open import Agda.Builtin.Size public
 
 open import Haskell.Prelude
-open import Haskell.Prim.Thunk
+
+open import Haskell.Data.Maybe
 open import Haskell.Extra.Refinement
+open import Haskell.Prim.Thunk
 
 private variable
   x y z : a

lib/Haskell/Prelude.agda

@@ -137,6 +137,3 @@ IsJust : Maybe a → Set
 IsJust Nothing  = ⊥
 IsJust (Just _) = ⊤
 
-fromJust : (x : Maybe a) → @0 {IsJust x} → a
-fromJust Nothing  = error "fromJust Nothing"
-fromJust (Just x) = x

lib/Haskell/Prim/Maybe.agda

@@ -11,7 +11,3 @@ data Maybe {@0 ℓ} (a : Set ℓ) : Set ℓ where
 maybe : ∀ {@0 ℓ₁ ℓ₂} {@0 a : Set ℓ₁} {@0 b : Set ℓ₂} → b → (a → b) → Maybe a → b
 maybe n j Nothing  = n
 maybe n j (Just x) = j x
-
-fromMaybe : {a : Set} → a → Maybe a → a
-fromMaybe d Nothing = d
-fromMaybe _ (Just x) = x

test/AllTests.agda

@@ -94,6 +94,7 @@ import FunCon
 import Issue308
 import Issue324
 import Assert
+import Issue377
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -185,4 +186,5 @@ import FunCon
 import Issue308
 import Issue324
 import Assert
+import Issue377
 #-}

test/Issue377.agda

@@ -0,0 +1,9 @@
+module Issue377 where
+
+open import Haskell.Prelude
+open import Haskell.Data.Maybe
+
+test : Integer
+test = fromMaybe 0 (Just 12)
+
+{-# COMPILE AGDA2HS test #-}

test/golden/AllTests.hs

@@ -89,4 +89,5 @@ import FunCon
 import Issue308
 import Issue324
 import Assert
+import Issue377
 

test/golden/Issue377.hs

@@ -0,0 +1,7 @@
+module Issue377 where
+
+import Data.Maybe (fromMaybe)
+
+test :: Integer
+test = fromMaybe 0 (Just 12)
+