```------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists, based on the Kleene star and plus, basic types and operations.
------------------------------------------------------------------------

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

module Data.List.Kleene.Base where

open import Data.Product.Base as Product
using (_×_; _,_; map₂; map₁; proj₁; proj₂)
open import Data.Nat.Base as ℕ using (ℕ; suc; zero)
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Level using (Level)

open import Algebra.Core using (Op₂)
open import Function.Base

private
variable
a b c : Level
A : Set a
B : Set b
C : Set c

------------------------------------------------------------------------
-- Definitions
--
-- These lists are exactly equivalent to normal lists, except the "cons"
-- case is split into its own data type. This lets us write all the same
-- functions as before, but it has 2 advantages:
--
-- * Some functions are easier to express on the non-empty type. Head,
--   for instance, has a natural safe implementation. Having the
--   non-empty type be defined mutually with the normal type makes the
--   use of this non-empty type occasionally more ergonomic.
-- * It can make some proofs easier. By using the non-empty type where
--   possible, we can avoid an extra pattern match, which can really
--   simplify certain proofs.

infixr 5 _&_ ∹_
infixl 4 _+ _*

record _+ {a} (A : Set a) : Set a
data _* {a} (A : Set a) : Set a

-- Non-Empty Lists
record _+ A where
inductive
constructor _&_
field
tail : A *

-- Possibly Empty Lists
data _* A where
[] : A *
∹_ : A + → A *
open _+ public

------------------------------------------------------------------------
-- Uncons

uncons : A * → Maybe (A +)
uncons []     = nothing
uncons (∹ xs) = just xs

------------------------------------------------------------------------
-- FoldMap

foldMap+ : Op₂ B → (A → B) → A + → B
foldMap+ _∙_ f (x & [])   = f x
foldMap+ _∙_ f (x & ∹ xs) = f x ∙ foldMap+ _∙_ f xs

foldMap* : Op₂ B → B → (A → B) → A * → B
foldMap* _∙_ ε f []     = ε
foldMap* _∙_ ε f (∹ xs) = foldMap+ _∙_ f xs

------------------------------------------------------------------------
-- Folds

module _ (f : A → B → B) (b : B) where
foldr+ : A + → B
foldr* : A * → B

foldr+ (x & xs) = f x (foldr* xs)

foldr* []     = b
foldr* (∹ xs) = foldr+ xs

module _ (f : B → A → B) where
foldl+ : B → A + → B
foldl* : B → A * → B

foldl+ b (x & xs) = foldl* (f b x) xs

foldl* b []     = b
foldl* b (∹ xs) = foldl+ b xs

------------------------------------------------------------------------
-- Concatenation

module Concat where
infixr 4 _++++_ _+++*_ _*+++_ _*++*_
_++++_ : A + → A + → A +
_+++*_ : A + → A * → A +
_*+++_ : A * → A + → A +
_*++*_ : A * → A * → A *

tail (xs +++* ys) = tail xs *++* ys

xs *++* ys = foldr* (λ x zs → ∹ x & zs) ys xs

xs ++++ ys = foldr+ (λ x zs → x & ∹ zs) ys xs

[]     *+++ ys = ys
(∹ xs) *+++ ys = xs ++++ ys
open Concat public using () renaming (_++++_ to _+++_; _*++*_ to _++*_)

------------------------------------------------------------------------
-- Mapping

module _  (f : A → B) where
map+ : A + → B +
map* : A * → B *

tail (map+ xs) = map* (tail xs)

map* []     = []
map* (∹ xs) = ∹ map+ xs

module _ (f : A → Maybe B) where
mapMaybe+ : A + → B *
mapMaybe* : A * → B *

mapMaybe+ (x & xs) with f x
... | just y  = ∹ y & mapMaybe* xs
... | nothing = mapMaybe* xs

mapMaybe* []     = []
mapMaybe* (∹ xs) = mapMaybe+ xs

------------------------------------------------------------------------
-- Applicative Operations

pure+ : A → A +
tail (pure+ x) = []

pure* : A → A *
pure* x = ∹ pure+ x

module Apply where
_*<*>*_ : (A → B) * → A * → B *
_+<*>*_ : (A → B) + → A * → B *
_*<*>+_ : (A → B) * → A + → B *
_+<*>+_ : (A → B) + → A + → B +

[]     *<*>* xs = []
(∹ fs) *<*>* xs = fs +<*>* xs

fs +<*>* xs = map* (head fs) xs ++* (tail fs *<*>* xs)

[]     *<*>+ xs = []
(∹ fs) *<*>+ xs = ∹ fs +<*>+ xs

fs +<*>+ xs = map+ (head fs) xs Concat.+++* (tail fs *<*>+ xs)
open Apply public using () renaming (_*<*>*_ to _<*>*_; _+<*>+_ to _<*>+_)

------------------------------------------------------------------------

module Bind where
_+>>=+_ : A + → (A → B +) → B +
_+>>=*_ : A + → (A → B *) → B *
_*>>=+_ : A * → (A → B +) → B *
_*>>=*_ : A * → (A → B *) → B *

(x & xs) +>>=+ k = k x Concat.+++* (xs *>>=+ k)

(x & xs) +>>=* k = k x Concat.*++* (xs *>>=* k)

[]     *>>=* k = []
(∹ xs) *>>=* k = xs +>>=* k

[]     *>>=+ k = []
(∹ xs) *>>=+ k = ∹ xs +>>=+ k
open Bind public using () renaming (_*>>=*_ to _>>=*_; _+>>=+_ to _>>=+_)

------------------------------------------------------------------------
-- Scans

module Scanr (f : A → B → B) (b : B) where
cons : A → B + → B +
tail (cons x xs) = ∹ xs

scanr+ : A + → B +
scanr* : A * → B +

scanr* = foldr* cons (b & [])
scanr+ = foldr+ cons (b & [])
open Scanr public using (scanr+; scanr*)

module _ (f : B → A → B) where
scanl* : B → A * → B +
head (scanl* b xs)     = b
tail (scanl* b [])     = []
tail (scanl* b (∹ xs)) = ∹ scanl* (f b (head xs)) (tail xs)

scanl+ : B → A + → B +
head (scanl+ b xs) = b
tail (scanl+ b xs) = ∹ scanl* (f b (head xs)) (tail xs)

scanl₁ : B → A + → B +
scanl₁ b xs = scanl* (f b (head xs)) (tail xs)

------------------------------------------------------------------------
-- Accumulating maps

module _ (f : B → A → (B × C)) where
mapAccumˡ* : B → A * → (B × C *)
mapAccumˡ+ : B → A + → (B × C +)

mapAccumˡ* b []     = b , []
mapAccumˡ* b (∹ xs) = map₂ ∹_ (mapAccumˡ+ b xs)

mapAccumˡ+ b (x & xs) =
let y , ys = f b x
z , zs = mapAccumˡ* y xs
in z , ys & zs

module _ (f : A → B → (C × B)) (b : B) where
mapAccumʳ* : A * → (C * × B)
mapAccumʳ+ : A + → (C + × B)

mapAccumʳ* [] = [] , b
mapAccumʳ* (∹ xs) = map₁ ∹_ (mapAccumʳ+ xs)

mapAccumʳ+ (x & xs) =
let ys , y = mapAccumʳ* xs
zs , z = f x y
in zs & ys , z

------------------------------------------------------------------------
-- Non-Empty Folds

last : A + → A
last (x & [])   = x
last (_ & ∹ xs) = last xs

module _ (f : A → A → A) where
foldr₁ : A + → A
foldr₁ (x & [])   = x
foldr₁ (x & ∹ xs) = f x (foldr₁ xs)

foldl₁ : A + → A
foldl₁ (x & xs) = foldl* f x xs

module _ (f : A → Maybe B → B) where
foldrMaybe* : A * → Maybe B
foldrMaybe+ : A + → B

foldrMaybe* []     = nothing
foldrMaybe* (∹ xs) = just (foldrMaybe+ xs)

foldrMaybe+ xs = f (head xs) (foldrMaybe* (tail xs))

------------------------------------------------------------------------
-- Indexing

infix 4 _[_]* _[_]+

_[_]* : A * → ℕ → Maybe A
_[_]+ : A + → ℕ → Maybe A

[]     [ _ ]* = nothing
(∹ xs) [ i ]* = xs [ i ]+

xs [ zero  ]+ = just (head xs)
xs [ suc i ]+ = tail xs [ i ]*

applyUpTo* : (ℕ → A) → ℕ → A *
applyUpTo+ : (ℕ → A) → ℕ → A +

applyUpTo* f zero    = []
applyUpTo* f (suc n) = ∹ applyUpTo+ f n

head (applyUpTo+ f n) = f zero
tail (applyUpTo+ f n) = applyUpTo* (f ∘ suc) n

upTo* : ℕ → ℕ *
upTo* = applyUpTo* id

upTo+ : ℕ → ℕ +
upTo+ = applyUpTo+ id

------------------------------------------------------------------------
-- Manipulation

module ZipWith (f : A → B → C) where
+zipWith+ : A + → B + → C +
*zipWith+ : A * → B + → C *
+zipWith* : A + → B * → C *
*zipWith* : A * → B * → C *

tail (+zipWith+ xs ys) = *zipWith* (tail xs) (tail ys)

*zipWith+ [] ys     = []
*zipWith+ (∹ xs) ys = ∹ +zipWith+ xs ys

+zipWith* xs []     = []
+zipWith* xs (∹ ys) = ∹ +zipWith+ xs ys

*zipWith* [] ys     = []
*zipWith* (∹ xs) ys = +zipWith* xs ys
open ZipWith public renaming (+zipWith+ to zipWith+; *zipWith* to zipWith*)

module Unzip (f : A → B × C) where
cons : B × C → B * × C * → B + × C +
cons = Product.zip′ _&_ _&_

unzipWith* : A * → B * × C *
unzipWith+ : A + → B + × C +

unzipWith* = foldr* (λ x xs → Product.map ∹_ ∹_ (cons (f x) xs)) ([] , [])

unzipWith+ xs = cons (f (head xs)) (unzipWith* (tail xs))
open Unzip using (unzipWith+; unzipWith*) public

module Partition (f : A → B ⊎ C) where
cons : B ⊎ C → B * × C * → B * × C *
proj₁ (cons (inj₁ x) xs) = ∹ x & proj₁ xs
proj₂ (cons (inj₁ x) xs) = proj₂ xs
proj₂ (cons (inj₂ x) xs) = ∹ x & proj₂ xs
proj₁ (cons (inj₂ x) xs) = proj₁ xs

partitionSumsWith* : A * → B * × C *
partitionSumsWith+ : A + → B * × C *

partitionSumsWith* = foldr* (cons ∘ f) ([] , [])

partitionSumsWith+ = foldr+ (cons ∘ f) ([] , [])
open Partition using (partitionSumsWith+; partitionSumsWith*) public

tails* : A * → (A +) *
tails+ : A + → (A +) +