-- editorconfig-checker-disable
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns      #-}

{- | Property tests for the `divideInteger` and `modInteger` builtins -}
module Evaluation.Builtins.Integer.DivModProperties (test_integer_div_mod_properties)
where

import Evaluation.Builtins.Common
import Evaluation.Builtins.Integer.Common

import Test.Tasty (TestName, TestTree, testGroup)
import Test.Tasty.QuickCheck

numberOfTests :: Int
numberOfTests :: Int
numberOfTests = Int
200

testProp :: Testable prop => TestName -> prop -> TestTree
testProp :: forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
s prop
p = TestName -> Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProperty TestName
s (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> prop -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
numberOfTests prop
p

-- `divideInteger _ 0` always fails.
prop_div_0_fails :: BigInteger -> Property
prop_div_0_fails :: BigInteger -> Property
prop_div_0_fails (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) =
  PlcTerm -> Property
fails (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm -> PlcTerm
divideInteger PlcTerm
a PlcTerm
zero

-- `modInteger _ 0` always fails.
prop_mod_0_fails :: BigInteger -> Property
prop_mod_0_fails :: BigInteger -> Property
prop_mod_0_fails (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) =
  PlcTerm -> Property
fails (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
zero

-- b /= 0 => a = b * (a `div` b) + (a `mod` b)
-- This is the crucial property relating `divideInteger` and `modInteger`.
prop_div_mod_compatible :: BigInteger -> NonZero BigInteger -> Property
prop_div_mod_compatible :: BigInteger -> NonZero BigInteger -> Property
prop_div_mod_compatible (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let t :: PlcTerm
t = PlcTerm -> PlcTerm -> PlcTerm
addInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
b (PlcTerm -> PlcTerm -> PlcTerm
divideInteger PlcTerm
a PlcTerm
b) ) (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b)
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t PlcTerm
a

-- (k*b) `div` b = b and (k*b) `mod` b = 0 for all k
prop_div_mod_multiple :: BigInteger -> NonZero BigInteger -> Property
prop_div_mod_multiple :: BigInteger -> NonZero BigInteger -> Property
prop_div_mod_multiple (BigInteger -> PlcTerm
biginteger -> PlcTerm
k) (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
    let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
divideInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
k PlcTerm
b) PlcTerm
b
        t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
modInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
k PlcTerm
b) PlcTerm
b
    in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
k Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t2 PlcTerm
zero

-- For fixed b, `modInteger _ b` is an additive homomorphism:
-- (a+a') `mod` b = ((a `mod` b) + (a' `mod` b)) `mod` b
-- Together with prop_div_mod_multiple this means that `mod _ b` is
-- periodic: (a+k*b) `mod` b = a mod b` for all k.
prop_mod_additive :: BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_mod_additive :: BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_mod_additive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
a') (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
modInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
a') PlcTerm
b
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
modInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b) (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a' PlcTerm
b)) PlcTerm
b
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- For fixed b, `modInteger _ b` is a multiplicative homomorphism:
-- (a*a') `mod` b = ((a `mod` b) * (a' `mod` b)) `mod` b
prop_mod_multiplicative :: BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_mod_multiplicative :: BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_mod_multiplicative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
a') (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
modInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
a') PlcTerm
b
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
modInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b) (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a' PlcTerm
b)) PlcTerm
b
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- For b > 0, 0 <= a `mod` b < b;
prop_mod_size_pos :: BigInteger -> Positive BigInteger -> Property
prop_mod_size_pos :: BigInteger -> Positive BigInteger -> Property
prop_mod_size_pos (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (Positive (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
zero (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b)
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
lessThanInteger (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b) PlcTerm
b
  in PlcTerm -> Property
evalOkTrue PlcTerm
t1 Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. PlcTerm -> Property
evalOkTrue PlcTerm
t2

-- For b < 0, b < a `mod` b <= 0
prop_mod_size_neg :: BigInteger -> Negative BigInteger -> Property
prop_mod_size_neg :: BigInteger -> Negative BigInteger -> Property
prop_mod_size_neg (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (Negative (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b) PlcTerm
zero
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
lessThanInteger PlcTerm
b (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b)
  in PlcTerm -> Property
evalOkTrue PlcTerm
t1 Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. PlcTerm -> Property
evalOkTrue PlcTerm
t2

-- a >= 0 && b > 0  =>  a `div` b >= 0  and  a `mod` b >= 0
-- a <= 0 && b > 0  =>  a `div` b <= 0  and  a `mod` b >= 0
-- a >= 0 && b < 0  =>  a `div` b <= 0  and  a `mod` b <= 0
-- a <  0 && b < 0  =>  a `div` b >= 0  and  a `mod` b <= 0

prop_div_pos_pos :: (NonNegative BigInteger) -> (Positive BigInteger) -> Property
prop_div_pos_pos :: NonNegative BigInteger -> Positive BigInteger -> Property
prop_div_pos_pos (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (Positive (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm
ge0 (PlcTerm -> PlcTerm -> PlcTerm
divideInteger PlcTerm
a PlcTerm
b)

prop_div_neg_pos :: (NonPositive BigInteger) -> (Positive BigInteger) -> Property
prop_div_neg_pos :: NonPositive BigInteger -> Positive BigInteger -> Property
prop_div_neg_pos (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (Positive (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm
le0 (PlcTerm -> PlcTerm -> PlcTerm
divideInteger PlcTerm
a PlcTerm
b)

prop_div_pos_neg :: (NonNegative BigInteger) -> (Negative BigInteger) -> Property
prop_div_pos_neg :: NonNegative BigInteger -> Negative BigInteger -> Property
prop_div_pos_neg (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (Negative (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm
le0 (PlcTerm -> PlcTerm -> PlcTerm
divideInteger PlcTerm
a PlcTerm
b)

prop_div_neg_neg :: (NonPositive BigInteger) -> (Negative BigInteger) -> Property
prop_div_neg_neg :: NonPositive BigInteger -> Negative BigInteger -> Property
prop_div_neg_neg (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (Negative (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm
ge0 (PlcTerm -> PlcTerm -> PlcTerm
divideInteger PlcTerm
a PlcTerm
b)

prop_mod_pos_pos :: (NonNegative BigInteger) -> (Positive BigInteger) -> Property
prop_mod_pos_pos :: NonNegative BigInteger -> Positive BigInteger -> Property
prop_mod_pos_pos (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (Positive (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm
ge0 (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b)

prop_mod_neg_pos :: (NonPositive BigInteger) -> (Positive BigInteger) -> Property
prop_mod_neg_pos :: NonPositive BigInteger -> Positive BigInteger -> Property
prop_mod_neg_pos (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (Positive (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm
ge0 (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b)

prop_mod_pos_neg :: (NonNegative BigInteger) -> (Negative BigInteger) -> Property
prop_mod_pos_neg :: NonNegative BigInteger -> Negative BigInteger -> Property
prop_mod_pos_neg (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (Negative (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm
le0 (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b)

prop_mod_neg_neg :: (NonPositive BigInteger) -> (Negative BigInteger) -> Property
prop_mod_neg_neg :: NonPositive BigInteger -> Negative BigInteger -> Property
prop_mod_neg_neg (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (Negative (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm
le0 (PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b)

test_integer_div_mod_properties :: TestTree
test_integer_div_mod_properties :: TestTree
test_integer_div_mod_properties =
  TestName -> [TestTree] -> TestTree
testGroup TestName
"Property tests for divideInteger and modInteger"
    [ TestName -> (BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"divideInteger _ 0 always fails" BigInteger -> Property
prop_div_0_fails
    , TestName -> (BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"modInteger _ 0 always fails" BigInteger -> Property
prop_mod_0_fails
    , TestName
-> (BigInteger -> NonZero BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"divideInteger and modInteger are compatible" BigInteger -> NonZero BigInteger -> Property
prop_div_mod_compatible
    , TestName
-> (BigInteger -> NonZero BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"divideInteger and modInteger behave sensibly on multiples of the divisor" BigInteger -> NonZero BigInteger -> Property
prop_div_mod_multiple
    , TestName
-> (BigInteger -> BigInteger -> NonZero BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"mod is an additive homomorphism" BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_mod_additive
    , TestName
-> (BigInteger -> BigInteger -> NonZero BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"mod is a multiplicative homomorphism" BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_mod_multiplicative
    , TestName
-> (BigInteger -> Positive BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"modInteger size is correct for positive modulus" BigInteger -> Positive BigInteger -> Property
prop_mod_size_pos
    , TestName
-> (BigInteger -> Negative BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"modInteger size is correct for negative modulus" BigInteger -> Negative BigInteger -> Property
prop_mod_size_neg
    , TestName
-> (NonNegative BigInteger -> Positive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"divideInteger (>= 0) (> 0) >= 0" NonNegative BigInteger -> Positive BigInteger -> Property
prop_div_pos_pos
    , TestName
-> (NonPositive BigInteger -> Positive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"divideInteger (<= 0) (> 0) <= 0" NonPositive BigInteger -> Positive BigInteger -> Property
prop_div_neg_pos
    , TestName
-> (NonNegative BigInteger -> Negative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"divideInteger (>= 0) (< 0) <= 0" NonNegative BigInteger -> Negative BigInteger -> Property
prop_div_pos_neg
    , TestName
-> (NonPositive BigInteger -> Negative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"divideInteger (<= 0) (< 0) >= 0" NonPositive BigInteger -> Negative BigInteger -> Property
prop_div_neg_neg
    , TestName
-> (NonNegative BigInteger -> Positive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"modInteger (>= 0) (> 0) >= 0 " NonNegative BigInteger -> Positive BigInteger -> Property
prop_mod_pos_pos
    , TestName
-> (NonPositive BigInteger -> Positive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"modInteger (>= 0) (< 0) >= 0" NonPositive BigInteger -> Positive BigInteger -> Property
prop_mod_neg_pos
    , TestName
-> (NonNegative BigInteger -> Negative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"modInteger (<= 0) (> 0) <= 0" NonNegative BigInteger -> Negative BigInteger -> Property
prop_mod_pos_neg
    , TestName
-> (NonPositive BigInteger -> Negative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"modInteger (<= 0) (< 0) <= 0" NonPositive BigInteger -> Negative BigInteger -> Property
prop_mod_neg_neg
    ]