Stage 1 of Relation.Nullary refactor

CHANGELOG.md

@@ -521,12 +521,32 @@ Non-backwards compatible changes
       ↦ ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y
     ```
 
+### Reorganisation of the `Relation.Nullary` hierarchy
+
+* It was very difficult to use the `Relation.Nullary` modules, as `Relation.Nullary`
+  contained the basic definitions of negation, decidability etc., and the operations and
+  proofs were smeared over `Relation.Nullary.(Negation/Product/Sum/Implication etc.)`.
+
+* In order to fix this:
+  - the definition of `Dec` and `recompute` have been moved to `Relation.Nullary.Decidable.Core`
+  - the definition of `Reflects` has been moved to `Relation.Nullary.Reflects`
+  - the definition of `¬_` has been moved to `Relation.Nullary.Negation.Core`
+
+* Backwards compatibility has been maintained, as `Relation.Nullary` still re-exports these publicly.
+
+* In order to facilitate this reorganisation the following breaking moves have occured:
+  - `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core`
+  - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`.
+  - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation` 
+	to `Relation.Nullary.Decidable`.
+  - `fromDec` and `toDec` have been mvoed from `Data.Sum.Base` to `Data.Sum`.
+
 ### Refactoring of the unindexed Functor/Applicative/Monad hiearchy
 
 * The unindexed versions are not defined in terms of the named versions anymore
 
 * The `RawApplicative` and `RawMonad` type classes have been relaxed so that the underlying
-  functors do not need to their domain and codomain to live at the same Set level.
+  functors do not need their domain and codomain to live at the same Set level.
   This is needed for level-increasing functors like `IO : Set l → Set (suc l)`.
 
 * `RawApplicative` is now `RawFunctor + pure + _<*>_` and `RawMonad` is now
@@ -657,6 +677,8 @@ Non-backwards compatible changes
   + `pigeonhole` has been strengthened: wlog, we return a proof that
     `i < j` rather than a mere `i ≢ j`.
 
+* In `Data.Sum.Base` the definitions `fromDec` and `toDec` have been moved to `Data.Sum`.
+
 * In `Codata.Guarded.Stream` the following functions have been modified to have simpler definitions:
   * `cycle`
   * `interleave⁺`
@@ -1245,6 +1267,11 @@ New modules
   Data.Nat.Combinatorics.Spec
   ```
 
