@@ -8,29 +8,59 @@ import Prelude.Either
88import Prelude.Foldable
99
1010||| Appends two strings together.
11+|||
12+||| Idris> "AB" ++ "C"
13+||| "ABC" : String
1114(++) : String -> String -> String
1215(++) = prim__concat
1316
1417||| Returns the first character in the specified string.
18+|||
19+||| Doesn't work for empty strings.
20+|||
21+||| Idris> strHead "A"
22+||| 'A' : Char
1523partial
1624strHead : String -> Char
1725strHead = prim__strHead
1826
1927||| Returns the characters specified after the head of the string.
28+|||
29+||| Doesn't work for empty strings.
30+|||
31+||| Idris> strTail "AB"
32+||| "B" : String
33+||| Idris> strTail "A"
34+||| "" : String
2035partial
2136strTail : String -> String
2237strTail = prim__strTail
2338
24−||| Adds a character to the from of the specified string.
39+||| Adds a character to the front of the specified string.
40+|||
41+||| Idris> strCons 'A' "B"
42+||| "AB" : String
43+||| Idris> strCons 'A' ""
44+||| "A" : String
2545strCons : Char -> String -> String
2646strCons = prim__strCons
2747
2848||| Returns the nth character (starting from 0) of the specified string.
49+|||
50+||| Precondition: '0 < i < length s' for 'strIndex s i'.
51+|||
52+||| Idris> strIndex "AB" 1
53+||| 'B' : Char
2954partial
3055strIndex : String -> Int -> Char
3156strIndex = prim__strIndex
3257
3358||| Reverses the elements within a String.
59+|||
60+||| Idris> reverse "ABC"
61+||| "CBA" : String
62+||| Idris> reverse ""
63+||| "" : String
3464reverse : String -> String
3565reverse = prim__strRev
3666
@@ -43,9 +73,11 @@ data StrM : String -> Type where
4373 StrNil : StrM ""
4474 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
4575
76+||| Version of 'strHead' that statically verifies that the string is not empty.
4677strHead' : (x : String) -> so (not (x == "")) -> Char
4778strHead' x p = assert_total $ prim__strHead x
4879
80+||| Version of 'strTail' that statically verifies that the string is not empty.
4981strTail' : (x : String) -> so (not (x == "")) -> String
5082strTail' x p = assert_total $ prim__strTail x
5183
@@ -61,14 +93,23 @@ strM x with (choose (not (x == "")))
6193-- a recursive argument, therefore the termination checker doesn't believe
6294-- the string is guaranteed smaller. It makes a good point.
6395
96+||| Turns a string into a list of characters.
97+|||
98+||| Idris> unpack "ABC"
99+||| ['A', 'B', 'C'] : List Char
64100unpack : String -> List Char
65101unpack s with (strM s)
66102 unpack "" | StrNil = []
67103 unpack (strCons x xs) | (StrCons x xs) = x :: assert_total (unpack xs)
68104
105+||| Turns a Foldable of characters into a string.
69106pack : (Foldable t) => t Char -> String
70107pack = foldr strCons ""
71108
109+||| Creates a string of a single character.
110+|||
111+||| Idris> singleton 'A'
112+||| "A" : String
72113singleton : Char -> String
73114singleton c = strCons c ""
74115
@@ -87,6 +128,13 @@ instance Semigroup String where
87128instance Monoid String where
88129 neutral = ""
89130
131+||| Splits the string into a part before the predicate
132+||| returns False and the rest of the string.
133+|||
134+||| Idris> span (/= 'C') "ABCD"
135+||| ("AB", "CD") : (String, String)
136+||| Idris> span (/= 'C') "EFGH"
137+||| ("EFGH", "") : (String, String)
90138span : (Char -> Bool) -> String -> (String, String)
91139span p xs with (strM xs)
92140 span p "" | StrNil = ("", "")
@@ -95,36 +143,76 @@ span p xs with (strM xs)
95143 | (ys, zs) = (strCons x ys, zs)
96144 | False = ("", strCons x xs)
97145
146+||| Splits the string into a part before the predicate
147+||| returns True and the rest of the string.
148+|||
149+||| Idris> break (== 'C') "ABCD"
150+||| ("AB", "CD") : (String, String)
151+||| Idris> break (== 'C') "EFGH"
152+||| ("EFGH", "") : (String, String)
98153break : (Char -> Bool) -> String -> (String, String)
99154break p = span (not . p)
100155
156+||| Splits the string into parts with the predicate
157+||| indicating separator characters.
158+|||
159+||| Idris> split (== '.') ".AB.C..D"
160+||| ["", "AB", "C", "", "D"] : List String
101161split : (Char -> Bool) -> String -> List String
102162split p xs = map pack (split p (unpack xs))
103163
164+||| Removes whitespace (determined with 'isSpace') from
165+||| the start of the string.
166+|||
167+||| Idris> ltrim " A\nB"
168+||| "A\nB" : String
169+||| Idris> ltrim " \nAB"
170+||| "AB" : String
104171ltrim : String -> String
105172ltrim xs with (strM xs)
106173 ltrim "" | StrNil = ""
107174 ltrim (strCons x xs) | StrCons _ _
108175 = if (isSpace x) then assert_total (ltrim xs) else (strCons x xs)
109176
177+||| Removes whitespace (determined with 'isSpace') from
178+||| the start and end of the string.
179+|||
180+||| Idris> trim " A\nB C "
181+||| "A\nB C" : String
110182trim : String -> String
111183trim xs = ltrim (reverse (ltrim (reverse xs)))
112184
185+||| Splits a character list into a list of whitespace separated character lists.
186+|||
187+||| Idris> words' (unpack " A B C D E ")
188+||| [['A'], ['B'], ['C'], ['D'], ['E']] : List (List Char)
113189words' : List Char -> List (List Char)
114190words' s = case dropWhile isSpace s of
115191 [] => []
116192 s' => let (w, s'') = break isSpace s'
117193 in w :: words' (assert_smaller s s'')
118194
195+||| Splits a string into a list of whitespace separated strings.
196+|||
197+||| Idris> words " A B C D E "
198+||| ["A", "B", "C", "D", "E"] : List String
119199words : String -> List String
120200words s = map pack $ words' $ unpack s
121201
202+||| Splits a character list into a list of newline separated character lists.
203+|||
204+||| Idris> lines' (unpack "\rA BC\nD\r\nE\n")
205+||| [['A', ' ', 'B', 'C'], ['D'], ['E']] : List (List Char)
122206lines' : List Char -> List (List Char)
123207lines' s = case dropWhile isNL s of
124208 [] => []
125209 s' => let (w, s'') = break isNL s'
126210 in w :: lines' (assert_smaller s s'')
127211
212+||| Splits a string into a list of newline separated strings.
213+|||
214+||| Idris> lines "\rA BC\nD\r\nE\n"
215+||| ["A BC", "D", "E"] : List String
128216lines : String -> List String
129217lines s = map pack $ lines' $ unpack s
130218
@@ -133,6 +221,10 @@ foldr1 : (a -> a -> a) -> List a -> a
133221foldr1 f [x] = x
134222foldr1 f (x::xs) = f x (foldr1 f xs)
135223
224+||| Joins the character lists by spaces into a single character list.
225+|||
226+||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]
227+||| ['A', ' ', 'B', 'C', ' ', 'D', ' ', 'E'] : List Char
136228unwords' : List (List Char) -> List Char
137229unwords' [] = []
138230unwords' ws = assert_total (foldr1 addSpace ws)
@@ -140,18 +232,36 @@ unwords' ws = assert_total (foldr1 addSpace ws)
140232 addSpace : List Char -> List Char -> List Char
141233 addSpace w s = w ++ (' ' :: s)
142234
235+||| Joins the strings by spaces into a single string.
236+|||
237+||| Idris> unwords ["A", "BC", "D", "E"]
238+||| "A BC D E" : String
143239unwords : List String -> String
144240unwords = pack . unwords' . map unpack
145241
242+||| Returns the length of the string.
243+|||
244+||| Idris> length ""
245+||| 0 : Nat
246+||| Idris> length "ABC"
247+||| 3 : Nat
146248length : String -> Nat
147249length = fromInteger . prim__zextInt_BigInt . prim_lenString
148250
251+||| Lowercases all characters in the string.
252+|||
253+||| Idris> toLower "aBc12!"
254+||| "abc12!" : String
149255toLower : String -> String
150256toLower x with (strM x)
151257 strToLower "" | StrNil = ""
152258 strToLower (strCons c cs) | (StrCons c cs) =
153259 strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))
154260
261+||| Uppercases all characters in the string.
262+|||
263+||| Idris> toLower "aBc12!"
264+||| "ABC12!" : String
155265toUpper : String -> String
156266toUpper x with (strM x)
157267 strToLower "" | StrNil = ""