[ new ] Data.SnocList.Base (re #2684)

CHANGELOG.md

@@ -18,6 +18,8 @@ Bug-fixes
 
 * Fix a typo in `Function.Construct.Constant`.
 
+* Fix a bug in `Data.List.Base`'s `linesBy` (the last empty line would be dropped).
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -177,6 +179,14 @@ New modules
 
 * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
 
+
+* A new type of lists that grow on the right.
+  This is typically useful to model contexts of typing rules
+  or type accumulators that need to be reversed in the base case.
+  ```
+  Data.SnocList.Base
+  ```
+
 * Added tactic ring solvers for rational numbers (issue #1879):
   ```agda
   Data.Rational.Tactic.RingSolver

src/Data/List/Base.agda

@@ -395,14 +395,16 @@ breakᵇ p = break (T? ∘ p)
 -- 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
+linesBy {A = A} P? = go [] where
 
-  go : Maybe (List A) → List A → List (List A)
-  go acc []       = maybe′ ([_] ∘′ reverse) [] acc
+  -- ideally this should use a snoclist for the accumulator
+  -- but unfortunately this is in the dependency graph of
+  -- Data.SnocList.Base
+  go : List A → List A → List (List A)
+  go acc []       = [ reverse acc ]
   go acc (c ∷ cs) = if does (P? c)
-    then reverse acc′ ∷ go nothing cs
-    else go (just (c ∷ acc′)) cs
-    where acc′ = Maybe.fromMaybe [] acc
+    then reverse acc ∷ go [] cs
+    else go (c ∷ acc) cs
 
 linesByᵇ : (A → Bool) → List A → List (List A)
 linesByᵇ p = linesBy (T? ∘ p)