0 | module Data.String.Extra
  1 |
  2 | import Data.Nat
  3 | import Data.String
  4 |
  5 | %default total
  6 |
  7 | export infixl 5 +>
  8 | export infixr 5 <+
  9 |
 10 | ||| Adds a character to the end of the specified string.
 11 | |||
 12 | ||| ```idris example
 13 | ||| strSnoc "AB" 'C'
 14 | ||| ```
 15 | ||| ```idris example
 16 | ||| strSnoc "" 'A'
 17 | ||| ```
 18 | public export
 19 | strSnoc : String -> Char -> String
 20 | strSnoc s c = s ++ (singleton c)
 21 |
 22 | ||| Alias of `strSnoc`
 23 | |||
 24 | ||| ```idris example
 25 | ||| "AB" +> 'C'
 26 | ||| ```
 27 | public export
 28 | (+>) : String -> Char -> String
 29 | (+>) = strSnoc
 30 |
 31 | ||| Alias of `strCons`
 32 | |||
 33 | ||| ```idris example
 34 | ||| 'A' <+ "AB"
 35 | ||| ```
 36 | public export
 37 | (<+) : Char -> String -> String
 38 | (<+) = strCons
 39 |
 40 | ||| Take the first `n` characters from a string. Returns the whole string
 41 | ||| if it's too short.
 42 | public export
 43 | take : (n : Nat) -> (input : String) -> String
 44 | take n str = substr Z n str
 45 |
 46 | ||| Take the last `n` characters from a string. Returns the whole string
 47 | ||| if it's too short.
 48 | public export
 49 | takeLast : (n : Nat) -> (input : String) -> String
 50 | takeLast n str with (length str)
 51 |   takeLast n str | len with (isLTE n len)
 52 |     takeLast n str | len | Yes prf = substr (len `minus` n) len str
 53 |     takeLast n str | len | No contra = str
 54 |
 55 | ||| Remove the first `n` characters from a string. Returns the empty string if
 56 | ||| the input string is too short.
 57 | public export
 58 | drop : (n : Nat) -> (input : String) -> String
 59 | drop n str = substr n (length str) str
 60 |
 61 | ||| Remove the last `n` characters from a string. Returns the empty string if
 62 | ||| the input string is too short.
 63 | public export
 64 | dropLast : (n : Nat) -> (input : String) -> String
 65 | dropLast n str = reverse (drop n (reverse str))
 66 |
 67 | ||| Remove the first and last `n` characters from a string. Returns the empty
 68 | ||| string if the input string is too short.
 69 | public export
 70 | shrink : (n : Nat) -> (input : String) -> String
 71 | shrink n str = dropLast n (drop n str)
 72 |
 73 | ||| Concatenate the strings from a `Foldable` containing strings, separated by
 74 | ||| the given string.
 75 | public export
 76 | join : (sep : String) -> Foldable t => (xs : t String) -> String
 77 | join sep xs = drop (length sep)
 78 |                    (foldl (\acc, x => acc ++ sep ++ x) "" xs)
 79 |
 80 | ||| Get a character from a string if the string is long enough.
 81 | public export
 82 | index : (n : Nat) -> (input : String) -> Maybe Char
 83 | index n str with (unpack str)
 84 |   index n str | [] = Nothing
 85 |   index Z str | (x :: xs) = Just x
 86 |   index (S n) str | (x :: xs) = index n str | xs
 87 |
 88 | ||| Indent each line of a given string by `n` spaces.
 89 | public export
 90 | indentLines : (n : Nat) -> String -> String
 91 | indentLines n str = unlines $ map (indent n) $ lines str
 92 |
 93 | ||| Left-justify a string to the given length, using the
 94 | ||| specified fill character on the right.
 95 | export
 96 | justifyLeft : Nat -> Char -> String -> String
 97 | justifyLeft n c s = s ++ replicate (n `minus` length s) c
 98 |
 99 | ||| Right-justify a string to the given length, using the
100 | ||| specified fill character on the left.
101 | export
102 | justifyRight : Nat -> Char -> String -> String
103 | justifyRight n c s = replicate (n `minus` length s) c ++ s
104 |
105 | ||| Truncates a string to the given length.
106 | ||| If the given string is longer, replace first characters with given prefix.
107 | |||
108 | ||| Say, `leftEllipsis 5 ".." "abcdefgh"` should give `"..fgh"` and
109 | ||| `leftEllipsis 5 "" "abcdefgh"` should give `"defgh"`.
110 | |||
111 | ||| Notice, that the resulting string can be longer than max length if the prefix is longer.
112 | export
113 | leftEllipsis : (maxLen : Nat) -> (pref : String) -> String -> String
114 | leftEllipsis maxLen pref str = do
115 |  let len = length str
116 |  case len `isLTE` maxLen of
117 |    Yes _ => str
118 |    No _  => pref ++ substr ((len + length pref) `minus` maxLen) len str
119 |
120 | ||| Truncates a string to the given length.
121 | ||| If the given string is longer, replace last characters with given suffix.
122 | |||
123 | ||| Say, `rightEllipsis 5 ".." "abcdefgh"` should give `"abc.."` and
124 | ||| `rightEllipsis 5 "" "abcdefgh"` should give `"abcde"`.
125 | |||
126 | ||| Notice, that the resulting string can be longer than max length if the suffix is longer.
127 | export
128 | rightEllipsis : (maxLen : Nat) -> (suff : String) -> String -> String
129 | rightEllipsis maxLen suff str = do
130 |   let len = length str
131 |   case len `isLTE` maxLen of
132 |     Yes _ => str
133 |     No _  => take (maxLen `minus` length suff) str ++ suff
134 |