------------------------------------------------------------------------
-- The Agda standard library
--
-- Vec is Foldable
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Vec.Effectful.Foldable where

open import Algebra.Bundles.Raw using (RawMonoid)
open import Data.Nat.Base using (ℕ)
open import Data.Vec.Base using (Vec; []; _∷_; foldr′; foldl′; toList)
open import Effect.Foldable using (RawFoldableWithDefaults; RawFoldable)
open import Function.Base using (id)
open import Level using (Level)

private
  variable
    a c ℓ : Level
    A : Set a
    n : ℕ

------------------------------------------------------------------------
-- Root implementation

module _ (M : RawMonoid c ℓ) where

  open RawMonoid M

  foldMap : (A → Carrier) → Vec A n → Carrier
  foldMap f []       = ε
  foldMap f (x ∷ xs) = f x ∙ foldMap f xs

------------------------------------------------------------------------
-- Basic implementation using supplied defaults

foldableWithDefaults : RawFoldableWithDefaults {a} (λ A → Vec A n)
foldableWithDefaults = record { foldMap = λ M → foldMap M }

------------------------------------------------------------------------
-- Specialised version using optimised implementations

foldable : RawFoldable {a} (λ A → Vec A n)
foldable = record
  { foldMap = λ M → foldMap M
  ; foldr = foldr′
  ; foldl = foldl′
  ; toList = toList
  }