------------------------------------------------------------------------
-- The Agda standard library
--
-- List scans: definitions
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.List.Scans.Base where
 
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_; toList)
open import Function.Base using (_∘_)
open import Level using (Level)
 
private
  variable
    a b : Level
    A : Set a
    B : Set b
 
 
------------------------------------------------------------------------
-- Definitions
 
-- Scanr
 
module _ (f : A → B → B) where
 
  scanr⁺ : (e : B) → List A → List⁺ B
  scanr⁺ e []       = e ∷ []
  scanr⁺ e (x ∷ xs) = let y ∷ ys = scanr⁺ e xs in f x y ∷ y ∷ ys
 
  scanr : (e : B) → List A → List B
  scanr e = toList ∘ scanr⁺ e
 
-- Scanl
 
module _ (f : A → B → A) where
 
  scanl⁺ : A → List B → List⁺ A
  scanl⁺ e xs = e ∷ go e xs
    where
    go : A → List B → List A
    go _ []       = []
    go e (x ∷ xs) = let fex = f e x in fex ∷ go fex xs
 
  scanl : A → List B → List A
  scanl e = toList ∘ scanl⁺ e