diff --git a/CHANGELOG.md b/CHANGELOG.md index 469c926af8..3e06ecdbc6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -49,6 +49,15 @@ Deprecated names _-_ ↦ _//_ ``` +* In `Data.List.Base`: + ```agda + scanr ↦ Data.List.scanr + ``` + +* In `Data.List.Properties`: (but not an exact replacement) + ```agda + scanr-defn ↦ Data.List.NonEmpty.Properties.toList-scanr⁺ + * In `Data.Nat.Divisibility.Core`: ```agda *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ @@ -271,6 +280,26 @@ Additions to existing modules i*j≢0 : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j) ``` +* In `Data.List`: + ```agda + scanr : (A → B → B) → B → List A → List B + ``` + +* In `Data.List.NonEmpty.Base`: + ```agda + tails⁺ : List A → List⁺ (List A) + scanr⁺ : (A → B → B) → B → List A → List⁺ B + ``` + +* In `Data.List.NonEmpty.Properties`: + ```agda + toList-injective : toList xs ≡ toList ys → xs ≡ ys + toList-map : (f : A → B) → toList ∘ map f ≗ List.map f ∘ toList + toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails + scanr⁺-defn : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺ + toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails + ``` + * In `Data.List.Properties`: ```agda applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n) diff --git a/src/Data/List.agda b/src/Data/List.agda index 7747cbbd74..ef77bd0f64 100644 --- a/src/Data/List.agda +++ b/src/Data/List.agda @@ -11,7 +11,30 @@ module Data.List where +import Data.List.NonEmpty.Base as List⁺ +open import Function.Base using (_∘_) + ------------------------------------------------------------------------ -- Types and basic operations -open import Data.List.Base public +open import Data.List.Base public hiding (scanr) + +------------------------------------------------------------------------ +-- scanr + +module _ {a b} {A : Set a} {B : Set b} (f : A → B → B) (e : B) where + + open List⁺ using (toList; scanr⁺) + +-- definition + + scanr : List A → List B + scanr = toList ∘ scanr⁺ f e + +{- +-- which satisfies the following property: + + scanr-defn : scanr ≗ map (foldr f e) ∘ tails + scanr-defn = Data.List.NonEmpty.Properties.toList-scanr⁺ +-} + diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 8b988c646d..fdab9679e4 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -210,12 +210,6 @@ updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f -- Scans -scanr : (A → B → B) → B → List A → List B -scanr f e [] = e ∷ [] -scanr f e (x ∷ xs) with scanr f e xs -... | [] = [] -- dead branch -... | y ∷ ys = f x y ∷ y ∷ ys - scanl : (A → B → A) → A → List B → List A scanl f e [] = e ∷ [] scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs @@ -570,3 +564,16 @@ _─_ = removeAt "Warning: _─_ was deprecated in v2.0. Please use removeAt instead." #-} + +-- Version 2.1 + +scanr : (A → B → B) → B → List A → List B +scanr f e [] = e ∷ [] +scanr f e (x ∷ xs) with scanr f e xs +... | [] = [] -- dead branch +... | ys@(y ∷ _) = f x y ∷ ys +{-# WARNING_ON_USAGE scanr +"Warning: scanr was deprecated in v2.1. +Please use List.scanr instead." +#-} + diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda index 82f16c270a..0d3f0d9e8f 100644 --- a/src/Data/List/NonEmpty/Base.agda +++ b/src/Data/List/NonEmpty/Base.agda @@ -143,6 +143,21 @@ concatMap f = concat ∘′ map f ap : List⁺ (A → B) → List⁺ A → List⁺ B ap fs as = concatMap (λ f → map f as) fs +-- Tails + +tails⁺ : List A → List⁺ (List A) +tails⁺ xs = xs ∷ go xs + where + go : List A → List (List A) + go [] = [] + go (x ∷ xs) = xs ∷ go xs + +-- Scanr + +scanr⁺ : (f : A → B → B) (e : B) → List A → List⁺ B +scanr⁺ f e [] = e ∷ [] +scanr⁺ f e (x ∷ xs) = let y ∷ ys = scanr⁺ f e xs in f x y ∷ y ∷ ys + -- Reverse reverse : List⁺ A → List⁺ A diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 45b27f46c3..7590341b8e 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -46,6 +46,9 @@ private η : ∀ (xs : List⁺ A) → head xs ∷ tail xs ≡ toList xs η _ = refl +toList-injective : {xs ys : List⁺ A} → toList xs ≡ toList ys → xs ≡ ys +toList-injective refl = refl + toList-fromList : ∀ x (xs : List A) → x ∷ xs ≡ toList (x ∷ xs) toList-fromList _ _ = refl @@ -113,6 +116,39 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs) map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs) +toList-map : (f : A → B) → toList ∘ map f ≗ List.map f ∘ toList +toList-map f (x ∷ xs) = refl + +------------------------------------------------------------------------ +-- tails + +toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails {A = A} +toList-tails⁺ [] = refl +toList-tails⁺ ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails⁺ xs) + +------------------------------------------------------------------------ +-- scanr + +module _ (f : A → B → B) (e : B) where + + private + h = List.foldr f e + + scanr⁺-defn : scanr⁺ f e ≗ map h ∘ tails⁺ + scanr⁺-defn [] = refl + scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs + in cong₂ (λ z → f x z ∷_) (cong head eq) (cong toList eq) + + toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map h ∘ List.tails + toList-scanr⁺ xs = begin + toList (scanr⁺ f e xs) + ≡⟨ cong toList (scanr⁺-defn xs) ⟩ + toList (map h (tails⁺ xs)) + ≡⟨ toList-map h (tails⁺ xs) ⟩ + List.map h (toList (tails⁺ xs)) + ≡⟨ cong (List.map h) (toList-tails⁺ xs) ⟩ + List.map h (List.tails xs) ∎ + ------------------------------------------------------------------------ -- groupSeqs diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 2d3c9e20e0..deae97067f 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -8,6 +8,7 @@ -- equalities than _≡_. {-# OPTIONS --cubical-compatible --safe #-} +{-# OPTIONS --warn=noUserWarning #-} -- for deprecated `scanr` (PR #2258) module Data.List.Properties where @@ -618,18 +619,6 @@ sum-++ (x ∷ xs) ys = begin ∈⇒∣product {n} {n ∷ ns} (here refl) = divides (product ns) (*-comm n (product ns)) ∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns) ------------------------------------------------------------------------- --- scanr - -scanr-defn : ∀ (f : A → B → B) (e : B) → - scanr f e ≗ map (foldr f e) ∘ tails -scanr-defn f e [] = refl -scanr-defn f e (x ∷ []) = refl -scanr-defn f e (x ∷ y∷xs@(_ ∷ _)) - with eq ← scanr-defn f e y∷xs - with z ∷ zs ← scanr f e y∷xs - = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq - ------------------------------------------------------------------------ -- scanl @@ -1331,3 +1320,19 @@ map-─ = map-removeAt "Warning: map-─ was deprecated in v2.0. Please use map-removeAt instead." #-} + +-- Version 2.1 + +scanr-defn : ∀ (f : A → B → B) (e : B) → + scanr f e ≗ map (foldr f e) ∘ tails +scanr-defn f e [] = refl +scanr-defn f e (x ∷ []) = refl +scanr-defn f e (x ∷ xs@(_ ∷ _)) + with eq ← scanr-defn f e xs + with ys@(_ ∷ _) ← scanr f e xs + = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) eq +{-# WARNING_ON_USAGE scanr-defn +"Warning: scanr-defn was deprecated in v2.1. +Please use Data.List.NonEmpty.toList-scanr⁺ instead." +#-} +