Refactor string functions, rewrite tests

libs/base/Data/String.idr

@@ -38,6 +38,19 @@ partial
 foldl1 : (a -> a -> a) -> List a -> a
 foldl1 f (x::xs) = foldl f x xs
 
+||| Remove the first `n` characters from a string. Returns the empty string if
+||| the input string is too short.
+public export
+drop : (n : Nat) -> (input : String) -> String
+drop n str = substr n (length str) str
+
+||| Concatenate the strings from a `Foldable` containing strings, separated by
+||| the given string.
+public export
+join : (sep : String) -> Foldable t => (xs : t String) -> String
+join sep xs = drop (length sep)
+                   (foldl (\acc, x => acc ++ sep ++ x) "" xs)
+
 -- This uses fastConcat internally so it won't compute at compile time.
 export
 fastUnlines : List String -> String
@@ -86,7 +99,7 @@ unwords' ws = assert_total (foldr1 addSpace ws) where
 ||| ```
 export
 unwords : List String -> String
-unwords = pack . unwords' . map unpack
+unwords = join " "
 
 ||| Splits a character list into a list of newline separated character lists.
 |||
@@ -132,7 +145,8 @@ unlines' (l::ls) = l ++ '\n' :: unlines' ls
 ||| ```
 export
 unlines : List String -> String
-unlines = pack . unlines' . map unpack
+unlines [] = ""
+unlines (x::xs) = x ++ "\n" ++ unlines xs
 
 %transform "fastUnlines" unlines = fastUnlines
 

libs/contrib/Data/String/Extra.idr

@@ -63,19 +63,19 @@ drop n str = substr n (length str) str
 ||| the input string is too short.
 public export
 dropLast : (n : Nat) -> (input : String) -> String
-dropLast n str = reverse (drop n (reverse str))
+dropLast n str = reverse (Libraries.Data.String.Extra.drop n (reverse str))
 
 ||| Remove the first and last `n` characters from a string. Returns the empty
 ||| string if the input string is too short.
 public export
 shrink : (n : Nat) -> (input : String) -> String
-shrink n str = dropLast n (drop n str)
+shrink n str = dropLast n (Libraries.Data.String.Extra.drop n str)
 
 ||| Concatenate the strings from a `Foldable` containing strings, separated by
 ||| the given string.
 public export
 join : (sep : String) -> Foldable t => (xs : t String) -> String
-join sep xs = drop (length sep)
+join sep xs = Libraries.Data.String.Extra.drop (length sep)
                    (foldl (\acc, x => acc ++ sep ++ x) "" xs)
 
 ||| Get a character from a string if the string is long enough.

src/Idris/Syntax.idr

@@ -770,8 +770,8 @@ parameters {0 nm : Type} (toName : nm -> Name)
   showPTermPrec d (PSectionR _ _ x op) = "(" ++ showPTermPrec d x ++ " " ++ showOpPrec d op ++ ")"
   showPTermPrec d (PEq fc l r) = showPTermPrec d l ++ " = " ++ showPTermPrec d r
   showPTermPrec d (PBracketed _ tm) = "(" ++ showPTermPrec d tm ++ ")"
-  showPTermPrec d (PString _ xs) = join " ++ " $ showPStr <$> xs
-  showPTermPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> concat xs) ++ ")"
+  showPTermPrec d (PString _ xs) = Libraries.Data.String.Extra.join " ++ " $ showPStr <$> xs
+  showPTermPrec d (PMultiline _ indent xs) = "multiline (" ++ (Libraries.Data.String.Extra.join " ++ " $ showPStr <$> concat xs) ++ ")"
   showPTermPrec d (PDoBlock _ ns ds)
         = "do " ++ showSep " ; " (map showDo ds)
   showPTermPrec d (PBang _ tm) = "!" ++ showPTermPrec d tm

src/Libraries/Utils/Path.idr

@@ -123,7 +123,7 @@ Show Path where
       sep = String.singleton dirSeparator
       showVol = maybe "" show path.volume
       showRoot = if path.hasRoot then sep else ""
-      showBody = join sep $ map show path.body
+      showBody = Libraries.Data.String.Extra.join sep $ map show path.body
       showTrail = if path.hasTrailSep then sep else ""
     in
       showVol ++ showRoot ++ showBody ++ showTrail

tests/Data/String/Test.idr

@@ -0,0 +1,19 @@
+module Data.String.Test
+
+import Data.String
+
+append_helper : (a : String) -> a = "" ++ a
+append_helper = believe_me ()
+
+unlines_is_distributive : (a, b : List String) -> unlines (a ++ b) = unlines a ++ unlines b
+unlines_is_distributive [] [] = Refl
+unlines_is_distributive [] a = append_helper (unlines a)
+unlines_is_distributive (x::xs) b = cong ((x++"")++) (unlines_is_distributive xs b)
+
+main : IO ()
+main = do printLn ("<" ++ (unlines []) ++ ">")
+          printLn ("<" ++ (unlines ["ab"]) ++ ">")
+          printLn ("<" ++ (unlines ["a", "b"]) ++ ">")
+          printLn ("<" ++ (fastUnlines []) ++ ">")
+          printLn ("<" ++ (fastUnlines ["ab"]) ++ ">")
+          printLn ("<" ++ (fastUnlines ["a", "b"]) ++ ">")

tests/Main.idr

@@ -311,6 +311,9 @@ templateTests = testsInDir "templates" (const True) "Test templates" [] Nothing
 baseLibraryTests : IO TestPool
 baseLibraryTests = testsInDir "base" (const True) "Base library" [Chez, Node] Nothing
 
+dataTests : IO TestPool
+dataTests = testsInDir "Data" (const True) "Data Structures" [] Nothing
+
 -- same behavior as `baseLibraryTests`
 contribLibraryTests : IO TestPool
 contribLibraryTests = testsInDir "contrib" (const True) "Contrib library" [Chez, Node] Nothing
@@ -341,6 +344,7 @@ main = runner $
   , !typeddTests
   , !ideModeTests
   , !preludeTests
+  , !dataTests
   , !baseLibraryTests
   , !contribLibraryTests
   , testPaths "chez" chezTests