From 196766082e913de0d7cd98e3b672935a3b4528b8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Fri, 5 Jul 2024 10:03:33 +0200
Subject: [PATCH] Revert "Improve `Data.List.Base` (fix #2359; deprecate use of
 `with` #2123) (#2365)" (#2423)

This reverts commit 438f9ed4c30751be35718297bbe0c8ec7d3fb669.

Specifically, it restores `with`-based definitions of the
`Decidable`-definable functions on `List`s, incl. `filter`
Fixes #2415
---
 src/Data/List/Base.agda       | 46 +++++++++++++++--------------------
 src/Data/List/Properties.agda | 30 +++++++++++------------
 2 files changed, 35 insertions(+), 41 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 5c98372dc5..0c63e34940 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -358,49 +358,45 @@ removeAt (x ∷ xs) (suc i)  = x ∷ removeAt xs i
 
 takeWhile : ∀ {P : Pred A p} → Decidable P → List A → List A
 takeWhile P? []       = []
-takeWhile P? (x ∷ xs) = if does (P? x)
-  then x ∷ takeWhile P? xs
-  else []
+takeWhile P? (x ∷ xs) with does (P? x)
+... | true  = x ∷ takeWhile P? xs
+... | false = []
 
 takeWhileᵇ : (A → Bool) → List A → List A
 takeWhileᵇ p = takeWhile (T? ∘ p)
 
 dropWhile : ∀ {P : Pred A p} → Decidable P → List A → List A
 dropWhile P? []       = []
-dropWhile P? (x ∷ xs) = if does (P? x)
-  then dropWhile P? xs
-  else x ∷ xs
+dropWhile P? (x ∷ xs) with does (P? x)
+... | true  = dropWhile P? xs
+... | false = x ∷ xs
 
 dropWhileᵇ : (A → Bool) → List A → List A
 dropWhileᵇ p = dropWhile (T? ∘ p)
 
 filter : ∀ {P : Pred A p} → Decidable P → List A → List A
 filter P? [] = []
-filter P? (x ∷ xs) =
-  let xs′ = filter P? xs in
-  if does (P? x)
-    then x ∷ xs′
-    else xs′
+filter P? (x ∷ xs) with does (P? x)
+... | false = filter P? xs
+... | true  = x ∷ filter P? xs
 
 filterᵇ : (A → Bool) → List A → List A
 filterᵇ p = filter (T? ∘ p)
 
 partition : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
-partition P? []       = [] , []
-partition P? (x ∷ xs) =
-  let ys , zs = partition P? xs in
-  if does (P? x)
-    then (x ∷ ys , zs)
-    else (ys , x ∷ zs)
+partition P? []       = ([] , [])
+partition P? (x ∷ xs) with does (P? x) | partition P? xs
+... | true  | (ys , zs) = (x ∷ ys , zs)
+... | false | (ys , zs) = (ys , x ∷ zs)
 
 partitionᵇ : (A → Bool) → List A → List A × List A
 partitionᵇ p = partition (T? ∘ p)
 
 span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
-span P? []          = [] , []
-span P? ys@(x ∷ xs) = if does (P? x)
-  then Product.map (x ∷_) id (span P? xs)
-  else ([] , ys)
+span P? []       = ([] , [])
+span P? ys@(x ∷ xs) with does (P? x)
+... | true  = Product.map (x ∷_) id (span P? xs)
+... | false = ([] , ys)
 
 
 spanᵇ : (A → Bool) → List A → List A × List A
@@ -452,11 +448,9 @@ wordsByᵇ p = wordsBy (T? ∘ p)
 derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A
 derun R? [] = []
 derun R? (x ∷ []) = x ∷ []
-derun R? (x ∷ xs@(y ∷ _)) =
-  let ys = derun R? xs in
-  if does (R? x y)
-    then ys
-    else x ∷ ys
+derun R? (x ∷ xs@(y ∷ _)) with does (R? x y) | derun R? xs
+... | true  | ys = ys
+... | false | ys = x ∷ ys
 
 derunᵇ : (A → A → Bool) → List A → List A
 derunᵇ r = derun (T? ∘₂ r)
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index d5bd6624f9..b9936f2a3b 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1163,13 +1163,13 @@ module _ {P : Pred A p} (P? : Decidable P) where
   filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
   filter-all {[]}     []         = refl
   filter-all {x ∷ xs} (px ∷ pxs) with P? x
