------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty lists: base type and operations
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.List.NonEmpty.Base where

open import Level using (Level)
open import Data.Bool.Base using (Bool; false; true; not; T)
open import Data.Bool.Properties using (T?)
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 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 using (does)

private
  variable
    a p : Level
    A B C : Set a

------------------------------------------------------------------------
-- Definition

infixr 5 _∷_

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 5 _∷⁺_

_∷⁺_ : 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  0  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 5 _⁺++⁺_ _++⁺_ _⁺++_

_⁺++⁺_ : 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

-- 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 5 _∷ʳ_ _⁺∷ʳ_

_∷ʳ_ : 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 5 _∷ʳ′_

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.

last : List⁺ A  A
last xs with snocView xs
last .(ys ∷ʳ y) | ys ∷ʳ′ y = y

-- 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ᵇ (ℕ._≡ᵇ 1) (1  2  3  1  1  2  1  []) 
                 inj₁ [ 1 ] 
                 inj₂ (2 ∷⁺ [ 3 ]) 
                 inj₁ (1 ∷⁺ [ 1 ]) 
                 inj₂ [ 2 ] 
                 inj₁ [ 1 ] 
                 []
  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ᵇ (ℕ._≡ᵇ 1) (1  2  3  1  1  2  1  []) 
               (2 ∷⁺ [ 3 ]) 
               [ 2 ] 
               []
  wordsBy-≡1 = refl