{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}

-- | Tests for self-explaning boolean predicates
module Test.Consensus.Util.Pred (tests) where

import Ouroboros.Consensus.Util.Pred
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck
  ( Arbitrary (..)
  , Gen
  , Property
  , forAll
  , frequency
  , sized
  , tabulate
  , testProperty
  , (===)
  )
import Test.Util.TestEnv (adjustQuickCheckTests)

tests :: TestTree
tests :: TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Pred"
    [ TestTree
evidenceUnitTests
    , TestTree
explanationUnitTests
    , TestTree
propertyTests
    ]

{-------------------------------------------------------------------------------
  Unit tests
-------------------------------------------------------------------------------}

-- Setup

data Prop = P | Q | R
  deriving stock (Int -> Prop -> ShowS
[Prop] -> ShowS
Prop -> TestName
(Int -> Prop -> ShowS)
-> (Prop -> TestName) -> ([Prop] -> ShowS) -> Show Prop
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Prop -> ShowS
showsPrec :: Int -> Prop -> ShowS
$cshow :: Prop -> TestName
show :: Prop -> TestName
$cshowList :: [Prop] -> ShowS
showList :: [Prop] -> ShowS
Show, Prop -> Prop -> Bool
(Prop -> Prop -> Bool) -> (Prop -> Prop -> Bool) -> Eq Prop
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Prop -> Prop -> Bool
== :: Prop -> Prop -> Bool
$c/= :: Prop -> Prop -> Bool
/= :: Prop -> Prop -> Bool
Eq)
  deriving Int -> ExplanationMode -> Prop -> TestName
ExplanationMode -> Prop -> TestName
(ExplanationMode -> Prop -> TestName)
-> (Int -> ExplanationMode -> Prop -> TestName) -> Explainable Prop
forall a.
(ExplanationMode -> a -> TestName)
-> (Int -> ExplanationMode -> a -> TestName) -> Explainable a
$cexplain :: ExplanationMode -> Prop -> TestName
explain :: ExplanationMode -> Prop -> TestName
$cexplainPrec :: Int -> ExplanationMode -> Prop -> TestName
explainPrec :: Int -> ExplanationMode -> Prop -> TestName
Explainable via ShowExplain Prop

p :: Pred Prop -- ~ True
p :: Pred Prop
p = Prop
P Prop -> Pred Prop -> Pred Prop
forall tag. tag -> Pred tag -> Pred tag
:= Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
True

q :: Pred Prop -- ~ False
q :: Pred Prop
q = Prop
Q Prop -> Pred Prop -> Pred Prop
forall tag. tag -> Pred tag -> Pred tag
:= (Int
5 Int -> Int -> Pred Prop
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
:<=: (Int
3 :: Int))

r :: Pred Prop -- ~ True
r :: Pred Prop
r = Prop
R Prop -> Pred Prop -> Pred Prop
forall tag. tag -> Pred tag -> Pred tag
:= Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not (Int
4 Int -> Int -> Pred Prop
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
:<=: (Int
2 :: Int))

proves :: Pred Prop -> Pred Prop -> TestTree
Pred Prop
evidence proves :: Pred Prop -> Pred Prop -> TestTree
`proves` Pred Prop
predicate =
  TestName -> Assertion -> TestTree
testCase
    (Pred Prop -> TestName
forall a. Explainable a => a -> TestName
explainDeep Pred Prop
evidence TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" ⊢ " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Pred Prop -> TestName
forall a. Explainable a => a -> TestName
explainShallow Pred Prop
predicate TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" => ⊤")
    ( Pred Prop
-> (forall (res :: Bool). Evidence res Prop -> Assertion)
-> Assertion
forall tag r.
Pred tag -> (forall (res :: Bool). Evidence res tag -> r) -> r
evalPred Pred Prop
predicate ((forall (res :: Bool). Evidence res Prop -> Assertion)
 -> Assertion)
-> (forall (res :: Bool). Evidence res Prop -> Assertion)
-> Assertion
forall a b. (a -> b) -> a -> b
$ \case
        ETrue Pred Prop
evidence' ->
          Pred Prop
evidence' Pred Prop -> Pred Prop -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Pred Prop
evidence
        EFalse Pred Prop
evidence' ->
          TestName -> Assertion
forall a. HasCallStack => TestName -> IO a
assertFailure (TestName -> Assertion) -> TestName -> Assertion
forall a b. (a -> b) -> a -> b
$ TestName
"Expected ETrue, but got EFalse: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Pred Prop -> TestName
forall a. Show a => a -> TestName
show Pred Prop
evidence'
    )

