da0a9a0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1925 from david-christiansen/issue/1924

da0a9a0David Christiansen12 years ago

libs/prelude/Prelude/Strings.idr+88−59

compare with master

unifiedsplit

@@ -17,8 +17,9 @@ import Decidable.Equality

18||| Appends two strings together.

19|||

20+||| ```idris example

20−||| Idris> "AB" ++ "C"

21+||| "AB" ++ "C"

21−||| "ABC" : String

22+||| ```

22(++) : String -> String -> String

23(++) : String -> String -> String

23(++) = prim__concat

24(++) = prim__concat

@@ -26,8 +27,9 @@ import Decidable.Equality

26|||

27|||

27||| Doesn't work for empty strings.

28||| Doesn't work for empty strings.

28|||

29|||

30+||| ```idris example

29−||| Idris> strHead "A"

31+||| strHead "A"

30−||| 'A' : Char

32+||| ```

31partial

33partial

32strHead : String -> Char

34strHead : String -> Char

33strHead = prim__strHead

35strHead = prim__strHead

@@ -36,20 +38,24 @@ strHead = prim__strHead

36|||

38|||

37||| Doesn't work for empty strings.

39||| Doesn't work for empty strings.

38|||

40|||

41+||| ```idris example

39−||| Idris> strTail "AB"

42+||| strTail "AB"

40−||| "B" : String

43+||| ```

44+||| ```idris example

41−||| Idris> strTail "A"

45+||| strTail "A"

42−||| "" : String

46+||| ```

43partial

47partial

44strTail : String -> String

48strTail : String -> String

45strTail = prim__strTail

49strTail = prim__strTail

47||| Adds a character to the front of the specified string.

51||| Adds a character to the front of the specified string.

48|||

52|||

53+||| ```idris example

49−||| Idris> strCons 'A' "B"

54+||| strCons 'A' "B"

50−||| "AB" : String

55+||| ```

56+||| ```idris example

51−||| Idris> strCons 'A' ""

57+||| strCons 'A' ""

52−||| "A" : String

58+||| ```

53strCons : Char -> String -> String

59strCons : Char -> String -> String

54strCons = prim__strCons

60strCons = prim__strCons

@@ -57,18 +63,21 @@ strCons = prim__strCons

57|||

63|||

58||| Precondition: '0 < i < length s' for 'strIndex s i'.

64||| Precondition: '0 < i < length s' for 'strIndex s i'.

59|||

65|||

66+||| ```idris example

60−||| Idris> strIndex "AB" 1

67+||| strIndex "AB" 1

61−||| 'B' : Char

68+||| ```

62partial

69partial

63strIndex : String -> Int -> Char

70strIndex : String -> Int -> Char

64strIndex = prim__strIndex

71strIndex = prim__strIndex

66||| Reverses the elements within a String.

73||| Reverses the elements within a String.

67|||

74|||

75+||| ```idris example

68−||| Idris> reverse "ABC"

76+||| reverse "ABC"

69−||| "CBA" : String

77+||| ```

78+||| ```idris example

70−||| Idris> reverse ""

79+||| reverse ""

71−||| "" : String

80+||| ```

72reverse : String -> String

81reverse : String -> String

73reverse = prim__strRev

82reverse = prim__strRev

@@ -103,8 +112,9 @@ strM x with (decEq (not (x == "")) True)

103

112

104||| Turns a string into a list of characters.

113||| Turns a string into a list of characters.

105|||

114|||

115+||| ```idris example

106−||| Idris> unpack "ABC"

116+||| unpack "ABC"

107−||| ['A', 'B', 'C'] : List Char

117+||| ```

108unpack : String -> List Char

118unpack : String -> List Char

109unpack s with (strM s)

119unpack s with (strM s)

110 unpack "" | StrNil = []

120 unpack "" | StrNil = []

@@ -116,8 +126,9 @@ pack = foldr strCons ""

116

126

117||| Creates a string of a single character.

127||| Creates a string of a single character.

118|||

128|||

129+||| ```idris example

119−||| Idris> singleton 'A'

130+||| singleton 'A'

120−||| "A" : String

131+||| ```

121singleton : Char -> String

132singleton : Char -> String

122singleton c = strCons c ""

133singleton c = strCons c ""

123

134

@@ -139,10 +150,12 @@ instance Monoid String where

139||| Splits the string into a part before the predicate

150||| Splits the string into a part before the predicate

140||| returns False and the rest of the string.

151||| returns False and the rest of the string.

141|||

152|||

