0 | module Libraries.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 a given string by `n` spaces.
89 | public export
90 | indent : (n : Nat) -> String -> String
91 | indent n x = replicate n ' ' ++ x
92 |
93 | ||| Indent each line of a given string by `n` spaces.
94 | public export
95 | indentLines : (n : Nat) -> String -> String
96 | indentLines n str = (join "\n") $ map (Extra.indent n) $ lines str
97 |