------------------------------------------------------------------------
-- 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; maybe′)
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
    head : A
    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 *

  head (xs +++* ys) = head xs
  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 *

  head (map+ xs) = f (head xs)
  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) = maybe′ (λ y z → ∹ y & z) id (f x) $ mapMaybe* xs

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

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

pure+ : A → A +
head (pure+ x) = x
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 _<*>+_)

------------------------------------------------------------------------
-- Monadic Operations

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 +
  head (cons x xs) = f x (head xs)
  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+ (x & xs) = f x (foldrMaybe* 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 *

  head (+zipWith+ xs ys) = f (head xs) (head ys)
  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 +) +

head (tails+ xs) = xs
tail (tails+ xs) = tails* (tail xs)

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

reverse* : A * → A *
reverse* = foldl* (λ xs x → ∹ x & xs) []

reverse+ : A + → A +
reverse+ (x & xs) = foldl* (λ ys y → y & ∹ ys) (x & []) xs