{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeSynonymInstances #-}

module Tests.Cardano.Ledger.NonIntegral where

import Cardano.Ledger.NonIntegral
import qualified Data.Fixed as FP
import Test.QuickCheck

data E34

instance FP.HasResolution E34 where
  resolution :: forall (p :: * -> *). p E34 -> Integer
resolution p E34
_ = Integer
10 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
34 :: Int)

type FixedPoint = FP.Fixed E34

epsD :: Double
epsD :: Double
epsD = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
10 Double -> Int -> Double
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
12 :: Int)

epsFP :: FixedPoint
epsFP :: FixedPoint
epsFP = FixedPoint
1 FixedPoint -> FixedPoint -> FixedPoint
forall a. Fractional a => a -> a -> a
/ FixedPoint
10 FixedPoint -> Int -> FixedPoint
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
16 :: Int)

eps :: Rational
eps :: Rational
eps = Rational
1 Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
10 Rational -> Int -> Rational
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
16 :: Int)

map2 :: (a -> b) -> (a, a) -> (b, b)
map2 :: forall a b. (a -> b) -> (a, a) -> (b, b)
map2 a -> b
f (a
x, a
y) = (a -> b
f a
x, a -> b
f a
y)

both :: (a -> Bool) -> (a, a) -> Bool
both :: forall a. (a -> Bool) -> (a, a) -> Bool
both a -> Bool
p (a
x, a
y) = a -> Bool
p a
x Bool -> Bool -> Bool
&& a -> Bool
p a
y

type Diff a = (a, a)

absDiff :: Num a => Diff a -> a
absDiff :: forall a. Num a => Diff a -> a
absDiff (a
x, a
y) = a -> a
forall a. Num a => a -> a
abs (a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y)

(~=) :: (Ord a, Num a) => Diff a -> a -> Bool
Diff a
w ~= :: forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= a
epsilon = Diff a -> a
forall a. Num a => Diff a -> a
absDiff Diff a
w a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
epsilon

newtype Normalized a = Norm (a, a) deriving (Int -> Normalized a -> ShowS
[Normalized a] -> ShowS
Normalized a -> String
(Int -> Normalized a -> ShowS)
-> (Normalized a -> String)
-> ([Normalized a] -> ShowS)
-> Show (Normalized a)
forall a. Show a => Int -> Normalized a -> ShowS
forall a. Show a => [Normalized a] -> ShowS
forall a. Show a => Normalized a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Normalized a -> ShowS
showsPrec :: Int -> Normalized a -> ShowS
$cshow :: forall a. Show a => Normalized a -> String
show :: Normalized a -> String
$cshowList :: forall a. Show a => [Normalized a] -> ShowS
showList :: [Normalized a] -> ShowS
Show)

newtype UnitInterval a = Unit a deriving (Int -> UnitInterval a -> ShowS
[UnitInterval a] -> ShowS
UnitInterval a -> String
(Int -> UnitInterval a -> ShowS)
-> (UnitInterval a -> String)
-> ([UnitInterval a] -> ShowS)
-> Show (UnitInterval a)
forall a. Show a => Int -> UnitInterval a -> ShowS
forall a. Show a => [UnitInterval a] -> ShowS
forall a. Show a => UnitInterval a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> UnitInterval a -> ShowS
showsPrec :: Int -> UnitInterval a -> ShowS
$cshow :: forall a. Show a => UnitInterval a -> String
show :: UnitInterval a -> String
$cshowList :: forall a. Show a => [UnitInterval a] -> ShowS
showList :: [UnitInterval a] -> ShowS
Show)

instance (Fractional a, Arbitrary a) => Arbitrary (Normalized a) where
  arbitrary :: Gen (Normalized a)
