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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
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.

`SChar` type only covers all unicode characters, following the specification in http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml. However, some of the recognizers only support the Latin1 subset, suffixed by `L1`. The reason for this is that there is no performant way of performing these functions for the entire unicode set. As SMTLib's capabilities increase, we will provide full unicode versions as well.

Synopsis

- elem :: SChar -> SString -> SBool
- notElem :: SChar -> SString -> SBool
- ord :: SChar -> SInteger
- chr :: SInteger -> SChar
- toLowerL1 :: SChar -> SChar
- toUpperL1 :: SChar -> SChar
- digitToInt :: SChar -> SInteger
- intToDigit :: SInteger -> SChar
- isControlL1 :: SChar -> SBool
- isSpaceL1 :: SChar -> SBool
- isLowerL1 :: SChar -> SBool
- isUpperL1 :: SChar -> SBool
- isAlphaL1 :: SChar -> SBool
- isAlphaNumL1 :: SChar -> SBool
- isPrintL1 :: SChar -> SBool
- isDigit :: SChar -> SBool
- isOctDigit :: SChar -> SBool
- isHexDigit :: SChar -> SBool
- isLetterL1 :: SChar -> SBool
- isMarkL1 :: SChar -> SBool
- isNumberL1 :: SChar -> SBool
- isPunctuationL1 :: SChar -> SBool
- isSymbolL1 :: SChar -> SBool
- isSeparatorL1 :: SChar -> SBool
- isAscii :: SChar -> SBool
- isLatin1 :: 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

toLowerL1 :: SChar -> SChar Source #

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

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

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

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

isLowerL1 :: SChar -> SBool Source #

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

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

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

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

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

isDigit :: SChar -> SBool Source #

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

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

isHexDigit :: SChar -> SBool Source #

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

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

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

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

isPunctuationL1 :: SChar -> SBool Source #

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

isSymbolL1 :: SChar -> SBool Source #

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

isSeparatorL1 :: SChar -> SBool Source #

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

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

isLatin1 :: SChar -> SBool Source #

Is this a Latin1 character?

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