From 11e306383d10f59db1b925a85b9c4c610a98b23b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Piotr=20Paradzi=C5=84ski?= Date: Wed, 22 Nov 2023 00:22:46 +0100 Subject: [PATCH 1/5] add map to Data.String --- src/Data/String/Base.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda index d583da042c..ee2a79b6d6 100644 --- a/src/Data/String/Base.agda +++ b/src/Data/String/Base.agda @@ -185,3 +185,6 @@ lines = linesByᵇ ('\n' Char.≈ᵇ_) -- `lines` preserves empty lines _ : lines "\nabc\n\nb\n\n\n" ≡ "" ∷ "abc" ∷ "" ∷ "b" ∷ "" ∷ "" ∷ [] _ = refl + +map : (Char → Char) → String → String +map f = fromList ∘ List.map f ∘ toList From ab4a31c43cbf058cff922b42be2419ccd62d1925 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Piotr=20Paradzi=C5=84ski?= Date: Wed, 22 Nov 2023 00:58:46 +0100 Subject: [PATCH 2/5] Add test for Data.String map --- src/Data/String/Base.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda index ee2a79b6d6..fb0ebc1526 100644 --- a/src/Data/String/Base.agda +++ b/src/Data/String/Base.agda @@ -188,3 +188,6 @@ _ = refl map : (Char → Char) → String → String map f = fromList ∘ List.map f ∘ toList + +_ : map Char.toUpper "abc" ≡ "ABC" +_ = refl From d1e303e3f637b0b94a4d3343e2ff43df290647bd Mon Sep 17 00:00:00 2001 From: lemastero Date: Fri, 24 Nov 2023 14:08:09 +0100 Subject: [PATCH 3/5] CHANGELOG.md add map to list of new functions in Data.String.Base --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0e50316b36..36d2f83d20 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3117,6 +3117,7 @@ Additions to existing modules ```agda wordsByᵇ : (Char → Bool) → String → List String linesByᵇ : (Char → Bool) → String → List String + map : (Char → Char) → String → String ``` * Added new proofs in `Data.String.Properties`: From 704ef159442d4c4530aa11f6696d789ec10a7b31 Mon Sep 17 00:00:00 2001 From: lemastero Date: Sat, 25 Nov 2023 11:28:52 +0100 Subject: [PATCH 4/5] precise import of Data.String to avoid conflict on map --- src/Text/Printf/Generic.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Text/Printf/Generic.agda b/src/Text/Printf/Generic.agda index 07c8856443..21aa36133a 100644 --- a/src/Text/Printf/Generic.agda +++ b/src/Text/Printf/Generic.agda @@ -15,7 +15,7 @@ open import Data.Maybe.Base hiding (map) open import Data.Nat.Base using (ℕ) open import Data.Product.Base hiding (map) open import Data.Product.Nary.NonDependent -open import Data.String.Base +open import Data.String.Base using (String) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Unit.Base using (⊤) open import Function.Nary.NonDependent From 4d6d0bfcc951fa6b2dacfc4b684086cf3f0e5b7a Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Wed, 27 Dec 2023 11:37:13 +0800 Subject: [PATCH 5/5] Fix import statements --- src/Data/Tree/Rose/Show.agda | 2 +- src/IO.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Tree/Rose/Show.agda b/src/Data/Tree/Rose/Show.agda index 5b293aeb70..1aa0509aae 100644 --- a/src/Data/Tree/Rose/Show.agda +++ b/src/Data/Tree/Rose/Show.agda @@ -15,7 +15,7 @@ open import Data.DifferenceList as DList renaming (DiffList to DList) using () open import Data.List.Base as List using (List; []; [_]; _∷_; _∷ʳ_) open import Data.Nat.Base using (ℕ; _∸_) open import Data.Product.Base using (_×_; _,_) -open import Data.String.Base hiding (show) +open import Data.String.Base using (String; _++_) open import Data.Tree.Rose using (Rose; node; map; fromBinary) open import Function.Base using (flip; _∘′_; id) diff --git a/src/IO.agda b/src/IO.agda index eebb5d7d92..96f7db2760 100644 --- a/src/IO.agda +++ b/src/IO.agda @@ -11,7 +11,7 @@ module IO where open import Codata.Musical.Notation open import Codata.Musical.Costring open import Data.Unit.Polymorphic.Base -open import Data.String.Base +open import Data.String.Base using (String) import Data.Unit.Base as Unit0 open import Function.Base using (_∘_; flip) import IO.Primitive as Prim