diff --git a/lib/Haskell/Data/Maybe.agda b/lib/Haskell/Data/Maybe.agda new file mode 100644 index 00000000..e8353cd6 --- /dev/null +++ b/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 diff --git a/lib/Haskell/Extra/Delay.agda b/lib/Haskell/Extra/Delay.agda index 40471b71..8f59c7ad 100644 --- a/lib/Haskell/Extra/Delay.agda +++ b/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 diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda index 70b6d560..6b927785 100644 --- a/lib/Haskell/Prelude.agda +++ b/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 diff --git a/lib/Haskell/Prim/Maybe.agda b/lib/Haskell/Prim/Maybe.agda index e3d6e1f6..bf261c3a 100644 --- a/lib/Haskell/Prim/Maybe.agda +++ b/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 diff --git a/test/AllTests.agda b/test/AllTests.agda index 53c2f9b7..e829b337 100644 --- a/test/AllTests.agda +++ b/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 #-} diff --git a/test/Issue377.agda b/test/Issue377.agda new file mode 100644 index 00000000..706be32a --- /dev/null +++ b/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 #-} diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index 1c79aa3e..99247aa1 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -89,4 +89,5 @@ import FunCon import Issue308 import Issue324 import Assert +import Issue377 diff --git a/test/golden/Issue377.hs b/test/golden/Issue377.hs new file mode 100644 index 00000000..8931a507 --- /dev/null +++ b/test/golden/Issue377.hs @@ -0,0 +1,7 @@ +module Issue377 where + +import Data.Maybe (fromMaybe) + +test :: Integer +test = fromMaybe 0 (Just 12) +