diff --git a/src/Cryptol/Testing/Concrete.hs b/src/Cryptol/Testing/Concrete.hs index 458e22d5..8c8af0e0 100644 --- a/src/Cryptol/Testing/Concrete.hs +++ b/src/Cryptol/Testing/Concrete.hs @@ -90,8 +90,8 @@ typeSize ty = (TCBit, _) -> Just 2 (TCInteger, _) -> Nothing (TCIntMod, [sz]) -> case tNoUser sz of - TCon (TC (TCNum n)) _ -> Just n - _ -> Nothing + TCon (TC (TCNum n)) _ | 0 < n -> Just n + _ -> Nothing (TCIntMod, _) -> Nothing (TCSeq, [sz,el]) -> case tNoUser sz of TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 5a13b4a4..24986c1a 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -72,6 +72,12 @@ randomValue ty = (TC TCInteger, []) -> Just randomInteger + (TC TCIntMod, [TCon (TC TCInf) []]) -> Just randomInteger + + (TC TCIntMod, [TCon (TC (TCNum n)) []]) + | 0 < n -> Just (randomIntMod n) + | otherwise -> Just randomInteger + (TC TCSeq, [TCon (TC TCInf) [], el]) -> do mk <- randomValue el return (randomStream mk) @@ -114,6 +120,11 @@ randomInteger _ g = (x, g2) = randomR (- 256^n, 256^n) g1 in (VInteger (integerLit x), g2) +randomIntMod :: (BitWord b w i, RandomGen g) => Integer -> Gen g b w i +randomIntMod modulus _ g = + let (x, g') = randomR (0, modulus-1) g + in (VInteger (integerLit x), g') + -- | Generate a random word of the given length (i.e., a value of type @[w]@) -- The size parameter is assumed to vary between 1 and 100, and we use -- it to generate smaller numbers first.