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 both sides of the string
169 | public export
170 | trim : String -> String
171 | trim = ltrim . reverse . ltrim . reverse
172 |
173 | ||| Splits the string into a part before the predicate
174 | ||| returns False and the rest of the string.
175 | |||
176 | ||| ```idris example
177 | ||| span (/= 'C') "ABCD"
178 | ||| ```
179 | ||| ```idris example
180 | ||| span (/= 'C') "EFGH"
181 | ||| ```
182 | public export
183 | span : (Char -> Bool) -> String -> (String, String)
184 | span p xs
185 |     = case span p (unpack xs) of
186 |            (x, y) => (pack x, pack y)
187 |
188 | ||| Splits the string into a part before the predicate
189 | ||| returns True and the rest of the string.
190 | |||
191 | ||| ```idris example
192 | ||| break (== 'C') "ABCD"
193 | ||| ```
194 | ||| ```idris example
195 | ||| break (== 'C') "EFGH"
196 | ||| ```
197 | public export
198 | break : (Char -> Bool) -> String -> (String, String)
199 | break p = span (not . p)
200 |
201 |
202 | ||| Splits the string into parts with the predicate
203 | ||| indicating separator characters.
204 | |||
205 | ||| ```idris example
206 | ||| split (== '.') ".AB.C..D"
207 | ||| ```
208 | public export
209 | split : (Char -> Bool) -> String -> List1 String
210 | split p xs = map pack (split p (unpack xs))
211 |
212 | public export
213 | stringToNatOrZ : String -> Nat
214 | stringToNatOrZ = fromInteger . prim__cast_StringInteger
215 |
216 | public export
217 | toUpper : String -> String
218 | toUpper str = pack (map toUpper (unpack str))
219 |
220 | public export
221 | toLower : String -> String
222 | toLower str = pack (map toLower (unpack str))
223 |
224 | public export partial
225 | strIndex : String -> Int -> Char
226 | strIndex = prim__strIndex
227 |
228 | public export covering
229 | strLength : String -> Int
230 | strLength = prim__strLength
231 |
232 | public export covering
233 | strSubstr : Int -> Int -> String -> String
234 | strSubstr = prim__strSubstr
235 |
236 | public export partial
237 | strTail : String -> String
238 | strTail = prim__strTail
239 |
240 | public export
241 | isPrefixOf : String -> String -> Bool
242 | isPrefixOf a b = isPrefixOf (unpack a) (unpack b)
243 |
244 | public export
245 | isSuffixOf : String -> String -> Bool
246 | isSuffixOf a b = isSuffixOf (unpack a) (unpack b)
247 |
248 | public export
249 | isInfixOf : String -> String -> Bool
250 | isInfixOf a b = isInfixOf (unpack a) (unpack b)
251 |
252 | public export
253 | parseNumWithoutSign : List Char -> Integer -> Maybe Integer
254 | parseNumWithoutSign []        acc = Just acc
255 | parseNumWithoutSign (c :: cs) acc =
256 |   if (c >= '0' && c <= '9')
257 |   then parseNumWithoutSign cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
258 |   else Nothing
259 |
260 | ||| Convert a positive number string to a Num.
261 | |||
262 | ||| ```idris example
263 | ||| parsePositive "123"
264 | ||| ```
265 | ||| ```idris example
266 | ||| parsePositive {a=Int} " +123"
267 | ||| ```
268 | public export
269 | parsePositive : Num a => String -> Maybe a
270 | parsePositive s = parsePosTrimmed (trim s)
271 |   where
272 |     parsePosTrimmed : String -> Maybe a
273 |     parsePosTrimmed s with (strM s)
274 |       parsePosTrimmed ""             | StrNil         = Nothing
275 |       parsePosTrimmed (strCons '+' xs) | (StrCons '+' xs) =
276 |         map fromInteger (parseNumWithoutSign (unpack xs) 0)
277 |       parsePosTrimmed (strCons x xs) | (StrCons x xs) =
278 |         if (x >= '0' && x <= '9')
279 |         then  map fromInteger (parseNumWithoutSign (unpack xs)  (cast (ord x - ord '0')))
280 |         else Nothing
281 |
282 | ||| Convert a number string to a Num.
283 | |||
284 | ||| ```idris example
285 | ||| parseInteger " 123"
286 | ||| ```
287 | ||| ```idris example
288 | ||| parseInteger {a=Int} " -123"
289 | ||| ```
290 | public export
291 | parseInteger : Num a => Neg a => String -> Maybe a
292 | parseInteger s = parseIntTrimmed (trim s)
293 |   where
294 |     parseIntTrimmed : String -> Maybe a
295 |     parseIntTrimmed s with (strM s)
296 |       parseIntTrimmed ""             | StrNil         = Nothing
297 |       parseIntTrimmed (strCons x xs) | (StrCons x xs) =
298 |         if (x == '-')
299 |           then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0)
300 |           else if (x == '+')
301 |             then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0))
302 |             else if (x >= '0' && x <= '9')
303 |             then map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
304 |               else Nothing
305 |
306 |
307 | ||| Convert a number string to a Double.
308 | |||
309 | ||| ```idris example
310 | ||| parseDouble "+123.123e-2"
311 | ||| ```
312 | ||| ```idris example
313 | ||| parseDouble " -123.123E+2"
314 | ||| ```
315 | ||| ```idris example
316 | ||| parseDouble " +123.123"
317 | ||| ```
318 | export -- it's a bit too slow at compile time
319 | covering
320 | parseDouble : String -> Maybe Double
321 | parseDouble = mkDouble . wfe . trim
322 |   where
323 |     intPow : Integer -> Integer -> Double
324 |     intPow base exp = assert_total $ if exp > 0 then (num base exp) else 1 / (num base exp)
325 |       where
326 |         num : Integer -> Integer -> Double
327 |         num base 0 = 1
328 |         num base e = if e < 0
329 |                      then cast base * num base (e + 1)
330 |                      else cast base * num base (e - 1)
331 |
332 |     natpow : Double -> Nat -> Double
333 |     natpow x Z = 1
334 |     natpow x (S n) = x * (natpow x n)
335 |
336 |     mkDouble : Maybe (Double, Double, Integer) -> Maybe Double
337 |     mkDouble (Just (w, f, e)) = let ex = intPow 10 e in
338 |                                 Just $ (w * ex + f * ex)
339 |     mkDouble Nothing = Nothing
340 |
341 |     wfe : String -> Maybe (Double, Double, Integer)
342 |     wfe cs = case split (== '.') cs of
343 |                (wholeAndExp ::: []) =>
344 |                  case split (\c => c == 'e' || c == 'E') wholeAndExp of
345 |                    (whole:::exp::[]) =>
346 |                      do
347 |                        w <- cast {from=Integer} <$> parseInteger whole
348 |                        e <- parseInteger exp
349 |                        pure (w, 0, e)
350 |                    (whole:::[]) =>
351 |                      do
352 |                        w <- cast {from=Integer} <$> parseInteger whole
353 |                        pure (w, 0, 0)
354 |                    _ => Nothing
355 |                (whole:::fracAndExp::[]) =>
356 |                  case split (\c => c == 'e' || c == 'E') fracAndExp of
357 |                    ("":::exp::[]) => Nothing
358 |                    (frac:::exp::[]) =>
359 |                      do
360 |                        w <- cast {from=Integer} <$> parseInteger whole
361 |                        f <- (/ (natpow 10 (length frac))) <$>
362 |                             (cast <$> parseNumWithoutSign (unpack frac) 0)
363 |                        e <- parseInteger exp
364 |                        pure (w, if w < 0 then (-f) else f, e)
365 |                    (frac:::[]) =>
366 |                      do
367 |                        w <- cast {from=Integer} <$> parseInteger whole
368 |                        f <- (/ (natpow 10 (length frac))) <$>
369 |                             (cast <$> parseNumWithoutSign (unpack frac) 0)
370 |                        pure (w, if w < 0 then (-f) else f, 0)
371 |                    _ => Nothing
372 |                _ => Nothing
373 |
374 | public export
375 | null : String -> Bool
376 | null = (== "")
377 |