[ fix ] lines should not drop empty lines (#1372)

Author: gallais

CHANGELOG.md

@@ -397,7 +397,13 @@ Other minor additions
   id-⟶     : A ⟶ A
   ```
 
-* Added new function to `Data.String.Base`:
+* Added new function to `Data.List.Base`:
+  ```agda
+  linesBy : Decidable P → List A → List (List A)
+  ```
+
+* Added new functions to `Data.String.Base`:
   ```agda
-  lines : String → List String
+  linesBy : Decidable P → String → List String
+  lines   : String → List String
   ```

src/Data/List/Base.agda

@@ -385,6 +385,23 @@ unsnoc as with initLast as
 ------------------------------------------------------------------------
 -- Splitting a list
 
+-- The predicate `P` represents the notion of newline character for the type `A`
+-- It is used to split the input list into a list of lines. Some lines may be
+-- empty if the input contains at least two consecutive newline characters.
+
+linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A)
+linesBy {A = A} P? = go nothing where
+
+  go : Maybe (List A) → List A → List (List A)
+  go acc []       = maybe′ ([_] ∘′ reverse) [] acc
+  go acc (c ∷ cs) with does (P? c)
+  ... | true  = reverse (Maybe.fromMaybe [] acc) ∷ go nothing cs
+  ... | false = go (just (c ∷ Maybe.fromMaybe [] acc)) cs
+
+-- The predicate `P` represents the notion of space character for the type `A`.
+-- It is used to split the input list into a list of words. All the words are
+-- non empty and the output does not contain any space characters.
+
 wordsBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A)
 wordsBy {A = A} P? = go [] where
 

src/Data/String/Base.agda

@@ -13,7 +13,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Bool.Properties using (T?)
 open import Data.Nat.Base as ℕ using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉)
 import Data.Nat.Properties as ℕₚ
-open import Data.List.Base as List using (List; [_])
+open import Data.List.Base as List using (List; _∷_; []; [_])
 open import Data.List.NonEmpty as NE using (List⁺)
 open import Data.List.Extrema ℕₚ.≤-totalOrder
 open import Data.List.Relation.Binary.Pointwise using (Pointwise)
@@ -23,6 +23,7 @@ open import Data.Char.Base as Char using (Char)
 import Data.Char.Properties as Char using (_≟_)
 open import Function
 open import Relation.Binary using (Rel)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Relation.Nullary using (does)
 open import Relation.Unary using (Pred; Decidable)
 
@@ -95,11 +96,22 @@ wordsBy P? = List.map fromList ∘ List.wordsBy P? ∘ toList
 words : String → List String
 words = wordsBy (T? ∘ Char.isSpace)
 
+-- `words` ignores contiguous whitespace
+_ : words " abc  b   " ≡ "abc" ∷ "b" ∷ []
+_ = refl
+
 unwords : List String → String
 unwords = intersperse " "
 
+linesBy : ∀ {p} {P : Pred Char p} → Decidable P → String → List String
+linesBy P? = List.map fromList ∘ List.linesBy P? ∘ toList
+
 lines : String → List String
-lines = wordsBy ('\n' Char.≟_)
+lines = linesBy ('\n' Char.≟_)
+
+-- `lines` preserves empty lines
+_ : lines "\nabc\n\nb\n\n\n" ≡ "" ∷ "abc" ∷ "" ∷ "b" ∷ "" ∷ "" ∷ []
+_ = refl
 
 unlines : List String → String
 unlines = intersperse "\n"