Refactor Data.Sum.{to|from}Dec via move+deprecate in Relation.Nullary.Decidable.Core (agda#2405)

* fixes agda#2059 on the model of agda#2336

* fixed `import` dependencies

* simplified `import` dependencies

* final tweak

* `CHANGELOG`

Author: jamesmckinna

CHANGELOG.md

@@ -113,6 +113,12 @@ Deprecated names
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
   ```
 
+* In `Data.Sum`:
+  ```agda
+  fromDec  ↦  Relation.Nullary.Decidable.Core.toSum
+  toDec    ↦  Relation.Nullary.Decidable.Core.fromSum
+  ```
+
 * In `IO.Base`:
   ```agda
   untilRight  ↦  untilInj₂
@@ -818,6 +824,8 @@ Additions to existing modules
 * Added new proof in `Relation.Nullary.Decidable.Core`:
   ```agda
   recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+  toSum              : Dec A → A ⊎ ¬ A
+  fromSum            : A ⊎ ¬ A → Dec A
   ```
 
 * Added new proof in `Relation.Nullary.Decidable`:

src/Data/List/Fresh/Relation/Unary/Any.agda

@@ -9,12 +9,11 @@
 module Data.List.Fresh.Relation.Unary.Any where
 
 open import Level using (Level; _⊔_; Lift)
-open import Data.Empty
 open import Data.Product.Base using (∃; _,_; -,_)
 open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Function.Bundles using (_⇔_; mk⇔)
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Decidable as Dec using (Dec; no; _⊎-dec_)
 open import Relation.Unary  as U
 open import Relation.Binary.Core using (Rel)
 
@@ -35,10 +34,10 @@ module _ {R : Rel A r} {P : Pred A p} {x} {xs : List# A R} {pr} where
 
   head : ¬ Any P xs → Any P (cons x xs pr) → P x
   head ¬tail (here p)   = p
-  head ¬tail (there ps) = ⊥-elim (¬tail ps)
+  head ¬tail (there ps) = contradiction ps ¬tail
 
   tail : ¬ P x → Any P (cons x xs pr) → Any P xs
-  tail ¬head (here p)   = ⊥-elim (¬head p)
+  tail ¬head (here p)   = contradiction p ¬head
   tail ¬head (there ps) = ps
 
   toSum : Any P (cons x xs pr) → P x ⊎ Any P xs

src/Data/List/Relation/Unary/Any.agda

@@ -13,9 +13,8 @@ open import Data.List.Base as List using (List; []; [_]; _∷_; removeAt)
 open import Data.Product.Base as Product using (∃; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary using (¬_; yes; no; _⊎-dec_)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core as Dec using (no; _⊎-dec_)
+open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary using (Pred; _⊆_; Decidable; Satisfiable)
 
 private

src/Data/List/Relation/Unary/First/Properties.agda

@@ -13,11 +13,12 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.List.Relation.Unary.First
-import Data.Sum as Sum
-open import Function.Base using (_∘′_; _$_; _∘_; id)
+import Data.Sum.Base as Sum
+open import Function.Base using (_∘′_; _∘_; id)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
+import Relation.Nullary.Decidable.Core as Dec
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
-open import Relation.Nullary.Negation using (contradiction)
 
 ------------------------------------------------------------------------
 -- map
@@ -80,14 +81,14 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 module _ {a p} {A : Set a} {P : Pred A p} where
 
   first? : Decidable P → Decidable (First P (∁ P))
-  first? P? xs = Sum.toDec
-               $ Sum.map₂ (All⇒¬First contradiction)
-               $ first (Sum.fromDec ∘ P?) xs
+  first? P? = Dec.fromSum
+            ∘ Sum.map₂ (All⇒¬First contradiction)
+            ∘ first (Dec.toSum ∘ P?)
 
   cofirst? : Decidable P → Decidable (First (∁ P) P)
-  cofirst? P? xs = Sum.toDec
-                 $ Sum.map₂ (All⇒¬First id)
-                 $ first (Sum.swap ∘ Sum.fromDec ∘ P?) xs
+  cofirst? P? = Dec.fromSum
+              ∘ Sum.map₂ (All⇒¬First id)
+              ∘ first (Sum.swap ∘ Dec.toSum ∘ P?)
 
 ------------------------------------------------------------------------
 -- Conversion to Any

src/Data/Sum.agda

@@ -8,15 +8,10 @@
 
 module Data.Sum where
 
-open import Agda.Builtin.Equality
-
-open import Data.Bool.Base using (true; false)
 open import Data.Unit.Polymorphic.Base using (⊤; tt)
 open import Data.Maybe.Base using (Maybe; just; nothing)
-open import Function.Base
 open import Level
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (Dec; yes; no; _because_; ¬_)
+import Relation.Nullary.Decidable.Core as Dec
 
 private
   variable
@@ -31,7 +26,7 @@ open import Data.Sum.Base public
 ------------------------------------------------------------------------
 -- Additional functions
 
-module _ {a b} {A : Set a} {B : Set b} where
+module _ {A : Set a} {B : Set b} where
 
   isInj₁ : A ⊎ B → Maybe A
   isInj₁ (inj₁ x) = just x
@@ -57,12 +52,13 @@ module _ {a b} {A : Set a} {B : Set b} where
   from-inj₂ (inj₁ _) = _
   from-inj₂ (inj₂ x) = x
 
--- Conversion back and forth with Dec
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
 
-fromDec : Dec A → A ⊎ ¬ A
-fromDec ( true because  [p]) = inj₁ (invert  [p])
-fromDec (false because [¬p]) = inj₂ (invert [¬p])
+open Dec public using (fromDec; toDec)
 
-toDec : A ⊎ ¬ A → Dec A
-toDec (inj₁ p)  = yes p
-toDec (inj₂ ¬p) = no ¬p

src/Data/Vec/Relation/Unary/Any.agda

@@ -8,15 +8,14 @@
 
 module Data.Vec.Relation.Unary.Any {a} {A : Set a} where
 
-open import Data.Empty
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Nat.Base using (ℕ; zero; suc; NonZero)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_)
 open import Data.Product.Base as Product using (∃; _,_)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation using (¬_; contradiction)
-open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_)
+open import Relation.Nullary.Decidable as Dec using (no; _⊎-dec_)
 open import Relation.Unary
 
 private
@@ -44,7 +43,7 @@ head ¬pxs (there pxs) = contradiction pxs ¬pxs
 
 -- If the head does not satisfy the predicate, then the tail will.
 tail : ∀ {x} → ¬ P x → Any P (x ∷ xs) → Any P xs
-tail ¬px (here  px)  = ⊥-elim (¬px px)
+tail ¬px (here  px)  = contradiction px ¬px
 tail ¬px (there pxs) = pxs
 
 -- Convert back and forth with sum

src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda

@@ -21,8 +21,8 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.Construct.Closure.Reflexive
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Decidable as Dec using (yes; no)
 open import Relation.Unary using (Pred)
 
 private
@@ -79,7 +79,7 @@ module _ {_~_ : Rel A ℓ} where
   ... | tri> _ _    c = inj₂ [ c ]
 
   dec : DecidableEquality A → Decidable _~_ → Decidable _~ᵒ_
-  dec ≡-dec ~-dec a b = Dec.map ⊎⇔Refl (≡-dec a b ⊎-dec ~-dec a b)
+  dec ≡-dec ~-dec a b = Dec.map ⊎⇔Refl (≡-dec a b Dec.⊎-dec ~-dec a b)
 
   decidable : Trichotomous _≡_ _~_ → Decidable _~ᵒ_
   decidable ~-tri a b with ~-tri a b

src/Relation/Nullary/Decidable/Core.agda

@@ -12,11 +12,11 @@
 module Relation.Nullary.Decidable.Core where
 
 open import Agda.Builtin.Equality using (_≡_)
-open import Level using (Level; Lift)
+open import Level using (Level)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product.Base using (_×_)
-open import Data.Sum.Base using (_⊎_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Recomputable as Recomputable hiding (recompute-constant)
 open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-constant)
@@ -103,6 +103,17 @@ _→-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 Sum
+
+toSum : Dec A → A ⊎ ¬ A
+toSum ( true because  [p]) = inj₁ (invert  [p])
+toSum (false because [¬p]) = inj₂ (invert [¬p])
+
+fromSum : A ⊎ ¬ A → Dec A
+fromSum (inj₁ p)  = yes p
+fromSum (inj₂ ¬p) = no ¬p
+
 ------------------------------------------------------------------------
 -- Relationship with booleans
 
@@ -201,3 +212,17 @@ excluded-middle = ¬¬-excluded-middle
 "Warning: excluded-middle was deprecated in v2.0.
 Please use ¬¬-excluded-middle instead."
 #-}
+
+-- Version 2.1
+
+fromDec = toSum
+{-# WARNING_ON_USAGE fromDec
+"Warning: fromDec was deprecated in v2.1.
+Please use Relation.Nullary.Decidable.Core.toSum instead."
+#-}
+
+toDec = fromSum
+{-# WARNING_ON_USAGE toDec
+"Warning: toDec was deprecated in v2.1.
+Please use Relation.Nullary.Decidable.Core.fromSum instead."
+#-}