git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3322 from zjhmale/fix-lines-unlines

make lines and unlines agree with Haskell

commitedb5d93d3c479b80f4fb9c33b18bfd27e223efdc authorNiklas Larsson <metaniklas@gmail.com> dateFri 5 Aug 2016, 21:20 (10 years ago) parent6e4a5e5e1d1ed8
2 files changed+12−16
compare with master
unifiedsplit
libs/prelude/Prelude/Strings.idr+6−7 test/prelude001/prelude001.idr+6−9
libs/prelude/Prelude/Strings.idr+6−7
@@ -247,10 +247,11 @@ words s = map pack $ words' $ unpack s
247247||| lines' (unpack "\rA BC\nD\r\nE\n")
248248||| ```
249249lines' : List Char -> List (List Char)
250−lines' s = case dropWhile isNL s of
251− [] => []
252− s' => let (w, s'') = break isNL s'
253− in w :: lines' (assert_smaller s s'')
250+lines' [] = []
251+lines' s = case break isNL s of
252+ (l, s') => l :: case s' of
253+ [] => []
254+ _ :: s'' => lines' (assert_smaller s s'')
254255
255256||| Splits a string into a list of newline separated strings.
256257|||
@@ -286,9 +287,7 @@ unwords = pack . unwords' . map unpack
286287||| ```
287288unlines' : List (List Char) -> List Char
288289unlines' [] = []
289−unlines' ls = assert_total (foldr1 addLine ls) where
290− addLine : List Char -> List Char -> List Char
291− addLine l s = l ++ ('\n' :: s)
290+unlines' (l::ls) = l ++ '\n' :: unlines' ls
292291
293292||| Joins the strings by newlines into a single string.
294293|||
test/prelude001/prelude001.idr+6−9
@@ -3,15 +3,12 @@ module Main
33main : IO ()
44main = do
55 printLn $ lines "" == []
6− -- `lines` seems to ignore too many trailing newlines.
7− printLn $ lines "\n" == [] -- FIXME: Should be [""].
8− printLn $ lines "\n\n" == [] -- FIXME: Should be ["", ""].
9− printLn $ lines "\n\n\n" == [] -- FIXME: Should be ["", "", ""].
6+ printLn $ lines "\n" == [""]
7+ printLn $ lines "\n\n" == ["", ""]
8+ printLn $ lines "\n\n\n" == ["", "", ""]
109 printLn $ lines "1\n2\n3" == ["1", "2", "3"]
1110 printLn $ lines "1\n2\n3\n" == ["1", "2", "3"]
1211 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"
16− printLn $ unlines ["1", "2"] == "1\n2" -- FIXME: Should be "1\n2\n"
17− printLn $ unlines ["1", "2", "3"] == "1\n2\n3" -- FIXME: Should be "1\n2\n3\n"
12+ printLn $ unlines ["1"] == "1\n"
13+ printLn $ unlines ["1", "2"] == "1\n2\n"
14+ printLn $ unlines ["1", "2", "3"] == "1\n2\n3\n"