------------------------------------------------------------------------
-- 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