infix 1 `proves`

refutes :: Pred Prop -> Pred Prop -> TestTree
Pred Prop
evidence refutes :: Pred Prop -> Pred Prop -> TestTree
`refutes` Pred Prop
predicate =
  TestName -> Assertion -> TestTree
testCase
    (Pred Prop -> TestName
forall a. Explainable a => a -> TestName
explainDeep Pred Prop
evidence TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" ⊢ " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Pred Prop -> TestName
forall a. Explainable a => a -> TestName
explainShallow Pred Prop
predicate)
    ( Pred Prop
-> (forall (res :: Bool). Evidence res Prop -> Assertion)
-> Assertion
forall tag r.
Pred tag -> (forall (res :: Bool). Evidence res tag -> r) -> r
evalPred Pred Prop
predicate ((forall (res :: Bool). Evidence res Prop -> Assertion)
 -> Assertion)
-> (forall (res :: Bool). Evidence res Prop -> Assertion)
-> Assertion
forall a b. (a -> b) -> a -> b
$ \case
        EFalse Pred Prop
evidence' ->
          Pred Prop
evidence' Pred Prop -> Pred Prop -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Pred Prop
evidence
        ETrue Pred Prop
evidence' ->
          TestName -> Assertion
forall a. HasCallStack => TestName -> IO a
assertFailure (TestName -> Assertion) -> TestName -> Assertion
forall a b. (a -> b) -> a -> b
$ TestName
"Expected EFalse, but got ETrue: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Pred Prop -> TestName
forall a. Show a => a -> TestName
show Pred Prop
evidence'
    )

infix 1 `refutes`

eq_explain :: (Show a, Explainable a) => ExplanationMode -> a -> a -> TestTree
eq_explain :: forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
eq_explain ExplanationMode
mode a
x a
y =
  TestName -> Assertion -> TestTree
