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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Char

Contents

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

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

Is the character in the string?

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

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

Is the character not in the string?

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

Conversion to/from SInteger

ord :: SChar -> SInteger Source #

The ord of a character.

chr :: SInteger -> SChar Source #

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 Source #

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

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 -> bnot (isDigit c ||| isHexDigit c) ==> digitToInt c .== -1
Q.E.D.

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.

>>> 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 Source #

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

isSpace :: SChar -> SBool Source #

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

isLower :: SChar -> SBool Source #

Is this a lower-case character?

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

isUpper :: SChar -> SBool Source #

Is this an upper-case character?

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

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 #

Is this an isAlpha or isNumber.

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

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.

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

isDigit :: SChar -> SBool Source #

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 Source #

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

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

isHexDigit :: SChar -> SBool Source #

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 Source #

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

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

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?

isSymbol :: SChar -> SBool Source #

Is this a symbol?

isSeparator :: SChar -> SBool Source #

Is this a separator?

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

Subranges

isAscii :: SChar -> SBool Source #

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

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.

>>> prove isLatin1
Q.E.D.

isAsciiLetter :: SChar -> SBool Source #

Is this an ASCII letter?

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

isAsciiUpper :: SChar -> SBool Source #

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 Source #

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.