git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/libs/contrib/Data/String/Extra.idr
72 lines 2.2 kB history raw
1module Data.String.Extra
3infixl 5 +>
4infixr 5 <+
6||| Adds a character to the end of the specified string.
7|||
8||| ```idris example
9||| strSnoc "AB" 'C'
10||| ```
11||| ```idris example
12||| strSnoc "" 'A'
13||| ```
14strSnoc : String -> Char -> String
15strSnoc s c = s ++ (singleton c)
17||| Alias of `strSnoc`
18|||
19||| ```idris example
20||| "AB" +> 'C'
21||| ```
22(+>) : String -> Char -> String
23(+>) = strSnoc
25||| Alias of `strCons`
26|||
27||| ```idris example
28||| 'A' <+ "AB"
29||| ```
30(<+) : Char -> String -> String
31(<+) = strCons
33||| Take the first `n` characters from a string. Returns the whole string
34||| if it's too short.
35take : (n : Nat) -> (input : String) -> String
36take n str = substr Z n str
38||| Take the last `n` characters from a string. Returns the whole string
39||| if it's too short.
40takeLast : (n : Nat) -> (input : String) -> String
41takeLast n str with (length str)
42 takeLast n str | len with (isLTE n len)
43 takeLast n str | len | Yes prf = substr (len - n) len str
44 takeLast n str | len | No contra = str
46||| Remove the first `n` characters from a string. Returns the empty string if
47||| the input string is too short.
48drop : (n : Nat) -> (input : String) -> String
49drop n str = substr n (length str) str
51||| Remove the last `n` characters from a string. Returns the empty string if
52||| the input string is too short.
53dropLast : (n : Nat) -> (input : String) -> String
54dropLast n str = reverse (drop n (reverse str))
56||| Remove the first and last `n` characters from a string. Returns the empty
57||| string if the input string is too short.
58shrink : (n : Nat) -> (input : String) -> String
59shrink n str = dropLast n (drop n str)
61||| Concatenate the strings from a `Foldable` containing strings, separated by
62||| the given string.
63join : (sep : String) -> Foldable t => (xs : t String) -> String
64join sep xs = drop (length sep)
65 (foldl (\acc, x => acc ++ sep ++ x) "" xs)
67||| Get a character from a string if the string is long enough.
68index : (n : Nat) -> (input : String) -> Maybe Char
69index n str with (unpack str)
70 index n str | [] = Nothing
71 index Z str | (x :: xs) = Just x
72 index (S n) str | (x :: xs) = index n str | xs