[ fix #1128 ] Use the BUILTIN Maybe (#1220)

Author: gallais

.travis.yml

@@ -140,7 +140,7 @@ matrix:
             mv html/* . ;
           fi
         - if [[ $TRAVIS_BRANCH = "experimental" ]]; then
-	    mkdir -p experimental ;
+            mkdir -p experimental ;
             mv html/* experimental/ ;
           fi
 
@@ -194,4 +194,4 @@ matrix:
         - stack ${ARGS} exec -- AllNonAsciiChars
       before_cache:
         - find ${TRAVIS_BUILD_DIR}/.stack-work -type f -name '*.agdai' -delete
-      after_success: []
+      after_success: []

CHANGELOG.md

@@ -21,14 +21,19 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
-* The `n` argument to `_⊜_` in `Tactic.RingSolver.NonReflective` has been made implict rather than explicit.
+* The `n` argument to `_⊜_` in `Tactic.RingSolver.NonReflective` has
+  been made implict rather than explicit.
 
 * `Data.Empty.Polymorphic` and `Data.Unit.Polymorphic` were rewritten
   to explicitly use `Lift` rather that defining new types. This means
   that these are now compatible with `⊥` and `⊤` from the rest of the
   library. This allowed them to be used in the rest of library where
   explicit `Lift` was used.
 
+* `Data.Maybe.Base` now re-exports the definition of `Maybe` given by
+  `Agda.Builtin.Maybe`. The `Foreign.Haskell` modules and definitions
+  corresponding to `Maybe` have been removed.
+
 * The representation of reflected syntax in `Reflection.Term` and
   `Reflection.Pattern` has been updated to match the new
   representation used in Agda 2.6.2. Specifically, the following changes were made:

GNUmakefile

@@ -13,7 +13,7 @@ test: Everything.agda check-whitespace
 	$(AGDA) -i. -isrc README.agda
 
 check-whitespace:
-	cabal exec -- fix-whitespace --check
+	cabal v1-exec -- fix-whitespace --check
 
 setup: Everything.agda
 
@@ -23,8 +23,8 @@ Everything.agda:
 # command `cabal install` is needed by cabal-install <= 2.4.*. I did
 # not found any problem running both commands with different versions
 # of cabal-install. See Issue #1001.
-	cabal clean && cabal build && cabal install
-	cabal exec -- GenerateEverything
+	cabal v1-clean && cabal v1-build && cabal v1-install
+	cabal v1-exec -- GenerateEverything
 
 .PHONY: listings
 listings: Everything.agda

README/Foreign/Haskell.agda

@@ -32,11 +32,11 @@ private
     a : Level
     A : Set a
 
--- Here we use the FFI version of Maybe and Pair.
+-- Here we use the FFI version of Pair.
 
 postulate
-  primUncons    : List A → FFI.Maybe (FFI.Pair A (List A))
-  primCatMaybes : List (FFI.Maybe A) → List A
+  primUncons    : List A → Maybe (FFI.Pair A (List A))
+  primCatMaybes : List (Maybe A) → List A
   primTestChar  : Char → Bool
   primIntEq     : Int → Int → Bool
 
@@ -53,21 +53,19 @@ postulate
 
 {-# COMPILE GHC primIntEq = (==) #-}
 
--- We however want to use the notion of Maybe and Pair internal to
--- the standard library. For this we use `coerce` to take use back
--- to the types we are used to.
+-- We however want to use the notion of Pair internal to the standard library.
+-- For this we use `coerce` to take use back to the types we are used to.
 
--- The typeclass mechanism uses the coercion rules for Maybe and Pair,
--- as well as the knowledge that natural numbers are represented as
--- integers.
--- We additionally benefit from the congruence rules for List, Char,
+-- The typeclass mechanism uses the coercion rules for Pair, as well as the
+-- knowledge that natural numbers are represented as integers.
+-- We additionally benefit from the congruence rules for List, Maybe, Char,
 -- Bool, and a reflexivity principle for variable A.
 
 uncons : List A → Maybe (A × List A)
 uncons = coerce primUncons
 
 catMaybes : List (Maybe A) → List A
-catMaybes = coerce primCatMaybes
+catMaybes = primCatMaybes
 
 testChar : Char → Bool
 testChar = coerce primTestChar

src/Data/Maybe/Base.agda

@@ -29,10 +29,8 @@ private
 ------------------------------------------------------------------------
 -- Definition
 
-data Maybe (A : Set a) : Set a where
-  nothing : Maybe A
-  just    : (x : A) → Maybe A
-
+open import Agda.Builtin.Maybe public
+  using (Maybe; just; nothing)
 
 ------------------------------------------------------------------------
 -- Some operations

src/Foreign/Haskell.agda

@@ -28,15 +28,6 @@ open import Foreign.Haskell.Either public
   ; fromForeign to fromForeignEither
   )
 
-------------------------------------------------------------------------
--- Maybe
-
-open import Foreign.Haskell.Maybe public
-  renaming
-  ( toForeign   to toForeignMaybe
-  ; fromForeign to fromForeignMaybe
-  )
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Foreign/Haskell/Coerce.agda

@@ -41,7 +41,6 @@ import Data.Maybe.Base as STD
 import Data.Product    as STD
 import Data.Sum        as STD
 
-import Foreign.Haskell.Maybe  as FFI
 import Foreign.Haskell.Pair   as FFI
 import Foreign.Haskell.Either as FFI
 
@@ -107,14 +106,6 @@ instance
 -- can be converted to their FFI equivalents which are bound to actual
 -- Haskell types.
 
--- Maybe
-
-  maybe-toFFI : Coercible₁ a b STD.Maybe FFI.Maybe
-  maybe-toFFI = TrustMe
-
-  maybe-fromFFI : Coercible₁ a b FFI.Maybe STD.Maybe
-  maybe-fromFFI = TrustMe
-
 -- Product
 
   pair-toFFI : Coercible₂ a b c d STD._×_ FFI.Pair
@@ -134,6 +125,11 @@ instance
 -- We follow up with purely structural rules for builtin data types which
 -- already have known low-level representations.
 
+-- Maybe
+
+  coerce-maybe : Coercible₁ a b STD.Maybe STD.Maybe
+  coerce-maybe = TrustMe
+
 -- List
 
   coerce-list : Coercible₁ a b STD.List STD.List

src/Foreign/Haskell/Maybe.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Which Maybe type which calls out to Haskell via the FFI
+-- This module is DEPRECATED. Please use the builtin Maybe instead.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K #-}
@@ -36,3 +36,24 @@ toForeign nothing = nothing
 fromForeign : Maybe A → Data.Maybe A
 fromForeign (just x) = just x
 fromForeign nothing = nothing
+
+
+{-# WARNING_ON_IMPORT
+"Warning: Foreign.Haskell.Maybe was deprecated in v1.4.
+Maybe is now an Agda builtin and does not need library support."
+#-}
+
+{-# WARNING_ON_USAGE Maybe
+"Warning: Foreign.Haskell.Maybe's Maybe was deprecated in v1.4.
+Maybe is now an Agda builtin and does not need library support."
+#-}
+
+{-# WARNING_ON_USAGE toForeign
+"Warning: toForeign was deprecated in v1.4.
+Maybe is now an Agda builtin and does not need library support."
+#-}
+
+{-# WARNING_ON_USAGE fromForeign
+"Warning: fromForeign was deprecated in v1.4.
+Maybe is now an Agda builtin and does not need library support."
+#-}