git.iko.soy/Idris-dev
on 229331c help sign in
Idris-dev/libs/contrib/Data/String/Extra.idr
88 lines 2.6 kB history raw
1module Data.String.Extra
3%access public export
4%default total
6infixl 5 +>
7infixr 5 <+
9||| Adds a character to the end of the specified string.
10|||
11||| ```idris example
12||| strSnoc "AB" 'C'
13||| ```
14||| ```idris example
15||| strSnoc "" 'A'
16||| ```
17strSnoc : String -> Char -> String
18strSnoc s c = s ++ (singleton c)
20||| Alias of `strSnoc`
21|||
22||| ```idris example
23||| "AB" +> 'C'
24||| ```
25(+>) : String -> Char -> String
26(+>) = strSnoc
28||| Alias of `strCons`
29|||
30||| ```idris example
31||| 'A' <+ "AB"
32||| ```
33(<+) : Char -> String -> String
34(<+) = strCons
36||| Take the first `n` characters from a string. Returns the whole string
37||| if it's too short.
38take : (n : Nat) -> (input : String) -> String
39take n str = substr Z n str
41||| Take the last `n` characters from a string. Returns the whole string
42||| if it's too short.
43takeLast : (n : Nat) -> (input : String) -> String
44takeLast n str with (length str)
45 takeLast n str | len with (isLTE n len)
46 takeLast n str | len | Yes prf = substr (len - n) len str
47 takeLast n str | len | No contra = str
49||| Remove the first `n` characters from a string. Returns the empty string if
50||| the input string is too short.
51drop : (n : Nat) -> (input : String) -> String
52drop n str = substr n (length str) str
54||| Remove the last `n` characters from a string. Returns the empty string if
55||| the input string is too short.
56dropLast : (n : Nat) -> (input : String) -> String
57dropLast n str = reverse (drop n (reverse str))
59||| Remove the first and last `n` characters from a string. Returns the empty
60||| string if the input string is too short.
61shrink : (n : Nat) -> (input : String) -> String
62shrink n str = dropLast n (drop n str)
64||| Concatenate the strings from a `Foldable` containing strings, separated by
65||| the given string.
66join : (sep : String) -> Foldable t => (xs : t String) -> String
67join sep xs = drop (length sep)
68 (foldl (\acc, x => acc ++ sep ++ x) "" xs)
70||| Get a character from a string if the string is long enough.
71index : (n : Nat) -> (input : String) -> Maybe Char
72index n str with (unpack str)
73 index n str | [] = Nothing
74 index Z str | (x :: xs) = Just x
75 index (S n) str | (x :: xs) = index n str | xs
77||| Produce a string by repeating the character `c` `n` times.
78replicate : (n : Nat) -> (c : Char) -> String
79replicate n c = pack $ replicate n c
81||| Indent a given string by `n` spaces.
82indent : (n : Nat) -> String -> String
83indent n x = replicate n ' ' ++ x
85||| Indent each line of a given string by `n` spaces.
86indentLines : (n : Nat) -> String -> String
87indentLines n str = unlines $ map (indent n) $ lines str