Change semantics of lines and unlines function to match Haskell and other languages (#1585)

* Add trailing newline on non-empty list in unlines

There are several reasons to do that:
* a line in a text file is something which ends with newline,
  and the last line is not special
* `unlines []` should be different from `unlines [""]`
* `unlines (a ++ b) = unlines a ++ unlines b`
* Haskell does it

* Change lines function behaviour

Author: stepancheg

libs/base/Data/String.idr

@@ -41,7 +41,10 @@ foldl1 f (x::xs) = foldl f x xs
 -- This uses fastConcat internally so it won't compute at compile time.
 export
 fastUnlines : List String -> String
-fastUnlines = fastConcat . intersperse "\n"
+fastUnlines = fastConcat . unlines'
+  where unlines' : List String -> List String
+        unlines' [] = []
+        unlines' (x :: xs) = x :: "\n" :: unlines' xs
 
 -- This is a deprecated alias for fastConcat for backwards compatibility
 -- (unfortunately, we don't have %deprecated yet).
@@ -97,34 +100,38 @@ unwords = pack . unwords' . map unpack
 ||| lines' (unpack "\rA BC\nD\r\nE\n")
 ||| ```
 export
-lines' : List Char -> List1 (List Char)
-lines' [] = singleton []
-lines' s  = case break isNL s of
-                 (l, s') => l ::: case s' of
-                                       [] => []
-                                       _ :: s'' => forget $ lines' (assert_smaller s s'')
+lines' : List Char -> List (List Char)
+lines' s = linesHelp [] s
+  where linesHelp : List Char -> List Char -> List (List Char)
+        linesHelp [] [] = []
+        linesHelp acc [] = [reverse acc]
+        linesHelp acc ('\n' :: xs) = reverse acc :: linesHelp [] xs
+        linesHelp acc ('\r' :: '\n' :: xs) = reverse acc :: linesHelp [] xs
+        linesHelp acc ('\r' :: xs) = reverse acc :: linesHelp [] xs
+        linesHelp acc (c :: xs) = linesHelp (c :: acc) xs
+
 
 ||| Splits a string into a list of newline separated strings.
 |||
 ||| ```idris example
 ||| lines  "\rA BC\nD\r\nE\n"
 ||| ```
 export
-lines : String -> List1 String
+lines : String -> List String
 lines s = map pack (lines' (unpack s))
 
-||| Joins the character lists by newlines into a single character list.
+||| 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']]
 ||| ```
 export
 unlines' : List (List Char) -> List Char
 unlines' [] = []
-unlines' [l] = l
 unlines' (l::ls) = l ++ '\n' :: unlines' ls
 
-||| Joins the strings by newlines into a single string.
+||| Joins the strings into a single string by appending a newline to each string.
 |||
 ||| ```idris example
 ||| unlines ["line", "line2", "ln3", "D"]

libs/contrib/Data/String/Extra.idr

@@ -92,7 +92,7 @@ index n str with (unpack str)
 ||| Indent each line of a given string by `n` spaces.
 public export
 indentLines : (n : Nat) -> String -> String
-indentLines n str = unlines $ map (indent n) $ forget $ lines str
+indentLines n str = unlines $ map (indent n) $ lines str
 
 ||| Return a string of the given character repeated
 ||| `n` times.

libs/contrib/System/Console/GetOpt.idr

@@ -97,8 +97,12 @@ fmtOpt : OptDescr a -> List (String,String,String)
 fmtOpt (MkOpt sos los ad descr) =
   let sosFmt = concat $ intersperse ", " (map (fmtShort ad) sos)
       losFmt = concat $ intersperse ", " (map (fmtLong ad) los)
-      (h ::: t) = lines descr in
+      (h ::: t) = lines1 descr in
       (sosFmt,losFmt,h) :: map (\s => ("","",s)) t
+  where lines1 : String -> List1 String
+        lines1 s = case lines s of
+                        [] => "" ::: []
+                        (x :: xs) => x ::: xs
 
 ||| Return a string describing the usage of a command, derived from
 ||| the header (first argument) and the options described by the

libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr

@@ -360,7 +360,7 @@ interface Pretty a where
 export
 Pretty String where
   pretty str = let str' = if "\n" `isSuffixOf` str then dropLast 1 str else str in
-                   vsep $ map unsafeTextWithoutNewLines $ forget $ lines str'
+                   vsep $ map unsafeTextWithoutNewLines $ lines str'
 
 public export
 FromString (Doc ann) where

libs/test/Test/Golden.idr

@@ -178,7 +178,7 @@ options args = case args of
                  | Nothing => pure (Just opts)
            Right only <- readFile fp
              | Left err => fail (show err)
-           pure $ Just $ record { onlyNames $= (forget (lines only) ++) } opts
+           pure $ Just $ record { onlyNames $= ((lines only) ++) } opts
 
 ||| Normalise strings between different OS.
 |||
@@ -235,7 +235,7 @@ runTest opts testPath = forkIO $ do
         (if opts.color then show . colored BrightRed else id) "FAILURE"
       if interactive opts
         then mayOverwrite (Just exp) out
-        else putStrLn . unlines $ expVsOut exp out
+        else putStr . unlines $ expVsOut exp out
 
   pure $ if result then Right testPath else Left testPath
 
@@ -266,7 +266,7 @@ runTest opts testPath = forkIO $ do
           code <- system $ "git diff --no-index --exit-code " ++
             (if opts.color then  "--word-diff=color " else "") ++
             testPath ++ "/expected " ++ testPath ++ "/output"
-          putStrLn . unlines $
+          putStr . unlines $
             ["Golden value differs from actual value."] ++
             (if (code < 0) then expVsOut exp out else []) ++
             ["Accept actual value as new golden value? [y/N]"]
@@ -454,7 +454,7 @@ poolRunner opts pool
     banner msgs = fastUnlines
         $ [ "", separator, pool.poolName ]
        ++ msgs
-       ++ [ separator, "" ]
+       ++ [ separator ]
 
     loop : Options -> Summary -> List String -> IO Summary
     loop opts acc [] = pure acc
@@ -489,7 +489,7 @@ runner tests
          let list = fastUnlines res.failure
          when (nfail > 0) $
            do putStrLn "Failing tests:"
-              putStrLn list
+              putStr list
          -- always overwrite the failure file, if it is given
          whenJust opts.failureFile $ \ path =>
            do Right _ <- writeFile path list

src/TTImp/Elab/Ambiguity.idr

@@ -368,7 +368,7 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected
                   logGlueNF "elab.ambiguous" 5 (fastConcat
                     [ "Ambiguous elaboration at ", show fc, ":\n"
                     , unlines (map show alts)
-                    , "\nWith default. Target type "
+                    , "With default. Target type "
                     ]) env exp'
                   alts' <- pruneByType env !(getNF exp') alts
                   log "elab.prune" 5 $
@@ -426,7 +426,7 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected
                               , " (", if delayed then "" else "not ", "delayed)"
                               , " at ", show fc, ":\n"
                               , unlines (map show alts')
-                              , "\nTarget type "
+                              , "Target type "
                               ]) env exp'
                           let tryall = case uniq of
                                             FirstSuccess => anyOne fc

tests/Main.idr

@@ -296,6 +296,8 @@ baseLibraryTests = MkTestPool "Base library" [Chez, Node] Nothing
   , "system_info_os001"
   , "system_system"
   , "data_bits001"
+  , "data_string_lines001"
+  , "data_string_unlines001"
   , "system_errno"
   , "system_info001"
   , "system_signal001", "system_signal002", "system_signal003", "system_signal004"

tests/base/data_string_lines001/Lines.idr

@@ -0,0 +1,11 @@
+import Data.String
+
+main : IO ()
+main = do printLn (lines "")
+          printLn (lines "ab")
+          printLn (lines "ab\n")
+          printLn (lines "ab\ncd")
+          printLn (lines "ab\ncd\n")
+          printLn (lines "a\rb")
+          printLn (lines "a\r\nb")
+          printLn (lines "\n\r\n\n")

tests/base/data_string_lines001/expected

@@ -0,0 +1,10 @@
+1/1: Building Lines (Lines.idr)
+Main> []
+["ab"]
+["ab"]
+["ab", "cd"]
+["ab", "cd"]
+["a", "b"]
+["a", "b"]
+["", "", ""]
+Main> Bye for now!

tests/base/data_string_lines001/input

@@ -0,0 +1,2 @@
+:exec main
+:q