------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty lists: base type and operations
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.List.NonEmpty.Base where
 
open import Level using (Level)
open import Data.Bool.Base using (Bool; false; true)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Maybe.Base using (Maybe ; nothing; just)
open import Data.Nat.Base as ℕ
open import Data.Product.Base as Prod using (∃; _×_; proj₁; proj₂; _,_; -,_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Data.These.Base as These using (These; this; that; these)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Function.Base
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; _≢_; refl)
open import Relation.Unary using (Pred; Decidable; U; ∅)
open import Relation.Unary.Properties using (U?; ∅?)
open import Relation.Nullary.Decidable using (does)
 
private
  variable
    a p : Level
    A B C : Set a
 
------------------------------------------------------------------------
-- Definition
 
infixr  _∷_
 
record List⁺ (A : Set a) : Set a where
  constructor _∷_
  field
    head : A
    tail : List A
 
open List⁺ public
 
------------------------------------------------------------------------
-- Basic combinators
 
uncons : List⁺ A → A × List A
uncons (hd ∷ tl) = hd , tl
 
[_] : A → List⁺ A
[ x ] = x ∷ []
 
infixr  _∷⁺_
 
_∷⁺_ : A → List⁺ A → List⁺ A
x ∷⁺ y ∷ xs = x ∷ y ∷ xs
 
length : List⁺ A → ℕ
length (x ∷ xs) = suc (List.length xs)
 
------------------------------------------------------------------------
-- Conversion
 
toList : List⁺ A → List A
toList (x ∷ xs) = x ∷ xs
 
fromList : List A → Maybe (List⁺ A)
fromList []       = nothing
fromList (x ∷ xs) = just (x ∷ xs)
 
fromVec : ∀ {n} → Vec A (suc n) → List⁺ A
fromVec (x ∷ xs) = x ∷ Vec.toList xs
 
toVec : (xs : List⁺ A) → Vec A (length xs)
toVec (x ∷ xs) = x ∷ Vec.fromList xs
 
lift : (∀ {m} → Vec A (suc m) → ∃ λ n → Vec B (suc n)) →
       List⁺ A → List⁺ B
lift f xs = fromVec (proj₂ (f (toVec xs)))
 
------------------------------------------------------------------------
-- Other operations
 
map : (A → B) → List⁺ A → List⁺ B
map f (x ∷ xs) = (f x ∷ List.map f xs)
 
replicate : ∀ n → n ≢  → A → List⁺ A
replicate n n≢0 a = a ∷ List.replicate (pred n) a
 
-- when dropping more than the size of the length of the list, the
-- last element remains
drop+ : ℕ → List⁺ A → List⁺ A
drop+ zero    xs           = xs
drop+ (suc n) (x ∷ [])     = x ∷ []
drop+ (suc n) (x ∷ y ∷ xs) = drop+ n (y ∷ xs)
 
-- Right fold. Note that s is only applied to the last element (see
-- the examples below).
 
foldr : (A → B → B) → (A → B) → List⁺ A → B
foldr {A = A} {B = B} c s (x ∷ xs) = foldr′ x xs
  where
  foldr′ : A → List A → B
  foldr′ x []       = s x
  foldr′ x (y ∷ xs) = c x (foldr′ y xs)
 
-- Right fold.
 
foldr₁ : (A → A → A) → List⁺ A → A
foldr₁ f = foldr f id
 
-- Left fold. Note that s is only applied to the first element (see
-- the examples below).
 
foldl : (B → A → B) → (A → B) → List⁺ A → B
foldl c s (x ∷ xs) = List.foldl c (s x) xs
 
-- Left fold.
 
foldl₁ : (A → A → A) → List⁺ A → A
foldl₁ f = foldl f id
 
-- Append (several variants).
 
infixr  _⁺++⁺_ _++⁺_ _⁺++_
 
_⁺++⁺_ : List⁺ A → List⁺ A → List⁺ A
(x ∷ xs) ⁺++⁺ (y ∷ ys) = x ∷ (xs List.++ y ∷ ys)
 
_⁺++_ : List⁺ A → List A → List⁺ A
(x ∷ xs) ⁺++ ys = x ∷ (xs List.++ ys)
 
_++⁺_ : List A → List⁺ A → List⁺ A
xs ++⁺ ys = List.foldr _∷⁺_ ys xs
 
