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

{- | Property tests for the `lessThanInteger` and `lessThanEqualsInteger` builtins
   and their interaction with the arithmetic functions. -}
module Evaluation.Builtins.Integer.OrderProperties (test_integer_order_properties)
where

import Prelude hiding (and, not, or)

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

{- Tests for standard properties of order relations.  In most of these we create
   totally random inputs and then create terms checking that the expected
   properties are satisfied.  The inputs are completely random, so in some cases
   we'll be checking vacuous implications (for example, in `add_pairs`, where
   only one quarter of the cases will be checking the property that we really
   want to check).  Instead we could have used `suchThat` to generate inputs
   that always satisified the preconditions and then created terms to check that
   the conclusion holds.  It's arguable which of these is better, but the way
   it's done here exercises the comparison builtins more so perhaps increases
   the probability of detecting unexpected behaviour. -}

lte_reflexive :: BigInteger -> Property
lte_reflexive :: BigInteger -> Property
lte_reflexive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
a PlcTerm
a

lte_antisymmetric :: BigInteger -> BigInteger -> Property
lte_antisymmetric :: BigInteger -> BigInteger -> Property
lte_antisymmetric (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$
    (PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
a PlcTerm
b PlcTerm -> PlcTerm -> PlcTerm
`and` PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
b PlcTerm
a)
    PlcTerm -> PlcTerm -> PlcTerm
`implies` PlcTerm -> PlcTerm -> PlcTerm
equalsInteger PlcTerm
a PlcTerm
b

lte_transitive :: BigInteger -> BigInteger -> BigInteger -> Property
lte_transitive :: BigInteger -> BigInteger -> BigInteger -> Property
lte_transitive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) (BigInteger -> PlcTerm
biginteger -> PlcTerm
c) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$
    (PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
a PlcTerm
b PlcTerm -> PlcTerm -> PlcTerm
`and` PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
b PlcTerm
c)
    PlcTerm -> PlcTerm -> PlcTerm
`implies` PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
a PlcTerm
c

