Reimplement split and flatten in Data.List.NonEmpty (#1723)

Author: MatthewDaggitt

CHANGELOG.md

@@ -418,6 +418,13 @@ Non-backwards compatible changes
   in order to keep another new definition of `_>>=_`, located in `DiagonalBind`
   which is also a submodule of `Data.Vec.Base`.
 
+* The functions `split`, `flatten` and `flatten-split` have been removed from
+  `Data.List.NonEmpty`. In their place `groupSeqs` and `ungroupSeqs`
+  have been added to `Data.List.NonEmpty.Base` which morally perform the same 
+  operations but without computing the accompanying proofs. The proofs can be
+  found in `Data.List.NonEmpty.Properties` under the names `groupSeqs-groups`
+  and `ungroupSeqs` and `groupSeqs`.
+
 * The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer
   exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)`
   directly to use them.
@@ -777,6 +784,11 @@ New modules
   Data.Vec.Reflection
   ```
 
+* The `All` predicate over non-empty lists:
+  ```
+  Data.List.NonEmpty.Relation.Unary.All
+  ```
+
 * A small library for heterogenous equational reasoning on vectors:
   ```
   Data.Vec.Properties.Heterogeneous

src/Data/List/NonEmpty.agda

@@ -27,160 +27,30 @@ open import Function.Equivalence
 open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl)
 open import Relation.Nullary.Decidable using (isYes)
 
-private
-  variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
-
 ------------------------------------------------------------------------
 -- Re-export basic type and operations
 
 open import Data.List.NonEmpty.Base public
 
-------------------------------------------------------------------------
--- More operations
-
--- Groups all contiguous elements for which the predicate returns the
--- same result into lists.
-
-split : (p : A → Bool) → List A →
-        List (List⁺ (∃ (T ∘ p)) ⊎ List⁺ (∃ (T ∘ not ∘ p)))
-split p []       = []
-split p (x ∷ xs) with p x | P.inspect p x | split p xs
-... | true  | P.[ px≡t ] | inj₁ xs′ ∷ xss = inj₁ ((x , Eq.from T-≡     ⟨$⟩ px≡t) ∷⁺ xs′) ∷ xss
-... | true  | P.[ px≡t ] | xss            = inj₁ [ x , Eq.from T-≡     ⟨$⟩ px≡t ]        ∷ xss
-... | false | P.[ px≡f ] | inj₂ xs′ ∷ xss = inj₂ ((x , Eq.from T-not-≡ ⟨$⟩ px≡f) ∷⁺ xs′) ∷ xss
-... | false | P.[ px≡f ] | xss            = inj₂ [ x , Eq.from T-not-≡ ⟨$⟩ px≡f ]        ∷ xss
-
--- If we flatten the list returned by split, then we get the list we
--- started with.
-
-flatten : ∀ {p q} {P : A → Set p} {Q : A → Set q} →
-          List (List⁺ (∃ P) ⊎ List⁺ (∃ Q)) → List A
-flatten = List.concat ∘
-          List.map Sum.[ toList ∘ map proj₁ , toList ∘ map proj₁ ]
-
-flatten-split : (p : A → Bool) (xs : List A) → flatten (split p xs) ≡ xs
-flatten-split p []       = refl
-flatten-split p (x ∷ xs)
-  with p x | P.inspect p x | split p xs | flatten-split p xs
-... | true  | P.[ _ ] | []         | hyp = P.cong (_∷_ x) hyp
-... | true  | P.[ _ ] | inj₁ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
-... | true  | P.[ _ ] | inj₂ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
-... | false | P.[ _ ] | []         | hyp = P.cong (_∷_ x) hyp
-... | false | P.[ _ ] | inj₁ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
-... | false | P.[ _ ] | inj₂ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
-
--- Groups all contiguous elements /not/ satisfying the predicate into
--- lists. Elements satisfying the predicate are dropped.
-
-wordsBy : (A → Bool) → List A → List (List⁺ A)
-wordsBy p =
-  List.mapMaybe Sum.[ const nothing , just ∘′ map proj₁ ] ∘ split p
 
 ------------------------------------------------------------------------
--- Examples
-
--- Note that these examples are simple unit tests, because the type
--- checker verifies them.
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
 private
- module Examples {A B : Set}
-                 (_⊕_ : A → B → B)
-                 (_⊗_ : B → A → B)
-                 (_⊙_ : A → A → A)
-                 (f : A → B)
-                 (a b c : A)
-                 where
-
-  hd : head (a ∷⁺ b ∷⁺ [ c ]) ≡ a
-  hd = refl
-
-  tl : tail (a ∷⁺ b ∷⁺ [ c ]) ≡ b ∷ c ∷ []
-  tl = refl
-
-  mp : map f (a ∷⁺ b ∷⁺ [ c ]) ≡ f a ∷⁺ f b ∷⁺ [ f c ]
-  mp = refl
-
-  right : foldr _⊕_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊕ (b ⊕ f c))
-  right = refl
-
-  right₁ : foldr₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊙ (b ⊙ c))
-  right₁ = refl
-
-  left : foldl _⊗_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ ((f a ⊗ b) ⊗ c)
-  left = refl
-
-  left₁ : foldl₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c)
-  left₁ = refl
-
-  ⁺app⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺++⁺ (b ∷⁺ [ c ]) ≡
-          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
-  ⁺app⁺ = refl
-
-  ⁺app : (a ∷⁺ b ∷⁺ [ c ]) ⁺++ (b ∷ c ∷ []) ≡
-          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
-  ⁺app = refl
-
-  app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷⁺ [ c ]) ≡
-          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
-  app⁺ = refl
-
-  conc : concat ((a ∷⁺ b ∷⁺ [ c ]) ∷⁺ [ b ∷⁺ [ c ] ]) ≡
-         a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
-  conc = refl
-
-  rev : reverse (a ∷⁺ b ∷⁺ [ c ]) ≡ c ∷⁺ b ∷⁺ [ a ]
-  rev = refl
-
-  snoc : (a ∷ b ∷ c ∷ []) ∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
-  snoc = refl
-
-  snoc⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
-  snoc⁺ = refl
-
-  split-true : split (const true) (a ∷ b ∷ c ∷ []) ≡
-               inj₁ ((a , tt) ∷⁺ (b , tt) ∷⁺ [ c , tt ]) ∷ []
-  split-true = refl
-
-  split-false : split (const false) (a ∷ b ∷ c ∷ []) ≡
-                inj₂ ((a , tt) ∷⁺ (b , tt) ∷⁺ [ c , tt ]) ∷ []
-  split-false = refl
-
-  split-≡1 :
-    split (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
-    inj₁ [ 1 , tt ] ∷ inj₂ ((2 , tt) ∷⁺ [ 3 , tt ]) ∷
-    inj₁ ((1 , tt) ∷⁺ [ 1 , tt ]) ∷ inj₂ [ 2 , tt ] ∷ inj₁ [ 1 , tt ] ∷
-    []
-  split-≡1 = refl
-
-  wordsBy-true : wordsBy (const true) (a ∷ b ∷ c ∷ []) ≡ []
-  wordsBy-true = refl
-
-  wordsBy-false : wordsBy (const false) (a ∷ b ∷ c ∷ []) ≡
-                  (a ∷⁺ b ∷⁺ [ c ]) ∷ []
-  wordsBy-false = refl
-
-  wordsBy-≡1 :
-    wordsBy (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
-    (2 ∷⁺ [ 3 ]) ∷ [ 2 ] ∷ []
-  wordsBy-≡1 = refl
-
-  ------------------------------------------------------------------------
-  -- DEPRECATED
-  ------------------------------------------------------------------------
-  -- Please use the new names as continuing support for the old names is
-  -- not guaranteed.
+  variable
+    a : Level
+    A : Set a
 
-  -- Version 1.4
+-- Version 1.4
 
-  infixl 5 _∷ʳ'_
+infixl 5 _∷ʳ'_
 
-  _∷ʳ'_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)
-  _∷ʳ'_ = SnocView._∷ʳ′_
-  {-# WARNING_ON_USAGE _∷ʳ'_
-  "Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4.
-  Please use _∷ʳ′_ (ending in a prime) instead."
-  #-}
+_∷ʳ'_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)
+_∷ʳ'_ = SnocView._∷ʳ′_
+{-# WARNING_ON_USAGE _∷ʳ'_
+"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4.
+Please use _∷ʳ′_ (ending in a prime) instead."
+#-}

src/Data/List/NonEmpty/Base.agda

@@ -10,6 +10,7 @@ module Data.List.NonEmpty.Base where
 
 open import Level using (Level)
 open import Data.Bool.Base using (Bool; false; true; not; T)
+open import Data.Bool.Properties using (T?)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Maybe.Base using (Maybe ; nothing; just)
 open import Data.Nat.Base as ℕ
@@ -18,17 +19,19 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Function.Base
-open import Relation.Binary.PropositionalEquality.Core using (_≢_)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; _≢_; refl)
+open import Relation.Unary using (Pred; Decidable; U; ∅)
+open import Relation.Unary.Properties using (U?; ∅?)
+open import Relation.Nullary using (does)
 
 private
   variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
+    a p : Level
+    A B C : Set a
 
 ------------------------------------------------------------------------
--- Non-empty lists
+-- Definition
 
 infixr 5 _∷_
 
@@ -40,6 +43,7 @@ record List⁺ (A : Set a) : Set a where
 
 open List⁺ public
 
+------------------------------------------------------------------------
 -- Basic combinators
 
 uncons : List⁺ A → A × List A
@@ -85,7 +89,8 @@ map f (x ∷ xs) = (f x ∷ List.map f xs)
 replicate : ∀ n → n ≢ 0 → A → List⁺ A
 replicate n n≢0 a = a ∷ List.replicate (pred n) a
 
--- when dropping more than the size of the length of the list, the last element remains
+-- when dropping more than the size of the length of the list, the
+-- last element remains
 drop+ : ℕ → List⁺ A → List⁺ A
 drop+ zero    xs           = xs
 drop+ (suc n) (x ∷ [])     = x ∷ []
@@ -199,3 +204,120 @@ snocView (x ∷ .(xs List.∷ʳ y)) | xs List.∷ʳ′ y = (x ∷ xs) ∷ʳ′ y
 last : List⁺ A → A
 last xs with snocView xs
 last .(ys ∷ʳ y) | ys ∷ʳ′ y = y
+
+-- Groups all contiguous elements for which the predicate returns the
+-- same result into lists. The left sums are the ones for which the
+-- predicate holds, the right ones are the ones for which it doesn't.
+groupSeqsᵇ : (A → Bool) → List A → List (List⁺ A ⊎ List⁺ A)
+groupSeqsᵇ p []       = []
+groupSeqsᵇ p (x ∷ xs) with p x | groupSeqsᵇ p xs
+... | true  | inj₁ xs′ ∷ xss = inj₁ (x ∷⁺ xs′) ∷ xss
+... | true  | xss            = inj₁ [ x ]      ∷ xss
+... | false | inj₂ xs′ ∷ xss = inj₂ (x ∷⁺ xs′) ∷ xss
+... | false | xss            = inj₂ [ x ]      ∷ xss
+
+-- Groups all contiguous elements /not/ satisfying the predicate into
+-- lists. Elements satisfying the predicate are dropped.
+wordsByᵇ : (A → Bool) → List A → List (List⁺ A)
+wordsByᵇ p = List.mapMaybe Sum.[ const nothing , just ] ∘ groupSeqsᵇ p
+
+groupSeqs : {P : Pred A p} → Decidable P → List A → List (List⁺ A ⊎ List⁺ A)
+groupSeqs P? = groupSeqsᵇ (does ∘ P?)
+
+wordsBy : {P : Pred A p} → Decidable P → List A → List (List⁺ A)
+wordsBy P? = wordsByᵇ (does ∘ P?)
+
+-- Inverse operation for groupSequences.
+ungroupSeqs : List (List⁺ A ⊎ List⁺ A) → List A
+ungroupSeqs = List.concat ∘ List.map Sum.[ toList , toList ]
+
+------------------------------------------------------------------------
+-- Examples
+
+-- Note that these examples are simple unit tests, because the type
+-- checker verifies them.
+
+private
+ module Examples {A B : Set}
+                 (_⊕_ : A → B → B)
+                 (_⊗_ : B → A → B)
+                 (_⊙_ : A → A → A)
+                 (f : A → B)
+                 (a b c : A)
+                 where
+
+  hd : head (a ∷⁺ b ∷⁺ [ c ]) ≡ a
+  hd = refl
+
+  tl : tail (a ∷⁺ b ∷⁺ [ c ]) ≡ b ∷ c ∷ []
+  tl = refl
+
+  mp : map f (a ∷⁺ b ∷⁺ [ c ]) ≡ f a ∷⁺ f b ∷⁺ [ f c ]
+  mp = refl
+
+  right : foldr _⊕_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊕ (b ⊕ f c))
+  right = refl
+
+  right₁ : foldr₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊙ (b ⊙ c))
+  right₁ = refl
+
+  left : foldl _⊗_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ ((f a ⊗ b) ⊗ c)
+  left = refl
+
+  left₁ : foldl₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c)
+  left₁ = refl
+
+  ⁺app⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺++⁺ (b ∷⁺ [ c ]) ≡
+          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
+  ⁺app⁺ = refl
+
+  ⁺app : (a ∷⁺ b ∷⁺ [ c ]) ⁺++ (b ∷ c ∷ []) ≡
+          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
+  ⁺app = refl
+
+  app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷⁺ [ c ]) ≡
+          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
+  app⁺ = refl
+
+  conc : concat ((a ∷⁺ b ∷⁺ [ c ]) ∷⁺ [ b ∷⁺ [ c ] ]) ≡
+         a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
+  conc = refl
+
+  rev : reverse (a ∷⁺ b ∷⁺ [ c ]) ≡ c ∷⁺ b ∷⁺ [ a ]
+  rev = refl
+
+  snoc : (a ∷ b ∷ c ∷ []) ∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
+  snoc = refl
+
+  snoc⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
+  snoc⁺ = refl
+
+  groupSeqs-true : groupSeqs U? (a ∷ b ∷ c ∷ []) ≡
+               inj₁ (a ∷⁺ b ∷⁺ [ c ]) ∷ []
+  groupSeqs-true = refl
+
+  groupSeqs-false : groupSeqs ∅? (a ∷ b ∷ c ∷ []) ≡
+                inj₂ (a ∷⁺ b ∷⁺ [ c ]) ∷ []
+  groupSeqs-false = refl
+
+  groupSeqs-≡1 : groupSeqsᵇ (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
+                 inj₁ [ 1 ] ∷
+                 inj₂ (2 ∷⁺ [ 3 ]) ∷
+                 inj₁ (1 ∷⁺ [ 1 ]) ∷
+                 inj₂ [ 2 ] ∷
+                 inj₁ [ 1 ] ∷
+                 []
+  groupSeqs-≡1 = refl
+
+  wordsBy-true : wordsByᵇ (const true) (a ∷ b ∷ c ∷ []) ≡ []
+  wordsBy-true = refl
+
+  wordsBy-false : wordsByᵇ (const false) (a ∷ b ∷ c ∷ []) ≡
+                  (a ∷⁺ b ∷⁺ [ c ]) ∷ []
+  wordsBy-false = refl
+
+  wordsBy-≡1 : wordsByᵇ (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
+               (2 ∷⁺ [ 3 ]) ∷
+               [ 2 ] ∷
+               []
+  wordsBy-≡1 = refl