{-# 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 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 forall a. Fractional a => a -> a -> a
/ Double
10 forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
12 :: Int)

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

eps :: Rational
eps :: Rational
eps = Rational
1 forall a. Fractional a => a -> a -> a
/ Rational
10 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) = forall a. Num a => a -> a
abs (a
x 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 = forall a. Num a => Diff a -> a
absDiff Diff a
w forall a. Ord a => a -> a -> Bool
< a
epsilon

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

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

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

instance (Fractional a, Arbitrary a) => Arbitrary (UnitInterval a) where
  arbitrary :: Gen (UnitInterval a)
arbitrary = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> UnitInterval a
Unit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => NonNegInts -> a
toUnit forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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) = (forall a. Ord a => a -> a -> a
min Integer
x Integer
y, 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 = forall a b. (a -> b) -> (a, a) -> (b, b)
map2 forall a. Num a => Integer -> a
fromInteger 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 = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Fractional a => a -> a -> a
(/) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> a -> Bool
< a
y
    then a -> b
f a
x forall a. Ord a => a -> a -> Bool
< a -> b
f a
y
    else a -> b
f a
x 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 = (forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' (a
x forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
y), a
y forall a. Num 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 = (forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' (a
x forall a. Num a => a -> a -> a
* a
y), forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' a
x forall a. Num 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 = (forall a. (RealFrac a, Show a) => a -> a
exp' (a
x forall a. Num a => a -> a -> a
+ a
y), forall a. (RealFrac a, Show a) => a -> a
exp' a
x forall a. Num 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 = (forall a. (RealFrac a, Show a) => a -> a
exp' (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 = (forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' (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 forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
y in a
z forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& a
z 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 forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Integer
n forall a. Ord a => a -> a -> Bool
<= a
x Bool -> Bool -> Bool
&& a
x forall a. Ord a => a -> a -> Bool
< a
e forall a b. (Fractional a, Integral b) => a -> b -> a
^^ (Integer
n forall a. Num a => a -> a -> a
+ Integer
1)
  where
    n :: Integer
n = forall a. RealFrac a => a -> a -> Integer
findE a
e a
x
    e :: a
e = 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 forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** (a
1 forall a. Fractional a => a -> a -> a
/ a
x)) forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
y, (a
z forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** a
y) forall a. (RealFrac a, Enum a, Show a) => a -> a -> a
*** (a
1 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 forall a. Num a => a -> a -> a
- ((a
1 forall a. Num a => a -> a -> a
- a
f) 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 forall a. RealFrac a => a -> a -> a -> CompareResult a
taylorExpCmp a
3 a
p a
s of
  ABOVE a
_ Int
_ -> a
p forall a. Ord a => a -> a -> Bool
>= a
a
  BELOW a
_ Int
_ -> a
p 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 forall a. RealFrac a => a -> a -> a -> CompareResult a
taylorExpCmp a
3 (a
1 forall a. Fractional a => a -> a -> a
/ a
q) (-a
sigma forall a. Num a => a -> a -> a
* a
c) of
  ABOVE a
_ Int
_ -> a
p forall a. Ord a => a -> a -> Bool
>= a
a
  BELOW a
_ Int
_ -> a
p forall a. Ord a => a -> a -> Bool
< a
a
  MaxReached Int
_ -> Bool
False
  where
    c :: a
c = forall a. (RealFrac a, Enum a, Show a) => a -> a
ln' (a
1 forall a. Num a => a -> a -> a
- a
f)
    q :: a
q = a
1 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 =
  forall a. (a -> Bool) -> (a, a) -> Bool
both FixedPoint -> Bool
constrain (FixedPoint
x, FixedPoint
y) forall prop. Testable prop => Bool -> prop -> Property
==>
    forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
zeroes String
"both zero case" forall a b. (a -> b) -> a -> b
$
      (Bool
zeroes Bool -> Bool -> Bool
|| forall a b. (Ord a, Ord b) => (a -> b) -> a -> a -> Bool
monotonic FixedPoint -> FixedPoint
f FixedPoint
x FixedPoint
y) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
  where
    zeroes :: Bool
zeroes = 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) 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 = forall a. Num a => Diff a -> a
absDiff (forall a. (RealFrac a, Enum a, Show a) => a -> (a, a) -> (a, a)
pow_Diff FixedPoint
z (FixedPoint, FixedPoint)
w)
   in forall prop. Testable prop => Bool -> String -> prop -> Property
classify (FixedPoint
e forall a. Ord a => a -> a -> Bool
< FixedPoint
epsFP) String
"OK 10e-16" forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => Bool -> String -> prop -> Property
classify (FixedPoint
e forall a. Ord a => a -> a -> Bool
< FixedPoint
epsFP forall a. Num a => a -> a -> a
* FixedPoint
1000 Bool -> Bool -> Bool
&& FixedPoint
e forall a. Ord a => a -> a -> Bool
>= FixedPoint
epsFP) String
"OK 10e-12" forall a b. (a -> b) -> a -> b
$
          forall prop. Testable prop => Bool -> String -> prop -> Property
classify (FixedPoint
e forall a. Ord a => a -> a -> Bool
>= FixedPoint
epsFP forall a. Num a => a -> a -> a
* FixedPoint
1000) String
"KO" forall a b. (a -> b) -> a -> b
$
            Bool
True 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) = (forall a. (RealFrac a, Show a) => a -> a -> Diff a
exp_law FixedPoint
x FixedPoint
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_law FixedPoint
x FixedPoint
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) 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) = forall a. (RealFrac a, Show a, Enum a) => a -> a -> Bool
exp_UnitInterval FixedPoint
x FixedPoint
y 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
exp_log FixedPoint
x forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
log_exp FixedPoint
x forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) 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) = forall a. (RealFrac a, Show a) => a -> Bool
findD FixedPoint
x 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 forall a. Ord a => a -> a -> Bool
> FixedPoint
0) forall prop. Testable prop => Bool -> prop -> Property
==> (forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_pow FixedPoint
x FixedPoint
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= FixedPoint
epsFP) 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) =
  forall a. (a -> Bool) -> (a, a) -> Bool
