Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Mar 8, 2022
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
05097c9
Reimplement `split` and `flatten` in `Data.List.NonEmpty`
MatthewDaggitt Feb 11, 2022
13ea4ad
Addressed @gallais feedback and shortened sequences to seqs
MatthewDaggitt Mar 7, 2022
cfb899e
Update CHANGELOG
MatthewDaggitt Mar 8, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -766,6 +773,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
Expand Down
160 changes: 15 additions & 145 deletions src/Data/List/NonEmpty.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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."
#-}
136 changes: 129 additions & 7 deletions src/Data/List/NonEmpty/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ℕ
Expand All @@ -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 _∷_

Expand All @@ -40,6 +43,7 @@ record List⁺ (A : Set a) : Set a where

open List⁺ public

------------------------------------------------------------------------
-- Basic combinators

uncons : List⁺ A → A × List A
Expand Down Expand Up @@ -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 ∷ []
Expand Down Expand Up @@ -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
Loading