arbitrary = Normalized a -> Gen (Normalized a)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Normalized a -> Gen (Normalized a))
-> (NonNegInts -> Normalized a) -> NonNegInts -> Gen (Normalized a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, a) -> Normalized a
forall a. (a, a) -> Normalized a
Norm ((a, a) -> Normalized a)
-> (NonNegInts -> (a, a)) -> NonNegInts -> Normalized a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonNegInts -> (a, a)
forall a. Fractional a => NonNegInts -> (a, a)
normalize (NonNegInts -> Gen (Normalized a))
-> Gen NonNegInts -> Gen (Normalized a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Gen NonNegInts
forall a. Arbitrary a => Gen a
arbitrary

instance (Fractional a, Arbitrary a) => Arbitrary (UnitInterval a) where
  arbitrary :: Gen (UnitInterval a)
arbitrary = UnitInterval a -> Gen (UnitInterval a)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnitInterval a -> Gen (UnitInterval a))
-> (NonNegInts -> UnitInterval a)
-> NonNegInts
-> Gen (UnitInterval a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> UnitInterval a
forall a. a -> UnitInterval a
Unit (a -> UnitInterval a)
-> (NonNegInts -> a) -> NonNegInts -> UnitInterval a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonNegInts -> a
forall a. Fractional a => NonNegInts -> a
toUnit (NonNegInts -> Gen (UnitInterval a))
-> Gen NonNegInts -> Gen (UnitInterval a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Gen NonNegInts
forall a. Arbitrary a => Gen a
arbitrary

type NonNegInts = (NonNegative Integer, Positive Integer)

-- | Normalizes the integers, return a pair of integers, such that:
-- fst >= 0, snd > 0, fst <= snd.
normalizeInts :: NonNegInts -> (Integer, Integer)
normalizeInts :: NonNegInts -> (Integer, Integer)
normalizeInts (NonNegative Integer
x, Positive Integer
y) = (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
x Integer
y, Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
x Integer
y)

normalize :: Fractional a => NonNegInts -> (a, a)
normalize :: forall a. Fractional a => NonNegInts -> (a, a)
normalize = (Integer -> a) -> (Integer, Integer) -> (a, a)
forall a b. (a -> b) -> (a, a) -> (b, b)
map2 Integer -> a
forall a. Num a => Integer -> a
fromInteger ((Integer, Integer) -> (a, a))
-> (NonNegInts -> (Integer, Integer)) -> NonNegInts -> (a, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonNegInts -> (Integer, Integer)
normalizeInts

toUnit :: Fractional a => NonNegInts -> a
toUnit :: forall a. Fractional a => NonNegInts -> a
toUnit = (a -> a -> a) -> (a, a) -> a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> a
forall a. Fractional a => a -> a -> a
(/) ((a, a) -> a) -> (NonNegInts -> (a, a)) -> NonNegInts -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonNegInts -> (a, a)
forall a. Fractional a => NonNegInts -> (a, a)
normalize -- [0,1]

------------------------
-- Generic Properties --
------------------------

type Monotonic a = (a -> Bool) -> (a -> a) -> a -> a -> Property

monotonic :: (Ord a, Ord b) => (a -> b) -> a -> a -> Bool
monotonic :: forall a b. (Ord a, Ord b) => (a -> b) -> a -> a -> Bool
monotonic a -> b
f a
x a
y =
  if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y
    then a -> b
f a
x b -> b -> Bool
forall a. Ord a => a -> a -> Bool
< a -> b
f a
y
    else a -> b
f a
x b -> b -> Bool
forall a. Ord a => a -> a -> Bool
>= a -> b
f a
y

log_pow :: (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_pow :: forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_pow a
x a
y = (a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' (a
x a -> a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
y), a
y a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' a
x)

log_law :: (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_law :: forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_law a
x a
y = (a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' (a
x a -> a -> a
forall a. Num a => a -> a -> a
* a
y), a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' a
y)

exp_law :: (RealFrac a, Show a) => a -> a -> Diff a
exp_law :: forall a. (RealFrac a, Show a) => a -> a -> Diff a
exp_law a
x a
y = (a -> a
forall a. (RealFrac a, Show a) => a -> a
exp' (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y), a -> a
forall a. (RealFrac a, Show a) => a -> a
exp' a
x a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a. (RealFrac a, Show a) => a -> a
exp' a
y)

exp_log, log_exp :: (RealFrac a, Show a, Enum a) => a -> Diff a
exp_log :: forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
exp_log a
x = (a -> a
forall a. (RealFrac a, Show a) => a -> a
exp' (a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' a
x), a
x)
log_exp :: forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
log_exp a
x = (a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' (a -> a
forall a. (RealFrac a, Show a) => a -> a
exp' a
x), a
x)

exp_UnitInterval :: (RealFrac a, Show a, Enum a) => a -> a -> Bool
exp_UnitInterval :: forall a. (RealFrac a, Show a, Enum a) => a -> a -> Bool
exp_UnitInterval a
x a
y = let z :: a
z = a
x a -> a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
y in a
z a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& a
z a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
1

findD :: (RealFrac a, Show a) => a -> Bool
findD :: forall a. (RealFrac a, Show a) => a -> Bool
findD a
x = a
e a -> Integer -> a
forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Integer
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
x Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
e a -> Integer -> a
forall a b. (Fractional a, Integral b) => a -> b -> a
^^ (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
  where
    n :: Integer
n = a -> a -> Integer
forall a. RealFrac a => a -> a -> Integer
findE a
e a
x
    e :: a
e = a -> a
forall a. (RealFrac a, Show a) => a -> a
exp' a
1

pow_Diff :: (RealFrac a, Enum a, Show a) => a -> (a, a) -> Diff a
pow_Diff :: forall a. (RealFrac a, Enum a, Show a) => a -> (a, a) -> (a, a)
pow_Diff a
z (a
y, a
x) = ((a
z a -> a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** (a
1 a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
x)) a -> a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
y, (a
z a -> a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
y) a -> a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** (a
1 a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
x))

leader :: (RealFrac a, Show a, Enum a) => a -> a -> a
leader :: forall a. (RealFrac a, Show a, Enum a) => a -> a -> a
leader a
f a
sigma = a
1 a -> a -> a
forall a. Num a => a -> a -> a
- ((a
1 a -> a -> a
forall a. Num a => a -> a -> a
- a
f) a -> a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
sigma)

taylorExpCmpCheck :: RealFrac a => a -> a -> a -> Bool
taylorExpCmpCheck :: forall a. RealFrac a => a -> a -> a -> Bool
taylorExpCmpCheck a
a a
p a
s = case a -> a -> a -> CompareResult a
forall a. RealFrac a => a -> a -> a -> CompareResult a
taylorExpCmp a
3 a
p a
s of
  ABOVE a
_ Int
_ -> a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
a
  BELOW a
_ Int
_ -> a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
a
  MaxReached Int
_ -> Bool
False

praosLeaderCheck :: (RealFrac a, Show a, Enum a) => a -> a -> a -> a -> Bool
praosLeaderCheck :: forall a. (RealFrac a, Show a, Enum a) => a -> a -> a -> a -> Bool
praosLeaderCheck a
f a
a a
p a
sigma = case a -> a -> a -> CompareResult a
forall a. RealFrac a => a -> a -> a -> CompareResult a
taylorExpCmp a
3 (a
1 a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
q) (-a
sigma a -> a -> a
forall a. Num a => a -> a -> a
* a
c) of
  ABOVE a
_ Int
_ -> a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
a
  BELOW a
_ Int
_ -> a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
a
  MaxReached Int
_ -> Bool
False
  where
    c :: a
c = a -> a
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' (a
1 a -> a -> a
forall a. Num a => a -> a -> a
- a
f)
    q :: a
q = a
1 a -> a -> a
forall a. Num a => a -> a -> a
- a
p

---------------------------------------
-- FixedPoint Versions of Properties --
---------------------------------------

prop_FPMonotonic :: Monotonic FixedPoint
prop_FPMonotonic :: Monotonic FixedPoint
prop_FPMonotonic FixedPoint -> Bool
constrain FixedPoint -> FixedPoint
f FixedPoint
x FixedPoint
y =
  (FixedPoint -> Bool) -> (FixedPoint, FixedPoint) -> Bool
forall a. (a -> Bool) -> (a, a) -> Bool
both FixedPoint -> Bool
constrain (FixedPoint
x, FixedPoint
y) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
    Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
zeroes String
"both zero case" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      (Bool
zeroes Bool -> Bool -> Bool
|| (FixedPoint -> FixedPoint) -> FixedPoint -> FixedPoint -> Bool
forall a b. (Ord a, Ord b) => (a -> b) -> a -> a -> Bool
monotonic FixedPoint -> FixedPoint
f FixedPoint
x FixedPoint
y) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
  where
    zeroes :: Bool
zeroes = (FixedPoint -> Bool) -> (FixedPoint, FixedPoint) -> Bool
forall a. (a -> Bool) -> (a, a) -> Bool
both FixedPoint -> Bool
zero (FixedPoint
x, FixedPoint
y)
    zero :: FixedPoint -> Bool
zero FixedPoint
a = (FixedPoint -> FixedPoint
f FixedPoint
a, FixedPoint
0) (FixedPoint, FixedPoint) -> FixedPoint -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP

prop_FPPowDiff :: UnitInterval FixedPoint -> Normalized FixedPoint -> Property
prop_FPPowDiff :: UnitInterval FixedPoint -> Normalized FixedPoint -> Property
prop_FPPowDiff (Unit FixedPoint
z) (Norm (FixedPoint, FixedPoint)
w) =
  let e :: FixedPoint
e = (FixedPoint, FixedPoint) -> FixedPoint
forall a. Num a => Diff a -> a
absDiff (FixedPoint -> (FixedPoint, FixedPoint) -> (FixedPoint, FixedPoint)
forall a. (RealFrac a, Enum a, Show a) => a -> (a, a) -> (a, a)
pow_Diff FixedPoint
z (FixedPoint, FixedPoint)
w)
   in Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify (FixedPoint
e FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
< FixedPoint
epsFP) String
"OK 10e-16" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify (FixedPoint
e FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
< FixedPoint
epsFP FixedPoint -> FixedPoint -> FixedPoint
forall a. Num a => a -> a -> a
* FixedPoint
1000 Bool -> Bool -> Bool
&& FixedPoint
e FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
>= FixedPoint
epsFP) String
"OK 10e-12" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify (FixedPoint
e FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
>= FixedPoint
epsFP FixedPoint -> FixedPoint -> FixedPoint
forall a. Num a => a -> a -> a
* FixedPoint
1000) String
"KO" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            Bool
True Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_FPExpLaw :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPExpLaw :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPExpLaw (Unit FixedPoint
x) (Unit FixedPoint
y) = (FixedPoint -> FixedPoint -> (FixedPoint, FixedPoint)
forall a. (RealFrac a, Show a) => a -> a -> Diff a
exp_law FixedPoint
x FixedPoint
y (FixedPoint, FixedPoint) -> FixedPoint -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_FPlnLaw :: Positive FixedPoint -> Positive FixedPoint -> Property
prop_FPlnLaw :: Positive FixedPoint -> Positive FixedPoint -> Property
prop_FPlnLaw (Positive FixedPoint
x) (Positive FixedPoint
y) = (FixedPoint -> FixedPoint -> (FixedPoint, FixedPoint)
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_law FixedPoint
x FixedPoint
y (FixedPoint, FixedPoint) -> FixedPoint -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_FPExpUnitInterval :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPExpUnitInterval :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPExpUnitInterval (Unit FixedPoint
x) (Unit FixedPoint
y) = FixedPoint -> FixedPoint -> Bool
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Bool
exp_UnitInterval FixedPoint
x FixedPoint
y Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_FPIdemPotent :: Positive FixedPoint -> Property
prop_FPIdemPotent :: Positive FixedPoint -> Property
prop_FPIdemPotent (Positive FixedPoint
x) = (FixedPoint -> (FixedPoint, FixedPoint)
forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
exp_log FixedPoint
x (FixedPoint, FixedPoint) -> FixedPoint -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_FPIdemPotent' :: Positive FixedPoint -> Property
prop_FPIdemPotent' :: Positive FixedPoint -> Property
prop_FPIdemPotent' (Positive FixedPoint
x) = (FixedPoint -> (FixedPoint, FixedPoint)
forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
log_exp FixedPoint
x (FixedPoint, FixedPoint) -> FixedPoint -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_FPfindD :: Positive FixedPoint -> Property
prop_FPfindD :: Positive FixedPoint -> Property
prop_FPfindD (Positive FixedPoint
x) = FixedPoint -> Bool
forall a. (RealFrac a, Show a) => a -> Bool
findD FixedPoint
x Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_FPlnPow :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPlnPow :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPlnPow (Unit FixedPoint
x) (Unit FixedPoint
y) = (FixedPoint
x FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
> FixedPoint
0) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (FixedPoint -> FixedPoint -> (FixedPoint, FixedPoint)
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_pow FixedPoint
x FixedPoint
y (FixedPoint, FixedPoint) -> FixedPoint -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_neg_taylorExpCmp :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_neg_taylorExpCmp :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_neg_taylorExpCmp (Unit FixedPoint
p) (Unit FixedPoint
s) =
  (FixedPoint -> Bool) -> (FixedPoint, FixedPoint) -> Bool
forall a. (a -> Bool) -> (a, a) -> Bool
both (\FixedPoint
x -> FixedPoint
0 FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
< FixedPoint
x Bool -> Bool -> Bool
&& FixedPoint
x FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
< FixedPoint
1) (FixedPoint
p, FixedPoint
s) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
    FixedPoint -> FixedPoint -> FixedPoint -> Bool
forall a. RealFrac a => a -> a -> a -> Bool
taylorExpCmpCheck (FixedPoint -> FixedPoint
forall a. (RealFrac a, Show a) => a -> a
exp' FixedPoint
sm) FixedPoint
p FixedPoint
sm
  where
    sm :: FixedPoint
sm = -FixedPoint
s

prop_LeaderCmp :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_LeaderCmp :: UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_LeaderCmp (Unit FixedPoint
p) (Unit FixedPoint
s) =
  (FixedPoint -> Bool) -> (FixedPoint, FixedPoint) -> Bool
forall a. (a -> Bool) -> (a, a) -> Bool
both (\FixedPoint
x -> FixedPoint
0 FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
< FixedPoint
x Bool -> Bool -> Bool
&& FixedPoint
x FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
< FixedPoint
1) (FixedPoint
p, FixedPoint
s) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
    Bool -> String -> Bool -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify (FixedPoint
p FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
< FixedPoint
a) String
"is leader" (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
      FixedPoint -> FixedPoint -> FixedPoint -> FixedPoint -> Bool
forall a. (RealFrac a, Show a, Enum a) => a -> a -> a -> a -> Bool
praosLeaderCheck FixedPoint
f FixedPoint
a FixedPoint
p FixedPoint
s
  where
    a :: FixedPoint
a = FixedPoint -> FixedPoint -> FixedPoint
forall a. (RealFrac a, Show a, Enum a) => a -> a -> a
leader FixedPoint
f FixedPoint
s
    f :: FixedPoint
f = FixedPoint
1 FixedPoint -> FixedPoint -> FixedPoint
forall a. Fractional a => a -> a -> a
/ FixedPoint
10

-----------------------------------
-- Double Versions of Properties --
-----------------------------------

prop_DMonotonic :: Monotonic Double
prop_DMonotonic :: Monotonic Double
prop_DMonotonic Double -> Bool
constrain Double -> Double
f Double
x Double
y =
  (Double -> Bool) -> (Double, Double) -> Bool
forall a. (a -> Bool) -> (a, a) -> Bool
both Double -> Bool
constrain (Double
x, Double
y) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (Double -> Double) -> Double -> Double -> Bool
forall a b. (Ord a, Ord b) => (a -> b) -> a -> a -> Bool
monotonic Double -> Double
f Double
x Double
y

-- | Takes very long, but (e *** b) *** c is not an operation that we use.
prop_DPowDiff :: UnitInterval Double -> Normalized Double -> Property
prop_DPowDiff :: UnitInterval Double -> Normalized Double -> Property
prop_DPowDiff (Unit Double
z) (Norm (Double, Double)
w) = (Double -> (Double, Double) -> (Double, Double)
forall a. (RealFrac a, Enum a, Show a) => a -> (a, a) -> (a, a)
pow_Diff Double
z (Double, Double)
w (Double, Double) -> Double -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_DExpLaw :: UnitInterval Double -> UnitInterval Double -> Property
prop_DExpLaw :: UnitInterval Double -> UnitInterval Double -> Property
prop_DExpLaw (Unit Double
x) (Unit Double
y) = (Double -> Double -> (Double, Double)
forall a. (RealFrac a, Show a) => a -> a -> Diff a
exp_law Double
x Double
y (Double, Double) -> Double -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_DlnLaw :: Positive Double -> Positive Double -> Property
prop_DlnLaw :: Positive Double -> Positive Double -> Property
prop_DlnLaw (Positive Double
x) (Positive Double
y) = (Double -> Double -> (Double, Double)
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_law Double
x Double
y (Double, Double) -> Double -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_DExpUnitInterval :: UnitInterval Double -> UnitInterval Double -> Property
prop_DExpUnitInterval :: UnitInterval Double -> UnitInterval Double -> Property
prop_DExpUnitInterval (Unit Double
x) (Unit Double
y) = Double -> Double -> Bool
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Bool
exp_UnitInterval Double
x Double
y Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_DIdemPotent :: Positive Double -> Property
prop_DIdemPotent :: Positive Double -> Property
prop_DIdemPotent (Positive Double
x) = (Double -> (Double, Double)
forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
exp_log Double
x (Double, Double) -> Double -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_DIdemPotent' :: Positive Double -> Property
prop_DIdemPotent' :: Positive Double -> Property
prop_DIdemPotent' (Positive Double
x) = (Double -> (Double, Double)
forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
log_exp Double
x (Double, Double) -> Double -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_DfindD :: Positive Double -> Property
prop_DfindD :: Positive Double -> Property
prop_DfindD (Positive Double
x) = Double -> Bool
forall a. (RealFrac a, Show a) => a -> Bool
findD Double
x Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_DlnPow :: UnitInterval Double -> UnitInterval Double -> Property
prop_DlnPow :: UnitInterval Double -> UnitInterval Double -> Property
prop_DlnPow (Unit Double
x) (Unit Double
y) = (Double
x Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
0) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (Double -> Double -> (Double, Double)
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_pow Double
x Double
y (Double, Double) -> Double -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

-----------------------------
-- Properties for Rational --
-----------------------------

prop_Monotonic :: Monotonic Rational
prop_Monotonic :: Monotonic Rational
prop_Monotonic Rational -> Bool
constrain Rational -> Rational
f Rational
x Rational
y =
  (Rational -> Bool) -> (Rational, Rational) -> Bool
forall a. (a -> Bool) -> (a, a) -> Bool
both Rational -> Bool
constrain (Rational
x, Rational
y) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (Rational -> Rational) -> Rational -> Rational -> Bool
forall a b. (Ord a, Ord b) => (a -> b) -> a -> a -> Bool
monotonic Rational -> Rational
f Rational
x Rational
y

prop_PowDiff :: UnitInterval Rational -> Normalized Rational -> Property
prop_PowDiff :: UnitInterval Rational -> Normalized Rational -> Property
prop_PowDiff (Unit Rational
z) (Norm (Rational, Rational)
w) = (Rational -> (Rational, Rational) -> (Rational, Rational)
forall a. (RealFrac a, Enum a, Show a) => a -> (a, a) -> (a, a)
pow_Diff Rational
z (Rational, Rational)
w (Rational, Rational) -> Rational -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_ExpLaw :: UnitInterval Rational -> UnitInterval Rational -> Property
prop_ExpLaw :: UnitInterval Rational -> UnitInterval Rational -> Property
prop_ExpLaw (Unit Rational
x) (Unit Rational
y) = (Rational -> Rational -> (Rational, Rational)
forall a. (RealFrac a, Show a) => a -> a -> Diff a
exp_law Rational
x Rational
y (Rational, Rational) -> Rational -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_lnLaw :: Positive Rational -> Positive Rational -> Property
prop_lnLaw :: Positive Rational -> Positive Rational -> Property
prop_lnLaw (Positive Rational
x) (Positive Rational
y) = (Rational -> Rational -> (Rational, Rational)
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_law Rational
x Rational
y (Rational, Rational) -> Rational -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_ExpUnitInterval :: UnitInterval Rational -> UnitInterval Rational -> Property
prop_ExpUnitInterval :: UnitInterval Rational -> UnitInterval Rational -> Property
prop_ExpUnitInterval (Unit Rational
x) (Unit Rational
y) = Rational -> Rational -> Bool
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Bool
exp_UnitInterval Rational
x Rational
y Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_IdemPotent :: Positive Rational -> Property
prop_IdemPotent :: Positive Rational -> Property
prop_IdemPotent (Positive Rational
x) = (Rational -> (Rational, Rational)
forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
exp_log Rational
x (Rational, Rational) -> Rational -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_IdemPotent' :: Positive Rational -> Property
prop_IdemPotent' :: Positive Rational -> Property
prop_IdemPotent' (Positive Rational
x) = (Rational -> (Rational, Rational)
forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
log_exp Rational
x (Rational, Rational) -> Rational -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_findD :: Positive Rational -> Property
prop_findD :: Positive Rational -> Property
prop_findD (Positive Rational
x) = Rational -> Bool
forall a. (RealFrac a, Show a) => a -> Bool
findD Rational
x Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

prop_lnPow :: UnitInterval Rational -> UnitInterval Rational -> Property
prop_lnPow :: UnitInterval Rational -> UnitInterval Rational -> Property
prop_lnPow (Unit Rational
x) (Unit Rational
y) = (Rational
x Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (Rational -> Rational -> (Rational, Rational)
forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_pow Rational
x Rational
y (Rational, Rational) -> Rational -> Bool
forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

qcWithLabel :: Testable prop => String -> Int -> prop -> IO ()
qcWithLabel :: forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel String
text Int
count prop
prop = do
  String -> IO ()
putStrLn String
text
  if Int
count Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
    then Property -> IO ()
forall prop. Testable prop => prop -> IO ()
quickCheck (Int -> prop -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
count prop
prop)
    else String -> IO ()
putStrLn String
"--- SKIPPED, takes too long"

-- Test of Double  --

property_exponential_is_monotonic_db :: IO ()
property_exponential_is_monotonic_db :: IO ()
property_exponential_is_monotonic_db =
  String -> Int -> (Double -> Double -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property-exponential-is-monotonic"
    Int
1000
    ((Double -> Double -> Property) -> IO ())
-> (Double -> Double -> Property) -> IO ()
forall a b. (a -> b) -> a -> b
$ Monotonic Double
prop_DMonotonic (Bool -> Double -> Bool
forall a b. a -> b -> a
const Bool
True) Double -> Double
forall a. (RealFrac a, Show a) => a -> a
exp'

property_logarithm_is_monotonic_db :: IO ()
property_logarithm_is_monotonic_db :: IO ()
property_logarithm_is_monotonic_db =
  String -> Int -> (Double -> Double -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm is monotonic"
    Int
1000
    ((Double -> Double -> Property) -> IO ())
-> (Double -> Double -> Property) -> IO ()
forall a b. (a -> b) -> a -> b
$ Monotonic Double
prop_DMonotonic (Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
0) Double -> Double
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln'

property_exp_maps_unit_interval_to_unit_interval_db :: IO ()
property_exp_maps_unit_interval_to_unit_interval_db :: IO ()
property_exp_maps_unit_interval_to_unit_interval_db =
  String
-> Int
-> (UnitInterval Double -> UnitInterval Double -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x,y in [0,1] -> x^y in [0,1]"
    Int
1000
    UnitInterval Double -> UnitInterval Double -> Property
prop_DExpUnitInterval

property_exp_of_ln_db :: IO ()
property_exp_of_ln_db :: IO ()
property_exp_of_ln_db =
  String -> Int -> (Positive Double -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x > 0 -> exp(ln(x)) = x"
    Int
1000
    Positive Double -> Property
prop_DIdemPotent

property_ln_of_exp_db :: IO ()
property_ln_of_exp_db :: IO ()
property_ln_of_exp_db =
  String -> Int -> (Positive Double -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x > 0 -> ln(exp(x)) = x"
    Int
1000
    Positive Double -> Property
prop_DIdemPotent'

property_power_diff_db :: IO ()
property_power_diff_db :: IO ()
property_power_diff_db =
  String
-> Int
-> (UnitInterval Double -> Normalized Double -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property pow diff in [0,1]: (a^(1/x))^y = (a^y)^(1/x)"
    Int
1000
    UnitInterval Double -> Normalized Double -> Property
prop_DPowDiff

property_exponential_law_db :: IO ()
property_exponential_law_db :: IO ()
property_exponential_law_db =
  String
-> Int
-> (UnitInterval Double -> UnitInterval Double -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property exponential law in [0,1]: exp(x + y) = exp(x) · exp(y)"
    Int
1000
    UnitInterval Double -> UnitInterval Double -> Property
prop_DExpLaw

property_log_law_db :: IO ()
property_log_law_db :: IO ()
property_log_law_db =
  String
-> Int -> (Positive Double -> Positive Double -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm law in (0,..): ln(x · y) = ln(x) + ln(y)"
    Int
1000
    Positive Double -> Positive Double -> Property
prop_DlnLaw

property_log_power_db :: IO ()
property_log_power_db :: IO ()
property_log_power_db =
  String
-> Int
-> (UnitInterval Double -> UnitInterval Double -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm of pow in [0,1]: ln(x^y) = y · ln(x)"
    Int
1000
    UnitInterval Double -> UnitInterval Double -> Property
prop_DlnPow

property_bound_findE_db :: IO ()
property_bound_findE_db :: IO ()
property_bound_findE_db =
  String -> Int -> (Positive Double -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"check bound of `findE`"
    Int
1000
    Positive Double -> Property
prop_DfindD

-- Test of 34 Decimal Digits Fixed Point --

prop_exp_is_monotonic_fp :: IO ()
prop_exp_is_monotonic_fp :: IO ()
prop_exp_is_monotonic_fp =
  String -> Int -> (FixedPoint -> FixedPoint -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property exponential is monotonic"
    Int
1000
    ((FixedPoint -> FixedPoint -> Property) -> IO ())
-> (FixedPoint -> FixedPoint -> Property) -> IO ()
forall a b. (a -> b) -> a -> b
$ Monotonic FixedPoint
prop_FPMonotonic (Bool -> FixedPoint -> Bool
forall a b. a -> b -> a
const Bool
True) FixedPoint -> FixedPoint
forall a. (RealFrac a, Show a) => a -> a
exp'

prop_log_is_monotonic_fp :: IO ()
prop_log_is_monotonic_fp :: IO ()
prop_log_is_monotonic_fp =
  String -> Int -> (FixedPoint -> FixedPoint -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm is monotonic"
    Int
1000
    ((FixedPoint -> FixedPoint -> Property) -> IO ())
-> (FixedPoint -> FixedPoint -> Property) -> IO ()
forall a b. (a -> b) -> a -> b
$ Monotonic FixedPoint
prop_FPMonotonic (FixedPoint -> FixedPoint -> Bool
forall a. Ord a => a -> a -> Bool
> FixedPoint
0) FixedPoint -> FixedPoint
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln'

property_exp_maps_unit_interval_to_unit_interval_fp :: IO ()
property_exp_maps_unit_interval_to_unit_interval_fp :: IO ()
property_exp_maps_unit_interval_to_unit_interval_fp =
  String
-> Int
-> (UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x,y in [0,1] -> x^y in [0,1]"
    Int
1000
    UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPExpUnitInterval

property_exp_of_ln_fp :: IO ()
property_exp_of_ln_fp :: IO ()
property_exp_of_ln_fp =
  String -> Int -> (Positive FixedPoint -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x > 0 -> exp(ln(x)) = x"
    Int
1000
    Positive FixedPoint -> Property
prop_FPIdemPotent

property_ln_of_exp_fp :: IO ()
property_ln_of_exp_fp :: IO ()
property_ln_of_exp_fp =
  String -> Int -> (Positive FixedPoint -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x > 0 -> ln(exp(x)) = x"
    Int
1000
    Positive FixedPoint -> Property
prop_FPIdemPotent'

property_power_diff_fp :: IO ()
property_power_diff_fp :: IO ()
property_power_diff_fp =
  String
-> Int
-> (UnitInterval FixedPoint -> Normalized FixedPoint -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property pow diff in [0,1]: (a^(1/x))^y = (a^y)^(1/x)"
    Int
1000
    UnitInterval FixedPoint -> Normalized FixedPoint -> Property
prop_FPPowDiff

property_exponential_law_fp :: IO ()
property_exponential_law_fp :: IO ()
property_exponential_law_fp =
  String
-> Int
-> (UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property exponential law in [0,1]: exp(x + y) = exp(x) · exp(y)"
    Int
1000
    UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPExpLaw

property_log_law_fp :: IO ()
property_log_law_fp :: IO ()
property_log_law_fp =
  String
-> Int
-> (Positive FixedPoint -> Positive FixedPoint -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm law in (0,..): ln(x · y) = ln(x) + ln(y)"
    Int
1000
    Positive FixedPoint -> Positive FixedPoint -> Property
prop_FPlnLaw

property_log_power_fp :: IO ()
property_log_power_fp :: IO ()
property_log_power_fp =
  String
-> Int
-> (UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm of pow in [0,1]: ln(x^y) = y · ln(x)"
    Int
1000
    UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_FPlnPow

property_bound_findE_fp :: IO ()
property_bound_findE_fp :: IO ()
property_bound_findE_fp =
  String -> Int -> (Positive FixedPoint -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"check bound of `findE`"
    Int
1000
    Positive FixedPoint -> Property
prop_FPfindD

property_negative_taylorExpCmp_comparison :: IO ()
property_negative_taylorExpCmp_comparison :: IO ()
property_negative_taylorExpCmp_comparison =
  String
-> Int
-> (UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property negative taylorExpCmp check"
    Int
10000
    UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_neg_taylorExpCmp

property_praos_leader_comparison :: IO ()
property_praos_leader_comparison :: IO ()
property_praos_leader_comparison =
  String
-> Int
-> (UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property σ,p in [0,1]: p < 1 - (1 - f)^σ <=> taylorExpCmp 3 (1/(1 - p)) (-σ · ln (1 - f))"
    Int
10000
    UnitInterval FixedPoint -> UnitInterval FixedPoint -> Property
prop_LeaderCmp

-- Test of Rational Numbers --

prop_exp_is_monotonic_q :: IO ()
prop_exp_is_monotonic_q :: IO ()
prop_exp_is_monotonic_q =
  String -> Int -> (Rational -> Rational -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property exponential is monotonic"
    Int
10
    ((Rational -> Rational -> Property) -> IO ())
-> (Rational -> Rational -> Property) -> IO ()
forall a b. (a -> b) -> a -> b
$ Monotonic Rational
prop_Monotonic (Bool -> Rational -> Bool
forall a b. a -> b -> a
const Bool
True) Rational -> Rational
forall a. (RealFrac a, Show a) => a -> a
exp'

prop_log_is_monotonic_q :: IO ()
prop_log_is_monotonic_q :: IO ()
prop_log_is_monotonic_q =
  String -> Int -> (Rational -> Rational -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm is monotonic"
    Int
10
    ((Rational -> Rational -> Property) -> IO ())
-> (Rational -> Rational -> Property) -> IO ()
forall a b. (a -> b) -> a -> b
$ Monotonic Rational
prop_Monotonic (Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0) Rational -> Rational
forall a. (RealFrac a, Enum a, Show a) => a -> a
ln'

property_exp_maps_unit_interval_to_unit_interval_q :: IO ()
property_exp_maps_unit_interval_to_unit_interval_q :: IO ()
property_exp_maps_unit_interval_to_unit_interval_q =
  String
-> Int
-> (UnitInterval Rational -> UnitInterval Rational -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x,y in [0,1] -> x^y in [0,1]"
    Int
10
    UnitInterval Rational -> UnitInterval Rational -> Property
prop_ExpUnitInterval

property_exp_of_ln_q :: IO ()
property_exp_of_ln_q :: IO ()
property_exp_of_ln_q =
  String -> Int -> (Positive Rational -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x > 0 -> exp(ln(x)) = x"
    Int
10
    Positive Rational -> Property
prop_IdemPotent

property_ln_of_exp_q :: IO ()
property_ln_of_exp_q :: IO ()
property_ln_of_exp_q =
  String -> Int -> (Positive Rational -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property x > 0 -> ln(exp(x)) = x"
    Int
10
    Positive Rational -> Property
prop_IdemPotent'

property_power_diff_q :: IO ()
property_power_diff_q :: IO ()
property_power_diff_q =
  String
-> Int
-> (UnitInterval Rational -> Normalized Rational -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property pow diff in [0,1]: (a^(1/x))^y = (a^y)^(1/x)"
    Int
0
    UnitInterval Rational -> Normalized Rational -> Property
prop_PowDiff

property_exponential_law_q :: IO ()
property_exponential_law_q :: IO ()
property_exponential_law_q =
  String
-> Int
-> (UnitInterval Rational -> UnitInterval Rational -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property exponential law in [0,1]: exp(x + y) = exp(x) · exp(y)"
    Int
10
    UnitInterval Rational -> UnitInterval Rational -> Property
prop_ExpLaw

property_log_law_q :: IO ()
property_log_law_q :: IO ()
property_log_law_q =
  String
-> Int
-> (Positive Rational -> Positive Rational -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm law in (0,..): ln(x · y) = ln(x) + ln(y)"
    Int
10
    Positive Rational -> Positive Rational -> Property
prop_lnLaw

property_log_power_q :: IO ()
property_log_power_q :: IO ()
property_log_power_q =
  String
-> Int
-> (UnitInterval Rational -> UnitInterval Rational -> Property)
-> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm of pow in [0,1]: ln(x^y) = y · ln(x)"
    Int
0
    UnitInterval Rational -> UnitInterval Rational -> Property
prop_lnPow

property_bound_findE_q :: IO ()
property_bound_findE_q :: IO ()
property_bound_findE_q =
  String -> Int -> (Positive Rational -> Property) -> IO ()
forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"check bound of `findE`"
    Int
100
    Positive Rational -> Property
prop_findD