both (\FixedPoint
x -> FixedPoint
0 forall a. Ord a => a -> a -> Bool
< FixedPoint
x Bool -> Bool -> Bool
&& FixedPoint
x forall a. Ord a => a -> a -> Bool
< FixedPoint
1) (FixedPoint
p, FixedPoint
s) forall prop. Testable prop => Bool -> prop -> Property
==>
    forall a. RealFrac a => a -> a -> a -> Bool
taylorExpCmpCheck (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) =
  forall a. (a -> Bool) -> (a, a) -> Bool
both (\FixedPoint
x -> FixedPoint
0 forall a. Ord a => a -> a -> Bool
< FixedPoint
x Bool -> Bool -> Bool
&& FixedPoint
x forall a. Ord a => a -> a -> Bool
< FixedPoint
1) (FixedPoint
p, FixedPoint
s) forall prop. Testable prop => Bool -> prop -> Property
==>
    forall prop. Testable prop => Bool -> String -> prop -> Property
classify (FixedPoint
p forall a. Ord a => a -> a -> Bool
< FixedPoint
a) String
"is leader" forall a b. (a -> b) -> a -> b
$
      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 = forall a. (RealFrac a, Show a, Enum a) => a -> a -> a
leader FixedPoint
f FixedPoint
s
    f :: FixedPoint
f = FixedPoint
1 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 =
  forall a. (a -> Bool) -> (a, a) -> Bool
both Double -> Bool
constrain (Double
x, Double
y) forall prop. Testable prop => Bool -> prop -> Property
==> 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) = (forall a. (RealFrac a, Enum a, Show a) => a -> (a, a) -> (a, a)
pow_Diff Double
z (Double, Double)
w forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) 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) = (forall a. (RealFrac a, Show a) => a -> a -> Diff a
exp_law Double
x Double
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_law Double
x Double
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) 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) = forall a. (RealFrac a, Show a, Enum a) => a -> a -> Bool
exp_UnitInterval Double
x Double
y 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
exp_log Double
x forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
log_exp Double
x forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) 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) = forall a. (RealFrac a, Show a) => a -> Bool
findD Double
x 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 forall a. Ord a => a -> a -> Bool
> Double
0) forall prop. Testable prop => Bool -> prop -> Property
==> (forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_pow Double
x Double
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Double
epsD) 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 =
  forall a. (a -> Bool) -> (a, a) -> Bool
both Rational -> Bool
constrain (Rational
x, Rational
y) forall prop. Testable prop => Bool -> prop -> Property
==> 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) = (forall a. (RealFrac a, Enum a, Show a) => a -> (a, a) -> (a, a)
pow_Diff Rational
z (Rational, Rational)
w forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) 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) = (forall a. (RealFrac a, Show a) => a -> a -> Diff a
exp_law Rational
x Rational
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_law Rational
x Rational
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) 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) = forall a. (RealFrac a, Show a, Enum a) => a -> a -> Bool
exp_UnitInterval Rational
x Rational
y 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
exp_log Rational
x forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) 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) = (forall a. (RealFrac a, Show a, Enum a) => a -> Diff a
log_exp Rational
x forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) 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) = forall a. (RealFrac a, Show a) => a -> Bool
findD Rational
x 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 forall a. Ord a => a -> a -> Bool
> Rational
0) forall prop. Testable prop => Bool -> prop -> Property
==> (forall a. (RealFrac a, Show a, Enum a) => a -> a -> Diff a
log_pow Rational
x Rational
y forall a. (Ord a, Num a) => Diff a -> a -> Bool
~= Rational
eps) 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 forall a. Ord a => a -> a -> Bool
> Int
0
    then forall prop. Testable prop => prop -> IO ()
quickCheck (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 =
  forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property-exponential-is-monotonic"
    Int
1000
    forall a b. (a -> b) -> a -> b
$ Monotonic Double
prop_DMonotonic (forall a b. a -> b -> a
const Bool
True) 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 =
  forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm is monotonic"
    Int
1000
    forall a b. (a -> b) -> a -> b
$ Monotonic Double
prop_DMonotonic (forall a. Ord a => a -> a -> Bool
> Double
0) 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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property exponential is monotonic"
    Int
1000
    forall a b. (a -> b) -> a -> b
$ Monotonic FixedPoint
prop_FPMonotonic (forall a b. a -> b -> a
const Bool
True) 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 =
  forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm is monotonic"
    Int
1000
    forall a b. (a -> b) -> a -> b
$ Monotonic FixedPoint
prop_FPMonotonic (forall a. Ord a => a -> a -> Bool
> FixedPoint
0) 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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property exponential is monotonic"
    Int
10
    forall a b. (a -> b) -> a -> b
$ Monotonic Rational
prop_Monotonic (forall a b. a -> b -> a
const Bool
True) 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 =
  forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"property logarithm is monotonic"
    Int
10
    forall a b. (a -> b) -> a -> b
$ Monotonic Rational
prop_Monotonic (forall a. Ord a => a -> a -> Bool
> Rational
0) 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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  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 =
  forall prop. Testable prop => String -> Int -> prop -> IO ()
qcWithLabel
    String
"check bound of `findE`"
    Int
100
    Positive Rational -> Property
prop_findD