Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
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` 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
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.
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 #
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?
isSeparator :: SChar -> SBool Source #
Is this a separator?
>>>
prove $ \c -> isSeparator c ==> isSpace c
Q.E.D.
Subranges
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.