testCase
    ( TestName
"explain "
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> ExplanationMode -> TestName
forall a. Show a => a -> TestName
show ExplanationMode
mode
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" "
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
x
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" == explain "
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> ExplanationMode -> TestName
forall a. Show a => a -> TestName
show ExplanationMode
mode
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" "
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
y
    )
    (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ TestName -> TestName -> TestName -> Assertion
forall a.
(Eq a, Show a, HasCallStack) =>
TestName -> a -> a -> Assertion
assertEqual
      TestName
"Expected equal explanations:"
      (ExplanationMode -> a -> TestName
forall a. Explainable a => ExplanationMode -> a -> TestName
explain ExplanationMode
mode a
x)
      (ExplanationMode -> a -> TestName
forall a. Explainable a => ExplanationMode -> a -> TestName
explain ExplanationMode
mode a
y)

neq_explain :: (Show a, Explainable a) => ExplanationMode -> a -> a -> TestTree
neq_explain :: forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
neq_explain ExplanationMode
mode a
x a
y =
  TestName -> Assertion -> TestTree
testCase
    ( TestName
"explain "
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> ExplanationMode -> TestName
forall a. Show a => a -> TestName
show ExplanationMode
mode
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" "
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
x
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" /= explain "
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> ExplanationMode -> TestName
forall a. Show a => a -> TestName
show ExplanationMode
mode
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" "
        TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
y
    )
    (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ TestName -> TestName -> TestName -> Assertion
forall a. (Eq a, Show a) => TestName -> a -> a -> Assertion
assertNotEqual
      TestName
"Expected different explanations:"
      (ExplanationMode -> a -> TestName
forall a. Explainable a => ExplanationMode -> a -> TestName
explain ExplanationMode
mode a
x)
      (ExplanationMode -> a -> TestName
forall a. Explainable a => ExplanationMode -> a -> TestName
explain ExplanationMode
mode a
y)

-- Surprising this is not already in 'tasty-hunit'
assertNotEqual :: (Eq a, Show a) => String -> a -> a -> IO ()
assertNotEqual :: forall a. (Eq a, Show a) => TestName -> a -> a -> Assertion
assertNotEqual TestName
preface a
expected a
actual
  | a
actual a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
expected = () -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise = TestName -> Assertion
forall a. HasCallStack => TestName -> IO a
assertFailure TestName
msg
 where
  msg :: TestName
msg =
    (if TestName -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null TestName
preface then TestName
"" else TestName
preface TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
"\n")
      TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
"\n but got: "
      TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
actual

-- | Basic tests ensuring that predicates produce the right evidence
evidenceUnitTests :: TestTree
evidenceUnitTests :: TestTree
evidenceUnitTests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"evidence unit tests"
    [ Pred Prop
p Pred Prop -> Pred Prop -> TestTree
`proves` Pred Prop
p
    , Pred Prop
q Pred Prop -> Pred Prop -> TestTree
`refutes` Pred Prop
q
    , Pred Prop
r Pred Prop -> Pred Prop -> TestTree
`proves` Pred Prop
r
    , Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not Pred Prop
p Pred Prop -> Pred Prop -> TestTree
`refutes` Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not Pred Prop
p
    , Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not Pred Prop
q Pred Prop -> Pred Prop -> TestTree
`proves` Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not Pred Prop
q
    , Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not Pred Prop
r Pred Prop -> Pred Prop -> TestTree
`refutes` Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not Pred Prop
r
    , Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
r Pred Prop -> Pred Prop -> TestTree
`proves` Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
r
    , Pred Prop
q Pred Prop -> Pred Prop -> TestTree
`refutes` Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
q
    , Pred Prop
q Pred Prop -> Pred Prop -> TestTree
`refutes` Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
r
    , Pred Prop
p Pred Prop -> Pred Prop -> TestTree
`proves` Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
q
    , Pred Prop
p Pred Prop -> Pred Prop -> TestTree
`proves` Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
p
    , Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
r Pred Prop -> Pred Prop -> TestTree
`proves` (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
q) Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: (Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
r)
    ]

-- Basic explanation rendering tests.
--
-- NOTE: we can't easily test equality/inequality of explanations without
-- turning these test into an annoying change detector (see [1]) but we
-- still _can_ test some specific case regarding operator precedence and
-- distributivity that should always hold regardless of implementation.
--
-- [1]: https://testing.googleblog.com/2015/01/testing-on-toilet-change-detector-tests.html
explanationUnitTests :: TestTree
explanationUnitTests :: TestTree
explanationUnitTests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"explain"
    ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ [[TestTree]] -> [TestTree]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ ExplanationMode -> Pred Prop -> Pred Prop -> TestTree
forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
eq_explain ExplanationMode
mode (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
r) ((Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
q) Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
r)
        , ExplanationMode -> Pred Prop -> Pred Prop -> TestTree
forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
eq_explain ExplanationMode
mode (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
r) (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: (Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
r))
        , ExplanationMode -> Pred Prop -> Pred Prop -> TestTree
forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
neq_explain ExplanationMode
mode (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
r) (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: (Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
r))
        , ExplanationMode -> Pred Prop -> Pred Prop -> TestTree
forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
neq_explain ExplanationMode
mode (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
q Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
r) ((Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
q) Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
r)
        , ExplanationMode -> Pred Prop -> Pred Prop -> TestTree
forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
neq_explain ExplanationMode
mode (Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
q)) (Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred Prop
q)
        , ExplanationMode -> Pred Prop -> Pred Prop -> TestTree
forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
neq_explain ExplanationMode
mode (Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not (Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
q)) (Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag
Not Pred Prop
p Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred Prop
q)
        , ExplanationMode -> Pred Prop -> Pred Prop -> TestTree
forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
neq_explain ExplanationMode
mode (Prop
P Prop -> Pred Prop -> Pred Prop
forall tag. tag -> Pred tag -> Pred tag
:= Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
True Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
False) ((Prop
P Prop -> Pred Prop -> Pred Prop
forall tag. tag -> Pred tag -> Pred tag
:= Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
True) Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
False)
        , ExplanationMode -> Pred Prop -> Pred Prop -> TestTree
forall a.
(Show a, Explainable a) =>
ExplanationMode -> a -> a -> TestTree
neq_explain ExplanationMode
mode (Prop
P Prop -> Pred Prop -> Pred Prop
forall tag. tag -> Pred tag -> Pred tag
:= Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
True Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
False) ((Prop
P Prop -> Pred Prop -> Pred Prop
forall tag. tag -> Pred tag -> Pred tag
:= Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
True) Pred Prop -> Pred Prop -> Pred Prop
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Bool -> Pred Prop
forall tag. Bool -> Pred tag
Bool Bool
False)
        ]
      | ExplanationMode
