git.iko.soy/Idris-dev
on master help sign in
make lines and unlines agree with Haskell
e1d1ed8zjhmale
libs/prelude/Prelude/Strings.idr+6−7
compare with master
unifiedsplit
@@ -247,10 +247,11 @@ words s = map pack $ words' $ unpack s
247||| lines' (unpack "\rA BC\nD\r\nE\n")
247||| lines' (unpack "\rA BC\nD\r\nE\n")
248||| ```
248||| ```
249lines' : List Char -> List (List Char)
249lines' : List Char -> List (List Char)
250+lines' [] = []
250−lines' s = case dropWhile isNL s of
251+lines' s = case break isNL s of
251− [] => []
252+ (l, s') => l :: case s' of
252− s' => let (w, s'') = break isNL s'
253+ [] => []
253− in w :: lines' (assert_smaller s s'')
254+ _ :: s'' => lines' (assert_smaller s s'')
254
255
255||| Splits a string into a list of newline separated strings.
256||| Splits a string into a list of newline separated strings.
256|||
257|||
@@ -286,9 +287,7 @@ unwords = pack . unwords' . map unpack
286||| ```
287||| ```
287unlines' : List (List Char) -> List Char
288unlines' : List (List Char) -> List Char
288unlines' [] = []
289unlines' [] = []
289−unlines' ls = assert_total (foldr1 addLine ls) where
290+unlines' (l::ls) = l ++ '\n' :: unlines' ls
290− addLine : List Char -> List Char -> List Char
291− addLine l s = l ++ ('\n' :: s)
292
291
293||| Joins the strings by newlines into a single string.
292||| Joins the strings by newlines into a single string.
294|||
293|||
test/prelude001/prelude001.idr+6−9
@@ -3,15 +3,12 @@ module Main
3main : IO ()
3main : IO ()
4main = do
4main = do
5 printLn $ lines "" == []
5 printLn $ lines "" == []
6− -- `lines` seems to ignore too many trailing newlines.
7− printLn $ lines "\n" == [] -- FIXME: Should be [""].
6+ printLn $ lines "\n" == [""]
8− printLn $ lines "\n\n" == [] -- FIXME: Should be ["", ""].
7+ printLn $ lines "\n\n" == ["", ""]
9− printLn $ lines "\n\n\n" == [] -- FIXME: Should be ["", "", ""].
8+ printLn $ lines "\n\n\n" == ["", "", ""]
10 printLn $ lines "1\n2\n3" == ["1", "2", "3"]
9 printLn $ lines "1\n2\n3" == ["1", "2", "3"]
11 printLn $ lines "1\n2\n3\n" == ["1", "2", "3"]
10 printLn $ lines "1\n2\n3\n" == ["1", "2", "3"]
12 printLn $ unlines [] == ""
11 printLn $ unlines [] == ""
13− -- `unlines` works as advertised doesn't follow Haskell here.
14− -- When files are written using unlines, vim complains of "noeoln".
15− printLn $ unlines ["1"] == "1" -- FIXME: Should be "1\n"
12+ printLn $ unlines ["1"] == "1\n"
16− printLn $ unlines ["1", "2"] == "1\n2" -- FIXME: Should be "1\n2\n"
13+ printLn $ unlines ["1", "2"] == "1\n2\n"
17− printLn $ unlines ["1", "2", "3"] == "1\n2\n3" -- FIXME: Should be "1\n2\n3\n"
14+ printLn $ unlines ["1", "2", "3"] == "1\n2\n3\n"