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