@@ -8,29 +8,59 @@ import Prelude.Either
8import Prelude.Foldable
8import Prelude.Foldable
10||| Appends two strings together.
10||| Appends two strings together.
12+||| Idris> "AB" ++ "C"
11(++) : String -> String -> String
14(++) : String -> String -> String
12(++) = prim__concat
15(++) = prim__concat
14||| Returns the first character in the specified string.
17||| Returns the first character in the specified string.
19+||| Doesn't work for empty strings.
21+||| Idris> strHead "A"
16strHead : String -> Char
24strHead : String -> Char
17strHead = prim__strHead
25strHead = prim__strHead
19||| Returns the characters specified after the head of the string.
27||| Returns the characters specified after the head of the string.
29+||| Doesn't work for empty strings.
31+||| Idris> strTail "AB"
33+||| Idris> strTail "A"
21strTail : String -> String
36strTail : String -> String
22strTail = prim__strTail
37strTail = prim__strTail
24−||| Adds a character to the from of the specified string.
39+||| Adds a character to the front of the specified string.
41+||| Idris> strCons 'A' "B"
43+||| Idris> strCons 'A' ""
25strCons : Char -> String -> String
45strCons : Char -> String -> String
26strCons = prim__strCons
46strCons = prim__strCons
28||| Returns the nth character (starting from 0) of the specified string.
48||| Returns the nth character (starting from 0) of the specified string.
50+||| Precondition: '0 < i < length s' for 'strIndex s i'.
52+||| Idris> strIndex "AB" 1
30strIndex : String -> Int -> Char
55strIndex : String -> Int -> Char
31strIndex = prim__strIndex
56strIndex = prim__strIndex
33||| Reverses the elements within a String.
58||| Reverses the elements within a String.
60+||| Idris> reverse "ABC"
34reverse : String -> String
64reverse : String -> String
35reverse = prim__strRev
65reverse = prim__strRev
@@ -43,9 +73,11 @@ data StrM : String -> Type where
43 StrNil : StrM ""
73 StrNil : StrM ""
44 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
74 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
76+||| Version of 'strHead' that statically verifies that the string is not empty.
46strHead' : (x : String) -> so (not (x == "")) -> Char
77strHead' : (x : String) -> so (not (x == "")) -> Char
47strHead' x p = assert_total $ prim__strHead x
78strHead' x p = assert_total $ prim__strHead x
80+||| Version of 'strTail' that statically verifies that the string is not empty.
49strTail' : (x : String) -> so (not (x == "")) -> String
81strTail' : (x : String) -> so (not (x == "")) -> String
50strTail' x p = assert_total $ prim__strTail x
82strTail' x p = assert_total $ prim__strTail x
@@ -61,14 +93,23 @@ strM x with (choose (not (x == "")))
61-- a recursive argument, therefore the termination checker doesn't believe
93-- a recursive argument, therefore the termination checker doesn't believe
62-- the string is guaranteed smaller. It makes a good point.
94-- the string is guaranteed smaller. It makes a good point.
96+||| Turns a string into a list of characters.
98+||| Idris> unpack "ABC"
99+||| ['A', 'B', 'C'] : List Char
64unpack : String -> List Char
100unpack : String -> List Char
65unpack s with (strM s)
101unpack s with (strM s)
66 unpack "" | StrNil = []
102 unpack "" | StrNil = []
67 unpack (strCons x xs) | (StrCons x xs) = x :: assert_total (unpack xs)
103 unpack (strCons x xs) | (StrCons x xs) = x :: assert_total (unpack xs)
105+||| Turns a Foldable of characters into a string.
69pack : (Foldable t) => t Char -> String
106pack : (Foldable t) => t Char -> String
70pack = foldr strCons ""
107pack = foldr strCons ""
109+||| Creates a string of a single character.
111+||| Idris> singleton 'A'
72singleton : Char -> String
113singleton : Char -> String
73singleton c = strCons c ""
114singleton c = strCons c ""
@@ -87,6 +128,13 @@ instance Semigroup String where
87instance Monoid String where
128instance Monoid String where
88 neutral = ""
129 neutral = ""
131+||| Splits the string into a part before the predicate
132+||| returns False and the rest of the string.
134+||| Idris> span (/= 'C') "ABCD"
135+||| ("AB", "CD") : (String, String)
136+||| Idris> span (/= 'C') "EFGH"
137+||| ("EFGH", "") : (String, String)
90span : (Char -> Bool) -> String -> (String, String)
138span : (Char -> Bool) -> String -> (String, String)
91span p xs with (strM xs)
139span p xs with (strM xs)
92 span p "" | StrNil = ("", "")
140 span p "" | StrNil = ("", "")
@@ -95,36 +143,76 @@ span p xs with (strM xs)
95 | (ys, zs) = (strCons x ys, zs)
143 | (ys, zs) = (strCons x ys, zs)
96 | False = ("", strCons x xs)
144 | False = ("", strCons x xs)
146+||| Splits the string into a part before the predicate
147+||| returns True and the rest of the string.
149+||| Idris> break (== 'C') "ABCD"
150+||| ("AB", "CD") : (String, String)
151+||| Idris> break (== 'C') "EFGH"
152+||| ("EFGH", "") : (String, String)
98break : (Char -> Bool) -> String -> (String, String)
153break : (Char -> Bool) -> String -> (String, String)
99break p = span (not . p)
154break p = span (not . p)
156+||| Splits the string into parts with the predicate
157+||| indicating separator characters.
159+||| Idris> split (== '.') ".AB.C..D"
160+||| ["", "AB", "C", "", "D"] : List String
101split : (Char -> Bool) -> String -> List String
161split : (Char -> Bool) -> String -> List String
102split p xs = map pack (split p (unpack xs))
162split p xs = map pack (split p (unpack xs))
164+||| Removes whitespace (determined with 'isSpace') from
165+||| the start of the string.
167+||| Idris> ltrim " A\nB"
169+||| Idris> ltrim " \nAB"
104ltrim : String -> String
171ltrim : String -> String
105ltrim xs with (strM xs)
172ltrim xs with (strM xs)
106 ltrim "" | StrNil = ""
173 ltrim "" | StrNil = ""
107 ltrim (strCons x xs) | StrCons _ _
174 ltrim (strCons x xs) | StrCons _ _
108 = if (isSpace x) then assert_total (ltrim xs) else (strCons x xs)
175 = if (isSpace x) then assert_total (ltrim xs) else (strCons x xs)
177+||| Removes whitespace (determined with 'isSpace') from
178+||| the start and end of the string.
180+||| Idris> trim " A\nB C "
181+||| "A\nB C" : String
110trim : String -> String
182trim : String -> String
111trim xs = ltrim (reverse (ltrim (reverse xs)))
183trim xs = ltrim (reverse (ltrim (reverse xs)))
185+||| Splits a character list into a list of whitespace separated character lists.
187+||| Idris> words' (unpack " A B C D E ")
188+||| [['A'], ['B'], ['C'], ['D'], ['E']] : List (List Char)
113words' : List Char -> List (List Char)
189words' : List Char -> List (List Char)
114words' s = case dropWhile isSpace s of
190words' s = case dropWhile isSpace s of
116 s' => let (w, s'') = break isSpace s'
192 s' => let (w, s'') = break isSpace s'
117 in w :: words' (assert_smaller s s'')
193 in w :: words' (assert_smaller s s'')
195+||| Splits a string into a list of whitespace separated strings.
197+||| Idris> words " A B C D E "
198+||| ["A", "B", "C", "D", "E"] : List String
119words : String -> List String
199words : String -> List String
120words s = map pack $ words' $ unpack s
200words s = map pack $ words' $ unpack s
202+||| Splits a character list into a list of newline separated character lists.
204+||| Idris> lines' (unpack "\rA BC\nD\r\nE\n")
205+||| [['A', ' ', 'B', 'C'], ['D'], ['E']] : List (List Char)
122lines' : List Char -> List (List Char)
206lines' : List Char -> List (List Char)
123lines' s = case dropWhile isNL s of
207lines' s = case dropWhile isNL s of
125 s' => let (w, s'') = break isNL s'
209 s' => let (w, s'') = break isNL s'
126 in w :: lines' (assert_smaller s s'')
210 in w :: lines' (assert_smaller s s'')
212+||| Splits a string into a list of newline separated strings.
214+||| Idris> lines "\rA BC\nD\r\nE\n"
215+||| ["A BC", "D", "E"] : List String
128lines : String -> List String
216lines : String -> List String
129lines s = map pack $ lines' $ unpack s
217lines s = map pack $ lines' $ unpack s
@@ -133,6 +221,10 @@ foldr1 : (a -> a -> a) -> List a -> a
133foldr1 f [x] = x
221foldr1 f [x] = x
134foldr1 f (x::xs) = f x (foldr1 f xs)
222foldr1 f (x::xs) = f x (foldr1 f xs)
224+||| Joins the character lists by spaces into a single character list.
226+||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]
227+||| ['A', ' ', 'B', 'C', ' ', 'D', ' ', 'E'] : List Char
136unwords' : List (List Char) -> List Char
228unwords' : List (List Char) -> List Char
137unwords' [] = []
229unwords' [] = []
138unwords' ws = assert_total (foldr1 addSpace ws)
230unwords' ws = assert_total (foldr1 addSpace ws)
@@ -140,18 +232,36 @@ unwords' ws = assert_total (foldr1 addSpace ws)
140 addSpace : List Char -> List Char -> List Char
232 addSpace : List Char -> List Char -> List Char
141 addSpace w s = w ++ (' ' :: s)
233 addSpace w s = w ++ (' ' :: s)
235+||| Joins the strings by spaces into a single string.
237+||| Idris> unwords ["A", "BC", "D", "E"]
238+||| "A BC D E" : String
143unwords : List String -> String
239unwords : List String -> String
144unwords = pack . unwords' . map unpack
240unwords = pack . unwords' . map unpack
242+||| Returns the length of the string.
246+||| Idris> length "ABC"
146length : String -> Nat
248length : String -> Nat
147length = fromInteger . prim__zextInt_BigInt . prim_lenString
249length = fromInteger . prim__zextInt_BigInt . prim_lenString
251+||| Lowercases all characters in the string.
253+||| Idris> toLower "aBc12!"
254+||| "abc12!" : String
149toLower : String -> String
255toLower : String -> String
150toLower x with (strM x)
256toLower x with (strM x)
151 strToLower "" | StrNil = ""
257 strToLower "" | StrNil = ""
152 strToLower (strCons c cs) | (StrCons c cs) =
258 strToLower (strCons c cs) | (StrCons c cs) =
153 strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))
259 strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))
261+||| Uppercases all characters in the string.
263+||| Idris> toLower "aBc12!"
264+||| "ABC12!" : String
155toUpper : String -> String
265toUpper : String -> String
156toUpper x with (strM x)
266toUpper x with (strM x)
157 strToLower "" | StrNil = ""
267 strToLower "" | StrNil = ""