From 1d2766097a2bae3c38a0de0b311bc0a6648af975 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 15 Apr 2024 16:53:13 +0100 Subject: [PATCH 1/3] refactor towards `if_then_else_` --- src/Data/List/Base.agda | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 8b988c646d..9343f4ebf4 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -428,9 +428,10 @@ 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 + go acc (c ∷ cs) = let acc′ = Maybe.fromMaybe [] acc in + if does (P? c) + then reverse acc′ ∷ go nothing cs + else go (just (c ∷ acc′)) cs linesByᵇ : (A → Bool) → List A → List (List A) linesByᵇ p = linesBy (T? ∘ p) @@ -448,9 +449,9 @@ wordsBy {A = A} P? = go [] where go : List A → List A → List (List A) go acc [] = cons acc [] - go acc (c ∷ cs) with does (P? c) - ... | true = cons acc (go [] cs) - ... | false = go (c ∷ acc) cs + go acc (c ∷ cs) = if does (P? c) + then cons acc (go [] cs) + else go (c ∷ acc) cs wordsByᵇ : (A → Bool) → List A → List (List A) wordsByᵇ p = wordsBy (T? ∘ p) From 6082bb61fd0631bcc25cec39e458033bc9e9f735 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Apr 2024 05:46:17 +0100 Subject: [PATCH 2/3] layout --- src/Data/List/Base.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 9343f4ebf4..b10887829e 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -428,10 +428,11 @@ 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) = let acc′ = Maybe.fromMaybe [] acc in + go acc (c ∷ cs) = + let acc′ = Maybe.fromMaybe [] acc in if does (P? c) - then reverse acc′ ∷ go nothing cs - else go (just (c ∷ acc′)) cs + then reverse acc′ ∷ go nothing cs + else go (just (c ∷ acc′)) cs linesByᵇ : (A → Bool) → List A → List (List A) linesByᵇ p = linesBy (T? ∘ p) From 5b6dc88f23811b47fb55467c7f2b8058278faf6d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 8 May 2024 10:44:55 +0100 Subject: [PATCH 3/3] `let` into `where` --- src/Data/List/Base.agda | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index b10887829e..992bc8084e 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -428,11 +428,10 @@ 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) = - let acc′ = Maybe.fromMaybe [] acc in - if does (P? c) - then reverse acc′ ∷ go nothing cs - else go (just (c ∷ acc′)) cs + 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 linesByᵇ : (A → Bool) → List A → List (List A) linesByᵇ p = linesBy (T? ∘ p)