|
| 1 | +-- editorconfig-checker-disable |
| 2 | +{-# LANGUAGE OverloadedStrings #-} |
| 3 | +{-# LANGUAGE ViewPatterns #-} |
| 4 | + |
| 5 | +{- | Property tests for the `divideInteger` and `modInteger` builtins -} |
| 6 | +module Evaluation.Builtins.Integer.DivModProperties (test_integer_div_mod_properties) |
| 7 | +where |
| 8 | + |
| 9 | +import Evaluation.Builtins.Common |
| 10 | +import Evaluation.Builtins.Integer.Common |
| 11 | + |
| 12 | +import Test.Tasty (TestName, TestTree, testGroup) |
| 13 | +import Test.Tasty.QuickCheck |
| 14 | + |
| 15 | +numberOfTests :: Int |
| 16 | +numberOfTests = 200 |
| 17 | + |
| 18 | +testProp :: Testable prop => TestName -> prop -> TestTree |
| 19 | +testProp s p = testProperty s $ withMaxSuccess numberOfTests p |
| 20 | + |
| 21 | +-- `divideInteger _ 0` always fails. |
| 22 | +prop_div_0_fails :: BigInteger -> Property |
| 23 | +prop_div_0_fails (biginteger -> a) = |
| 24 | + fails $ divideInteger a zero |
| 25 | + |
| 26 | +-- `modInteger _ 0` always fails. |
| 27 | +prop_mod_0_fails :: BigInteger -> Property |
| 28 | +prop_mod_0_fails (biginteger -> a) = |
| 29 | + fails $ modInteger a zero |
| 30 | + |
| 31 | +-- b /= 0 => a = b * (a `div` b) + (a `mod` b) |
| 32 | +-- This is the crucial property relating `divideInteger` and `modInteger`. |
| 33 | +prop_div_mod_compatible :: BigInteger -> NonZero BigInteger -> Property |
| 34 | +prop_div_mod_compatible (biginteger -> a) (NonZero (biginteger -> b)) = |
| 35 | + let t = addInteger (multiplyInteger b (divideInteger a b) ) (modInteger a b) |
| 36 | + in evalOkEq t a |
| 37 | + |
| 38 | +-- (k*b) `div` b = b and (k*b) `mod` b = 0 for all k |
| 39 | +prop_div_mod_multiple :: BigInteger -> NonZero BigInteger -> Property |
| 40 | +prop_div_mod_multiple (biginteger -> k) (NonZero (biginteger -> b)) = |
| 41 | + let t1 = divideInteger (multiplyInteger k b) b |
| 42 | + t2 = modInteger (multiplyInteger k b) b |
| 43 | + in evalOkEq t1 k .&&. evalOkEq t2 zero |
| 44 | + |
| 45 | +-- For fixed b, `modInteger _ b` is an additive homomorphism: |
| 46 | +-- (a+a') `mod` b = ((a `mod` b) + (a' `mod` b)) `mod` b |
| 47 | +-- Together with prop_div_mod_multiple this means that `mod _ b` is |
| 48 | +-- periodic: (a+k*b) `mod` b = a mod b` for all k. |
| 49 | +prop_mod_additive :: BigInteger -> BigInteger -> NonZero BigInteger -> Property |
| 50 | +prop_mod_additive (biginteger -> a) (biginteger -> a') (NonZero (biginteger -> b)) = |
| 51 | + let t1 = modInteger (addInteger a a') b |
| 52 | + t2 = modInteger (addInteger (modInteger a b) (modInteger a' b)) b |
| 53 | + in evalOkEq t1 t2 |
| 54 | + |
| 55 | +-- For fixed b, `modInteger _ b` is a multiplicative homomorphism: |
| 56 | +-- (a*a') `mod` b = ((a `mod` b) * (a' `mod` b)) `mod` b |
| 57 | +prop_mod_multiplicative :: BigInteger -> BigInteger -> NonZero BigInteger -> Property |
| 58 | +prop_mod_multiplicative (biginteger -> a) (biginteger -> a') (NonZero (biginteger -> b)) = |
| 59 | + let t1 = modInteger (multiplyInteger a a') b |
| 60 | + t2 = modInteger (multiplyInteger (modInteger a b) (modInteger a' b)) b |
| 61 | + in evalOkEq t1 t2 |
| 62 | + |
| 63 | +-- For b > 0, 0 <= a `mod` b < b; |
| 64 | +prop_mod_size_pos :: BigInteger -> Positive BigInteger -> Property |
| 65 | +prop_mod_size_pos (biginteger -> a) (Positive (biginteger -> b)) = |
| 66 | + let t1 = lessThanEqualsInteger zero (modInteger a b) |
| 67 | + t2 = lessThanInteger (modInteger a b) b |
| 68 | + in evalOkTrue t1 .&&. evalOkTrue t2 |
| 69 | + |
| 70 | +-- For b < 0, b < a `mod` b <= 0 |
| 71 | +prop_mod_size_neg :: BigInteger -> Negative BigInteger -> Property |
| 72 | +prop_mod_size_neg (biginteger -> a) (Negative (biginteger -> b)) = |
| 73 | + let t1 = lessThanEqualsInteger (modInteger a b) zero |
| 74 | + t2 = lessThanInteger b (modInteger a b) |
| 75 | + in evalOkTrue t1 .&&. evalOkTrue t2 |
| 76 | + |
| 77 | +-- a >= 0 && b > 0 => a `div` b >= 0 and a `mod` b >= 0 |
| 78 | +-- a <= 0 && b > 0 => a `div` b <= 0 and a `mod` b >= 0 |
| 79 | +-- a >= 0 && b < 0 => a `div` b <= 0 and a `mod` b <= 0 |
| 80 | +-- a < 0 && b < 0 => a `div` b >= 0 and a `mod` b <= 0 |
| 81 | + |
| 82 | +prop_div_pos_pos :: (NonNegative BigInteger) -> (Positive BigInteger) -> Property |
| 83 | +prop_div_pos_pos (NonNegative (biginteger -> a)) (Positive (biginteger -> b)) = |
| 84 | + evalOkTrue $ ge0 (divideInteger a b) |
| 85 | + |
| 86 | +prop_div_neg_pos :: (NonPositive BigInteger) -> (Positive BigInteger) -> Property |
| 87 | +prop_div_neg_pos (NonPositive (biginteger -> a)) (Positive (biginteger -> b)) = |
| 88 | + evalOkTrue $ le0 (divideInteger a b) |
| 89 | + |
| 90 | +prop_div_pos_neg :: (NonNegative BigInteger) -> (Negative BigInteger) -> Property |
| 91 | +prop_div_pos_neg (NonNegative (biginteger -> a)) (Negative (biginteger -> b)) = |
| 92 | + evalOkTrue $ le0 (divideInteger a b) |
| 93 | + |
| 94 | +prop_div_neg_neg :: (NonPositive BigInteger) -> (Negative BigInteger) -> Property |
| 95 | +prop_div_neg_neg (NonPositive (biginteger -> a)) (Negative (biginteger -> b)) = |
| 96 | + evalOkTrue $ ge0 (divideInteger a b) |
| 97 | + |
| 98 | +prop_mod_pos_pos :: (NonNegative BigInteger) -> (Positive BigInteger) -> Property |
| 99 | +prop_mod_pos_pos (NonNegative (biginteger -> a)) (Positive (biginteger -> b)) = |
| 100 | + evalOkTrue $ ge0 (modInteger a b) |
| 101 | + |
| 102 | +prop_mod_neg_pos :: (NonPositive BigInteger) -> (Positive BigInteger) -> Property |
| 103 | +prop_mod_neg_pos (NonPositive (biginteger -> a)) (Positive (biginteger -> b)) = |
| 104 | + evalOkTrue $ ge0 (modInteger a b) |
| 105 | + |
| 106 | +prop_mod_pos_neg :: (NonNegative BigInteger) -> (Negative BigInteger) -> Property |
| 107 | +prop_mod_pos_neg (NonNegative (biginteger -> a)) (Negative (biginteger -> b)) = |
| 108 | + evalOkTrue $ le0 (modInteger a b) |
| 109 | + |
| 110 | +prop_mod_neg_neg :: (NonPositive BigInteger) -> (Negative BigInteger) -> Property |
| 111 | +prop_mod_neg_neg (NonPositive (biginteger -> a)) (Negative (biginteger -> b)) = |
| 112 | + evalOkTrue $ le0 (modInteger a b) |
| 113 | + |
| 114 | +test_integer_div_mod_properties :: TestTree |
| 115 | +test_integer_div_mod_properties = |
| 116 | + testGroup "Property tests for divideInteger and modInteger" |
| 117 | + [ testProp "divideInteger _ 0 always fails" prop_div_0_fails |
| 118 | + , testProp "modInteger _ 0 always fails" prop_mod_0_fails |
| 119 | + , testProp "divideInteger and modInteger are compatible" prop_div_mod_compatible |
| 120 | + , testProp "divideInteger and modInteger behave sensibly on multiples of the divisor" prop_div_mod_multiple |
| 121 | + , testProp "mod is an additive homomorphism" prop_mod_additive |
| 122 | + , testProp "mod is a multiplicative homomorphism" prop_mod_multiplicative |
| 123 | + , testProp "modInteger size is correct for positive modulus" prop_mod_size_pos |
| 124 | + , testProp "modInteger size is correct for negative modulus" prop_mod_size_neg |
| 125 | + , testProp "divideInteger (>= 0) (> 0) >= 0" prop_div_pos_pos |
| 126 | + , testProp "divideInteger (<= 0) (> 0) <= 0" prop_div_neg_pos |
| 127 | + , testProp "divideInteger (>= 0) (< 0) <= 0" prop_div_pos_neg |
| 128 | + , testProp "divideInteger (<= 0) (< 0) >= 0" prop_div_neg_neg |
| 129 | + , testProp "modInteger (>= 0) (> 0) >= 0 " prop_mod_pos_pos |
| 130 | + , testProp "modInteger (>= 0) (< 0) >= 0" prop_mod_neg_pos |
| 131 | + , testProp "modInteger (<= 0) (> 0) <= 0" prop_mod_pos_neg |
| 132 | + , testProp "modInteger (<= 0) (< 0) <= 0" prop_mod_neg_neg |
| 133 | + ] |
| 134 | + |
0 commit comments