module Haskell.Prim.Foldable where

open import Haskell.Prim
open import Haskell.Prim.Num
open import Haskell.Prim.Eq
open import Haskell.Prim.List
open import Haskell.Prim.Int
open import Haskell.Prim.Bool
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either
open import Haskell.Prim.Tuple
open import Haskell.Prim.Monoid

--------------------------------------------------
-- Foldable

record Foldable (t : Set → Set) : Set₁ where
  field
    foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b

open Foldable ⦃ ... ⦄ public

{-# COMPILE AGDA2HS Foldable existing-class #-}

foldr : ⦃ Foldable t ⦄ → (a → b → b) → b → t a → b
foldr f z t = foldMap ⦃ it ⦄ ⦃ MonoidEndo ⦄ f t z

foldl : ⦃ Foldable t ⦄ → (b → a → b) → b → t a → b
foldl f z t = foldMap ⦃ it ⦄ ⦃ MonoidEndoᵒᵖ ⦄ (flip f) t z

any : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool
any = foldMap ⦃ it ⦄ ⦃ MonoidDisj ⦄

all : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool
all = foldMap ⦃ it ⦄ ⦃ MonoidConj ⦄

and : ⦃ Foldable t ⦄ → t Bool → Bool
and = all id

or : ⦃ Foldable t ⦄ → t Bool → Bool
or = any id

null : ⦃ Foldable t ⦄ → t a → Bool
null = all (const False)

concat : ⦃ Foldable t ⦄ → t (List a) → List a
concat = foldMap id

concatMap : ⦃ Foldable t ⦄ → (a → List b) → t a → List b
concatMap = foldMap

elem : ⦃ Foldable t ⦄ → ⦃ Eq a ⦄ → a → t a → Bool
elem x = foldMap ⦃ it ⦄ ⦃ MonoidDisj ⦄ (x ==_)

notElem : ⦃ Foldable t ⦄ → ⦃ Eq a ⦄ → a → t a → Bool
notElem x t = not (elem x t)

toList : ⦃ Foldable t ⦄ → t a → List a
toList = foldr _∷_ []

sum : ⦃ Foldable t ⦄ → ⦃ iNum : Num a ⦄ → t a → a
sum = foldMap ⦃ it ⦄ ⦃ MonoidSum ⦄ id

product : ⦃ Foldable t ⦄ → ⦃ iNum : Num a ⦄ → t a → a
product = foldMap ⦃ it ⦄ ⦃ MonoidProduct ⦄ id

length : ⦃ Foldable t ⦄ → t a → Int
length = foldMap ⦃ it ⦄ ⦃ MonoidSum ⦄ (const )

instance
  iFoldableList : Foldable List
  iFoldableList .foldMap = foldMapList
    where
      foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b
      foldMapList f []       = mempty
      foldMapList f (x ∷ xs) = f x <> foldMapList f xs

  iFoldableMaybe : Foldable Maybe
  iFoldableMaybe .foldMap _ Nothing  = mempty
  iFoldableMaybe .foldMap f (Just x) = f x

  iFoldableEither : Foldable (Either a)
  iFoldableEither .foldMap _ (Left _) = mempty
  iFoldableEither .foldMap f (Right x) = f x

  iFoldablePair : Foldable (a ×_)
  iFoldablePair .foldMap f (_ , x) = f x