-- This implies that lessThanEqualsInteger is a total order.
trichotomy :: BigInteger -> BigInteger -> Property
trichotomy :: BigInteger -> BigInteger -> Property
trichotomy (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$
    PlcTerm -> PlcTerm -> PlcTerm
lessThanInteger PlcTerm
a PlcTerm
b PlcTerm -> PlcTerm -> PlcTerm
`xor` PlcTerm -> PlcTerm -> PlcTerm
equalsInteger PlcTerm
a PlcTerm
b PlcTerm -> PlcTerm -> PlcTerm
`xor` PlcTerm -> PlcTerm -> PlcTerm
lessThanInteger PlcTerm
b PlcTerm
a

-- This establishes a connection between < and <=, allowing us to limit
-- ourselves to checking properties of <=.
lt_versus_lte :: BigInteger -> BigInteger -> Property
lt_versus_lte :: BigInteger -> BigInteger -> Property
lt_versus_lte (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$
    PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
a PlcTerm
b PlcTerm -> PlcTerm -> PlcTerm
`iff` (PlcTerm -> PlcTerm -> PlcTerm
lessThanInteger PlcTerm
a PlcTerm
b PlcTerm -> PlcTerm -> PlcTerm
`xor` PlcTerm -> PlcTerm -> PlcTerm
equalsInteger PlcTerm
a PlcTerm
b)

-- Tests of some relations between the comparison operators and the arithmetic
-- operators.

-- Check that a <= b and c <= d => a+c <= b+d.  In conjunction with the ring
-- properties this implies, for example, that the sum of two positive integers
-- is positive and the sum of two negative integers is negative, and that a <=
-- a+k for positive k.
add_pairs :: BigInteger -> BigInteger -> BigInteger -> BigInteger -> Property
add_pairs :: BigInteger -> BigInteger -> BigInteger -> BigInteger -> Property
add_pairs (BigInteger -> PlcTerm
biginteger -> PlcTerm
a) (BigInteger -> PlcTerm
biginteger -> PlcTerm
b) (BigInteger -> PlcTerm
biginteger -> PlcTerm
c) (BigInteger -> PlcTerm
biginteger -> PlcTerm
d) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$
    (PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
a PlcTerm
b PlcTerm -> PlcTerm -> PlcTerm
`and` PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
c PlcTerm
d)
    PlcTerm -> PlcTerm -> PlcTerm
`implies` PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
c) (PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
b PlcTerm
d)

-- Test that the signs of various types of product are correct.
mul_pos_pos :: NonNegative BigInteger -> NonNegative BigInteger -> Property
mul_pos_pos :: NonNegative BigInteger -> NonNegative BigInteger -> Property
mul_pos_pos (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
zero (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
b)

mul_pos_neg :: NonNegative BigInteger -> NonPositive BigInteger -> Property
mul_pos_neg :: NonNegative BigInteger -> NonPositive BigInteger -> Property
mul_pos_neg (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
b) PlcTerm
zero

mul_neg_pos :: NonPositive BigInteger -> NonNegative BigInteger -> Property
mul_neg_pos :: NonPositive BigInteger -> NonNegative BigInteger -> Property
mul_neg_pos (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (NonNegative (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
b) PlcTerm
zero

mul_neg_neg :: NonPositive BigInteger -> NonPositive BigInteger -> Property
mul_neg_neg :: NonPositive BigInteger -> NonPositive BigInteger -> Property
mul_neg_neg (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
a)) (NonPositive (BigInteger -> PlcTerm
biginteger -> PlcTerm
b)) =
  PlcTerm -> Property
evalOkTrue (PlcTerm -> Property) -> PlcTerm -> Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
zero (PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
b)

test_integer_order_properties :: TestTree
test_integer_order_properties :: TestTree
test_integer_order_properties =
  TestName -> [TestTree] -> TestTree
testGroup TestName
"Property tests involving integer ordering"
    [ TestName -> (BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"lessThanEqualsInteger is reflexive" BigInteger -> Property
lte_reflexive
    , TestName -> (BigInteger -> BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"lessThanEqualsInteger is antisymmetric" BigInteger -> BigInteger -> Property
lte_antisymmetric
    , TestName
-> (BigInteger -> BigInteger -> BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"lessThanEqualsInteger is transitive" BigInteger -> BigInteger -> BigInteger -> Property
lte_transitive
    , TestName -> (BigInteger -> BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"a <= b <=> a < b or a = b" BigInteger -> BigInteger -> Property
lt_versus_lte
    , TestName -> (BigInteger -> BigInteger -> Property) -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"a < b or a = b or b < a" BigInteger -> BigInteger -> Property
trichotomy
    , TestName
-> (BigInteger
    -> BigInteger -> BigInteger -> BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"a <= b and c <= d => addInteger a c <= addInteger b d" BigInteger -> BigInteger -> BigInteger -> BigInteger -> Property
add_pairs
    , TestName
-> (NonNegative BigInteger -> NonNegative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"multiplyInteger (>= 0) (>= 0) >= 0" NonNegative BigInteger -> NonNegative BigInteger -> Property
mul_pos_pos
    , TestName
-> (NonNegative BigInteger -> NonPositive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"multiplyInteger (>= 0) (<= 0) <= 0" NonNegative BigInteger -> NonPositive BigInteger -> Property
mul_pos_neg
    , TestName
-> (NonPositive BigInteger -> NonNegative BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"multiplyInteger (<= 0) (>= 0) <= 0" NonPositive BigInteger -> NonNegative BigInteger -> Property
mul_neg_pos
    , TestName
-> (NonPositive BigInteger -> NonPositive BigInteger -> Property)
-> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"multiplyInteger (<= 0) (<= 0) >= 0" NonPositive BigInteger -> NonPositive BigInteger -> Property
mul_neg_neg
    ]