+* New base module for `Data.Product` containing only the basic definitions.
+  ```
+  Data.Product.Base
+  ```
+
 * Reflection utilities for some specific types:
   ```
   Data.List.Reflection

README/Data/Trie/NonDependent.agda

@@ -63,7 +63,7 @@ open import Data.These       as These
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
 open import Relation.Binary using (Rel)
-open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Decidable using (¬?)
 
 open import Data.Trie Char.<-strictTotalOrder
 open import Data.Tree.AVL.Value

src/Axiom/DoubleNegationElimination.agda

@@ -12,6 +12,7 @@ open import Axiom.ExcludedMiddle
 open import Level
 open import Relation.Nullary
 open import Relation.Nullary.Negation
+open import Relation.Nullary.Decidable
 
 ------------------------------------------------------------------------
 -- Definition

src/Codata/Musical/Colist.agda

@@ -36,6 +36,7 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
 open import Relation.Nullary.Negation
+open import Relation.Nullary.Decidable using (excluded-middle)
 open import Relation.Unary using (Pred)
 
 private

src/Data/Digit/Properties.agda

@@ -15,8 +15,7 @@ open import Data.Product using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
-open import Relation.Nullary.Decidable using (True; from-yes)
-open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Decidable using (True; from-yes; ¬?)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
 open import Function using (_∘_)
 

src/Data/List/Base.agda

@@ -22,7 +22,7 @@ open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (id; _∘_ ; _∘′_; _∘₂_; const; flip)
 open import Level using (Level)
 open import Relation.Nullary using (does)
-open import Relation.Nullary.Negation.Core using (¬?)
+open import Relation.Nullary.Decidable using (¬?)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Unary.Properties using (∁?)
 open import Relation.Binary.Core using (Rel)

src/Data/List/Membership/DecSetoid.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary using (Decidable; DecSetoid)
-open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Decidable using (¬?)
 
 module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
 

src/Data/List/Membership/Propositional/Properties.agda

@@ -42,7 +42,8 @@ open import Relation.Unary using (_⟨×⟩_; Decidable)
 import Relation.Nullary.Reflects as Reflects
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (¬_; Dec; does; yes; no; _because_)
-open import Relation.Nullary.Negation
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable using (excluded-middle)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})

src/Data/List/Membership/Setoid/Properties.agda

@@ -31,7 +31,8 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Unary as U using (Decidable; Pred)
 open import Relation.Nullary using (¬_; does; _because_; yes; no)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Negation using (¬?; contradiction)
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable using (¬?)
 open Setoid using (Carrier)
 
 private

src/Data/List/Properties.agda

@@ -36,8 +36,8 @@ open import Relation.Binary.PropositionalEquality as P hiding ([_])
 open import Relation.Binary as B using (Rel)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no)
-open import Relation.Nullary.Negation using (contradiction; ¬?)
-open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋)
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?)
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Unary using (Pred; Decidable; ∁)
 open import Relation.Unary.Properties using (∁?)

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

@@ -31,8 +31,7 @@ open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔)
 
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_)
-open import Relation.Nullary.Negation using (¬?)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable as Dec using (¬?)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)

src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda

@@ -11,28 +11,25 @@ open import Relation.Binary using (Setoid; _⇒_; _Preserves_⟶_)
 module Data.List.Relation.Binary.Sublist.Setoid.Properties
   {c ℓ} (S : Setoid c ℓ) where
 
-open import Level
-
 open import Data.List.Base hiding (_∷ʳ_)
-import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
-import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
-import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
-  as HeteroProperties
-import Data.List.Membership.Setoid as SetoidMembership
 open import Data.List.Relation.Unary.Any using (Any)
-
 import Data.Maybe.Relation.Unary.All as Maybe
 open import Data.Nat.Base using (_≤_; _≥_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (∃; _,_; proj₂)
-
 open import Function.Base
 open import Function.Bundles using (_⇔_; _⤖_)
-
+open import Level
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
 open import Relation.Unary using (Pred; Decidable; Irrelevant)
 open import Relation.Nullary using (¬_)
-open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Decidable using (¬?)
+
+import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
+import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
+import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
+  as HeteroProperties
+import Data.List.Membership.Setoid as SetoidMembership
 
 open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl)
 open SetoidEquality S using (_≋_; ≋-refl)

src/Data/List/Relation/Ternary/Interleaving.agda

@@ -14,7 +14,7 @@ open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Function
+open import Function.Base
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 

src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda

@@ -15,7 +15,7 @@ open import Data.List.Base using (List; []; _∷_; filter; _++_)
 open import Data.Bool.Base using (true; false)
 open import Relation.Unary using (Decidable)
 open import Relation.Nullary using (does)
-open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Decidable using (¬?)
 open import Function
 
 open import Data.List.Relation.Binary.Equality.Setoid S using (≋-refl)

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

@@ -41,9 +41,10 @@ open import Level using (Level)
 open import Relation.Binary as B using (REL; Setoid; _Respects_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; cong; cong₂; _≗_)
-open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
-open import Relation.Nullary.Negation using (¬?; contradiction; decidable-stable)
+open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable using (¬?; decidable-stable)
 open import Relation.Unary
   using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)

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

@@ -46,7 +46,8 @@ open import Relation.Binary.PropositionalEquality as P
 open import Relation.Unary as U
   using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no)
-open import Relation.Nullary.Negation using (contradiction; ¬?; decidable-stable)
+open import Relation.Nullary.Decidable using (¬?; decidable-stable)
+open import Relation.Nullary.Negation using (contradiction)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})

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

@@ -16,7 +16,7 @@ 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 (Any; here; there)
 open import Data.Product as Prod using (∃; -,_; _,_)
-open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
 open import Function
 open import Relation.Unary
 open import Relation.Nullary

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

@@ -14,7 +14,7 @@ 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.Base as Sum
+import Data.Sum as Sum
 open import Function
 open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; _≗_)
 open import Relation.Unary

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

@@ -15,10 +15,9 @@ open import Data.Product using (_×_; _,_)
 open import Relation.Binary as B using (REL; Rel)
 open import Relation.Unary as U using (Pred)
 open import Relation.Nullary using (¬_; yes)
-open import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable as Dec using (¬?)
 open import Relation.Nullary.Sum using (_⊎-dec_)
 open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Negation using (¬?)
 open import Level using (_⊔_)
 
 infixr 5 _∷≉_ _∷≈_
@@ -32,10 +31,12 @@ module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
   grouped? : B.Decidable _≈_ → U.Decidable (Grouped _≈_)
   grouped? _≟_ [] = yes []
   grouped? _≟_ (x ∷ []) = yes ([] ∷≉ [])
-  grouped? _≟_ (x ∷ y ∷ xs) = map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs))) where
+  grouped? _≟_ (x ∷ y ∷ xs) = Dec.map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs)))
+    where
     from : ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
     from (inj₁ x≈y          , grouped[y∷xs]) = x≈y          ∷≈ grouped[y∷xs]
     from (inj₂ all[x≉,y∷xs] , grouped[y∷xs]) = all[x≉,y∷xs] ∷≉ grouped[y∷xs]
+
     to : Grouped _≈_ (x ∷ y ∷ xs) → ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs)
     to (all[x≉,y∷xs] ∷≉ grouped[y∷xs]) = inj₂ all[x≉,y∷xs] , grouped[y∷xs]
     to (x≈y          ∷≈ grouped[y∷xs]) = inj₁ x≈y , grouped[y∷xs]

src/Data/List/Relation/Unary/Unique/DecPropositional.agda

@@ -8,9 +8,6 @@
 
 open import Relation.Binary using (DecSetoid; DecidableEquality)
 open import Relation.Binary.PropositionalEquality using (decSetoid)
-import Data.List.Relation.Unary.AllPairs as AllPairs
-open import Relation.Unary using (Decidable)
-open import Relation.Nullary.Negation using (¬?)
 
 module Data.List.Relation.Unary.Unique.DecPropositional
   {a} {A : Set a} (_≟_ : DecidableEquality A) where

src/Data/List/Relation/Unary/Unique/DecSetoid.agda

@@ -9,7 +9,7 @@
 open import Relation.Binary using (DecSetoid)
 import Data.List.Relation.Unary.AllPairs as AllPairs
 open import Relation.Unary using (Decidable)
-open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Decidable using (¬?)
 
 module Data.List.Relation.Unary.Unique.DecSetoid
   {a ℓ} (DS : DecSetoid a ℓ) where

src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda

@@ -12,7 +12,7 @@ open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Data.List.Relation.Unary.Unique.Setoid.Properties
 open import Level
 open import Relation.Binary using (DecSetoid)
-open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Decidable using (¬?)
 
 module Data.List.Relation.Unary.Unique.DecSetoid.Properties where
 

src/Data/Nat/Primality.agda

@@ -17,10 +17,10 @@ open import Data.Product
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (flip; _∘_; _∘′_)
 open import Relation.Nullary using (yes; no; ¬_)
-open import Relation.Nullary.Decidable as Dec using (from-yes)
+open import Relation.Nullary.Decidable as Dec using (from-yes; ¬?; decidable-stable)
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Nullary.Implication using (_→-dec_)
-open import Relation.Nullary.Negation using (¬?; contradiction; decidable-stable)
+open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Decidable)
 open import Relation.Binary.PropositionalEquality using (refl; sym; cong; subst)