153+||| ```idris example

142−||| Idris> span (/= 'C') "ABCD"

154+||| span (/= 'C') "ABCD"

143−||| ("AB", "CD") : (String, String)

155+||| ```

156+||| ```idris example

144−||| Idris> span (/= 'C') "EFGH"

157+||| span (/= 'C') "EFGH"

145−||| ("EFGH", "") : (String, String)

158+||| ```

146span : (Char -> Bool) -> String -> (String, String)

159span : (Char -> Bool) -> String -> (String, String)

147span p xs with (strM xs)

160span p xs with (strM xs)

148 span p "" | StrNil = ("", "")

161 span p "" | StrNil = ("", "")

@@ -154,28 +167,33 @@ span p xs with (strM xs)

154||| Splits the string into a part before the predicate

167||| Splits the string into a part before the predicate

155||| returns True and the rest of the string.

168||| returns True and the rest of the string.

156|||

169|||

170+||| ```idris example

157−||| Idris> break (== 'C') "ABCD"

171+||| break (== 'C') "ABCD"

158−||| ("AB", "CD") : (String, String)

172+||| ```

173+||| ```idris example

159−||| Idris> break (== 'C') "EFGH"

174+||| break (== 'C') "EFGH"

160−||| ("EFGH", "") : (String, String)

175+||| ```

161break : (Char -> Bool) -> String -> (String, String)

176break : (Char -> Bool) -> String -> (String, String)

162break p = span (not . p)

177break p = span (not . p)

163

178

164||| Splits the string into parts with the predicate

179||| Splits the string into parts with the predicate

165||| indicating separator characters.

180||| indicating separator characters.

166|||

181|||

182+||| ```idris example

167−||| Idris> split (== '.') ".AB.C..D"

183+||| split (== '.') ".AB.C..D"

168−||| ["", "AB", "C", "", "D"] : List String

184+||| ```

169split : (Char -> Bool) -> String -> List String

185split : (Char -> Bool) -> String -> List String

170split p xs = map pack (split p (unpack xs))

186split p xs = map pack (split p (unpack xs))

171

187

172||| Removes whitespace (determined with 'isSpace') from

188||| Removes whitespace (determined with 'isSpace') from

173||| the start of the string.

189||| the start of the string.

174|||

190|||

191+||| ```idris example

175−||| Idris> ltrim " A\nB"

192+||| ltrim " A\nB"

176−||| "A\nB" : String

193+||| ```

194+||| ```idris example

177−||| Idris> ltrim " \nAB"

195+||| ltrim " \nAB"

178−||| "AB" : String

196+||| ```

179ltrim : String -> String

197ltrim : String -> String

180ltrim xs with (strM xs)

198ltrim xs with (strM xs)

181 ltrim "" | StrNil = ""

199 ltrim "" | StrNil = ""

@@ -185,15 +203,17 @@ ltrim xs with (strM xs)

185||| Removes whitespace (determined with 'isSpace') from

203||| Removes whitespace (determined with 'isSpace') from

186||| the start and end of the string.

204||| the start and end of the string.

187|||

205|||

206+||| ```idris example

188−||| Idris> trim " A\nB C "

207+||| trim " A\nB C "

189−||| "A\nB C" : String

208+||| ```

190trim : String -> String

209trim : String -> String

191trim xs = ltrim (reverse (ltrim (reverse xs)))

210trim xs = ltrim (reverse (ltrim (reverse xs)))

192

211

193||| Splits a character list into a list of whitespace separated character lists.

212||| Splits a character list into a list of whitespace separated character lists.

194|||

213|||

214+||| ```idris example

195−||| Idris> words' (unpack " A B C D E ")

215+||| words' (unpack " A B C D E ")

196−||| [['A'], ['B'], ['C'], ['D'], ['E']] : List (List Char)

216+||| ```

197words' : List Char -> List (List Char)

217words' : List Char -> List (List Char)

198words' s = case dropWhile isSpace s of

218words' s = case dropWhile isSpace s of

199 [] => []

219 [] => []

@@ -202,15 +222,17 @@ words' s = case dropWhile isSpace s of

202

222

203||| Splits a string into a list of whitespace separated strings.

223||| Splits a string into a list of whitespace separated strings.

204|||

224|||

225+||| ```idris example

205−||| Idris> words " A B C D E "

226+||| words " A B C D E "

206−||| ["A", "B", "C", "D", "E"] : List String

227+||| ```

207words : String -> List String

228words : String -> List String

208words s = map pack $ words' $ unpack s

229words s = map pack $ words' $ unpack s

