sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Data.SBV.Char

Description

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

Occurrence in a string

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.


Is the character not in the string?

>>> prove $\c s -> c elem s .<=> sNot (c notElem s) Q.E.D.  Conversion to/from SInteger The ord of a character. 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 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.  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 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.  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. >>> 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

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

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

Is this a lower-case character?

>>> prove $\c -> isUpper c .=> isLower (toLower c) Q.E.D.  Is this an upper-case character? >>> prove$ \c -> sNot (isLower c .&& isUpper c)
Q.E.D.


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

Is this an isAlpha or isNumber.

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


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.  Is this an Octal digit, i.e., one of 0..7. >>> prove$ \c -> isOctDigit c .=> isDigit c
Q.E.D.


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

>>> prove $\c -> isHexDigit c .=> isAlphaNum c Q.E.D.  Is this an alphabet character. Note that this function is equivalent to isAlpha. >>> prove$ \c -> isLetter c .<=> isAlpha c
Q.E.D.


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.  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. Is this a punctuation mark? Is this a symbol? Is this a separator? >>> prove$ \c -> isSeparator c .=> isSpace c
Q.E.D.


Subranges

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

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.


Is this an ASCII letter?

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