Regular expressions. Note that regular expressions themselves are concrete, but the match function from the RegExpMatchable class can check membership against a symbolic string/character. Also, we are preferring a datatype approach here, as opposed to coming up with some string-representation; there are way too many alternatives already so inventing one isn't a priority. Please get in touch if you would like a parser for this type as it might be easier to use.

Matchable class. Things we can match against a RegExp. (TODO: Currently SBV does *not* optimize this call if the input is a concrete string or a character, but rather directly calls down to the solver. We might want to perform the operation on the Haskell side for performance reasons, should this become important.)

For instance, you can generate valid-looking phone numbers like this:

>>> :set -XOverloadedStrings
>>> let dig09 = Range '0' '9'
>>> let dig19 = Range '1' '9'
>>> let pre   = dig19 * Loop 2 2 dig09
>>> let post  = dig19 * Loop 3 3 dig09
>>> let phone = pre * "-" * post
>>> sat $ \s -> (s :: SString) `match` phone
Satisfiable. Model:
  s0 = "224-4222" :: String

A literal regular-expression, matching the given string exactly. Note that with OverloadedStrings extension, you can simply use a Haskell string to mean the same thing, so this function is rarely needed.

>>> prove $ \(s :: SString) -> s `match` exactly "LITERAL" <=> s .== "LITERAL"
Q.E.D.

Helper to define a character class.

>>> prove $ \(c :: SChar) -> c `match` oneOf "ABCD" <=> bAny (c .==) (map literal "ABCD")
Q.E.D.

Recognize a newline. Also includes carriage-return and form-feed.

>>> newline
(re.union (str.to.re "\n") (str.to.re "\r") (str.to.re "\f"))
>>> prove $ \c -> c `match` newline ==> isSpace c
Q.E.D.

Recognize white-space, but without a new line.

>>> whiteSpaceNoNewLine
(re.union (str.to.re "\x09") (re.union (str.to.re "\v") (str.to.re "\xa0") (str.to.re " ")))
>>> prove $ \c -> c `match` whiteSpaceNoNewLine ==> c `match` whiteSpace &&& c ./= literal '\n'
Q.E.D.

Recognize white space.

>>> prove $ \c -> c `match` whiteSpace ==> isSpace c
Q.E.D.

Recognize a tab.

>>> tab
(str.to.re "\x09")
>>> prove $ \c -> c `match` tab ==> c .== literal '\t'
Q.E.D.

Recognize a punctuation character. Anything that satisfies the predicate isPunctuation will be accepted. (TODO: Will need modification when we move to unicode.)

>>> prove $ \c -> c `match` punctuation ==> isPunctuation c
Q.E.D.

Recognize an alphabet letter, i.e., A..Z, a..z.

>>> asciiLetter
(re.union (re.range "a" "z") (re.range "A" "Z"))
>>> prove $ \c -> c `match` asciiLetter <=> toUpper c `match` asciiLetter
Q.E.D.
>>> prove $ \c -> c `match` asciiLetter <=> toLower c `match` asciiLetter
Q.E.D.

Recognize an ASCII lower case letter

>>> asciiLower
(re.range "a" "z")
>>> prove $ \c -> (c :: SChar) `match` asciiLower  ==> c `match` asciiLetter
Q.E.D.
>>> prove $ \c -> c `match` asciiLower  ==> toUpper c `match` asciiUpper
Q.E.D.
>>> prove $ \c -> c `match` asciiLetter ==> toLower c `match` asciiLower
Q.E.D.

Recognize an upper case letter

>>> asciiUpper
(re.range "A" "Z")
>>> prove $ \c -> (c :: SChar) `match` asciiUpper  ==> c `match` asciiLetter
Q.E.D.
>>> prove $ \c -> c `match` asciiUpper  ==> toLower c `match` asciiLower
Q.E.D.
>>> prove $ \c -> c `match` asciiLetter ==> toUpper c `match` asciiUpper
Q.E.D.

Recognize a digit. One of 0..9.

>>> digit
(re.range "0" "9")
>>> prove $ \c -> c `match` digit <=> let v = digitToInt c in 0 .<= v &&& v .< 10
Q.E.D.

Recognize an octal digit. One of 0..7.

>>> octDigit
(re.range "0" "7")
>>> prove $ \c -> c `match` octDigit <=> let v = digitToInt c in 0 .<= v &&& v .< 8
Q.E.D.
>>> prove $ \(c :: SChar) -> c `match` octDigit ==> c `match` digit
Q.E.D.

Recognize a hexadecimal digit. One of 0..9, a..f, A..F.

>>> hexDigit
(re.union (re.range "0" "9") (re.range "a" "f") (re.range "A" "F"))
>>> prove $ \c -> c `match` hexDigit <=> let v = digitToInt c in 0 .<= v &&& v .< 16
Q.E.D.
>>> prove $ \(c :: SChar) -> c `match` digit ==> c `match` hexDigit
Q.E.D.

Recognize a decimal number.

>>> decimal
(re.+ (re.range "0" "9"))
>>> prove $ \s -> (s::SString) `match` decimal ==> bnot (s `match` KStar asciiLetter)
Q.E.D.

Recognize an octal number. Must have a prefix of the form 0o/0O.

>>> octal
(re.++ (re.union (str.to.re "0o") (str.to.re "0O")) (re.+ (re.range "0" "7")))
>>> prove $ \s -> s `match` octal ==> bAny (.== take 2 s) ["0o", "0O"]
Q.E.D.

Recognize a hexadecimal number. Must have a prefix of the form 0x/0X.

>>> hexadecimal
(re.++ (re.union (str.to.re "0x") (str.to.re "0X")) (re.+ (re.union (re.range "0" "9") (re.range "a" "f") (re.range "A" "F"))))
>>> prove $ \s -> s `match` hexadecimal ==> bAny (.== take 2 s) ["0x", "0X"]
Q.E.D.

Recognize a floating point number. The exponent part is optional if a fraction is present. The exponent may or may not have a sign.

>>> prove $ \s -> s `match` floating ==> length s .>= 3
Q.E.D.

For the purposes of this regular expression, an identifier consists of a letter followed by zero or more letters, digits, underscores, and single quotes. The first letter must be lowercase.

>>> prove $ \s -> s `match` identifier ==> isAsciiLower (head s)
Q.E.D.
>>> prove $ \s -> s `match` identifier ==> length s .>= 1
Q.E.D.