concat : List⁺ (List⁺ A) → List⁺ A
concat (xs ∷ xss) = xs ⁺++ List.concat (List.map toList xss)
 
concatMap : (A → List⁺ B) → List⁺ A → List⁺ B
concatMap f = concat ∘′ map f
 
ap : List⁺ (A → B) → List⁺ A → List⁺ B
ap fs as = concatMap (λ f → map f as) fs
 
-- Inits
 
inits : List A → List⁺ (List A)
inits xs = [] ∷ List.Inits.tail xs
 
-- Tails
 
tails : List A → List⁺ (List A)
tails xs = xs ∷ List.Tails.tail xs
 
-- Reverse
 
reverse : List⁺ A → List⁺ A
reverse = lift (-,_ ∘′ Vec.reverse)
 
-- Align and Zip
 
alignWith : (These A B → C) → List⁺ A → List⁺ B → List⁺ C
alignWith f (a ∷ as) (b ∷ bs) = f (these a b) ∷ List.alignWith f as bs
 
zipWith : (A → B → C) → List⁺ A → List⁺ B → List⁺ C
zipWith f (a ∷ as) (b ∷ bs) = f a b ∷ List.zipWith f as bs
 
unalignWith : (A → These B C) → List⁺ A → These (List⁺ B) (List⁺ C)
unalignWith f = foldr (These.alignWith mcons mcons ∘′ f)
                    (These.map [_] [_] ∘′ f)
 
  where mcons : ∀ {e} {E : Set e} → These E (List⁺ E) → List⁺ E
        mcons = These.fold [_] id _∷⁺_
 
unzipWith : (A → B × C) → List⁺ A → List⁺ B × List⁺ C
unzipWith f (a ∷ as) = Prod.zip _∷_ _∷_ (f a) (List.unzipWith f as)
 
align : List⁺ A → List⁺ B → List⁺ (These A B)
align = alignWith id
 
zip : List⁺ A → List⁺ B → List⁺ (A × B)
zip = zipWith _,_
 
unalign : List⁺ (These A B) → These (List⁺ A) (List⁺ B)
unalign = unalignWith id
 
unzip : List⁺ (A × B) → List⁺ A × List⁺ B
unzip = unzipWith id
 
-- Snoc.
 
infixl  _∷ʳ_ _⁺∷ʳ_
 
_∷ʳ_ : List A → A → List⁺ A
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs List.∷ʳ y)
 
_⁺∷ʳ_ : List⁺ A → A → List⁺ A
xs ⁺∷ʳ x = toList xs ∷ʳ x
 
-- A snoc-view of non-empty lists.
 
infixl  _∷ʳ′_
 
data SnocView {A : Set a} : List⁺ A → Set a where
  _∷ʳ′_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)
 
snocView : (xs : List⁺ A) → SnocView xs
snocView (x ∷ xs)              with List.initLast xs
snocView (x ∷ .[])             | []            = []       ∷ʳ′ x
snocView (x ∷ .(xs List.∷ʳ y)) | xs List.∷ʳ′ y = (x ∷ xs) ∷ʳ′ y
 
-- The last element in the list.
 
private
  last′ : ∀ {l} → SnocView {A = A} l → A
  last′ (_ ∷ʳ′ y) = y
 
last : List⁺ A → A
last = last′ ∘ snocView
 
-- Groups all contiguous elements for which the predicate returns the
-- same result into lists. The left sums are the ones for which the
-- predicate holds, the right ones are the ones for which it doesn't.
groupSeqsᵇ : (A → Bool) → List A → List (List⁺ A ⊎ List⁺ A)
groupSeqsᵇ p []       = []
groupSeqsᵇ p (x ∷ xs) with p x | groupSeqsᵇ p xs
... | true  | inj₁ xs′ ∷ xss = inj₁ (x ∷⁺ xs′) ∷ xss
... | true  | xss            = inj₁ [ x ]      ∷ xss
... | false | inj₂ xs′ ∷ xss = inj₂ (x ∷⁺ xs′) ∷ xss
... | false | xss            = inj₂ [ x ]      ∷ xss
 