-  ... | false because [¬px] = contradiction px (invert [¬px])
-  ... | true  because _     = cong (x ∷_) (filter-all pxs)
+  ... | no          ¬px = contradiction px ¬px
+  ... | true  because _ = cong (x ∷_) (filter-all pxs)
 
   filter-notAll : ∀ xs → Any (∁ P) xs → length (filter P? xs) < length xs
   filter-notAll (x ∷ xs) (here ¬px) with P? x
-  ... | false because _    = s≤s (length-filter xs)
-  ... | true  because [px] = contradiction (invert [px]) ¬px
+  ... | false because _ = s≤s (length-filter xs)
+  ... | yes          px = contradiction px ¬px
   filter-notAll (x ∷ xs) (there any) with ih ← filter-notAll xs any | does (P? x)
   ... | false = m≤n⇒m≤1+n ih
   ... | true  = s≤s ih
@@ -1185,8 +1185,8 @@ module _ {P : Pred A p} (P? : Decidable P) where
   filter-none : ∀ {xs} → All (∁ P) xs → filter P? xs ≡ []
   filter-none {[]}     []           = refl
   filter-none {x ∷ xs} (¬px ∷ ¬pxs) with P? x
-  ... | false because _    = filter-none ¬pxs
-  ... | true  because [px] = contradiction (invert [px]) ¬px
+  ... | false because _ = filter-none ¬pxs
+  ... | yes          px = contradiction px ¬px
 
   filter-complete : ∀ {xs} → length (filter P? xs) ≡ length xs →
                     filter P? xs ≡ xs
@@ -1197,13 +1197,13 @@ module _ {P : Pred A p} (P? : Decidable P) where
 
   filter-accept : ∀ {x xs} → P x → filter P? (x ∷ xs) ≡ x ∷ (filter P? xs)
   filter-accept {x} Px with P? x
-  ... | true  because _     = refl
-  ... | false because [¬Px] = contradiction Px (invert [¬Px])
+  ... | true because _ = refl
+  ... | no         ¬Px = contradiction Px ¬Px
 
   filter-reject : ∀ {x xs} → ¬ P x → filter P? (x ∷ xs) ≡ filter P? xs
   filter-reject {x} ¬Px with P? x
-  ... | true  because [Px] = contradiction (invert [Px]) ¬Px
-  ... | false because _    = refl
+  ... | yes          Px = contradiction Px ¬Px
+  ... | false because _ = refl
 
   filter-idem : filter P? ∘ filter P? ≗ filter P?
   filter-idem []       = refl
@@ -1241,13 +1241,13 @@ module _ {R : Rel A p} (R? : B.Decidable R) where
 
   derun-reject : ∀ {x y} xs → R x y → derun R? (x ∷ y ∷ xs) ≡ derun R? (y ∷ xs)
   derun-reject {x} {y} xs Rxy with R? x y
-  ... | true  because _      = refl
-  ... | false because [¬Rxy] = contradiction Rxy (invert [¬Rxy])
+  ... | yes _    = refl
+  ... | no  ¬Rxy = contradiction Rxy ¬Rxy
 
   derun-accept : ∀ {x y} xs → ¬ R x y → derun R? (x ∷ y ∷ xs) ≡ x ∷ derun R? (y ∷ xs)
   derun-accept {x} {y} xs ¬Rxy with R? x y
-  ... | true  because [Rxy] = contradiction (invert [Rxy]) ¬Rxy
-  ... | false because  _    = refl
+  ... | yes Rxy = contradiction Rxy ¬Rxy
+  ... | no  _   = refl
 
 ------------------------------------------------------------------------
 -- partition
@@ -1260,7 +1260,7 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ...  | true  = cong (Product.map (x ∷_) id) ih
   ...  | false = cong (Product.map id (x ∷_)) ih
 
-  length-partition : ∀ xs → (let ys , zs = partition P? xs) →
+  length-partition : ∀ xs → (let (ys , zs) = partition P? xs) →
                      length ys ≤ length xs × length zs ≤ length xs
   length-partition []       = z≤n , z≤n
   length-partition (x ∷ xs) with ih ← length-partition xs | does (P? x)