Implement move-via-deprecate of decToMaybe as per #2330

src/Algebra/Solver/CommutativeMonoid.agda

@@ -14,7 +14,7 @@ module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁
 
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe
-  using (Maybe; decToMaybe; From-just; from-just)
+  using (Maybe; From-just; from-just)
 open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
 open import Data.Nat.GeneralisedArithmetic using (fold)
 open import Data.Product.Base using (_×_; uncurry)
@@ -28,7 +28,7 @@ import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable using (Dec; decToMaybe)
 
 open CommutativeMonoid M
 open ≈-Reasoning setoid

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -13,7 +13,7 @@ open import Algebra
 open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe
-  using (Maybe; decToMaybe; From-just; from-just)
+  using (Maybe; From-just; from-just)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_)
 open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
@@ -26,7 +26,7 @@ import Relation.Nullary.Decidable            as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; decSetoid)
-open import Relation.Nullary.Decidable using (Dec)
+open Dec using (Dec; decToMaybe)
 
 module Algebra.Solver.IdempotentCommutativeMonoid
   {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where

src/Algebra/Solver/Monoid.agda

@@ -15,7 +15,7 @@ import Data.Fin.Properties as Fin
 open import Data.List.Base hiding (lookup)
 import Data.List.Relation.Binary.Equality.DecPropositional as ListEq
 open import Data.Maybe.Base as Maybe
-  using (Maybe; decToMaybe; From-just; from-just)
+  using (Maybe; From-just; from-just)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; lookup)
@@ -24,8 +24,7 @@ open import Relation.Binary.Definitions using (Decidable)
 
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 import Relation.Binary.Reflection
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+import Relation.Nullary.Decidable.Core as Dec
 
 open Monoid M
 open import Relation.Binary.Reasoning.Setoid setoid
@@ -123,7 +122,7 @@ nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
 
 prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma $ decToMaybe (normalise e₁ ≟ normalise e₂)
+  Maybe.map lemma $ Dec.decToMaybe (normalise e₁ ≟ normalise e₂)
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =

src/Data/Graph/Acyclic.agda

@@ -20,13 +20,13 @@ open import Data.Fin as Fin
   using (Fin; Fin′; zero; suc; #_; toℕ; _≟_; opposite) renaming (_ℕ-ℕ_ to _-_)
 import Data.Fin.Properties as Fin
 open import Data.Product.Base as Prod using (∃; _×_; _,_)
-open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; decToMaybe)
-open import Data.Empty
+open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
+open import Data.Empty using (⊥)
 open import Data.Unit.Base using (⊤; tt)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Function.Base using (_$_; _∘′_; _∘_; id)
-open import Relation.Nullary
+open import Relation.Nullary.Decidable.Core using (decToMaybe)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------

src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda

@@ -21,7 +21,7 @@ module Data.List.Relation.Binary.Sublist.Heterogeneous.Solver
 
 open import Level using (_⊔_)
 open import Data.Fin as Fin
-open import Data.Maybe.Base as Maybe
+open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 open import Data.Nat.Base as ℕ using (ℕ)
 open import Data.Product.Base using (Σ-syntax; _,_)
 open import Data.Vec.Base as Vec using (Vec ; lookup)
@@ -30,11 +30,11 @@ open import Data.List.Properties
 open import Data.List.Relation.Binary.Sublist.Heterogeneous
   hiding (lookup)
 open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
-open import Function
+open import Function.Base
 
 open import Relation.Binary.PropositionalEquality as ≡
   using (_≡_; _≗_; sym; cong; cong₂; subst₂)
-open import Relation.Nullary
+open import Relation.Nullary.Decidable.Core using (decToMaybe)
 
 open ≡.≡-Reasoning
 
@@ -150,5 +150,5 @@ solveT t u =
 
 -- Prover for ASTs
 
-prove : ∀ {n} (d e : TList n) → From-just (solveT d e)
-prove d e = from-just (solveT d e)
+prove : ∀ {n} (d e : TList n) → Maybe.From-just (solveT d e)
+prove d e = Maybe.from-just (solveT d e)

src/Data/Maybe/Base.agda

@@ -10,14 +10,12 @@
 
 module Data.Maybe.Base where
 
-open import Level
+open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; true; false; not)
 open import Data.Unit.Base using (⊤)
 open import Data.These.Base using (These; this; that; these)
 open import Data.Product.Base as Prod using (_×_; _,_)
-open import Function.Base
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Decidable.Core
+open import Function.Base using (_∘_; id; const)
 
 private
   variable
@@ -46,10 +44,6 @@ is-just nothing  = false
 is-nothing : Maybe A → Bool
 is-nothing = not ∘ is-just
 
-decToMaybe : Dec A → Maybe A
-decToMaybe ( true because [a]) = just (invert [a])
-decToMaybe (false because  _ ) = nothing
-
 -- A dependent eliminator.
 
 maybe : ∀ {A : Set a} {B : Maybe A → Set b} →
@@ -137,3 +131,22 @@ thisM a = maybe′ (these a) (this a)
 
 thatM : Maybe A → B → These A B
 thatM = maybe′ these that
+
+------------------------------------------------------------------------
+-- Deprecated
+
+-- Version 2.1
+-- decToMaybe
+
+open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary.Decidable.Core
+  using (_because_; Dec)
+
+decToMaybe : Dec A → Maybe A
+decToMaybe ( true because [a]) = just (invert [a])
+decToMaybe (false because  _ ) = nothing
+
+{-# WARNING_ON_USAGE decToMaybe
+"Warning: decToMaybe was deprecated in v2.1.
+Please use Relation.Nullary.Decidable's decToMaybe instead."
+#-}

src/Relation/Binary/Consequences.agda

@@ -8,7 +8,7 @@
 
 module Relation.Binary.Consequences where
 
-open import Data.Maybe.Base using (just; nothing; decToMaybe)
+open import Data.Maybe.Base using (just; nothing)
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
 open import Data.Product.Base using (_,_)
 open import Data.Empty.Irrelevant using (⊥-elim)
@@ -17,7 +17,7 @@ open import Level using (Level)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Nullary using (yes; no; recompute; ¬_)
-open import Relation.Nullary.Decidable.Core using (map′)
+open import Relation.Nullary.Decidable.Core using (map′; decToMaybe)
 open import Relation.Unary using (∁; Pred)
 
 private

src/Relation/Nullary/Decidable/Core.agda

@@ -11,6 +11,10 @@
 
 module Relation.Nullary.Decidable.Core where
 
+-- decToMaybe was deprecated in v2.1
+-- this can go through `Data.Maybe.Base` once the deprecation of `decToMaybe`
+-- is fully done.
+open import Agda.Builtin.Maybe using (Maybe; just; nothing)
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Polymorphic.Base using (⊤)
@@ -98,6 +102,13 @@ _→-dec_ : Dec A → Dec B → Dec (A → B)
 does  (a? →-dec b?) = not (does a?) ∨ does b?
 proof (a? →-dec b?) = proof a? →-reflects proof b?
 
+------------------------------------------------------------------------
+-- Relationship with Maybe
+
+decToMaybe : Dec A → Maybe A
+decToMaybe ( true because [a]) = just (invert [a])
+decToMaybe (false because  _ ) = nothing
+
 ------------------------------------------------------------------------
 -- Relationship with booleans