Fails to compile with SBV 7.*

[taktoa]

Leaving this as a reminder to myself (since I am currently too busy to work on it) that I'd like to use this package in the future and should write a pull request updating it to sbv == 7.*.

When the sbv == 5.* constraint is removed, the compile fails with the following errors: compile log. This is with GHC == 8.0.2.

Other issues that I'll probably tackle (if you are okay with merging them):

• Use Text instead of String in public API
• Expose versions of these functions that take regular expression ASTs instead of just strings (since people may want to use this library with other regular expression syntaxes)
• Avoid using -XImplicitParams, especially for such trivial functions as genexWith and regexMatch

There are only a few packages that depend on regex-genex (hedgehog-gen-json, locked-poll, and quickcheck-regex), and I would be willing to write PRs so that these dependencies compile with these API changes.

[LeventErkok]

@audreyt @taktoa This would indeed be nice! I'll point out that the latest release of SBV have direct support for regular expressions. But they are weaker than Audrey's: For instance they don't support backreferences, or boundaries; and all the other awesome features.

If your regex doesn't involve these fancy features, then you can directly use SBV out-of-box to solve this problem:

{-# LANGUAGE OverloadedStrings #-}

import Data.SBV
import qualified Data.SBV.String as S
import Data.SBV.RegExp

gen = allSatWith z3{allSatMaxModelCount = Just 10} $ do
                s <- sString "s"

                constrain $ S.length s .== 5
                constrain $ s `match` (KPlus asciiLetter * "&" * KPlus digit)

                return (true :: SBool)

When I run this, I get:

*Main> gen
Solution #1:
  s = "M&000" :: String
Solution #2:
  s = "m&023" :: String
Solution #3:
  s = "u&023" :: String
Solution #4:
  s = "u&022" :: String
Solution #5:
  s = "t&022" :: String
Solution #6:
  s = "x&022" :: String
Solution #7:
  s = "y&022" :: String
Solution #8:
  s = "d&022" :: String
Solution #9:
  s = "e&022" :: String
Solution #10:
  s = "h&022" :: String
Search stopped since model count request was reached.

It would be really nice if someone tackled the more general regular-expressions that Audrey implemented directly in SBV. Patches are most welcome!