Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

A collection of character utilities, follows the namings
in Data.Char and is intended to be imported qualified.
Also, it is recommended you use the `OverloadedStrings`

extension to allow literal strings to be used as
symbolic-strings when working with symbolic characters
and strings.

Note that currently `SChar`

type only covers Latin1 (i.e., the first 256
characters), as opposed to Haskell's Unicode character support. However,
there is a pending SMTLib proposal to extend this set to Unicode, at
which point we will update these functions to match the implementations.
For details, see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

## Synopsis

- elem :: SChar -> SString -> SBool
- notElem :: SChar -> SString -> SBool
- ord :: SChar -> SInteger
- chr :: SInteger -> SChar
- toLower :: SChar -> SChar
- toUpper :: SChar -> SChar
- digitToInt :: SChar -> SInteger
- intToDigit :: SInteger -> SChar
- isControl :: SChar -> SBool
- isSpace :: SChar -> SBool
- isLower :: SChar -> SBool
- isUpper :: SChar -> SBool
- isAlpha :: SChar -> SBool
- isAlphaNum :: SChar -> SBool
- isPrint :: SChar -> SBool
- isDigit :: SChar -> SBool
- isOctDigit :: SChar -> SBool
- isHexDigit :: SChar -> SBool
- isLetter :: SChar -> SBool
- isMark :: SChar -> SBool
- isNumber :: SChar -> SBool
- isPunctuation :: SChar -> SBool
- isSymbol :: SChar -> SBool
- isSeparator :: SChar -> SBool
- isAscii :: SChar -> SBool
- isLatin1 :: SChar -> SBool
- isAsciiLetter :: SChar -> SBool
- isAsciiUpper :: SChar -> SBool
- isAsciiLower :: SChar -> SBool

# Occurrence in a string

elem :: SChar -> SString -> SBool Source #

Is the character in the string?

`>>>`

`:set -XOverloadedStrings`

`>>>`

Q.E.D.`prove $ \c -> c `elem` singleton c`

`>>>`

Q.E.D.`prove $ \c -> sNot (c `elem` "")`

notElem :: SChar -> SString -> SBool Source #

Is the character not in the string?

`>>>`

Q.E.D.`prove $ \c s -> c `elem` s .<=> sNot (c `notElem` s)`

# Conversion to/from

`SInteger`

chr :: SInteger -> SChar Source #

Conversion from an integer to a character.

`>>>`

Q.E.D.`prove $ \x -> 0 .<= x .&& x .< 256 .=> ord (chr x) .== x`

`>>>`

Q.E.D.`prove $ \x -> chr (ord x) .== x`

# Conversion to upper/lower case

toLower :: SChar -> SChar Source #

Convert to lower-case.

`>>>`

Q.E.D.`prove $ \c -> toLower (toLower c) .== toLower c`

`>>>`

Q.E.D.`prove $ \c -> isLower c .=> toLower (toUpper c) .== c`

toUpper :: SChar -> SChar Source #

Convert to upper-case. N.B. There are three special cases!

- The character 223 is special. It corresponds to the German Eszett, it is considered lower-case, and furthermore it's upper-case maps back to itself within our character-set. So, we leave it untouched.
- The character 181 maps to upper-case 924, which is beyond our character set. We leave it untouched. (This is the A with an acute accent.)
- The character 255 maps to upper-case 376, which is beyond our character set. We leave it untouched. (This is the non-breaking space character.)

`>>>`

Q.E.D.`prove $ \c -> toUpper (toUpper c) .== toUpper c`

`>>>`

Q.E.D.`prove $ \c -> isUpper c .=> toUpper (toLower c) .== c`

# Converting digits to ints and back

digitToInt :: SChar -> SInteger Source #

Convert a digit to an integer. Works for hexadecimal digits too. If the input isn't a digit, then return -1.

`>>>`

Q.E.D.`prove $ \c -> isDigit c .|| isHexDigit c .=> digitToInt c .>= 0 .&& digitToInt c .<= 15`

`>>>`

Q.E.D.`prove $ \c -> sNot (isDigit c .|| isHexDigit c) .=> digitToInt c .== -1`

intToDigit :: SInteger -> SChar Source #

Convert an an integer to a digit, inverse of `digitToInt`

. If the integer is out of
bounds, we return the arbitrarily chosen space character. Note that for hexadecimal
letters, we return the corresponding lowercase letter.

`>>>`

