Add map to Data.String.Base (#2208)

* add map to Data.String * Add test for Data.String map * CHANGELOG.md add map to list of new functions in Data.String.Base * precise import of Data.String to avoid conflict on map * Fix import statements --------- Co-authored-by: lemastero <[email protected]> Co-authored-by: MatthewDaggitt <[email protected]>
agda · Dec 27, 2023 · 660d983 · 660d983
1 parent 54cea92
commit 660d983
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 3 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -80,3 +80,8 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
+
+* Added new functions in `Data.String.Base`:
+  ```agda
+  map : (Char → Char) → String → String
+  ```
diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda
@@ -185,3 +185,9 @@ 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
+
+_ : map Char.toUpper "abc" ≡ "ABC"
+_ = refl
diff --git 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
@@ -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

diff --git 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