-- Groups all contiguous elements /not/ satisfying the predicate into
-- lists. Elements satisfying the predicate are dropped.
wordsByᵇ : (A → Bool) → List A → List (List⁺ A)
wordsByᵇ p = List.mapMaybe Sum.[ const nothing , just ] ∘ groupSeqsᵇ p
 
groupSeqs : {P : Pred A p} → Decidable P → List A → List (List⁺ A ⊎ List⁺ A)
groupSeqs P? = groupSeqsᵇ (does ∘ P?)
 
wordsBy : {P : Pred A p} → Decidable P → List A → List (List⁺ A)
wordsBy P? = wordsByᵇ (does ∘ P?)
 
-- Inverse operation for groupSequences.
ungroupSeqs : List (List⁺ A ⊎ List⁺ A) → List A
ungroupSeqs = List.concat ∘ List.map Sum.[ toList , toList ]
 
------------------------------------------------------------------------
-- Examples
 
-- Note that these examples are simple unit tests, because the type
-- checker verifies them.
 
private
 module Examples {A B : Set}
                 (_⊕_ : A → B → B)
                 (_⊗_ : B → A → B)
                 (_⊙_ : A → A → A)
                 (f : A → B)
                 (a b c : A)
                 where
 
  hd : head (a ∷⁺ b ∷⁺ [ c ]) ≡ a
  hd = refl
 
  tl : tail (a ∷⁺ b ∷⁺ [ c ]) ≡ b ∷ c ∷ []
  tl = refl
 
  mp : map f (a ∷⁺ b ∷⁺ [ c ]) ≡ f a ∷⁺ f b ∷⁺ [ f c ]
  mp = refl
 
  right : foldr _⊕_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊕ (b ⊕ f c))
  right = refl
 
  right₁ : foldr₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊙ (b ⊙ c))
  right₁ = refl
 
  left : foldl _⊗_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ ((f a ⊗ b) ⊗ c)
  left = refl
 
  left₁ : foldl₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c)
  left₁ = refl
 
  ⁺app⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺++⁺ (b ∷⁺ [ c ]) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  ⁺app⁺ = refl
 
  ⁺app : (a ∷⁺ b ∷⁺ [ c ]) ⁺++ (b ∷ c ∷ []) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  ⁺app = refl
 
  app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷⁺ [ c ]) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  app⁺ = refl
 
  conc : concat ((a ∷⁺ b ∷⁺ [ c ]) ∷⁺ [ b ∷⁺ [ c ] ]) ≡
         a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  conc = refl
 
  rev : reverse (a ∷⁺ b ∷⁺ [ c ]) ≡ c ∷⁺ b ∷⁺ [ a ]
  rev = refl
 
  snoc : (a ∷ b ∷ c ∷ []) ∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
  snoc = refl
 
  snoc⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
  snoc⁺ = refl
 
  groupSeqs-true : groupSeqs U? (a ∷ b ∷ c ∷ []) ≡
               inj₁ (a ∷⁺ b ∷⁺ [ c ]) ∷ []
  groupSeqs-true = refl
 
  groupSeqs-false : groupSeqs ∅? (a ∷ b ∷ c ∷ []) ≡
                inj₂ (a ∷⁺ b ∷⁺ [ c ]) ∷ []
  groupSeqs-false = refl
 
  groupSeqs-≡1 : groupSeqsᵇ (ℕ._≡ᵇ ) ( ∷  ∷  ∷  ∷  ∷  ∷  ∷ []) ≡
                 inj₁ [  ] ∷
                 inj₂ ( ∷⁺ [  ]) ∷
                 inj₁ ( ∷⁺ [  ]) ∷
                 inj₂ [  ] ∷
                 inj₁ [  ] ∷
                 []
  groupSeqs-≡1 = refl
 
  wordsBy-true : wordsByᵇ (const true) (a ∷ b ∷ c ∷ []) ≡ []
  wordsBy-true = refl
 
  wordsBy-false : wordsByᵇ (const false) (a ∷ b ∷ c ∷ []) ≡
                  (a ∷⁺ b ∷⁺ [ c ]) ∷ []
  wordsBy-false = refl
 
  wordsBy-≡1 : wordsByᵇ (ℕ._≡ᵇ ) ( ∷  ∷  ∷  ∷  ∷  ∷  ∷ []) ≡
               ( ∷⁺ [  ]) ∷
               [  ] ∷
               []
  wordsBy-≡1 = refl