From 07ea94768a676454990c57112ea7062b1dcd138b Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Fri, 7 Jul 2023 17:17:22 -0400
Subject: [PATCH 1/2] simplifiedd `String` import in stdl

In `src.Text.Tabular.Vec` and `src.Relection.AST.Show`
still need to import `Data.String` to use `rectangle` and `parensIfSpace`
---
 README/Data/List/Relation/Binary/Subset.agda | 3 ++-
 README/Data/Tree/AVL.agda                    | 2 +-
 README/Data/Trie/NonDependent.agda           | 3 ++-
 README/Function/Reasoning.agda               | 3 ++-
 README/IO.agda                               | 2 +-
 src/Data/Rational.agda                       | 2 +-
 src/Reflection/AST/Abstraction.agda          | 3 ++-
 src/Reflection/AST/Literal.agda              | 2 +-
 src/Reflection/AST/Show.agda                 | 4 ++--
 src/Reflection/AST/Term.agda                 | 3 ++-
 src/Reflection/AST/Traversal.agda            | 2 +-
 src/Test/Golden.agda                         | 3 ++-
 src/Text/Tabular/List.agda                   | 2 +-
 src/Text/Tabular/Vec.agda                    | 3 ++-
 14 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/README/Data/List/Relation/Binary/Subset.agda b/README/Data/List/Relation/Binary/Subset.agda
index f6ef7690a1..ccef725cca 100644
--- a/README/Data/List/Relation/Binary/Subset.agda
+++ b/README/Data/List/Relation/Binary/Subset.agda
@@ -21,7 +21,8 @@ module README.Data.List.Relation.Binary.Subset where
 -- tell Agda which equality relation to use.
 
 -- Decidable equality over Strings
-open import Data.String using (String; _≟_)
+open import Data.String.Base using (String)
+open import Data.String.Properties using (_≟_)
 
 -- Open the decidable membership module using Decidable ≡ over Strings
 open import Data.List.Membership.DecPropositional _≟_
diff --git a/README/Data/Tree/AVL.agda b/README/Data/Tree/AVL.agda
index 7994afed41..abba7bfd0b 100644
--- a/README/Data/Tree/AVL.agda
+++ b/README/Data/Tree/AVL.agda
@@ -21,7 +21,7 @@ import Data.Tree.AVL
 
 open import Data.Nat.Properties using (<-strictTotalOrder)
 open import Data.Product as Prod using (_,_; _,′_)
-open import Data.String using (String)
+open import Data.String.Base using (String)
 open import Data.Vec using (Vec; _∷_; [])
 open import Relation.Binary.PropositionalEquality
 
diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda
index 2387a71242..7bdcaa4a39 100644
--- a/README/Data/Trie/NonDependent.agda
+++ b/README/Data/Trie/NonDependent.agda
@@ -57,7 +57,8 @@ open import Data.List.Base   as List using (List; []; _∷_)
 open import Data.List.Fresh  as List# using (List#; []; _∷#_)
 open import Data.Maybe       as Maybe
 open import Data.Product     as Prod
-open import Data.String      as String using (String)
+open import Data.String.Base as String using (String)
+open import Data.String.Properties as String using (_≟_)
 open import Data.These       as These
 
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
diff --git a/README/Function/Reasoning.agda b/README/Function/Reasoning.agda
index 0c9afa4532..548abdb724 100644
--- a/README/Function/Reasoning.agda
+++ b/README/Function/Reasoning.agda
@@ -35,7 +35,8 @@ module _ {A B C : Set} {A→B : A → B} {B→C : B → C} where
 open import Data.Nat
 open import Data.List.Base
 open import Data.Char.Base
-open import Data.String as String using (String; toList; fromList; _==_)
+open import Data.String.Base as String using (String; toList; fromList)
+open import Data.String.Properties as String using (_==_)
 open import Function
 open import Data.Bool hiding (_≤?_)
 open import Data.Product as P using (_×_; <_,_>; uncurry; proj₁)
diff --git a/README/IO.agda b/README/IO.agda
index 880ad1fa32..37553edd1d 100644
--- a/README/IO.agda
+++ b/README/IO.agda
@@ -11,7 +11,7 @@ module README.IO where
 open import Level
 open import Data.Nat.Base
 open import Data.Nat.Show using (show)
-open import Data.String using (String; _++_; lines)
+open import Data.String.Base using (String; _++_; lines)
 open import Data.Unit.Polymorphic
 open import IO
 
diff --git a/src/Data/Rational.agda b/src/Data/Rational.agda
index 260aa44951..2345466dcb 100644
--- a/src/Data/Rational.agda
+++ b/src/Data/Rational.agda
@@ -26,7 +26,7 @@ open import Data.Rational.Properties public
 -- Version 1.5
 
 import Data.Integer.Show as ℤ
-open import Data.String using (String; _++_)
+open import Data.String.Base using (String; _++_)
 
 show : ℚ → String
 show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)
diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda
index 793c729aec..8ccffa3a7a 100644
--- a/src/Reflection/AST/Abstraction.agda
+++ b/src/Reflection/AST/Abstraction.agda
@@ -9,7 +9,8 @@
 module Reflection.AST.Abstraction where
 
 open import Data.Product                               using (_×_; <_,_>; uncurry)
