------------------------------------------------------------------------ -- 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 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 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 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. 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ᵇ (ℕ._≡ᵇ 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