{-# 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) ]