This library contains a model for DepTyCheck which can be used to generate random regular expressions. Currently, only POSIX ERE syntax is supported.
Usage example:
import Control.Monad.Random
import Data.Fuel
import Data.List.Lazy
import Data.Vect
import Random.Regex
import System
import System.Random.Pure.StdGen
import Test.DepTyCheck.Gen
main : IO ()
main = do
seed <- initSeed
printLn seed
let Just regexModel : Maybe (Regex ERE) :=
evalRandom seed $ unGen' $ genRegex (limit 3) ERE
| Nothing => die "Error: can't generate a regex"
printLn regexModel
let examples := unGenTryN 10 seed $ do
exemplify (limit 10) regexModel
Lazy.for_ examples putStrLn
genRegex regexFuel syntax generates a regular expression based on the given syntax. The larger the regexFuel, the more complex the result tends to be on average.
exemplify exampleFuel regex generates a random string that matches the given regex. Due to some simplifications in the model, it can rarely produce invalid output. The exampleFuel parameter influences the average length of the generated string.