Data.SBV.Char

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

Occurrence in a string

elem :: SChar -> SString -> SBool

Is the character in the string?

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

notElem :: SChar -> SString -> SBool

Is the character not in the string?

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

Conversion to/from SInteger

ord :: SChar -> SInteger

The ord of a character.

chr :: SInteger -> SChar

Conversion from an integer to a character.

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

Conversion to upper/lower case

toLower :: SChar -> SChar

Convert to lower-case.

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

toUpper :: SChar -> SChar

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.)

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

Converting digits to ints and back

digitToInt :: SChar -> SInteger

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

>>> 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
Q.E.D.

intToDigit :: SInteger -> SChar

Convert 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.

>>> 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 ' '
Q.E.D.

Character classification

isControl :: SChar -> SBool

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

isSpace :: SChar -> SBool

Is this white-space? That is, one of "tnvfr 160".

isLower :: SChar -> SBool

Is this a lower-case character?

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

isUpper :: SChar -> SBool

Is this an upper-case character?

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

isAlpha :: SChar -> SBool

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

Is this an isAlpha or isNumber.

>>> prove $ \c -> isAlphaNum c .<=> isAlpha c .|| isNumber c
Q.E.D.

isPrint :: SChar -> SBool

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.

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

isDigit :: SChar -> SBool

Is this an ASCII digit, i.e., one of 0..9. Note that this is a subset of isNumber

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

isOctDigit :: SChar -> SBool

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

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

isHexDigit :: SChar -> SBool

Is this a Hex digit, i.e, one of 0..9, a..f, A..F.

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

isLetter :: SChar -> SBool

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

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

isMark :: SChar -> SBool

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.

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

isNumber :: SChar -> SBool

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

Is this a punctuation mark?

isSymbol :: SChar -> SBool

Is this a symbol?

isSeparator :: SChar -> SBool

Is this a separator?

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

Subranges

isAscii :: SChar -> SBool

Is this an ASCII character, i.e., the first 128 characters.

isLatin1 :: SChar -> SBool

Is this a Latin1 character? Note that this function is always true since SChar corresponds precisely to Latin1 for the time being.

>>> prove isLatin1
Q.E.D.

isAsciiLetter :: SChar -> SBool

Is this an ASCII letter?

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

isAsciiUpper :: SChar -> SBool

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

>>> 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
Q.E.D.

isAsciiLower :: SChar -> SBool

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

>>> 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
Q.E.D.