209

230

210||| Splits a character list into a list of newline separated character lists.

231||| Splits a character list into a list of newline separated character lists.

211|||

232|||

233+||| ```idris example

212−||| Idris> lines' (unpack "\rA BC\nD\r\nE\n")

234+||| lines' (unpack "\rA BC\nD\r\nE\n")

213−||| [['A', ' ', 'B', 'C'], ['D'], ['E']] : List (List Char)

235+||| ```

214lines' : List Char -> List (List Char)

236lines' : List Char -> List (List Char)

215lines' s = case dropWhile isNL s of

237lines' s = case dropWhile isNL s of

216 [] => []

238 [] => []

@@ -219,8 +241,9 @@ lines' s = case dropWhile isNL s of

219

241

220||| Splits a string into a list of newline separated strings.

242||| Splits a string into a list of newline separated strings.

221|||

243|||

244+||| ```idris example

222−||| Idris> lines "\rA BC\nD\r\nE\n"

245+||| lines "\rA BC\nD\r\nE\n"

223−||| ["A BC", "D", "E"] : List String

246+||| ```

224lines : String -> List String

247lines : String -> List String

225lines s = map pack $ lines' $ unpack s

248lines s = map pack $ lines' $ unpack s

226

249

@@ -235,8 +258,9 @@ foldl1 f (x::xs) = foldl f x xs

235

258

236||| Joins the character lists by spaces into a single character list.

259||| Joins the character lists by spaces into a single character list.

237|||

260|||

261+||| ```idris example

238−||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]

262+||| unwords' [['A'], ['B', 'C'], ['D'], ['E']]

239−||| ['A', ' ', 'B', 'C', ' ', 'D', ' ', 'E'] : List Char

263+||| ```

240unwords' : List (List Char) -> List Char

264unwords' : List (List Char) -> List Char

241unwords' [] = []

265unwords' [] = []

242unwords' ws = assert_total (foldr1 addSpace ws)

266unwords' ws = assert_total (foldr1 addSpace ws)

@@ -246,24 +270,28 @@ unwords' ws = assert_total (foldr1 addSpace ws)

246

270

247||| Joins the strings by spaces into a single string.

271||| Joins the strings by spaces into a single string.

248|||

272|||

273+||| ```idris example

249−||| Idris> unwords ["A", "BC", "D", "E"]

274+||| unwords ["A", "BC", "D", "E"]

250−||| "A BC D E" : String

275+||| ```

251unwords : List String -> String

276unwords : List String -> String

252unwords = pack . unwords' . map unpack

277unwords = pack . unwords' . map unpack

253

278

254||| Returns the length of the string.

279||| Returns the length of the string.

255|||

280|||

281+||| ```idris example

256−||| Idris> length ""

282+||| length ""

257−||| 0 : Nat

283+||| ```

284+||| ```idris example

258−||| Idris> length "ABC"

285+||| length "ABC"

259−||| 3 : Nat

286+||| ```

260length : String -> Nat

287length : String -> Nat

261length = fromInteger . prim__zextInt_BigInt . prim_lenString

288length = fromInteger . prim__zextInt_BigInt . prim_lenString

262

289

263||| Lowercases all characters in the string.

290||| Lowercases all characters in the string.

264|||

291|||

292+||| ```idris example

265−||| Idris> toLower "aBc12!"

293+||| toLower "aBc12!"

266−||| "abc12!" : String

294+||| ```

267toLower : String -> String

295toLower : String -> String

268toLower x with (strM x)

296toLower x with (strM x)

269 strToLower "" | StrNil = ""

297 strToLower "" | StrNil = ""

@@ -272,14 +300,15 @@ toLower x with (strM x)

272

300

273||| Uppercases all characters in the string.

301||| Uppercases all characters in the string.

274|||

302|||

303+||| ```idris example

275−||| Idris> toLower "aBc12!"

304+||| toLower "aBc12!"

276−||| "ABC12!" : String

305+||| ```

277toUpper : String -> String

306toUpper : String -> String

278toUpper x with (strM x)

307toUpper x with (strM x)

279 strToLower "" | StrNil = ""

308 strToLower "" | StrNil = ""

280 strToLower (strCons c cs) | (StrCons c cs) =

309 strToLower (strCons c cs) | (StrCons c cs) =

281 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))

310 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))

282−

311+

283--------------------------------------------------------------------------------

312--------------------------------------------------------------------------------

284-- Predicates

313-- Predicates

285--------------------------------------------------------------------------------

314--------------------------------------------------------------------------------