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

{- | Property tests for the `addInteger`, `subtractInteger`, and `multiplyInteger` builtins -}
module Evaluation.Builtins.Integer.RingProperties (test_integer_ring_properties)
where

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

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

-- a+(b+c) = (a+b)+c
prop_addition_associative :: BigInteger -> BigInteger -> BigInteger -> Property
prop_addition_associative :: BigInteger -> BigInteger -> BigInteger -> Property
prop_addition_associative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) (BigInteger -> PlcTerm
biginteger -> PlcTerm
c) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
b PlcTerm
c)
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
addInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
b) PlcTerm
c
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- a+b = b+a
prop_addition_commutative :: BigInteger -> BigInteger -> Property
prop_addition_commutative :: BigInteger -> BigInteger -> Property
prop_addition_commutative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) =
  PlcTerm -> PlcTerm -> Property
evalOkEq (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
b) (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
b PlcTerm
a)

-- a+0 = a
prop_zero_additive_identity :: BigInteger -> Property
prop_zero_additive_identity :: BigInteger -> Property
prop_zero_additive_identity (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) =
  PlcTerm -> PlcTerm -> Property
evalOkEq (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
zero) PlcTerm
a

-- (a+b)-b = a
prop_add_subtract_inverse :: BigInteger -> BigInteger -> Property
prop_add_subtract_inverse :: BigInteger -> BigInteger -> Property
prop_add_subtract_inverse (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) =
  PlcTerm -> PlcTerm -> Property
evalOkEq (PlcTerm -> PlcTerm -> PlcTerm
subtractInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
b) PlcTerm
b) PlcTerm
a

-- a*(b*c) = (a*b)*c
prop_multiplication_associative :: BigInteger -> BigInteger -> BigInteger -> Property
prop_multiplication_associative :: BigInteger -> BigInteger -> BigInteger -> Property
prop_multiplication_associative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) (BigInteger -> PlcTerm
biginteger -> PlcTerm
c) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
b PlcTerm
c)
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
b) PlcTerm
c
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- a*b = b*a
prop_multiplication_commutative :: BigInteger -> BigInteger -> Property
prop_multiplication_commutative :: BigInteger -> BigInteger -> Property
prop_multiplication_commutative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
b
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
b PlcTerm
a
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- a*1 = a
prop_one_multiplicative_identity :: BigInteger -> Property
prop_one_multiplicative_identity :: BigInteger -> Property
prop_one_multiplicative_identity (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) =
  let t :: PlcTerm
t = PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
one
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t PlcTerm
a

-- a*(b+c) = a*b + a*c
prop_distibutive :: BigInteger -> BigInteger -> BigInteger -> Property
prop_distibutive :: BigInteger -> BigInteger -> BigInteger -> Property
prop_distibutive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) (BigInteger -> PlcTerm
biginteger -> PlcTerm
c) =
  let t1 :: PlcTerm
t1 = PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
b PlcTerm
c)
      t2 :: PlcTerm
t2 = PlcTerm -> PlcTerm -> PlcTerm
addInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
b) (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
c)
  in PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

test_integer_ring_properties :: TestTree
test_integer_ring_properties :: TestTree
test_integer_ring_properties =
  TestName -> [TestTree] -> TestTree
testGroup TestName
"Ring properties for integer arithmetic builtins"
  [ TestName
-> (BigInteger -> BigInteger -> BigInteger -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"addInteger is associative" BigInteger -> BigInteger -> BigInteger -> Property
prop_addition_associative
  , TestName -> (BigInteger -> BigInteger -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"addInteger is commutative" BigInteger -> BigInteger -> Property
prop_addition_commutative
  , TestName -> (BigInteger -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"0 is an identity element for addInteger" BigInteger -> Property
prop_zero_additive_identity
  , TestName -> (BigInteger -> BigInteger -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"subtraction is the inverse of addition" BigInteger -> BigInteger -> Property
prop_add_subtract_inverse
  , TestName
-> (BigInteger -> BigInteger -> BigInteger -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"multiplyInteger is associative" BigInteger -> BigInteger -> BigInteger -> Property
prop_multiplication_associative
  , TestName -> (BigInteger -> BigInteger -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"multiplyInteger is commutative" BigInteger -> BigInteger -> Property
prop_multiplication_commutative
  , TestName -> (BigInteger -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"1 is a multiplicative identity" BigInteger -> Property
prop_one_multiplicative_identity
  , TestName
-> (BigInteger -> BigInteger -> BigInteger -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"multiplyInteger distributes over addInteger" BigInteger -> BigInteger -> BigInteger -> Property
prop_distibutive
  ]