-open import Data.String as String                      using (String)
+open import Data.String.Base as String                 using (String)
+open import Data.String.Properties as String           using (_≟_)
 open import Level
 open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
 open import Relation.Binary                            using (DecidableEquality)
diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda
index ff8835236a..f400c9f1dc 100644
--- a/src/Reflection/AST/Literal.agda
+++ b/src/Reflection/AST/Literal.agda
@@ -12,7 +12,7 @@ open import Data.Bool.Base   using (Bool; true; false)
 import Data.Char as Char     using (_≟_)
 import Data.Float as Float   using (_≟_)
 import Data.Nat as ℕ        using (_≟_)
-import Data.String as String using (_≟_)
+import Data.String.Properties as String using (_≟_)
 import Data.Word as Word     using (_≟_)
 import Reflection.AST.Meta as Meta
 import Reflection.AST.Name as Name
diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda
index f0291cf447..cbdeb04e61 100644
--- a/src/Reflection/AST/Show.agda
+++ b/src/Reflection/AST/Show.agda
@@ -16,8 +16,8 @@ import Data.Float as Float using (show)
 open import Data.List.Base hiding (_++_; intersperse)
 import Data.Nat.Show as ℕ using (show)
 open import Data.Product   using (_×_; _,_)
-open import Data.String as String
-  using (String; _++_; intersperse; braces; parens; parensIfSpace; _<+>_)
+open import Data.String.Base as String using (String; _++_; intersperse; braces; parens; _<+>_)
+open import Data.String as String using (parensIfSpace)
 import Data.Word as Word   using (toℕ)
 open import Function.Base using (id; _∘′_; case_of_)
 open import Relation.Nullary.Decidable using (yes; no)
diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda
index cfa7e70cb1..a9b9da1d17 100644
--- a/src/Reflection/AST/Term.agda
+++ b/src/Reflection/AST/Term.agda
@@ -14,7 +14,8 @@ open import Data.Nat as ℕ          using (ℕ; zero; suc)
 open import Data.Product            using (_×_; _,_; <_,_>; uncurry; map₁)
 open import Data.Product.Properties using (,-injective)
 open import Data.Maybe.Base         using (Maybe; just; nothing)
-open import Data.String as String   using (String)
+open import Data.String.Base    using (String)
+open import Data.String.Properties as String hiding (_≟_)
 open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
 open import Relation.Binary                            using (Decidable; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda
index c311567c7f..04a40e1faa 100644
--- a/src/Reflection/AST/Traversal.agda
+++ b/src/Reflection/AST/Traversal.agda
@@ -14,7 +14,7 @@ module Reflection.AST.Traversal
 open import Data.Nat          using (ℕ; zero; suc; _+_)
 open import Data.List.Base    using (List; []; _∷_; _++_; reverse; length)
 open import Data.Product      using (_×_; _,_)
-open import Data.String       using (String)
+open import Data.String.Base  using (String)
 open import Function.Base     using (_∘_)
 open import Reflection        hiding (pure)
 
diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda
index 81f9f2af1a..53086e9281 100644
--- a/src/Test/Golden.agda
+++ b/src/Test/Golden.agda
@@ -90,7 +90,8 @@ open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
 import Data.Nat.Show as ℕ
 open import Data.Product using (_×_; _,_)
-open import Data.String as String using (String; lines; unlines; unwords; concat; _≟_)
+open import Data.String.Base as String using (String; lines; unlines; unwords; concat)
+open import Data.String.Properties as String using (_≟_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Unit.Base using (⊤)
 
diff --git a/src/Text/Tabular/List.agda b/src/Text/Tabular/List.agda
index dd06ea809a..4490cb01a1 100644
--- a/src/Text/Tabular/List.agda
+++ b/src/Text/Tabular/List.agda
@@ -8,7 +8,7 @@
 
 module Text.Tabular.List where
 
-open import Data.String using (String)
+open import Data.String.Base using (String)
 open import Data.List.Base
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (-,_; proj₂)
diff --git a/src/Text/Tabular/Vec.agda b/src/Text/Tabular/Vec.agda
index 74f899905c..65ed3f6006 100644
--- a/src/Text/Tabular/Vec.agda
+++ b/src/Text/Tabular/Vec.agda
@@ -10,7 +10,8 @@ module Text.Tabular.Vec where
 
 open import Data.List.Base using (List)
 open import Data.Product as Prod using (uncurry)
-open import Data.String using (String; rectangle; fromAlignment)
+open import Data.String.Base using (String; fromAlignment)
+open import Data.String using (rectangle)
 open import Data.Vec.Base
 open import Function.Base
 

From 765199288b1ddac75293df26aae0248d0fcba349 Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Fri, 14 Jul 2023 15:10:06 -0400
Subject: [PATCH 2/2] rectification on import Data.String

---
 src/Text/Tabular/Vec.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Text/Tabular/Vec.agda b/src/Text/Tabular/Vec.agda
index 65ed3f6006..74f899905c 100644
--- a/src/Text/Tabular/Vec.agda
+++ b/src/Text/Tabular/Vec.agda
@@ -10,8 +10,7 @@ module Text.Tabular.Vec where
 
 open import Data.List.Base using (List)
 open import Data.Product as Prod using (uncurry)
-open import Data.String.Base using (String; fromAlignment)
-open import Data.String using (rectangle)
+open import Data.String using (String; rectangle; fromAlignment)
 open import Data.Vec.Base
 open import Function.Base