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

{- | Property tests for the `quotientInteger` and `remainderInteger` builtins -}
module Evaluation.Builtins.Integer.QuotRemProperties (test_integer_quot_rem_properties)
where

import Prelude hiding (abs)

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

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

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

-- b /= 0 => a = b * (a `quot` b) + (a `rem` b)
-- This is the crucial property relating `quotientInteger` and `remainderInteger`.
prop_quot_rem_compatible :: BigInteger -> NonZero BigInteger -> Property
prop_quot_rem_compatible :: BigInteger -> NonZero BigInteger -> Property
prop_quot_rem_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
quotientInteger PlcTerm
a PlcTerm
b) ) (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a PlcTerm
b)
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t PlcTerm
a

-- (k*b) `quot` b = b and (k*b) `rem` b = 0 for all k
prop_quot_rem_multiple :: BigInteger -> NonZero BigInteger -> Property
prop_quot_rem_multiple :: BigInteger -> NonZero BigInteger -> Property
prop_quot_rem_multiple (BigInteger -> PlcTerm
biginteger -> PlcTerm
k) (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
    let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
quotientInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
k PlcTerm
b) PlcTerm
b
        t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
remainderInteger (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

-- `remainderInteger _ b` is not an additive homomorphism in general (and hence
-- not periodic) because the sign of `remainderInteger a b` is different for
-- positive and negative a.  For example (writing `rem` for short instead of
-- `remainderInteger`) `rem (-1) 5 = -1` and `rem 5 5 = 0` but `rem (-1+5) 5 =
-- 4`.  However, rem (a + a') b = rem ((rem a b) + (rem a' b)) b if a and a'
-- have the same sign, so we test that instead of checking for arbitrary a and
-- a'.

-- For fixed b, `remainderInteger _ b` is an additive homomorphism on non-negative integers
-- (a+a') `rem` b = ((a `rem` b) + (a' `rem` b)) `rem` b
prop_rem_additive_pos :: NonNegative BigInteger -> NonNegative BigInteger -> NonZero BigInteger -> Property
prop_rem_additive_pos :: NonNegative BigInteger
-> NonNegative BigInteger -> NonZero BigInteger -> Property
prop_rem_additive_pos (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a')) (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
remainderInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
a') PlcTerm
b
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
remainderInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a PlcTerm
b) (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a' PlcTerm
b)) PlcTerm
b
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- For fixed b, `remainderInteger _ b` is an additive homomorphism on non-postive integers
-- (a+a') `rem` b = ((a `rem` b) + (a' `rem` b)) `rem` b
prop_rem_additive_neg :: NonPositive BigInteger -> NonPositive BigInteger -> NonZero BigInteger -> Property
prop_rem_additive_neg :: NonPositive BigInteger
-> NonPositive BigInteger -> NonZero BigInteger -> Property
prop_rem_additive_neg (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a')) (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
remainderInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
a') PlcTerm
b
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
remainderInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a PlcTerm
b) (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a' PlcTerm
b)) PlcTerm
b
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- Somewhat unexpectedly, for fixed b, `remainderInteger _ b` is a
-- multiplicative homomorphism: : (a*a') `rem` b = ((a `rem` b) * (a' `rem` b))
-- `rem` b
prop_rem_multiplicative :: BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_rem_multiplicative :: BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_rem_multiplicative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
a') (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
remainderInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
a') PlcTerm
b
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
remainderInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a PlcTerm
b) (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a' PlcTerm
b)) PlcTerm
b
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- For a >= 0 and b > 0, 0 <= |a `rem` b| < |b|
-- The sign of the remainder is a bit tricky in this case.  We test that the
-- absolute value of the remainder is in the expected range and leave the sign
-- to later tests.
prop_rem_size :: BigInteger -> NonZero BigInteger -> Property
prop_rem_size :: BigInteger -> NonZero BigInteger -> Property
prop_rem_size (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (NonZero (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  let r :: PlcTerm
r = PlcTerm -> PlcTerm
abs (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a PlcTerm
b)
      t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
zero PlcTerm
r
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
lessThanInteger PlcTerm
r (PlcTerm -> PlcTerm
abs 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 `quot` b >= 0  and  a `rem` b >= 0
-- a <= 0 && b > 0  =>  a `quot` b <= 0  and  a `rem` b <= 0
-- a >= 0 && b < 0  =>  a `quot` b <= 0  and  a `rem` b >= 0
-- a <= 0 && b < 0  =>  a `quot` b >= 0  and  a `rem` b <= 0

prop_quot_pos_pos :: NonNegative BigInteger -> Positive BigInteger -> Property
prop_quot_pos_pos :: NonNegative BigInteger -> Positive BigInteger -> Property
prop_quot_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
quotientInteger PlcTerm
a PlcTerm
b)

prop_quot_neg_pos :: NonPositive BigInteger -> Positive BigInteger -> Property
prop_quot_neg_pos :: NonPositive BigInteger -> Positive BigInteger -> Property
prop_quot_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
quotientInteger PlcTerm
a PlcTerm
b)

prop_quot_pos_neg :: NonNegative BigInteger -> Negative BigInteger -> Property
prop_quot_pos_neg :: NonNegative BigInteger -> Negative BigInteger -> Property
prop_quot_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
quotientInteger PlcTerm
a PlcTerm
b)

prop_quot_neg_neg :: NonPositive BigInteger -> Negative BigInteger -> Property
prop_quot_neg_neg :: NonPositive BigInteger -> Negative BigInteger -> Property
prop_quot_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
quotientInteger PlcTerm
a PlcTerm
b)

