0 | module Data.String
  1 |
  2 | import public Data.List
  3 | import Data.List1
  4 | import public Data.SnocList
  5 |
  6 | %default total
  7 |
  8 | public export
  9 | singleton : Char -> String
 10 | singleton c = strCons c ""
 11 |
 12 | ||| Create a string by using n copies of a character
 13 | public export
 14 | replicate : Nat -> Char -> String
 15 | replicate n c = pack (replicate n c)
 16 |
 17 | ||| Indent a given string by `n` spaces.
 18 | public export
 19 | indent : (n : Nat) -> String -> String
 20 | indent n x = replicate n ' ' ++ x
 21 |
 22 | ||| Pad a string on the left
 23 | public export
 24 | padLeft : Nat -> Char -> String -> String
 25 | padLeft n c str = replicate (minus n (String.length str)) c ++ str
 26 |
 27 | ||| Pad a string on the right
 28 | public export
 29 | padRight : Nat -> Char -> String -> String
 30 | padRight n c str = str ++ replicate (minus n (String.length str)) c
 31 |
 32 | -- This uses fastConcat internally so it won't compute at compile time.
 33 | export
 34 | fastUnlines : List String -> String
 35 | fastUnlines = fastConcat . unlines'
 36 |   where unlines' : List String -> List String
 37 |         unlines' [] = []
 38 |         unlines' (x :: xs) = x :: "\n" :: unlines' xs
 39 |
 40 | ||| Splits a string into a list of whitespace separated strings.
 41 | |||
 42 | ||| ```idris example
 43 | ||| words " A B C  D E   "
 44 | ||| ```
 45 | public export
 46 | words : String -> List String
 47 | words s = map pack (words' (unpack s) [<] [<])
 48 |   where
 49 |     -- append a word to the list of words, only if it's non-empty
 50 |     wordsHelper : SnocList Char -> SnocList (List Char) -> SnocList (List Char)
 51 |     wordsHelper [<] css = css
 52 |     wordsHelper sc  css = css :< (sc <>> Nil)
 53 |
 54 |     ||| Splits a character list into a list of whitespace separated character lists.
 55 |     |||
 56 |     ||| ```idris example
 57 |     ||| words' (unpack " A B C  D E   ") [<] [<]
 58 |     ||| ```
 59 |     words' :  List Char
 60 |            -> SnocList Char
 61 |            -> SnocList (List Char)
 62 |            -> List (List Char)
 63 |     words' (c :: cs) sc css =
 64 |       if isSpace c
 65 |          then words' cs [<] (wordsHelper sc css)
 66 |          else words' cs (sc :< c) css
 67 |     words' [] sc css = wordsHelper sc css <>> Nil
 68 |
 69 | ||| Joins the strings using the provided separator
 70 | ||| ```idris example
 71 | ||| joinBy ", " ["A", "BC", "D"] === "A, BC, D"
 72 | ||| ```
 73 | public export
 74 | joinBy : String -> List String -> String
 75 | joinBy sep ws = concat (intersperse sep ws)
 76 |
 77 | ||| Joins the strings by spaces into a single string.
 78 | |||
 79 | ||| ```idris example
 80 | ||| unwords ["A", "BC", "D", "E"] === "A BC D E"
 81 | ||| ```
 82 | public export
 83 | unwords : List String -> String
 84 | unwords = joinBy " "
 85 |
 86 | ||| Splits a character list into a list of newline separated character lists.
 87 | |||
 88 | ||| The empty string becomes an empty list. The last newline, if not followed by
 89 | ||| any additional characters, is eaten (there will never be an empty string last element
 90 | ||| in the result).
 91 | |||
 92 | ||| ```idris example
 93 | ||| lines' (unpack "\rA BC\nD\r\nE\n")
 94 | ||| ```
 95 | public export
 96 | lines' : List Char -> List (List Char)
 97 | lines' s = linesHelp [] s
 98 |   where linesHelp : List Char -> List Char -> List (List Char)
 99 |         linesHelp [] [] = []
100 |         linesHelp acc [] = [reverse acc]
101 |         linesHelp acc ('\n' :: xs) = reverse acc :: linesHelp [] xs
102 |         linesHelp acc ('\r' :: '\n' :: xs) = reverse acc :: linesHelp [] xs
103 |         linesHelp acc ('\r' :: xs) = reverse acc :: linesHelp [] xs
104 |         linesHelp acc (c :: xs) = linesHelp (c :: acc) xs
105 |
106 |
107 | ||| Splits a string into a list of newline separated strings.
108 | |||
109 | ||| The empty string becomes an empty list. The last newline, if not followed by
110 | ||| any additional characters, is eaten (there will never be an empty string last element
111 | ||| in the result).
112 | |||
113 | ||| ```idris example
114 | ||| lines  "\rA BC\nD\r\nE\n"
115 | ||| ```
116 | public export
117 | lines : String -> List String
118 | lines s = map pack (lines' (unpack s))
119 |
120 | ||| Joins the strings into a single string by appending a newline to each string.
121 | |||
122 | ||| ```idris example
123 | ||| unlines ["line", "line2", "ln3", "D"]
124 | ||| ```
125 | public export
126 | unlines : List String -> String
127 | unlines ls = concat (interleave ls ("\n" <$ ls))
128 |
129 | %transform "fastUnlines" unlines = fastUnlines
130 |
131 | ||| A view checking whether a string is empty
132 | ||| and, if not, returning its head and tail
133 | public export
134 | data StrM : String -> Type where
135 |     StrNil : StrM ""
136 |     StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
137 |
138 | ||| To each string we can associate its StrM view
139 | public export
140 | strM : (x : String) -> StrM x
141 | strM "" = StrNil
142 | strM x
143 |   -- Using primitives, so `assert_total` and `believe_me` needed
144 |     = assert_total $ believe_me $
145 |         StrCons (prim__strHead x) (prim__strTail x)
146 |
147 | ||| A view of a string as a lazy linked list of characters
148 | public export
149 | data AsList : String -> Type where
150 |   Nil  : AsList ""
151 |   (::) : (c : Char) -> {str : String} -> Lazy (AsList str) -> AsList (strCons c str)
152 |
153 | ||| To each string we can associate the lazy linked list of characters
154 | ||| it corresponds to once unpacked.
155 | public export
156 | asList : (str : String) -> AsList str
157 | asList str with (strM str)
158 |   asList "" | StrNil = []
159 |   asList str@(strCons x xs) | StrCons _ _ = x :: asList (assert_smaller str xs)
160 |
161 | ||| Trim whitespace on the left of the string
162 | public export
163 | ltrim : String -> String
164 | ltrim str with (asList str)
165 |   ltrim ""  | [] = ""
166 |   ltrim str@_ | x :: xs = if isSpace x then ltrim _ | xs else str
167 |
168 | ||| Trim whitespace on the right of the string
169 | public export
170 | rtrim : String -> String
171 | rtrim = reverse . ltrim . reverse
172 |
173 | ||| Trim whitespace on both sides of the string
174 | public export
175 | trim : String -> String
176 | trim = ltrim . rtrim
177 |
178 | ||| Splits the string into a part before the predicate
179 | ||| returns False and the rest of the string.
180 | |||
181 | ||| ```idris example
182 | ||| span (/= 'C') "ABCD"
183 | ||| ```
184 | ||| ```idris example
185 | ||| span (/= 'C') "EFGH"
186 | ||| ```
187 | public export
188 | span : (Char -> Bool) -> String -> (String, String)
189 | span p xs
190 |     = case span p (unpack xs) of
191 |            (x, y) => (pack x, pack y)
192 |
193 | ||| Splits the string into a part before the predicate
194 | ||| returns True and the rest of the string.
195 | |||
196 | ||| ```idris example
197 | ||| break (== 'C') "ABCD"
198 | ||| ```
199 | ||| ```idris example
200 | ||| break (== 'C') "EFGH"
201 | ||| ```
202 | public export
203 | break : (Char -> Bool) -> String -> (String, String)
204 | break p = span (not . p)
205 |
206 |
207 | ||| Splits the string into parts with the predicate
208 | ||| indicating separator characters.
209 | |||
210 | ||| ```idris example
211 | ||| split (== '.') ".AB.C..D"
212 | ||| ```
213 | public export
214 | split : (Char -> Bool) -> String -> List1 String
215 | split p xs = map pack (split p (unpack xs))
216 |
217 | public export
218 | stringToNatOrZ : String -> Nat
219 | stringToNatOrZ = fromInteger . prim__cast_StringInteger
220 |
221 | public export
222 | toUpper : String -> String
223 | toUpper str = pack (map toUpper (unpack str))
224 |
225 | public export
226 | toLower : String -> String
227 | toLower str = pack (map toLower (unpack str))
228 |
229 | public export partial
230 | strIndex : String -> Int -> Char
231 | strIndex = prim__strIndex
232 |
233 | public export covering
234 | strLength : String -> Int
235 | strLength = prim__strLength
236 |
237 | public export covering
238 | strSubstr : Int -> Int -> String -> String
239 | strSubstr = prim__strSubstr
240 |
241 | public export partial
242 | strTail : String -> String
243 | strTail = prim__strTail
244 |
245 | public export
246 | isPrefixOf : String -> String -> Bool
247 | isPrefixOf a b = isPrefixOf (unpack a) (unpack b)
248 |
249 | public export
250 | isSuffixOf : String -> String -> Bool
251 | isSuffixOf a b = isSuffixOf (unpack a) (unpack b)
252 |
253 | public export
254 | isInfixOf : String -> String -> Bool
255 | isInfixOf a b = isInfixOf (unpack a) (unpack b)
256 |
257 | public export
258 | parseNumWithoutSign : List Char -> Integer -> Maybe Integer
259 | parseNumWithoutSign []        acc = Just acc
260 | parseNumWithoutSign (c :: cs) acc =
261 |   if (c >= '0' && c <= '9')
262 |   then parseNumWithoutSign cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
263 |   else Nothing
264 |
265 | ||| Convert a positive number string to a Num.
266 | |||
267 | ||| ```idris example
268 | ||| parsePositive "123"
269 | ||| ```
270 | ||| ```idris example
271 | ||| parsePositive {a=Int} " +123"
272 | ||| ```
273 | public export
274 | parsePositive : Num a => String -> Maybe a
275 | parsePositive s = parsePosTrimmed (trim s)
276 |   where
277 |     parsePosTrimmed : String -> Maybe a
278 |     parsePosTrimmed s with (strM s)
279 |       parsePosTrimmed ""             | StrNil         = Nothing
280 |       parsePosTrimmed (strCons '+' xs) | (StrCons '+' xs) =
281 |         map fromInteger (parseNumWithoutSign (unpack xs) 0)
282 |       parsePosTrimmed (strCons x xs) | (StrCons x xs) =
283 |         if (x >= '0' && x <= '9')
284 |         then  map fromInteger (parseNumWithoutSign (unpack xs)  (cast (ord x - ord '0')))
285 |         else Nothing
286 |
287 | ||| Convert a number string to a Num.
288 | |||
289 | ||| ```idris example
290 | ||| parseInteger " 123"
291 | ||| ```
292 | ||| ```idris example
293 | ||| parseInteger {a=Int} " -123"
294 | ||| ```
295 | public export
296 | parseInteger : Num a => Neg a => String -> Maybe a
297 | parseInteger s = parseIntTrimmed (trim s)
298 |   where
299 |     parseIntTrimmed : String -> Maybe a
300 |     parseIntTrimmed s with (strM s)
301 |       parseIntTrimmed ""             | StrNil         = Nothing
302 |       parseIntTrimmed (strCons x xs) | (StrCons x xs) =
303 |         if (x == '-')
304 |           then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0)
305 |           else if (x == '+')
306 |             then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0))
307 |             else if (x >= '0' && x <= '9')
308 |             then map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
309 |               else Nothing
310 |
311 |
312 | ||| Convert a number string to a Double.
313 | |||
314 | ||| ```idris example
315 | ||| parseDouble "+123.123e-2"
316 | ||| ```
317 | ||| ```idris example
318 | ||| parseDouble " -123.123E+2"
319 | ||| ```
320 | ||| ```idris example
321 | ||| parseDouble " +123.123"
322 | ||| ```
323 | export -- it's a bit too slow at compile time
324 | covering
325 | parseDouble : String -> Maybe Double
326 | parseDouble = mkDouble . wfe . trim
327 |   where
328 |     intPow : Integer -> Integer -> Double
329 |     intPow base exp = assert_total $ if exp > 0 then (num base exp) else 1 / (num base exp)
330 |       where
331 |         num : Integer -> Integer -> Double
332 |         num base 0 = 1
333 |         num base e = if e < 0
334 |                      then cast base * num base (e + 1)
335 |                      else cast base * num base (e - 1)
336 |
337 |     natpow : Double -> Nat -> Double
338 |     natpow x Z = 1
339 |     natpow x (S n) = x * (natpow x n)
340 |
341 |     mkDouble : Maybe (Double, Double, Integer) -> Maybe Double
342 |     mkDouble (Just (w, f, e)) = let ex = intPow 10 e in
343 |                                 Just $ (w * ex + f * ex)
344 |     mkDouble Nothing = Nothing
345 |
346 |     wfe : String -> Maybe (Double, Double, Integer)
347 |     wfe cs = case split (== '.') cs of
348 |                (wholeAndExp ::: []) =>
349 |                  case split (\c => c == 'e' || c == 'E') wholeAndExp of
350 |                    (whole:::exp::[]) =>
351 |                      do
352 |                        w <- cast {from=Integer} <$> parseInteger whole
353 |                        e <- parseInteger exp
354 |                        pure (w, 0, e)
355 |                    (whole:::[]) =>
356 |                      do
357 |                        w <- cast {from=Integer} <$> parseInteger whole
358 |                        pure (w, 0, 0)
359 |                    _ => Nothing
360 |                (whole:::fracAndExp::[]) =>
361 |                  case split (\c => c == 'e' || c == 'E') fracAndExp of
362 |                    ("":::exp::[]) => Nothing
363 |                    (frac:::exp::[]) =>
364 |                      do
365 |                        w <- cast {from=Integer} <$> parseInteger whole
366 |                        f <- (/ (natpow 10 (length frac))) <$>
367 |                             (cast <$> parseNumWithoutSign (unpack frac) 0)
368 |                        e <- parseInteger exp
369 |                        pure (w, if w < 0 then (-f) else f, e)
370 |                    (frac:::[]) =>
371 |                      do
372 |                        w <- cast {from=Integer} <$> parseInteger whole
373 |                        f <- (/ (natpow 10 (length frac))) <$>
374 |                             (cast <$> parseNumWithoutSign (unpack frac) 0)
375 |                        pure (w, if w < 0 then (-f) else f, 0)
376 |                    _ => Nothing
377 |                _ => Nothing
378 |
379 | public export
380 | null : String -> Bool
381 | null = (== "")
382 |