    ------------------------------------------------------------------------
    -- 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 Algebra.Core using (Op₂)
    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 Function.Base using (id; _$_; _∘_)
    open import Level using (Level)

    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