git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2473 from xged/unlines
b89ea52Niklas Larsson
libs/prelude/Prelude/Strings.idr+32−14
compare with master
unifiedsplit
@@ -15,6 +15,15 @@ import Prelude.List
15import Prelude.Nat
15import Prelude.Nat
16import Decidable.Equality
16import Decidable.Equality
17
17
18+partial
19+foldr1 : (a -> a -> a) -> List a -> a
20+foldr1 _ [x] = x
21+foldr1 f (x::xs) = f x (foldr1 f xs)
22+
23+partial
24+foldl1 : (a -> a -> a) -> List a -> a
25+foldl1 f (x::xs) = foldl f x xs
26+
18||| Appends two strings together.
27||| Appends two strings together.
19|||
28|||
20||| ```idris example
29||| ```idris example
@@ -247,15 +256,6 @@ lines' s = case dropWhile isNL s of
247lines : String -> List String
256lines : String -> List String
248lines s = map pack $ lines' $ unpack s
257lines s = map pack $ lines' $ unpack s
249
258
250−partial
251−foldr1 : (a -> a -> a) -> List a -> a
252−foldr1 _ [x] = x
253−foldr1 f (x::xs) = f x (foldr1 f xs)
254−
255−partial
256−foldl1 : (a -> a -> a) -> List a -> a
257−foldl1 f (x::xs) = foldl f x xs
258−
259||| Joins the character lists by spaces into a single character list.
259||| Joins the character lists by spaces into a single character list.
260|||
260|||
261||| ```idris example
261||| ```idris example
@@ -263,12 +263,11 @@ foldl1 f (x::xs) = foldl f x xs
263||| ```
263||| ```
264unwords' : List (List Char) -> List Char
264unwords' : List (List Char) -> List Char
265unwords' [] = []
265unwords' [] = []
266−unwords' ws = assert_total (foldr1 addSpace ws)
266+unwords' ws = assert_total (foldr1 addSpace ws) where
267− where
268− addSpace : List Char -> List Char -> List Char
267+ addSpace : List Char -> List Char -> List Char
269− addSpace w s = w ++ (' ' :: s)
268+ addSpace w s = w ++ (' ' :: s)
270
269
271−||| Joins the strings by spaces into a single string.
270+||| Joins the strings by spaces into a single string.
272|||
271|||
273||| ```idris example
272||| ```idris example
274||| unwords ["A", "BC", "D", "E"]
273||| unwords ["A", "BC", "D", "E"]
@@ -276,6 +275,25 @@ unwords' ws = assert_total (foldr1 addSpace ws)
276unwords : List String -> String
275unwords : List String -> String
277unwords = pack . unwords' . map unpack
276unwords = pack . unwords' . map unpack
278
277
278+||| Joins the character lists by newlines into a single character list.
279+|||
280+||| ```idris example
281+||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]
282+||| ```
283+unlines' : List (List Char) -> List Char
284+unlines' [] = []
285+unlines' ls = assert_total (foldr1 addLine ls) where
286+ addLine : List Char -> List Char -> List Char
287+ addLine l s = l ++ ('\n' :: s)
288+
289+||| Joins the strings by newlines into a single string.
290+|||
291+||| ```idris example
292+||| unlines ["line", "line2", "ln3", "D"]
293+||| ```
294+unlines : List String -> String
295+unlines = pack . unlines' . map unpack
296+
279||| Returns the length of the string.
297||| Returns the length of the string.
280|||
298|||
281||| ```idris example
299||| ```idris example