a better scanr, via Data.List.NonEmpty

CHANGELOG.md

@@ -21,6 +21,16 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Data.List.Base`:
+  ```agda
+  scanr  : (A → B → B) → B → List A → List B
+  ```
+
+* In `Data.List.Properties`:
+  ```agda
+  scanr-defn : scanr f e ≗ map (foldr f e) ∘ tails
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -37,6 +47,12 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
+* In `Data.List`:
+  ```agda
+  scanr      : (A → B → B) → B → List A → List B
+  scanr-defn : scanr f e ≗ map (foldr f e) ∘ tails
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)

src/Data/List.agda

@@ -11,7 +11,35 @@
 
 module Data.List where
 
+import Data.List.NonEmpty.Base as List⁺
+import Data.List.Properties as List
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality using (refl; cong₂; _≗_)
+
 ------------------------------------------------------------------------
 -- 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 (List⁺; _∷_; toList)
+
+-- definition
+
+  scanr : List A → List B
+  scanr = toList ∘ go where
+    go : List A → List⁺ B
+    go []       = e ∷ []
+    go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
+
+-- property
+
+  scanr-defn : scanr ≗ map (foldr f e) ∘ tails
+  scanr-defn []                 = refl
+  scanr-defn (x ∷ [])           = refl
+  scanr-defn (x ∷ y∷ys@(_ ∷ _)) = let eq = scanr-defn y∷ys in
+    cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq

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."
+#-}
+

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
 
@@ -1292,3 +1281,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 List.scanr-defn instead."
+#-}
+