From fd02bf8b3e08f440f375e738c1e533bbdf485fb7 Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Mar 2022 18:34:06 +0000
Subject: [PATCH] [ fix #2303 ] remove quadratic unwords (#2345)

---
 libs/base/Data/List.idr   | 14 ++++++++++++--
 libs/base/Data/String.idr | 37 +++++++++++--------------------------
 2 files changed, 23 insertions(+), 28 deletions(-)

diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index cc171099e..24dfd516a 100644
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@@ -632,6 +632,16 @@ toList1' : (l : List a) -> Maybe (List1 a)
 toList1' [] = Nothing
 toList1' (x :: xs) = Just (x ::: xs)
 
+||| Interleave two lists.
+||| ```idris example
+||| > interleave ["a", "c", "e"]  ["b", "d", "f"]
+||| ["a", "b", "c", "d", "e", "f"]
+||| ```
+public export
+interleave : (xs, ys : List a) -> List a
+interleave [] ys = ys
+interleave (x :: xs) ys = x :: interleave ys xs
+
 ||| Prefix every element in the list with the given element.
 |||
 ||| @ sep the value to prefix
@@ -641,7 +651,7 @@ toList1' (x :: xs) = Just (x ::: xs)
 ||| > with List (mergeReplicate '>' ['a', 'b', 'c', 'd', 'e'])
 ||| ['>', 'a', '>', 'b', '>', 'c', '>', 'd', '>', 'e']
 ||| ```
-export
+public export
 mergeReplicate : (sep : a) -> (xs : List a) -> List a
 mergeReplicate sep []      = []
 mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys
@@ -655,7 +665,7 @@ mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys
 ||| > with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
 ||| ['a', ',', 'b', ',', 'c', ',', 'd', ',', 'e']
 ||| ```
-export
+public export
 intersperse : (sep : a) -> (xs : List a) -> List a
 intersperse sep []      = []
 intersperse sep (x::xs) = x :: mergeReplicate sep xs
diff --git a/libs/base/Data/String.idr b/libs/base/Data/String.idr
index c15ebbf9e..04bdb1200 100644
--- a/libs/base/Data/String.idr
+++ b/libs/base/Data/String.idr
@@ -67,26 +67,22 @@ words s = map pack (words' (unpack s) [<] [<])
          else words' cs (sc :< c) css
     words' [] sc css = wordsHelper sc css <>> Nil
 
+||| Joins the strings using the provided separator
+||| ```idris example
+||| joinBy ", " ["A", "BC", "D"] === "A, BC, D"
+||| ```
+public export
+joinBy : String -> List String -> String
+joinBy sep ws = concat (intersperse sep ws)
+
 ||| Joins the strings by spaces into a single string.
 |||
 ||| ```idris example
-||| unwords ["A", "BC", "D", "E"]
+||| unwords ["A", "BC", "D", "E"] === "A BC D E"
 ||| ```
 public export
 unwords : List String -> String
-unwords = pack . unwords' . map unpack
-  where
-    addSpace : List Char -> List Char -> List Char
-    addSpace w s = w ++ (' ' :: s)
-
-    ||| Joins the character lists by spaces into a single character list.
-    |||
-    ||| ```idris example
-    ||| unwords' [['A'], ['B', 'C'], ['D'], ['E']]
-    ||| ```
-    unwords' : List (List Char) -> List Char
-    unwords' [] = []
-    unwords' (ws :: wss) = foldl addSpace ws wss
+unwords = joinBy " "
 
 ||| Splits a character list into a list of newline separated character lists.
 |||
@@ -122,17 +118,6 @@ public export
 lines : String -> List String
 lines s = map pack (lines' (unpack s))
 
-||| Joins the character lists by a single character list by appending a newline
-||| to each line.
-|||
-||| ```idris example
-||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]
-||| ```
-public export
-unlines' : List (List Char) -> List Char
-unlines' [] = []
-unlines' (l::ls) = l ++ '\n' :: unlines' ls
-
 ||| Joins the strings into a single string by appending a newline to each string.
 |||
 ||| ```idris example
@@ -140,7 +125,7 @@ unlines' (l::ls) = l ++ '\n' :: unlines' ls
 ||| ```
 public export
 unlines : List String -> String
-unlines = pack . unlines' . map unpack
+unlines ls = concat (interleave ls ("\n" <$ ls))
 
 %transform "fastUnlines" unlines = fastUnlines