module Language.Boogie.Generator where
import Control.Monad.Identity hiding (join)
import Control.Monad.Stream
import System.Random
data Generator m = Generator {
genBool :: m Bool,
genInteger :: m Integer,
genIndex :: Int -> m Int
}
defaultGenerator :: Generator Identity
defaultGenerator = Generator {
genBool = Identity False,
genInteger = Identity 0,
genIndex = Identity . const 0
}
exhaustiveGenerator :: Maybe Integer -> Generator Stream
exhaustiveGenerator mBound = Generator {
genBool = return False `mplus` return True,
genInteger = case mBound of
Nothing -> allIntegers
Just b -> fromInterval $ intInterval b,
genIndex = \n -> fromInterval $ case mBound of
Nothing -> natInterval n
Just b -> natInterval $ fromInteger (b `min` toInteger n)
}
where
allIntegers = fromList [0, 1..] `mplus` fromList [1..]
fromInterval (a, b)
| b < a = mzero
| a >= 0 || b <= 0 = fromList [a..b]
| otherwise = fromList [0, 1..a] `mplus` fromList [1..b]
randomGenerator :: StdGen -> Maybe Integer -> Generator Stream
randomGenerator rGen mBound = Generator {
genBool = fromList $ randoms rGen,
genInteger = fromList $ case mBound of
Nothing -> randoms rGen
Just b -> randomRs (intInterval b) rGen,
genIndex = \n -> fromList $ case mBound of
Nothing -> randomRs (natInterval n) rGen
Just b -> randomRs (natInterval $ fromInteger (b `min` toInteger n)) rGen
}
intInterval n = let n2 = n `div` 2 in (n2, n n2 1)
natInterval n = (0, n 1)
fromList :: [a] -> Stream a
fromList xs = foldr1 mplus (map return xs)