sbv-8.10: 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

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