
   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 . swfe . 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, Double, Integer) -> Maybe Double
 342 |     mkDouble (Just (s, w, f, e)) = let ex = intPow 10 e in
 343 |                                 Just $ s * (w * ex + f * ex)
 344 |     mkDouble Nothing = Nothing
 345 | 
 346 | 
 347 |     wfe : String -> Maybe (Double, Double, Integer)
 348 |     wfe cs = case split (== '.') cs of
 349 |                (wholeAndExp ::: []) =>
 350 |                  case split (\c => c == 'e' || c == 'E') wholeAndExp of
 351 |                    (whole:::exp::[]) =>
 352 |                      do
 353 |                        w <- cast {from=Integer} <$> parsePositive whole
 354 |                        e <- parseInteger exp
 355 |                        pure (w, 0, e)
 356 |                    (whole:::[]) =>
 357 |                      do
 358 |                        w <- cast {from=Integer} <$> parsePositive whole
 359 |                        pure (w, 0, 0)
 360 |                    _ => Nothing
 361 |                (whole:::fracAndExp::[]) =>
 362 |                  case split (\c => c == 'e' || c == 'E') fracAndExp of
 363 |                    ("":::exp::[]) => Nothing
 364 |                    (frac:::exp::[]) =>
 365 |                      do
 366 |                        w <- cast {from=Integer} <$> parsePositive whole
 367 |                        f <- (/ (natpow 10 (length frac))) <$>
 368 |                             (cast <$> parseNumWithoutSign (unpack frac) 0)
 369 |                        e <- parseInteger exp
 370 |                        pure (w, if w < 0 then (-f) else f, e)
 371 |                    (frac:::[]) =>
 372 |                      do
 373 |                        w <- cast {from=Integer} <$> parsePositive whole
 374 |                        f <- (/ (natpow 10 (length frac))) <$>
 375 |                             (cast <$> parseNumWithoutSign (unpack frac) 0)
 376 |                        pure (w, if w < 0 then (-f) else f, 0)
 377 |                    _ => Nothing
 378 |                _ => Nothing
 379 | 
 380 |     -- sign, whole, fractional, exponent
 381 |     swfe : String -> Maybe (Double, Double, Double, Integer)
 382 |     swfe cs = if isPrefixOf "-" cs
 383 |              then (-1.0, ) <$> wfe (assert_total $ strTail cs)
 384 |              else ( 1.0, ) <$> wfe cs
 385 | 
 386 | public export
 387 | null : String -> Bool
 388 | null = (== "")
 389 |