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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Char

Contents

- Occurrence in a string
- Conversion to/from `SInteger`
- Conversion to upper/lower case
- Converting digits to ints and back
- Character classification
- Subranges

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

- 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
    >>> prove $ \c -> c `elem` singleton c
    Q.E.D.
    >>> prove $ \c -> sNot (c `elem` "")
    Q.E.D.

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

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 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 -> sNot (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 -> sNot (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 .<=> sNot (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 $ sNot . 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.