Implement move-via-deprecate of decToMaybe as per #2330 (#2336)

* Make the main home of `decToMaybe` be `Relation.Nullary.Decidable.Core`, but
deprecate the one in `Data.Maybe.Base` instead of removing it entirely.
Fix the library accordingly.

Note that this forces `Relation.Nullary.Decidable.Core` to use `Agda.Builtin.Maybe`
to avoid a cyclic import. This can be fixed once the deprecation is done.

* Update src/Relation/Nullary/Decidable/Core.agda

Good idea.

Co-authored-by: G. Allais <[email protected]>

* simplified the deprecation

* `CHANGELOG`

* narrowed import too far

* tweak a couple of the solvers for consistency, as per suggestions.

* chnage to `public` re-export of `Relation.Nullary.Decidable.Core.decToMaybe`

* Revert "chnage to `public` re-export of `Relation.Nullary.Decidable.Core.decToMaybe`"

This reverts commit 256a505.

* `fix-whitespace`

* simplify `import`s

* make consistent with `Idempotent` case

* tidy up

* instead of an alias, open public so that Agda knows these really are the same. This is a better deprecation strategy.

* rename(provisional)+deprecate

* knock-on

* knock-on: refactor via `dec⇒maybe`

* deprecation via delegation

* fix `CHANGELOG`

---------

Co-authored-by: G. Allais <[email protected]>
Co-authored-by: James McKinna <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>

Author: 3 people

CHANGELOG.md

@@ -76,6 +76,11 @@ Deprecated names
   _-_  ↦  _//_
   ```
 
+* In `Data.Maybe.Base`:
+  ```agda
+  decToMaybe  ↦  Relation.Nullary.Decidable.Core.dec⇒maybe
+  ```
+
 * In `Algebra.Structures.Biased`:
   ```agda
   IsRing*  ↦  Algebra.Structures.IsRing
@@ -821,8 +826,9 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
-* Added new proof in `Relation.Nullary.Decidable.Core`:
+* Added new definition and proof in `Relation.Nullary.Decidable.Core`:
   ```agda
+  dec⇒maybe : Dec A → Maybe A
   recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
   toSum              : Dec A → A ⊎ ¬ A
   fromSum            : A ⊎ ¬ A → Dec A
@@ -842,7 +848,7 @@ Additions to existing modules
   ```agda
   recompute          : Reflects A b → Recomputable A
   recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
