IdrisDoc: Prelude.Strings

Prelude.Strings

words' : List Char -> List (List Char)

Splits a character list into a list of whitespace separated character lists.

words' (unpack " A B C  D E   ")
words : String -> List String

Splits a string into a list of whitespace separated strings.

words " A B C  D E   "
unwords' : List (List Char) -> List Char

Joins the character lists by spaces into a single character list.

unwords' [['A'], ['B', 'C'], ['D'], ['E']]
unwords : List String -> String

Joins the strings by spaces into a single string.

unwords ["A", "BC", "D", "E"]
unpack : String -> List Char

Turns a string into a list of characters.

unpack "ABC"
unlines' : List (List Char) -> List Char

Joins the character lists by newlines into a single character list.

unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]
unlines : List String -> String

Joins the strings by newlines into a single string.

unlines ["line", "line2", "ln3", "D"]
trim : String -> String

Removes whitespace (determined by 'isSpace') from
the start and end of the string.

trim " A\nB C "
toUpper : String -> String

Uppercases all characters in the string.

toUpper "aBc12!"
toLower : String -> String

Lowercases all characters in the string.

toLower "aBc12!"
substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String

Returns a substring of a given string

index

The (zero based) index of the string to extract. If this is
beyond the end of the string, the function returns the empty
string.

len

The desired length of the substring. Truncated if this exceeds
the length of the input.

subject

The string to return a portion of

strTail' : (x : String) -> (not (x == "") = True) -> String

Version of 'strTail' that statically verifies that the string is not empty.

strTail : String -> String

Returns the characters specified after the head of the string.

Doesn't work for empty strings.

strTail "AB"
strTail "A"
strM : (x : String) -> StrM x
strIndex : String -> Int -> Char

Returns the nth character (starting from 0) of the specified string.

Precondition: '0 < i < length s' for 'strIndex s i'.

strIndex "AB" 1
strHead' : (x : String) -> (not (x == "") = True) -> Char

Version of 'strHead' that statically verifies that the string is not empty.

strHead : String -> Char

Returns the first character in the specified string.

Doesn't work for empty strings.

strHead "A"
strCons : Char -> String -> String

Adds a character to the front of the specified string.

strCons 'A' "B"
strCons 'A' ""
split : (Char -> Bool) -> String -> List String

Splits the string into parts with the predicate
indicating separator characters.

split (== '.') ".AB.C..D"
span : (Char -> Bool) -> String -> (String, String)

Splits the string into a part before the predicate
returns False and the rest of the string.

span (/= 'C') "ABCD"
span (/= 'C') "EFGH"
singleton : Char -> String

Creates a string of a single character.

singleton 'A'
reverse : String -> String

Reverses the elements within a String.

reverse "ABC"
reverse ""
pack : Foldable t => t Char -> String

Turns a Foldable of characters into a string.

nullStr : String -> IO Bool

Check if a supposed string was actually a null pointer

nullPtr : Ptr -> IO Bool

Check if a foreign pointer is null

null : Ptr
newStringBuffer : (len : Int) -> IO StringBuffer

Create a buffer for a string with maximum length len

ltrim : String -> String

Removes whitespace (determined by 'isSpace') from
the start of the string.

ltrim " A\nB"
ltrim " \nAB"
lines' : List Char -> List (List Char)

Splits a character list into a list of newline separated character lists.

lines' (unpack "\rA BC\nD\r\nE\n")
lines : String -> List String

Splits a string into a list of newline separated strings.

lines  "\rA BC\nD\r\nE\n"
length : String -> Nat

Returns the length of the string.

length ""
length "ABC"
isSuffixOf : String -> String -> Bool
isPrefixOf : String -> String -> Bool
isInfixOf : String -> String -> Bool
getStringFromBuffer : StringBuffer -> IO String

Get the string from a string buffer. The buffer is invalid after
this.

foldr1 : (a -> a -> a) -> List a -> a
foldl1 : (a -> a -> a) -> List a -> a
break : (Char -> Bool) -> String -> (String, String)

Splits the string into a part before the predicate
returns True and the rest of the string.

break (== 'C') "ABCD"
break (== 'C') "EFGH"
addToStringBuffer : StringBuffer -> String -> IO ()

Append a string to the end of a string buffer

data StringBuffer : Type

A preallocated buffer for building a String. This allows a function (in IO)
to allocate enough space for a string which will be built from smaller
pieces without having to allocate at every step.
To build a string using a StringBuffer, see newStringBuffer,
addToStringBuffer and getStringFromBuffer.

MkString : Ptr -> StringBuffer
data StrM : String -> Type
StrNil : StrM ""
StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
(++) : String -> String -> String

Appends two strings together.

"AB" ++ "C"
Fixity
Left associative, precedence 7