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

toLowerL1 :: SChar -> SChar

Convert to lower-case. Only works for the Latin1 subset, otherwise returns its argument unchanged.

>>> prove $ \c -> toLowerL1 (toLowerL1 c) .== toLowerL1 c
Q.E.D.
>>> prove $ \c -> isLowerL1 c .&& c `notElem` "\181\255" .=> toLowerL1 (toUpperL1 c) .== c
Q.E.D.

toUpperL1 :: SChar -> SChar

Convert to upper-case. Only works for the Latin1 subset, otherwise returns its argument unchanged.

>>> prove $ \c -> toUpperL1 (toUpperL1 c) .== toUpperL1 c
Q.E.D.
>>> prove $ \c -> isUpperL1 c .=> toUpperL1 (toLowerL1 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

isControlL1 :: SChar -> SBool

Is this a control character? Control characters are essentially the non-printing characters. Only works for the Latin1 subset, otherwise returns sFalse.

isSpaceL1 :: SChar -> SBool

Is this white-space? Only works for the Latin1 subset, otherwise returns sFalse.

isLowerL1 :: SChar -> SBool

Is this a lower-case character? Only works for the Latin1 subset, otherwise returns sFalse.

>>> prove $ \c -> isUpperL1 c .=> isLowerL1 (toLowerL1 c)
Q.E.D.

isUpperL1 :: SChar -> SBool

Is this an upper-case character? Only works for the Latin1 subset, otherwise returns sFalse.

>>> prove $ \c -> sNot (isLowerL1 c .&& isUpperL1 c)
Q.E.D.

isAlphaL1 :: 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. Only works for the Latin1 subset, otherwise returns sFalse.

isAlphaNumL1 :: SChar -> SBool

Is this an alphabetical character or a digit? Only works for the Latin1 subset, otherwise returns sFalse.

>>> prove $ \c -> isAlphaNumL1 c .<=> isAlphaL1 c .|| isNumberL1 c
Q.E.D.

isPrintL1 :: SChar -> SBool

Is this a printable character? Only works for the Latin1 subset, otherwise returns sFalse.

isDigit :: SChar -> SBool

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

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

isOctDigit :: SChar -> SBool

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

isHexDigit :: SChar -> SBool

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

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

isLetterL1 :: SChar -> SBool

Is this an alphabet character. Only works for the Latin1 subset, otherwise returns sFalse.

>>> prove $ \c -> isLetterL1 c .<=> isAlphaL1 c
Q.E.D.

isMarkL1 :: SChar -> SBool

Is this a mark? Only works for the Latin1 subset, otherwise returns sFalse.

Note that there are no marks in the Latin1 set, so this function always returns false!

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

isNumberL1 :: SChar -> SBool

Is this a number character? Only works for the Latin1 subset, otherwise returns sFalse.

isPunctuationL1 :: SChar -> SBool

Is this a punctuation mark? Only works for the Latin1 subset, otherwise returns sFalse.

isSymbolL1 :: SChar -> SBool

Is this a symbol? Only works for the Latin1 subset, otherwise returns sFalse.

isSeparatorL1 :: SChar -> SBool

Is this a separator? Only works for the Latin1 subset, otherwise returns sFalse.

>>> prove $ \c -> isSeparatorL1 c .=> isSpaceL1 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?

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 .&& isUpperL1 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 .&& isLowerL1 c
Q.E.D.