-  ```
+ ```
 
 * Added new definitions in `Relation.Unary`
   ```

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)
@@ -27,8 +27,9 @@ import Relation.Binary.Reflection as Reflection
 import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable as Dec using (Dec)
 
 open CommutativeMonoid M
 open ≈-Reasoning setoid
@@ -184,7 +185,7 @@ nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
 
 prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma (decToMaybe (normalise e₁ ≟ normalise e₂))
+  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -13,7 +13,7 @@ open import Algebra.Bundles using (IdempotentCommutativeMonoid)
 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)
@@ -22,12 +22,13 @@ open import Function.Base using (_∘_)
 
 import Relation.Binary.Reasoning.Setoid  as ≈-Reasoning
 import Relation.Binary.Reflection            as Reflection
-import Relation.Nullary.Decidable            as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable as Dec using (Dec)
+
 
 module Algebra.Solver.IdempotentCommutativeMonoid
   {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where
@@ -198,7 +199,7 @@ nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂)
 
 prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma (decToMaybe (normalise e₁ ≟ normalise e₂))
+  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =

src/Algebra/Solver/Monoid.agda

@@ -15,17 +15,17 @@ 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)
 open import Function.Base using (_∘_; _$_)
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.Definitions using (DecidableEquality)
 
 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 +123,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⇒weaklyDec _≟_ (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)
+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.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------
@@ -238,7 +238,7 @@ preds (c & g) (suc i) =
             (List.map (Prod.map suc id) $ preds g i)
   where
   p : ∀ {e} {E : Set e} {n} (i : Fin n) → E × Fin n → Maybe (Fin′ (suc i) × E)
-  p i (e , j) = Maybe.map (λ{ refl → zero , e }) (decToMaybe (i ≟ j))
+  p i (e , j) = Maybe.map (λ{ refl → zero , e }) (dec⇒weaklyDec _≟_ i j)
 
 private
 

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; From-just; from-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)
@@ -32,6 +32,7 @@ open import Data.List.Relation.Binary.Sublist.Heterogeneous
 open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
 open import Function.Base using (_$_; case_of_)
 
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≗_; sym; cong; cong₂; subst₂)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
@@ -124,8 +125,8 @@ private
 
 -- Solver for items
 solveI : ∀ {n} (a b : Item n) → Maybe (a ⊆I b)
-solveI (var k) (var l) = Maybe.map var $ decToMaybe (k Fin.≟ l)
-solveI (val a) (val b) = Maybe.map val $ decToMaybe (R? a b)
+solveI (var k) (var l) = Maybe.map var $ dec⇒weaklyDec Fin._≟_ k  l
+solveI (val a) (val b) = Maybe.map val $ dec⇒weaklyDec R? a b
 solveI _ _ = nothing
 
 -- Solver for linearised expressions

src/Data/Maybe/Base.agda

@@ -10,14 +10,13 @@
 
 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 using (const; _∘_; id)
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Decidable.Core using (Dec; _because_)
+open import Function.Base using (_∘_; id; const)
+import Relation.Nullary.Decidable.Core as Dec
 
 private
   variable
@@ -46,10 +45,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 +132,14 @@ thisM a = maybe′ (these a) (this a)
 
 thatM : Maybe A → B → These A B
 thatM = maybe′ these that
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+-- decToMaybe
+
+open Dec using (decToMaybe) public

src/Relation/Binary/Consequences.agda

@@ -8,16 +8,16 @@
 
 module Relation.Binary.Consequences where
 
-open import Data.Maybe.Base using (just; nothing; decToMaybe)
-open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
+open import Data.Empty using (⊥-elim)
 open import Data.Product.Base using (_,_)
-open import Data.Empty.Irrelevant using (⊥-elim)
+open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘_; _∘₂_; _$_; flip)
 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.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core
+  using (yes; no; recompute; map′; dec⇒maybe)
 open import Relation.Unary using (∁; Pred)
 
 private
@@ -193,7 +193,7 @@ module _  {_R_ : Rel A ℓ₁} {Q : Rel A ℓ₂} where
 module _ {R : REL A B p} where
 
   dec⇒weaklyDec : Decidable R → WeaklyDecidable R
-  dec⇒weaklyDec dec x y = decToMaybe (dec x y)
+  dec⇒weaklyDec dec x y = dec⇒maybe (dec x y)
 
   dec⇒recomputable : Decidable R → Recomputable R
   dec⇒recomputable dec {a} {b} = recompute $ dec a b

src/Relation/Nullary/Decidable/Core.agda

@@ -11,6 +11,10 @@
 
 module Relation.Nullary.Decidable.Core where
 
+-- decToMaybe was deprecated in v2.1 #2330/#2336
+-- this can go through `Data.Maybe.Base` once that deprecation is fully done.
+open import Agda.Builtin.Maybe using (Maybe; just; nothing)
+
 open import Agda.Builtin.Equality using (_≡_)
 open import Level using (Level)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
@@ -103,6 +107,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
+
+dec⇒maybe : Dec A → Maybe A
+dec⇒maybe ( true because [a]) = just (invert [a])
+dec⇒maybe (false because  _ ) = nothing
+
 ------------------------------------------------------------------------
 -- Relationship with Sum
 
@@ -215,6 +226,12 @@ Please use ¬¬-excluded-middle instead."
 
 -- Version 2.1
 
+decToMaybe = dec⇒maybe
+{-# WARNING_ON_USAGE decToMaybe
+"Warning: decToMaybe was deprecated in v2.1.
+Please use Relation.Nullary.Decidable.Core.dec⇒maybe instead."
+#-}
+
 fromDec = toSum
 {-# WARNING_ON_USAGE fromDec
 "Warning: fromDec was deprecated in v2.1.