mode <- [ExplanationMode
Shallow, ExplanationMode
Deep]
      ]

{-------------------------------------------------------------------------------
  QuickCheck properties
-------------------------------------------------------------------------------}

propertyTests :: TestTree
propertyTests :: TestTree
propertyTests =
  (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckTests (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
100) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
    TestName -> [TestTree] -> TestTree
testGroup
      TestName
"property tests"
      [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"prop_evalPred" Property
prop_evalPred
      ]

genPred :: Gen (Pred ())
genPred :: Gen (Pred ())
genPred = (Int -> Gen (Pred ())) -> Gen (Pred ())
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen (Pred ())
go
 where
  go :: Int -> Gen (Pred ())
go Int
0 =
    Bool -> Pred ()
forall tag. Bool -> Pred tag
Bool (Bool -> Pred ()) -> Gen Bool -> Gen (Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
  go Int
n =
    [(Int, Gen (Pred ()))] -> Gen (Pred ())
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
n, () -> Pred () -> Pred ()
forall tag. tag -> Pred tag -> Pred tag
(:=) (() -> Pred () -> Pred ()) -> Gen () -> Gen (Pred () -> Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> Gen ()
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () Gen (Pred () -> Pred ()) -> Gen (Pred ()) -> Gen (Pred ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Gen (Pred ())
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
      , (Int
1, Bool -> Pred ()
forall tag. Bool -> Pred tag
Bool (Bool -> Pred ()) -> Gen Bool -> Gen (Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bool
forall a. Arbitrary a => Gen a
arbitrary)
      , (Int
n, Pred () -> Pred ()
forall tag. Pred tag -> Pred tag
Not (Pred () -> Pred ()) -> Gen (Pred ()) -> Gen (Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (Pred ())
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
      , (Int
1, Int -> Int -> Pred ()
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
(:>:) (Int -> Int -> Pred ()) -> Gen Int -> Gen (Int -> Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary @Int Gen (Int -> Pred ()) -> Gen Int -> Gen (Pred ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @Int)
      , (Int
1, Int -> Int -> Pred ()
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
(:<=:) (Int -> Int -> Pred ()) -> Gen Int -> Gen (Int -> Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary @Int Gen (Int -> Pred ()) -> Gen Int -> Gen (Pred ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @Int)
      , (Int
1, Int -> Int -> Pred ()
forall a tag. (Typeable a, Eq a, Show a) => a -> a -> Pred tag
(:==:) (Int -> Int -> Pred ()) -> Gen Int -> Gen (Int -> Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary @Int Gen (Int -> Pred ()) -> Gen Int -> Gen (Pred ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @Int)
      , (Int
n, Pred () -> Pred () -> Pred ()
forall tag. Pred tag -> Pred tag -> Pred tag
(:/\:) (Pred () -> Pred () -> Pred ())
-> Gen (Pred ()) -> Gen (Pred () -> Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (Pred ())
go (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) Gen (Pred () -> Pred ()) -> Gen (Pred ()) -> Gen (Pred ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Gen (Pred ())
go (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2))
      , (Int
n, Pred () -> Pred () -> Pred ()
forall tag. Pred tag -> Pred tag -> Pred tag
(:/\:) (Pred () -> Pred () -> Pred ())
-> Gen (Pred ()) -> Gen (Pred () -> Pred ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (Pred ())
go (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) Gen (Pred () -> Pred ()) -> Gen (Pred ()) -> Gen (Pred ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Gen (Pred ())
go (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2))
      ]

predSize :: Pred a -> Int
predSize :: forall a. Pred a -> Int
predSize = \case
  a
_ := Pred a
a -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Pred a -> Int
forall a. Pred a -> Int
predSize Pred a
a
  Bool Bool
_ -> Int
1
  Not Pred a
a -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Pred a -> Int
forall a. Pred a -> Int
predSize Pred a
a
  a
_ :>: a
_ -> Int
1
  a
_ :<=: a
_ -> Int
1
  a
_ :==: a
_ -> Int
1
  Pred a
a :/\: Pred a
b -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Pred a -> Int
forall a. Pred a -> Int
predSize Pred a
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Pred a -> Int
forall a. Pred a -> Int
predSize Pred a
b
  Pred a
a :\/: Pred a
b -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Pred a -> Int
forall a. Pred a -> Int
predSize Pred a
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Pred a -> Int
forall a. Pred a -> Int
predSize Pred a
b

-- | The overall judgment of 'evalPred' conforms to a trivial evaluator.
prop_evalPred :: Property
prop_evalPred :: Property
prop_evalPred =
  Gen (Pred ()) -> (Pred () -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen (Pred ())
genPred ((Pred () -> Property) -> Property)
-> (Pred () -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Pred ()
predicate -> do
    let expected :: Bool
expected = Pred () -> Bool
evalDirect Pred ()
predicate
    let actual :: Bool
actual = Pred () -> (forall (res :: Bool). Evidence res () -> Bool) -> Bool
forall tag r.
Pred tag -> (forall (res :: Bool). Evidence res tag -> r) -> r
evalPred Pred ()
predicate Evidence res () -> Bool
forall (res :: Bool). Evidence res () -> Bool
forall (res :: Bool) a. Evidence res a -> Bool
forgetEvidence
    Pred () -> Property -> Property
forall a. Pred a -> Property -> Property
tabulateSize Pred ()
predicate (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      Bool
expected Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
actual
 where
  evalDirect :: Pred () -> Bool
  evalDirect :: Pred () -> Bool
evalDirect = \case
    ()
_ := Pred ()
a -> Pred () -> Bool
evalDirect Pred ()
a
    Bool Bool
b -> Bool
b
    Not Pred ()
a -> Bool -> Bool
not (Pred () -> Bool
evalDirect Pred ()
a)
    a
a :>: a
b -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
b
    a
a :<=: a
b -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b
    a
a :==: a
b -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
    Pred ()
a :/\: Pred ()
b -> Pred () -> Bool
evalDirect Pred ()
a Bool -> Bool -> Bool
&& Pred () -> Bool
evalDirect Pred ()
b
    Pred ()
a :\/: Pred ()
b -> Pred () -> Bool
evalDirect Pred ()
a Bool -> Bool -> Bool
|| Pred () -> Bool
evalDirect Pred ()
b

  tabulateSize :: Pred a -> Property -> Property
  tabulateSize :: forall a. Pred a -> Property -> Property
tabulateSize Pred a
predicate = do
    let bucket :: Int
bucket = Pred a -> Int
forall a. Pred a -> Int
predSize Pred a
predicate Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
10
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate
      TestName
"Predicate size"
      [Int -> TestName
forall a. Show a => a -> TestName
show Int
bucket TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
"0-" TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> TestName
forall a. Show a => a -> TestName
show (Int
bucket Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
"0"]