Q.E.D.`prove $ \i -> i .>= 0 .&& i .<= 15 .=> digitToInt (intToDigit i) .== i`

`>>>`

Q.E.D.`prove $ \i -> i .< 0 .|| i .> 15 .=> digitToInt (intToDigit i) .== -1`

`>>>`

Q.E.D.`prove $ \c -> digitToInt c .== -1 .<=> intToDigit (digitToInt c) .== literal ' '`

# Character classification

isControl :: SChar -> SBool Source #

Is this a control character? Control characters are essentially the non-printing characters.

isLower :: SChar -> SBool Source #

Is this a lower-case character?

`>>>`

Q.E.D.`prove $ \c -> isUpper c .=> isLower (toLower c)`

isUpper :: SChar -> SBool Source #

Is this an upper-case character?

`>>>`

Q.E.D.`prove $ \c -> sNot (isLower c .&& isUpper c)`

isAlpha :: SChar -> SBool Source #

Is this an alphabet character? That is lower-case, upper-case and title-case letters, plus letters of caseless scripts and modifiers letters.

isAlphaNum :: SChar -> SBool Source #

isPrint :: SChar -> SBool Source #

Is this a printable character? Essentially the complement of `isControl`

, with one
exception. The Latin-1 character 173 is neither control nor printable. Go figure.

`>>>`

Q.E.D.`prove $ \c -> c .== literal '\173' .|| isControl c .<=> sNot (isPrint c)`

isDigit :: SChar -> SBool Source #

Is this an ASCII digit, i.e., one of `0`

..`9`

. Note that this is a subset of `isNumber`

`>>>`

Q.E.D.`prove $ \c -> isDigit c .=> isNumber c`

isOctDigit :: SChar -> SBool Source #

Is this an Octal digit, i.e., one of `0`

..`7`

.

`>>>`

Q.E.D.`prove $ \c -> isOctDigit c .=> isDigit c`

isHexDigit :: SChar -> SBool Source #

Is this a Hex digit, i.e, one of `0`

..`9`

, `a`

..`f`

, `A`

..`F`

.

`>>>`

Q.E.D.`prove $ \c -> isHexDigit c .=> isAlphaNum c`

isLetter :: SChar -> SBool Source #

Is this an alphabet character. Note that this function is equivalent to `isAlpha`

.

`>>>`

Q.E.D.`prove $ \c -> isLetter c .<=> isAlpha c`

isMark :: SChar -> SBool Source #

Is this a mark? Note that the Latin-1 subset doesn't have any marks; so this function is simply constant false for the time being.

`>>>`

Q.E.D.`prove $ sNot . isMark`

isNumber :: SChar -> SBool Source #

Is this a number character? Note that this set contains not only the digits, but also
the codes for a few numeric looking characters like 1/2 etc. Use `isDigit`

for the digits `0`

through `9`

.

isPunctuation :: SChar -> SBool Source #

Is this a punctuation mark?

isSeparator :: SChar -> SBool Source #

Is this a separator?

`>>>`

Q.E.D.`prove $ \c -> isSeparator c .=> isSpace c`

# Subranges

isLatin1 :: SChar -> SBool Source #

Is this a Latin1 character? Note that this function is always true since `SChar`

corresponds
precisely to Latin1 for the time being.

`>>>`

Q.E.D.`prove isLatin1`

isAsciiLetter :: SChar -> SBool Source #

Is this an ASCII letter?

`>>>`

Q.E.D.`prove $ \c -> isAsciiLetter c .<=> isAsciiUpper c .|| isAsciiLower c`

isAsciiUpper :: SChar -> SBool Source #

Is this an ASCII Upper-case letter? i.e., `A`

thru `Z`

`>>>`

Q.E.D.`prove $ \c -> isAsciiUpper c .<=> ord c .>= ord (literal 'A') .&& ord c .<= ord (literal 'Z')`

`>>>`

Q.E.D.`prove $ \c -> isAsciiUpper c .<=> isAscii c .&& isUpper c`

isAsciiLower :: SChar -> SBool Source #

Is this an ASCII Lower-case letter? i.e., `a`

thru `z`

`>>>`

Q.E.D.`prove $ \c -> isAsciiLower c .<=> ord c .>= ord (literal 'a') .&& ord c .<= ord (literal 'z')`

`>>>`

Q.E.D.`prove $ \c -> isAsciiLower c .<=> isAscii c .&& isLower c`