prop_rem_pos_pos :: (NonNegative BigInteger) -> (Positive BigInteger) -> Property
prop_rem_pos_pos :: NonNegative BigInteger -> Positive BigInteger -> Property
prop_rem_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
remainderInteger PlcTerm
a PlcTerm
b)

prop_rem_neg_pos :: (NonPositive BigInteger) -> (Positive BigInteger) -> Property
prop_rem_neg_pos :: NonPositive BigInteger -> Positive BigInteger -> Property
prop_rem_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
remainderInteger PlcTerm
a PlcTerm
b)

prop_rem_pos_neg :: (NonNegative BigInteger) -> (Negative BigInteger) -> Property
prop_rem_pos_neg :: NonNegative BigInteger -> Negative BigInteger -> Property
prop_rem_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
ge0 (PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a PlcTerm
b)

prop_rem_neg_neg :: (NonPositive BigInteger) -> (Negative BigInteger) -> Property
prop_rem_neg_neg :: NonPositive BigInteger -> Negative BigInteger -> Property
prop_rem_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
remainderInteger PlcTerm
a PlcTerm
b)

test_integer_quot_rem_properties :: TestTree
test_integer_quot_rem_properties :: TestTree
test_integer_quot_rem_properties =
  TestName -> [TestTree] -> TestTree
testGroup TestName
"Property tests for quotientInteger and remainderInteger"
    [ TestName -> (BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"quotientInteger _ 0 always fails" BigInteger -> Property
prop_quot_0_fails
    , TestName -> (BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger _ 0 always fails" BigInteger -> Property
prop_rem_0_fails
    , TestName
-> (BigInteger -> NonZero BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"quotientInteger and remainderInteger are compatible" BigInteger -> NonZero BigInteger -> Property
prop_quot_rem_compatible
    , TestName
-> (BigInteger -> NonZero BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"quotientInteger and remainderInteger behave sensibly on multiples of the divisor" BigInteger -> NonZero BigInteger -> Property
prop_quot_rem_multiple
    , TestName
-> (NonNegative BigInteger
    -> NonNegative BigInteger -> NonZero BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger _ b is additive on non-negative inputs" NonNegative BigInteger
-> NonNegative BigInteger -> NonZero BigInteger -> Property
prop_rem_additive_pos
    , TestName
-> (NonPositive BigInteger
    -> NonPositive BigInteger -> NonZero BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger _ b is additive on non-positive inputs" NonPositive BigInteger
-> NonPositive BigInteger -> NonZero BigInteger -> Property
prop_rem_additive_neg
    , TestName
-> (BigInteger -> BigInteger -> NonZero BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger is a multiplicative homomorphism" BigInteger -> BigInteger -> NonZero BigInteger -> Property
prop_rem_multiplicative
    , TestName
-> (BigInteger -> NonZero BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger size correct" BigInteger -> NonZero BigInteger -> Property
prop_rem_size
    , TestName
-> (NonNegative BigInteger -> Positive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"quotientInteger (>= 0) (> 0) >= 0"  NonNegative BigInteger -> Positive BigInteger -> Property
prop_quot_pos_pos
    , TestName
-> (NonPositive BigInteger -> Positive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"quotientInteger (<= 0) (> 0) <= 0"  NonPositive BigInteger -> Positive BigInteger -> Property
prop_quot_neg_pos
    , TestName
-> (NonNegative BigInteger -> Negative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"quotientInteger (>= 0) (< 0) <= 0"  NonNegative BigInteger -> Negative BigInteger -> Property
prop_quot_pos_neg
    , TestName
-> (NonPositive BigInteger -> Negative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"quotientInteger (<= 0) (< 0) >= 0"  NonPositive BigInteger -> Negative BigInteger -> Property
prop_quot_neg_neg
    , TestName
-> (NonNegative BigInteger -> Positive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger (>= 0) (> 0) >= 0" NonNegative BigInteger -> Positive BigInteger -> Property
prop_rem_pos_pos
    , TestName
-> (NonPositive BigInteger -> Positive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger (<= 0) (> 0) <= 0" NonPositive BigInteger -> Positive BigInteger -> Property
prop_rem_neg_pos
    , TestName
-> (NonNegative BigInteger -> Negative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger (>= 0) (< 0) >= 0" NonNegative BigInteger -> Negative BigInteger -> Property
prop_rem_pos_neg
    , TestName
-> (NonPositive BigInteger -> Negative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"remainderInteger (<= 0) (< 0) <= 0" NonPositive BigInteger -> Negative BigInteger -> Property
prop_rem_neg_neg
    ]