{-# LANGUAGE OverloadedStrings #-}
module Hedgehog.Laws.Lattice where

import Hedgehog (Property, cover, forAll, property)
import Hedgehog qualified
import Hedgehog.Laws.Common
import PlutusTx.Lattice
import Prelude
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Hedgehog (testProperty)

joinLatticeLaws :: (Show a, Eq a, JoinSemiLattice a) => Hedgehog.Gen a -> TestTree
joinLatticeLaws :: forall a. (Show a, Eq a, JoinSemiLattice a) => Gen a -> TestTree
joinLatticeLaws Gen a
g = TestName -> [TestTree] -> TestTree
testGroup TestName
"join semilattice laws"
  [ TestName -> Property -> TestTree
testProperty TestName
"idempotent" (Gen a -> (a -> a -> a) -> Property
forall a. (Show a, Eq a) => Gen a -> (a -> a -> a) -> Property
prop_idempotent Gen a
g a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
(\/))
  , TestName -> Property -> TestTree
testProperty TestName
"commutative" (Gen a -> (a -> a -> a) -> Property
forall a. (Show a, Eq a) => Gen a -> (a -> a -> a) -> Property
prop_commutative Gen a
g a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
(\/))
  , TestName -> Property -> TestTree
testProperty TestName
"associative" (Gen a -> (a -> a -> a) -> Property
forall a. (Show a, Eq a) => Gen a -> (a -> a -> a) -> Property
prop_associative Gen a
g a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
(\/))
  ]

boundedJoinLatticeLaws :: (Show a, Eq a, BoundedJoinSemiLattice a) => Hedgehog.Gen a -> TestTree
boundedJoinLatticeLaws :: forall a.
(Show a, Eq a, BoundedJoinSemiLattice a) =>
Gen a -> TestTree
boundedJoinLatticeLaws Gen a
g = TestName -> [TestTree] -> TestTree
testGroup TestName
"bounded join semilattice laws"
  [ Gen a -> TestTree
forall a. (Show a, Eq a, JoinSemiLattice a) => Gen a -> TestTree
joinLatticeLaws Gen a
g
  , TestName -> Property -> TestTree
testProperty TestName
"unit" (Gen a -> (a -> a -> a) -> a -> Property
forall a. (Show a, Eq a) => Gen a -> (a -> a -> a) -> a -> Property
prop_unit Gen a
g a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
(\/) a
forall a. BoundedJoinSemiLattice a => a
bottom)
  ]

meetLatticeLaws :: (Show a, Eq a, MeetSemiLattice a) => Hedgehog.Gen a -> TestTree
meetLatticeLaws :: forall a. (Show a, Eq a, MeetSemiLattice a) => Gen a -> TestTree
meetLatticeLaws Gen a
g = TestName -> [TestTree] -> TestTree
testGroup TestName
"meet semilattice laws"
  [ TestName -> Property -> TestTree
testProperty TestName
"idempotent" (Gen a -> (a -> a -> a) -> Property
forall a. (Show a, Eq a) => Gen a -> (a -> a -> a) -> Property
prop_idempotent Gen a
g a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
(/\))
  , TestName -> Property -> TestTree
testProperty TestName
"commutative" (Gen a -> (a -> a -> a) -> Property
forall a. (Show a, Eq a) => Gen a -> (a -> a -> a) -> Property
prop_commutative Gen a
g a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
(/\))
  , TestName -> Property -> TestTree
testProperty TestName
"associative" (Gen a -> (a -> a -> a) -> Property
forall a. (Show a, Eq a) => Gen a -> (a -> a -> a) -> Property
prop_associative Gen a
g a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
(/\))
  ]

boundedMeetLatticeLaws :: (Show a, Eq a, BoundedMeetSemiLattice a) => Hedgehog.Gen a -> TestTree
boundedMeetLatticeLaws :: forall a.
(Show a, Eq a, BoundedMeetSemiLattice a) =>
Gen a -> TestTree
boundedMeetLatticeLaws Gen a
g = TestName -> [TestTree] -> TestTree
testGroup TestName
"bounded meet semilattice laws"
  [ Gen a -> TestTree
forall a. (Show a, Eq a, MeetSemiLattice a) => Gen a -> TestTree
meetLatticeLaws Gen a
g
  , TestName -> Property -> TestTree
testProperty TestName
"unit" (Gen a -> (a -> a -> a) -> a -> Property
forall a. (Show a, Eq a) => Gen a -> (a -> a -> a) -> a -> Property
prop_unit Gen a
g a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
(/\) a
forall a. BoundedMeetSemiLattice a => a
top)
  ]

prop_latticeAbsorb :: (Show a, Eq a, Lattice a) => Hedgehog.Gen a -> Property
prop_latticeAbsorb :: forall a. (Show a, Eq a, Lattice a) => Gen a -> Property
prop_latticeAbsorb Gen a
g = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
x <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
g
  a
y <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
g
  CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover CoverPercentage
10 LabelName
"different" (Bool -> PropertyT IO ()) -> Bool -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y
  a
x a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ (a
x a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
y) a -> a -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
Hedgehog.=== a
x
  a
x a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ (a
x a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
y) a -> a -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
Hedgehog.=== a
x

latticeLaws :: (Show a, Eq a, Lattice a) => Hedgehog.Gen a -> TestTree
latticeLaws :: forall a. (Show a, Eq a, Lattice a) => Gen a -> TestTree
latticeLaws Gen a
g = TestName -> [TestTree] -> TestTree
testGroup TestName
"lattice laws"
  [ Gen a -> TestTree
forall a. (Show a, Eq a, JoinSemiLattice a) => Gen a -> TestTree
joinLatticeLaws Gen a
g
  , Gen a -> TestTree
forall a. (Show a, Eq a, MeetSemiLattice a) => Gen a -> TestTree
meetLatticeLaws Gen a
g
  , TestName -> Property -> TestTree
testProperty TestName
"absorption" (Gen a -> Property
forall a. (Show a, Eq a, Lattice a) => Gen a -> Property
prop_latticeAbsorb Gen a
g)
  ]

boundedLatticeLaws :: (Show a, Eq a, BoundedLattice a) => Hedgehog.Gen a -> TestTree
boundedLatticeLaws :: forall a. (Show a, Eq a, BoundedLattice a) => Gen a -> TestTree
boundedLatticeLaws Gen a
g = TestName -> [TestTree] -> TestTree
testGroup TestName
"bounded lattice laws"
  [ Gen a -> TestTree
forall a.
(Show a, Eq a, BoundedJoinSemiLattice a) =>
Gen a -> TestTree
boundedJoinLatticeLaws Gen a
g
  , Gen a -> TestTree
forall a.
(Show a, Eq a, BoundedMeetSemiLattice a) =>
Gen a -> TestTree
boundedMeetLatticeLaws Gen a
g
  , TestName -> Property -> TestTree
testProperty TestName
"absorption" (Gen a -> Property
forall a. (Show a, Eq a, Lattice a) => Gen a -> Property
prop_latticeAbsorb Gen a
g)
  ]