{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}

module Plutarch.Test.Laws (
  checkLedgerPropertiesValue,
  checkLedgerPropertiesAssocMap,
  checkLedgerProperties,
  checkLedgerPropertiesPCountable,
  checkLedgerPropertiesPEnumerable,
  checkHaskellOrdEquivalent,
  checkHaskellNumEquivalent,
  checkPLiftableLaws,
  checkPLiftableLawsForDeriveTags,
  checkPOrdLaws,
  checkPAdditiveSemigroupLaws,
  checkPAdditiveMonoidLaws,
  checkPAdditiveGroupLaws,
  checkPlutusTypeLaws,
  checkPSemigroupLaws,
  checkPMonoidLaws,
) where

import Control.Applicative ((<|>))
import Data.Data (Proxy (Proxy))
import Data.Kind (Type)
import GHC.Exts (Any)
import GHC.Generics (Generic)
import Generics.SOP qualified as SOP
import Plutarch.LedgerApi.V1 qualified as V1
import Plutarch.Prelude
import Plutarch.Test.QuickCheck (checkHaskellEquivalent, checkHaskellEquivalent2)
import Plutarch.Test.Utils (instanceOfType, precompileTerm, prettyEquals, prettyShow, typeName')
import Plutarch.Unsafe (punsafeCoerce)
import PlutusLedgerApi.Common qualified as Plutus
import PlutusLedgerApi.V1.Orphans ()
import Prettyprinter (Pretty (pretty))
import Test.QuickCheck (
  Arbitrary (arbitrary, shrink),
  Arbitrary1 (liftArbitrary, liftShrink),
  Property,
  forAllShrinkShow,
  oneof,
  (=/=),
  (===),
 )
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Type.Reflection (Typeable, typeRep)

{- | Verifies that the specified Plutarch type satisfies the 'PSemigroup' laws
for mandatory methods.

@since 1.0.0
-}
checkPSemigroupLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , PSemigroup a
  , PEq a
  , PLiftable a
  ) =>
  TestTree
checkPSemigroupLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), PSemigroup a,
 PEq a, PLiftable a) =>
TestTree
checkPSemigroupLaws =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"PSemigroup"
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#<> is associative" Property
psemiAssociative
    ]
  where
    psemiAssociative :: Property
    psemiAssociative :: Property
psemiAssociative = Gen (AsHaskell a, AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a, AsHaskell a)
    -> [(AsHaskell a, AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a, AsHaskell a)
-> [(AsHaskell a, AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
 -> Property)
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y, AsHaskell a
z) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift
        ( (forall (s0 :: S). Term s0 (a :--> (a :--> (a :--> PBool))))
-> forall (s0 :: S). Term s0 (a :--> (a :--> (a :--> PBool)))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> (a :--> PBool)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> (a :--> PBool)))
plam ((Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> (a :--> PBool))))
-> (Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> (a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 Term s0 a
arg3 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> (Term s0 a
arg2 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> Term s0 a
arg3)) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== ((Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> Term s0 a
arg2) Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> Term s0 a
arg3))
            # pconstant @a x
            # pconstant y
            # pconstant z
        )

{- | Verifies that the specified Plutarch type satisfies the 'PMonoid' laws for
mandatory methods.

@since 1.0.0
-}
checkPMonoidLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , PMonoid a
  , PEq a
  , PLiftable a
  ) =>
  TestTree
checkPMonoidLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), PMonoid a, PEq a,
 PLiftable a) =>
TestTree
checkPMonoidLaws =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"PMonoid"
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pmempty is a left identity for #<>" Property
pmemptyLeftId
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pmemoty is a right identity for #<>" Property
pmemptyRightId
    ]
  where
    pmemptyLeftId :: Property
    pmemptyLeftId :: Property
pmemptyLeftId = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> Term s0 a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PMonoid a => Term s a
pmempty) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
arg1) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
    pmemptyRightId :: Property
    pmemptyRightId :: Property
pmemptyRightId = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> (Term s0 a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PMonoid a => Term s a
pmempty Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> Term s0 a
arg1) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
arg1) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)

{- | Verifies that the specified Plutarch type satisfies the
'PAdditiveSemigroup' laws for mandatory methods.

@since 1.0.0
-}
checkPAdditiveSemigroupLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , PAdditiveSemigroup a
  , PEq a
  , PLiftable a
  ) =>
  TestTree
checkPAdditiveSemigroupLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a),
 PAdditiveSemigroup a, PEq a, PLiftable a) =>
TestTree
checkPAdditiveSemigroupLaws =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"PAdditiveSemigroup"
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#+ is commutative" Property
plusSymmetric
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#+ is associative" Property
plusAssociative
    ]
  where
    plusSymmetric :: Property
    plusSymmetric :: Property
plusSymmetric = Gen (AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a) -> AsHaskell PBool) -> Property)
-> ((AsHaskell a, AsHaskell a) -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> (a :--> PBool)))
-> forall (s0 :: S). Term s0 (a :--> (a :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> PBool))
plam ((Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> PBool)))
-> (Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s0 a
arg2) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s0 a
arg2 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s0 a
arg1)) Term s (a :--> (a :--> PBool)) -> Term s a -> Term s (a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
y)
    plusAssociative :: Property
    plusAssociative :: Property
plusAssociative = Gen (AsHaskell a, AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a, AsHaskell a)
    -> [(AsHaskell a, AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a, AsHaskell a)
-> [(AsHaskell a, AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
 -> Property)
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y, AsHaskell a
z) ->
        (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift
          ( (forall (s0 :: S). Term s0 (a :--> (a :--> (a :--> PBool))))
-> forall (s0 :: S). Term s0 (a :--> (a :--> (a :--> PBool)))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> (a :--> PBool)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> (a :--> PBool)))
plam ((Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> (a :--> PBool))))
-> (Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> (a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 Term s0 a
arg3 -> ((Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s0 a
arg2) Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s0 a
arg3) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ (Term s0 a
arg2 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s0 a
arg3)))
              # pconstant @a x
              # pconstant y
              # pconstant z
          )

{- | Verifies that the specified Plutarch type satisfies the 'PAdditiveMonoid'
laws for mandatory methods.

@since 1.0.0
-}
checkPAdditiveMonoidLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , PAdditiveMonoid a
  , PEq a
  , PLiftable a
  ) =>
  TestTree
checkPAdditiveMonoidLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), PAdditiveMonoid a,
 PEq a, PLiftable a) =>
TestTree
checkPAdditiveMonoidLaws =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"PAdditiveMonoid"
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pzero is the identity for #+" Property
pzeroIdentity
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pzero does not scale" Property
pzeroScale
    ]
  where
    pzeroIdentity :: Property
    pzeroIdentity :: Property
pzeroIdentity = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) -> (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s0 a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
arg1) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
    pzeroScale :: Property
    pzeroScale :: Property
pzeroScale = Gen Positive
-> (Positive -> [Positive])
-> (Positive -> TestName)
-> (Positive -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen Positive
forall a. Arbitrary a => Gen a
arbitrary Positive -> [Positive]
forall a. Arbitrary a => a -> [a]
shrink Positive -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((Positive -> AsHaskell PBool) -> Property)
-> (Positive -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$
      \(Positive
p :: Positive) -> (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (PPositive :--> PBool))
-> forall (s0 :: S). Term s0 (PPositive :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 PPositive -> Term s0 PBool)
-> Term s0 (PPositive :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 PPositive -> Term s0 PBool)
 -> Term s0 (PPositive :--> PBool))
-> (Term s0 PPositive -> Term s0 PBool)
-> Term s0 (PPositive :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 PPositive
arg1 -> Term s0 a -> Term s0 PPositive -> Term s0 a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive (forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero @a) Term s0 PPositive
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero) Term s (PPositive :--> PBool) -> Term s PPositive -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PPositive AsHaskell PPositive
Positive
p)

{- | Verifies that the specified Plutarch type satisfies the 'PAdditiveGroup'
laws for mandatory methods.

@since 1.0.0
-}
checkPAdditiveGroupLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , PAdditiveGroup a
  , PEq a
  , PLiftable a
  ) =>
  TestTree
checkPAdditiveGroupLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), PAdditiveGroup a,
 PEq a, PLiftable a) =>
TestTree
checkPAdditiveGroupLaws =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"PAdditiveGroup"
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pnegate is an additive inverse" Property
pnegateAdditiveInverse
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pnegate is self-inverting" Property
pnegateSelfInverting
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"x #- x = pzero" Property
pminusSelf
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pnegate is difference from pzero" Property
pnegatePZeroConsistency1
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"x #- y = x #+ pnegate y" Property
pnegatePZeroConsistency2
    ]
  where
    pnegateAdditiveInverse :: Property
    pnegateAdditiveInverse :: Property
pnegateAdditiveInverse = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> ((Term s0 (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s0 (a :--> a) -> Term s0 a -> Term s0 a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s0 a
arg1) Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s0 a
arg1) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
    pnegateSelfInverting :: Property
    pnegateSelfInverting :: Property
pnegateSelfInverting = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> (Term s0 (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s0 (a :--> a) -> Term s0 a -> Term s0 a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s0 (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s0 (a :--> a) -> Term s0 a -> Term s0 a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s0 a
arg1) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
arg1) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
    pminusSelf :: Property
    pminusSelf :: Property
pminusSelf = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s a -> Term s a -> Term s a
#- Term s0 a
arg1) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
    pnegatePZeroConsistency1 :: Property
    pnegatePZeroConsistency1 :: Property
pnegatePZeroConsistency1 = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> (Term s0 (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s0 (a :--> a) -> Term s0 a -> Term s0 a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s0 a
arg1) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s0 a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s a -> Term s a -> Term s a
#- Term s0 a
arg1)) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
    pnegatePZeroConsistency2 :: Property
    pnegatePZeroConsistency2 :: Property
pnegatePZeroConsistency2 = Gen (AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a) -> AsHaskell PBool) -> Property)
-> ((AsHaskell a, AsHaskell a) -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y) ->
        (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift
          ( (forall (s0 :: S). Term s0 (a :--> (a :--> PBool)))
-> forall (s0 :: S). Term s0 (a :--> (a :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> PBool))
plam ((Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> PBool)))
-> (Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s a -> Term s a -> Term s a
#- Term s0 a
arg2) Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ (Term s0 (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s0 (a :--> a) -> Term s0 a -> Term s0 a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s0 a
arg2)))
              # pconstant @a x
              # pconstant y
          )

{- | Verifies that the specified Plutarch type satisfies the 'POrd' laws for
mandatory methods.

@since 1.0.0
-}
checkPOrdLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , PLiftable a
  , POrd a
  ) =>
  [TestTree]
checkPOrdLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), PLiftable a,
 POrd a) =>
[TestTree]
checkPOrdLaws =
  [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#<= is reflexive" Property
leqReflexive
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#<= is transitive" Property
leqTransitive
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#<= is total" Property
leqTotal
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#< is irreflexive" Property
ltIrreflexive
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#< is transitive" Property
ltTransitive
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#< is trichotomous" Property
ltTrichotomous
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"#< is the equivalent strict order to #<=" Property
ltEquivLeq
  ]
  where
    leqReflexive :: Property
    leqReflexive :: Property
leqReflexive = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s0 a
arg1) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
    -- We have to restate (x <= y && y <= z) -> x <= z, which gives (after some
    -- DeMorganing) x > y || y > z || x <= z
    leqTransitive :: Property
    leqTransitive :: Property
leqTransitive = Gen (Triplet (AsHaskell a))
-> (Triplet (AsHaskell a) -> [Triplet (AsHaskell a)])
-> (Triplet (AsHaskell a) -> TestName)
-> (Triplet (AsHaskell a) -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (Triplet (AsHaskell a))
forall a. Arbitrary a => Gen a
arbitrary Triplet (AsHaskell a) -> [Triplet (AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink Triplet (AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((Triplet (AsHaskell a) -> AsHaskell PBool) -> Property)
-> (Triplet (AsHaskell a) -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Triplet (AsHaskell a)
t :: Triplet (AsHaskell a)) ->
      let (AsHaskell a
x, AsHaskell a
y, AsHaskell a
z) = Triplet (AsHaskell a) -> (AsHaskell a, AsHaskell a, AsHaskell a)
forall a. Triplet a -> (a, a, a)
toTriple Triplet (AsHaskell a)
t
       in (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift
            ( (forall (s0 :: S). Term s0 (a :--> (a :--> (a :--> PBool))))
-> forall (s0 :: S). Term s0 (a :--> (a :--> (a :--> PBool)))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> (a :--> PBool)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> (a :--> PBool)))
plam ((Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> (a :--> PBool))))
-> (Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> (a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 Term s0 a
arg3 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s0 a
arg2) Term s0 PBool -> Term s0 PBool -> Term s0 PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s0 a
arg2 Term s0 a -> Term s0 a -> Term s0 PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s0 a
arg3) Term s0 PBool -> Term s0 PBool -> Term s0 PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s0 a
arg3))
                # pconstant @a x
                # pconstant y
                # pconstant z
            )
    leqTotal :: Property
    leqTotal :: Property
leqTotal = Gen (AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a) -> AsHaskell PBool) -> Property)
-> ((AsHaskell a, AsHaskell a) -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift
        ( (forall (s0 :: S). Term s0 (a :--> (a :--> PBool)))
-> forall (s0 :: S). Term s0 (a :--> (a :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> PBool))
plam ((Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> PBool)))
-> (Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s0 a
arg2) Term s0 PBool -> Term s0 PBool -> Term s0 PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s0 a
arg2 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s0 a
arg1))
            # pconstant @a x
            # pconstant y
        )
    ltIrreflexive :: Property
    ltIrreflexive :: Property
ltIrreflexive = Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PBool))
-> forall (s0 :: S). Term s0 (a :--> PBool)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PBool) -> Term s0 (c :--> PBool)
plam ((Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool))
-> (Term s0 a -> Term s0 PBool) -> Term s0 (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 -> Term s0 (PBool :--> PBool)
forall (s :: S). Term s (PBool :--> PBool)
pnot Term s0 (PBool :--> PBool) -> Term s0 PBool -> Term s0 PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s0 a
arg1) Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
    -- We have to restate (x < y && y < z) -> x < z, which gives (after some
    -- DeMorganing) x >= y || y >= z || x < z
    ltTransitive :: Property
    ltTransitive :: Property
ltTransitive = Gen (AsHaskell a, AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a, AsHaskell a)
    -> [(AsHaskell a, AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a, AsHaskell a)
-> [(AsHaskell a, AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
 -> Property)
-> ((AsHaskell a, AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y :: AsHaskell a, AsHaskell a
z :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift
        ( (forall (s0 :: S). Term s0 (a :--> (a :--> (a :--> PBool))))
-> forall (s0 :: S). Term s0 (a :--> (a :--> (a :--> PBool)))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> (a :--> PBool)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> (a :--> PBool)))
plam ((Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> (a :--> PBool))))
-> (Term s0 a -> Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> (a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 Term s0 a
arg3 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#>= Term s0 a
arg2) Term s0 PBool -> Term s0 PBool -> Term s0 PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s0 a
arg2 Term s0 a -> Term s0 a -> Term s0 PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#>= Term s0 a
arg3) Term s0 PBool -> Term s0 PBool -> Term s0 PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s0 a
arg3))
            # pconstant @a x
            # pconstant y
            # pconstant z
        )
    ltTrichotomous :: Property
    ltTrichotomous :: Property
ltTrichotomous = Gen (AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a) -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a) -> AsHaskell PBool) -> Property)
-> ((AsHaskell a, AsHaskell a) -> AsHaskell PBool) -> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift
        ( (forall (s0 :: S). Term s0 (a :--> (a :--> PBool)))
-> forall (s0 :: S). Term s0 (a :--> (a :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> PBool))
plam ((Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> PBool)))
-> (Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s0 a
arg2) Term s0 PBool -> Term s0 PBool -> Term s0 PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s0 a
arg2 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s0 a
arg1) Term s0 PBool -> Term s0 PBool -> Term s0 PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
arg2))
            # pconstant @a x
            # pconstant y
        )
    ltEquivLeq :: Property
    ltEquivLeq :: Property
ltEquivLeq = Gen (AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a) -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a) -> Property) -> Property)
-> ((AsHaskell a, AsHaskell a) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y :: AsHaskell a) ->
      (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> (a :--> PBool)))
-> forall (s0 :: S). Term s0 (a :--> (a :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> PBool))
plam ((Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> PBool)))
-> (Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 -> Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s0 a
arg2) Term s (a :--> (a :--> PBool)) -> Term s a -> Term s (a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# AsHaskell a -> Term s a
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell a
y)
        AsHaskell PBool -> AsHaskell PBool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift
          ( (forall (s0 :: S). Term s0 (a :--> (a :--> PBool)))
-> forall (s0 :: S). Term s0 (a :--> (a :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a -> Term s0 PBool)
-> Term s0 (c :--> (a :--> PBool))
plam ((Term s0 a -> Term s0 a -> Term s0 PBool)
 -> Term s0 (a :--> (a :--> PBool)))
-> (Term s0 a -> Term s0 a -> Term s0 PBool)
-> Term s0 (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s0 a
arg1 Term s0 a
arg2 -> (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s0 a
arg2) Term s0 PBool -> Term s0 PBool -> Term s0 PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s0 a
arg1 Term s0 a -> Term s0 a -> Term s0 PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s0 a
arg2))
              # pconstant @a x
              # pconstant y
          )

{- | Verifies that the specified Plutarch and Haskell types satisfy the laws of
'PLiftable'.

@since 1.0.0
-}
checkPLiftableLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , Eq (AsHaskell a)
  , PLiftable a
  , Show (AsHaskell a)
  ) =>
  [TestTree]
checkPLiftableLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), Eq (AsHaskell a),
 PLiftable a, Show (AsHaskell a)) =>
[TestTree]
checkPLiftableLaws =
  [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"plutToRepr . reprToPlut = Right"
      (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow
      ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
        (forall (a :: S -> Type).
PLiftable a =>
PlutusRepr a -> Either LiftError (AsHaskell a)
reprToHask @a (PlutusRepr a -> Either LiftError (AsHaskell a))
-> Either LiftError (PlutusRepr a)
-> Either LiftError (Either LiftError (AsHaskell a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). PLifted s a) -> Either LiftError (PlutusRepr a)
plutToRepr @a (PlutusRepr a -> PLifted s a
forall (s :: S). PlutusRepr a -> PLifted s a
forall (a :: S -> Type) (s :: S).
PLiftable a =>
PlutusRepr a -> PLifted s a
reprToPlut (forall (a :: S -> Type). PLiftable a => AsHaskell a -> PlutusRepr a
haskToRepr @a AsHaskell a
x))) Either LiftError (Either LiftError (AsHaskell a))
-> Either LiftError (Either LiftError (AsHaskell a)) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (forall (a :: S -> Type).
PLiftable a =>
PlutusRepr a -> Either LiftError (AsHaskell a)
reprToHask @a (PlutusRepr a -> Either LiftError (AsHaskell a))
-> Either LiftError (PlutusRepr a)
-> Either LiftError (Either LiftError (AsHaskell a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> PlutusRepr a -> Either LiftError (PlutusRepr a)
forall a b. b -> Either a b
Right (forall (a :: S -> Type). PLiftable a => AsHaskell a -> PlutusRepr a
haskToRepr @a AsHaskell a
x))
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"reprToHask . haskToRepr = Right"
      (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow
      ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
        forall (a :: S -> Type).
PLiftable a =>
PlutusRepr a -> Either LiftError (AsHaskell a)
reprToHask @a (forall (a :: S -> Type). PLiftable a => AsHaskell a -> PlutusRepr a
haskToRepr @a AsHaskell a
x) Either LiftError (AsHaskell a)
-> Either LiftError (AsHaskell a) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== AsHaskell a -> Either LiftError (AsHaskell a)
forall a b. b -> Either a b
Right AsHaskell a
x
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"plift . pconstant = id" (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
      (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x) AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` AsHaskell a
x
  ]

{- | Verifies that `PLiftable` instances derived by `DeriveAsTag` encode to valid integer ranges

@since 1.0.2
-}
checkPLiftableLawsForDeriveTags ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , PLiftable a
  , PlutusRepr a ~ Integer
  , SOP.Generic (a Any)
  ) =>
  [TestTree]
checkPLiftableLawsForDeriveTags :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), PLiftable a,
 (PlutusRepr a :: Type) ~ (Integer :: Type),
 Generic (a (Any @S))) =>
[TestTree]
checkPLiftableLawsForDeriveTags =
  [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"range check" (Property -> TestTree)
-> ((AsHaskell a -> Bool) -> Property)
-> (AsHaskell a -> Bool)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Bool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> Bool) -> TestTree)
-> (AsHaskell a -> Bool) -> TestTree
forall a b. (a -> b) -> a -> b
$
      ( \(AsHaskell a
x :: AsHaskell a) ->
          let n :: Int
n = forall k (xs :: [k]) (proxy :: [k] -> Type).
SListI @k xs =>
proxy xs -> Int
SOP.lengthSList @_ @(SOP.Code (a Any)) Proxy @[[Type]] (Code (a (Any @S)))
forall {k} (t :: k). Proxy @k t
Proxy
              hask :: PlutusRepr a
hask = forall (a :: S -> Type). PLiftable a => AsHaskell a -> PlutusRepr a
haskToRepr @a AsHaskell a
x
           in PlutusRepr a
hask PlutusRepr a -> PlutusRepr a -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
PlutusRepr a
0 Bool -> Bool -> Bool
&& PlutusRepr a
hask PlutusRepr a -> PlutusRepr a -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n
      )
  ]

-- | @since 1.0.2
newtype Foo (a :: S -> Type) (s :: S) = Foo (Term s a)
  deriving stock ((forall x. Foo a s -> Rep (Foo a s) x)
-> (forall x. Rep (Foo a s) x -> Foo a s) -> Generic (Foo a s)
forall x. Rep (Foo a s) x -> Foo a s
forall x. Foo a s -> Rep (Foo a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x. Rep (Foo a s) x -> Foo a s
forall (a :: S -> Type) (s :: S) x. Foo a s -> Rep (Foo a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x. Foo a s -> Rep (Foo a s) x
from :: forall x. Foo a s -> Rep (Foo a s) x
$cto :: forall (a :: S -> Type) (s :: S) x. Rep (Foo a s) x -> Foo a s
to :: forall x. Rep (Foo a s) x -> Foo a s
Generic)
  deriving anyclass
    ( All @[Type] (SListI @Type) (Code (Foo a s))
All @[Type] (SListI @Type) (Code (Foo a s)) =>
(Foo a s -> Rep (Foo a s))
-> (Rep (Foo a s) -> Foo a s) -> Generic (Foo a s)
Rep (Foo a s) -> Foo a s
Foo a s -> Rep (Foo a s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: S -> Type) (s :: S).
All @[Type] (SListI @Type) (Code (Foo a s))
forall (a :: S -> Type) (s :: S). Rep (Foo a s) -> Foo a s
forall (a :: S -> Type) (s :: S). Foo a s -> Rep (Foo a s)
$cfrom :: forall (a :: S -> Type) (s :: S). Foo a s -> Rep (Foo a s)
from :: Foo a s -> Rep (Foo a s)
$cto :: forall (a :: S -> Type) (s :: S). Rep (Foo a s) -> Foo a s
to :: Rep (Foo a s) -> Foo a s
SOP.Generic
    )

-- | @since 1.0.2
deriving via DeriveNewtypePlutusType (Foo a) instance PlutusType (Foo a)

-- | @since 1.0.2
instance PEq a => PEq (Foo a) where
  #== :: forall (s :: S). Term s (Foo a) -> Term s (Foo a) -> Term s PBool
(#==) Term s (Foo a)
x Term s (Foo a)
y = Term s (Foo a :--> (Foo a :--> PBool))
forall {a :: S -> Type} {s :: S}.
PEq a =>
Term s (Foo a :--> (Foo a :--> PBool))
inner Term s (Foo a :--> (Foo a :--> PBool))
-> Term s (Foo a) -> Term s (Foo a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (Foo a)
x Term s (Foo a :--> PBool) -> Term s (Foo a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (Foo a)
y
    where
      inner :: Term s (Foo a :--> (Foo a :--> PBool))
inner = (Term s (Foo a) -> Term s (Foo a) -> Term s PBool)
-> Term s (Foo a :--> (Foo a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (Foo a) -> Term s PBool)
-> Term s (c :--> (Foo a :--> PBool))
plam ((Term s (Foo a) -> Term s (Foo a) -> Term s PBool)
 -> Term s (Foo a :--> (Foo a :--> PBool)))
-> (Term s (Foo a) -> Term s (Foo a) -> Term s PBool)
-> Term s (Foo a :--> (Foo a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (Foo a)
x' Term s (Foo a)
y' ->
        Term s (Foo a) -> (Foo a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (Foo a)
x' (\(Foo Term s a
x'') -> Term s (Foo a) -> (Foo a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (Foo a)
y' (\(Foo Term s a
y'') -> Term s a
x'' Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
y''))

{- | Verify that PlutusType laws hold

@since 1.0.2
-}
checkPlutusTypeLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , PEq a
  , PLiftable a
  ) =>
  [TestTree]
checkPlutusTypeLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), PEq a,
 PLiftable a) =>
[TestTree]
checkPlutusTypeLaws =
  [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pmatch (pcon x) f = f x" (Property -> TestTree)
-> ((AsHaskell a -> AsHaskell PBool) -> Property)
-> (AsHaskell a -> AsHaskell PBool)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> AsHaskell PBool)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> AsHaskell PBool) -> TestTree)
-> (AsHaskell a -> AsHaskell PBool) -> TestTree
forall a b. (a -> b) -> a -> b
$
      ( \(AsHaskell a
x :: AsHaskell a) ->
          ( let
              script :: Term s' (a :--> PBool)
              script :: forall (s' :: S). Term s' (a :--> PBool)
script =
                let f :: a s' -> Term s' (Foo a)
                    f :: forall (s' :: S). a s' -> Term s' (Foo a)
f = Foo a s' -> Term s' (Foo a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Foo a s' -> Term s' (Foo a))
-> (a s' -> Foo a s') -> a s' -> Term s' (Foo a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s' a -> Foo a s'
forall (a :: S -> Type) (s :: S). Term s a -> Foo a s
Foo (Term s' a -> Foo a s') -> (a s' -> Term s' a) -> a s' -> Foo a s'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s' -> Term s' a
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon
                 in (Term s' a -> Term s' PBool) -> Term s' (a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s' c -> Term s' PBool) -> Term s' (c :--> PBool)
plam \Term s' a
x' -> Term s' a -> (a s' -> Term s' PBool) -> Term s' PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s' a
x' ((a s' -> Term s' PBool) -> Term s' PBool)
-> (a s' -> Term s' PBool) -> Term s' PBool
forall a b. (a -> b) -> a -> b
$ \a s'
x'' ->
                      Term s' a -> (a s' -> Term s' (Foo a)) -> Term s' (Foo a)
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon @a a s'
x'') a s' -> Term s' (Foo a)
forall (s' :: S). a s' -> Term s' (Foo a)
f Term s' (Foo a) -> Term s' (Foo a) -> Term s' PBool
forall (s :: S). Term s (Foo a) -> Term s (Foo a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== a s' -> Term s' (Foo a)
forall (s' :: S). a s' -> Term s' (Foo a)
f a s'
x''
             in
              (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s :: S). Term s PBool) -> AsHaskell PBool)
-> (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s PBool) -> forall (s :: S). Term s PBool
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm (Term s0 (a :--> PBool)
forall (s' :: S). Term s' (a :--> PBool)
script Term s0 (a :--> PBool) -> Term s0 a -> Term s0 PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
          )
      )
  ]

{- | Like `checkLedgerProperties` but specialized to `PRawValue`

This is an ugly kludge because PValue doesn't have a direct PData conversion,
and bringing one in would break too much other stuff to be worth it.

@since 1.0.0
-}
checkLedgerPropertiesValue :: TestTree
checkLedgerPropertiesValue :: TestTree
checkLedgerPropertiesValue =
  TestName -> [TestTree] -> TestTree
testGroup TestName
"PRawValue" ([TestTree] -> TestTree)
-> ([[TestTree]] -> [TestTree]) -> [[TestTree]] -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[TestTree]] -> [TestTree]
forall a. Monoid a => [a] -> a
mconcat ([[TestTree]] -> TestTree) -> [[TestTree]] -> TestTree
forall a b. (a -> b) -> a -> b
$
    [ forall (a :: S -> Type).
(Arbitrary (AsHaskell a), PLiftable a, PIsData a, Eq (AsHaskell a),
 ToData (AsHaskell a), Pretty (AsHaskell a)) =>
TestName -> [TestTree]
pisDataLaws @V1.PRawValue TestName
"PRawValue"
    , forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), Eq (AsHaskell a),
 PLiftable a, Show (AsHaskell a)) =>
[TestTree]
checkPLiftableLaws @V1.PRawValue
    ]

{- | Like `checkLedgerProperties` but specialized to `PMap`

Same as above

@since 1.0.0
-}
checkLedgerPropertiesAssocMap :: TestTree
checkLedgerPropertiesAssocMap :: TestTree
checkLedgerPropertiesAssocMap =
  TestName -> [TestTree] -> TestTree
testGroup TestName
"PMap" ([TestTree] -> TestTree)
-> ([[TestTree]] -> [TestTree]) -> [[TestTree]] -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[TestTree]] -> [TestTree]
forall a. Monoid a => [a] -> a
mconcat ([[TestTree]] -> TestTree) -> [[TestTree]] -> TestTree
forall a b. (a -> b) -> a -> b
$
    [ forall (a :: S -> Type).
(Arbitrary (AsHaskell a), PLiftable a, PIsData a, Eq (AsHaskell a),
 ToData (AsHaskell a), Pretty (AsHaskell a)) =>
TestName -> [TestTree]
pisDataLaws @(V1.PUnsortedMap PInteger PInteger) TestName
"PMap"
    , forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), Eq (AsHaskell a),
 PLiftable a, Show (AsHaskell a)) =>
[TestTree]
checkPLiftableLaws @(V1.PUnsortedMap PInteger PInteger)
    ]

-- | @since 1.0.0
checkLedgerProperties ::
  forall (a :: S -> Type).
  ( Typeable a
  , PLiftable a
  , Eq (AsHaskell a)
  , PIsData a
  , Plutus.ToData (AsHaskell a)
  , Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , Show (AsHaskell a)
  ) =>
  TestTree
checkLedgerProperties :: forall (a :: S -> Type).
(Typeable @(S -> Type) a, PLiftable a, Eq (AsHaskell a), PIsData a,
 ToData (AsHaskell a), Arbitrary (AsHaskell a),
 Pretty (AsHaskell a), Show (AsHaskell a)) =>
TestTree
checkLedgerProperties =
  TestName -> [TestTree] -> TestTree
testGroup (forall k (a :: k). Typeable @k a => TestName -> TestName
instanceOfType @(S -> Type) @a TestName
"Ledger Laws") ([TestTree] -> TestTree)
-> ([[TestTree]] -> [TestTree]) -> [[TestTree]] -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[TestTree]] -> [TestTree]
forall a. Monoid a => [a] -> a
mconcat ([[TestTree]] -> TestTree) -> [[TestTree]] -> TestTree
forall a b. (a -> b) -> a -> b
$
    [ forall (a :: S -> Type).
(Arbitrary (AsHaskell a), PLiftable a, PIsData a, Eq (AsHaskell a),
 ToData (AsHaskell a), Pretty (AsHaskell a)) =>
TestName -> [TestTree]
pisDataLaws @a (Bool -> TypeRep @(S -> Type) a -> TestName
forall {k1} (k2 :: k1). Bool -> TypeRep @k1 k2 -> TestName
typeName' Bool
False (forall {k} (a :: k). Typeable @k a => TypeRep @k a
forall (a :: S -> Type).
Typeable @(S -> Type) a =>
TypeRep @(S -> Type) a
typeRep @a)) -- it'll get wrapped in PAsData so not top level
    , forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), Eq (AsHaskell a),
 PLiftable a, Show (AsHaskell a)) =>
[TestTree]
checkPLiftableLaws @a
    ]

-- | @since 1.0.0
checkLedgerPropertiesPCountable ::
  forall (a :: S -> Type).
  ( Typeable a
  , PCountable a
  , Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , Eq (AsHaskell a)
  , Show (AsHaskell a)
  , PLiftable a
  ) =>
  TestTree
checkLedgerPropertiesPCountable :: forall (a :: S -> Type).
(Typeable @(S -> Type) a, PCountable a, Arbitrary (AsHaskell a),
 Pretty (AsHaskell a), Eq (AsHaskell a), Show (AsHaskell a),
 PLiftable a) =>
TestTree
checkLedgerPropertiesPCountable =
  TestName -> [TestTree] -> TestTree
testGroup (forall k (a :: k). Typeable @k a => TestName -> TestName
instanceOfType @(S -> Type) @a TestName
"PCountable") (forall (a :: S -> Type).
(PCountable a, Arbitrary (AsHaskell a), Pretty (AsHaskell a),
 Eq (AsHaskell a), Show (AsHaskell a), PLiftable a) =>
[TestTree]
pcountableLaws @a)

-- | @since 1.0.0
checkLedgerPropertiesPEnumerable ::
  forall (a :: S -> Type).
  ( Typeable a
  , PEnumerable a
  , Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , Eq (AsHaskell a)
  , PLiftable a
  ) =>
  TestTree
checkLedgerPropertiesPEnumerable :: forall (a :: S -> Type).
(Typeable @(S -> Type) a, PEnumerable a, Arbitrary (AsHaskell a),
 Pretty (AsHaskell a), Eq (AsHaskell a), PLiftable a) =>
TestTree
checkLedgerPropertiesPEnumerable =
  TestName -> [TestTree] -> TestTree
testGroup (forall k (a :: k). Typeable @k a => TestName -> TestName
instanceOfType @(S -> Type) @a TestName
"PEnumerable") (forall (a :: S -> Type).
(PEnumerable a, Arbitrary (AsHaskell a), Pretty (AsHaskell a),
 Eq (AsHaskell a), PLiftable a) =>
[TestTree]
penumerableLaws @a)

-- | @since 1.0.0
checkHaskellOrdEquivalent ::
  forall (plutarchInput :: S -> Type).
  ( PLiftable plutarchInput
  , Pretty (AsHaskell plutarchInput)
  , Arbitrary (AsHaskell plutarchInput)
  , Typeable (AsHaskell plutarchInput)
  , Ord (AsHaskell plutarchInput)
  , Typeable plutarchInput
  , POrd plutarchInput
  ) =>
  TestTree
checkHaskellOrdEquivalent :: forall (plutarchInput :: S -> Type).
(PLiftable plutarchInput, Pretty (AsHaskell plutarchInput),
 Arbitrary (AsHaskell plutarchInput),
 Typeable @Type (AsHaskell plutarchInput),
 Ord (AsHaskell plutarchInput), Typeable @(S -> Type) plutarchInput,
 POrd plutarchInput) =>
TestTree
checkHaskellOrdEquivalent =
  TestName -> [TestTree] -> TestTree
testGroup
    ( [TestName] -> TestName
forall a. Monoid a => [a] -> a
mconcat
        [ forall k (a :: k). Typeable @k a => TestName -> TestName
instanceOfType @Type @(AsHaskell plutarchInput) TestName
"Ord"
        , TestName
Item [TestName]
" <-> "
        , forall k (a :: k). Typeable @k a => TestName -> TestName
instanceOfType @(S -> Type) @plutarchInput TestName
"POrd"
        ]
    )
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"== = #==" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        (AsHaskell plutarchInput
 -> AsHaskell plutarchInput -> AsHaskell PBool)
-> (forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> Property
forall (plutarchInput1 :: S -> Type) (plutarchInput2 :: S -> Type)
       (plutarchOutput :: S -> Type).
(PLiftable plutarchInput1, Pretty (AsHaskell plutarchInput1),
 Arbitrary (AsHaskell plutarchInput1), PLiftable plutarchInput2,
 Pretty (AsHaskell plutarchInput2),
 Arbitrary (AsHaskell plutarchInput2), PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput1
 -> AsHaskell plutarchInput2 -> AsHaskell plutarchOutput)
-> (forall (s0 :: S).
    Term s0 (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput)))
-> Property
checkHaskellEquivalent2 (forall a. Eq a => a -> a -> Bool
(==) @(AsHaskell plutarchInput)) ((forall (s0 :: S).
 Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> forall (s0 :: S).
   Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((forall (s0 :: S).
  Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
 -> forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> (forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> forall (s0 :: S).
   Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s0 plutarchInput -> Term s0 plutarchInput -> Term s0 PBool)
-> Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 plutarchInput -> Term s0 PBool)
-> Term s0 (c :--> (plutarchInput :--> PBool))
plam (forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
(#==) @plutarchInput))
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"< = #<" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        (AsHaskell plutarchInput
 -> AsHaskell plutarchInput -> AsHaskell PBool)
-> (forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> Property
forall (plutarchInput1 :: S -> Type) (plutarchInput2 :: S -> Type)
       (plutarchOutput :: S -> Type).
(PLiftable plutarchInput1, Pretty (AsHaskell plutarchInput1),
 Arbitrary (AsHaskell plutarchInput1), PLiftable plutarchInput2,
 Pretty (AsHaskell plutarchInput2),
 Arbitrary (AsHaskell plutarchInput2), PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput1
 -> AsHaskell plutarchInput2 -> AsHaskell plutarchOutput)
-> (forall (s0 :: S).
    Term s0 (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput)))
-> Property
checkHaskellEquivalent2 (forall a. Ord a => a -> a -> Bool
(<) @(AsHaskell plutarchInput)) ((forall (s0 :: S).
 Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> forall (s0 :: S).
   Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((forall (s0 :: S).
  Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
 -> forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> (forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> forall (s0 :: S).
   Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s0 plutarchInput -> Term s0 plutarchInput -> Term s0 PBool)
-> Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 plutarchInput -> Term s0 PBool)
-> Term s0 (c :--> (plutarchInput :--> PBool))
plam (forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
(#<) @plutarchInput))
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"<= = #<=" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        (AsHaskell plutarchInput
 -> AsHaskell plutarchInput -> AsHaskell PBool)
-> (forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> Property
forall (plutarchInput1 :: S -> Type) (plutarchInput2 :: S -> Type)
       (plutarchOutput :: S -> Type).
(PLiftable plutarchInput1, Pretty (AsHaskell plutarchInput1),
 Arbitrary (AsHaskell plutarchInput1), PLiftable plutarchInput2,
 Pretty (AsHaskell plutarchInput2),
 Arbitrary (AsHaskell plutarchInput2), PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput1
 -> AsHaskell plutarchInput2 -> AsHaskell plutarchOutput)
-> (forall (s0 :: S).
    Term s0 (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput)))
-> Property
checkHaskellEquivalent2 (forall a. Ord a => a -> a -> Bool
(<=) @(AsHaskell plutarchInput)) ((forall (s0 :: S).
 Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> forall (s0 :: S).
   Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((forall (s0 :: S).
  Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
 -> forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> (forall (s0 :: S).
    Term s0 (plutarchInput :--> (plutarchInput :--> PBool)))
-> forall (s0 :: S).
   Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s0 plutarchInput -> Term s0 plutarchInput -> Term s0 PBool)
-> Term s0 (plutarchInput :--> (plutarchInput :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 plutarchInput -> Term s0 PBool)
-> Term s0 (c :--> (plutarchInput :--> PBool))
plam (forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
(#<=) @plutarchInput))
    ]

checkHaskellNumEquivalent ::
  forall (plutarchInput :: S -> Type).
  ( PLiftable plutarchInput
  , Pretty (AsHaskell plutarchInput)
  , Arbitrary (AsHaskell plutarchInput)
  , Eq (AsHaskell plutarchInput)
  , Typeable (AsHaskell plutarchInput)
  , Num (AsHaskell plutarchInput)
  , Typeable plutarchInput
  , PIntegralDomain plutarchInput
  ) =>
  TestTree
checkHaskellNumEquivalent :: forall (plutarchInput :: S -> Type).
(PLiftable plutarchInput, Pretty (AsHaskell plutarchInput),
 Arbitrary (AsHaskell plutarchInput), Eq (AsHaskell plutarchInput),
 Typeable @Type (AsHaskell plutarchInput),
 Num (AsHaskell plutarchInput), Typeable @(S -> Type) plutarchInput,
 PIntegralDomain plutarchInput) =>
TestTree
checkHaskellNumEquivalent =
  TestName -> [TestTree] -> TestTree
testGroup
    ( [TestName] -> TestName
forall a. Monoid a => [a] -> a
mconcat
        [ forall k (a :: k). Typeable @k a => TestName -> TestName
instanceOfType @Type @(AsHaskell plutarchInput) TestName
"Num"
        , TestName
Item [TestName]
" <-> "
        , forall k (a :: k). Typeable @k a => TestName -> TestName
instanceOfType @(S -> Type) @plutarchInput TestName
"PNum"
        ]
    )
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"+ = #+" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ forall (plutarchInput1 :: S -> Type) (plutarchInput2 :: S -> Type)
       (plutarchOutput :: S -> Type).
(PLiftable plutarchInput1, Pretty (AsHaskell plutarchInput1),
 Arbitrary (AsHaskell plutarchInput1), PLiftable plutarchInput2,
 Pretty (AsHaskell plutarchInput2),
 Arbitrary (AsHaskell plutarchInput2), PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput1
 -> AsHaskell plutarchInput2 -> AsHaskell plutarchOutput)
-> (forall (s0 :: S).
    Term s0 (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput)))
-> Property
checkHaskellEquivalent2 @plutarchInput AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a -> a
(+) ((Term s0 plutarchInput
 -> Term s0 plutarchInput -> Term s0 plutarchInput)
-> Term s0 (plutarchInput :--> (plutarchInput :--> plutarchInput))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 plutarchInput -> Term s0 plutarchInput)
-> Term s0 (c :--> (plutarchInput :--> plutarchInput))
plam Term s0 plutarchInput
-> Term s0 plutarchInput -> Term s0 plutarchInput
forall (s :: S).
Term s plutarchInput
-> Term s plutarchInput -> Term s plutarchInput
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+))
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"- = #-" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ forall (plutarchInput1 :: S -> Type) (plutarchInput2 :: S -> Type)
       (plutarchOutput :: S -> Type).
(PLiftable plutarchInput1, Pretty (AsHaskell plutarchInput1),
 Arbitrary (AsHaskell plutarchInput1), PLiftable plutarchInput2,
 Pretty (AsHaskell plutarchInput2),
 Arbitrary (AsHaskell plutarchInput2), PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput1
 -> AsHaskell plutarchInput2 -> AsHaskell plutarchOutput)
-> (forall (s0 :: S).
    Term s0 (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput)))
-> Property
checkHaskellEquivalent2 @plutarchInput AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a -> a
(-) ((Term s0 plutarchInput
 -> Term s0 plutarchInput -> Term s0 plutarchInput)
-> Term s0 (plutarchInput :--> (plutarchInput :--> plutarchInput))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 plutarchInput -> Term s0 plutarchInput)
-> Term s0 (c :--> (plutarchInput :--> plutarchInput))
plam Term s0 plutarchInput
-> Term s0 plutarchInput -> Term s0 plutarchInput
forall (s :: S).
Term s plutarchInput
-> Term s plutarchInput -> Term s plutarchInput
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s a -> Term s a -> Term s a
(#-))
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"* = #*" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ forall (plutarchInput1 :: S -> Type) (plutarchInput2 :: S -> Type)
       (plutarchOutput :: S -> Type).
(PLiftable plutarchInput1, Pretty (AsHaskell plutarchInput1),
 Arbitrary (AsHaskell plutarchInput1), PLiftable plutarchInput2,
 Pretty (AsHaskell plutarchInput2),
 Arbitrary (AsHaskell plutarchInput2), PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput1
 -> AsHaskell plutarchInput2 -> AsHaskell plutarchOutput)
-> (forall (s0 :: S).
    Term s0 (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput)))
-> Property
checkHaskellEquivalent2 @plutarchInput AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a -> a
(*) ((Term s0 plutarchInput
 -> Term s0 plutarchInput -> Term s0 plutarchInput)
-> Term s0 (plutarchInput :--> (plutarchInput :--> plutarchInput))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 plutarchInput -> Term s0 plutarchInput)
-> Term s0 (c :--> (plutarchInput :--> plutarchInput))
plam Term s0 plutarchInput
-> Term s0 plutarchInput -> Term s0 plutarchInput
forall (s :: S).
Term s plutarchInput
-> Term s plutarchInput -> Term s plutarchInput
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
(#*))
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"negate = pnegate" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ forall (plutarchInput :: S -> Type) (plutarchOutput :: S -> Type).
(PLiftable plutarchInput, PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchInput),
 Arbitrary (AsHaskell plutarchInput),
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput -> AsHaskell plutarchOutput)
-> (forall (s0 :: S). Term s0 (plutarchInput :--> plutarchOutput))
-> Property
checkHaskellEquivalent @plutarchInput AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a
negate Term s0 (plutarchInput :--> plutarchInput)
forall (s0 :: S). Term s0 (plutarchInput :--> plutarchInput)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"abs = pabs" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ forall (plutarchInput :: S -> Type) (plutarchOutput :: S -> Type).
(PLiftable plutarchInput, PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchInput),
 Arbitrary (AsHaskell plutarchInput),
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput -> AsHaskell plutarchOutput)
-> (forall (s0 :: S). Term s0 (plutarchInput :--> plutarchOutput))
-> Property
checkHaskellEquivalent @plutarchInput AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a
abs Term s0 (plutarchInput :--> plutarchInput)
forall (s0 :: S). Term s0 (plutarchInput :--> plutarchInput)
forall (a :: S -> Type) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
pabs
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"signum = psignum" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ forall (plutarchInput :: S -> Type) (plutarchOutput :: S -> Type).
(PLiftable plutarchInput, PLiftable plutarchOutput,
 Pretty (AsHaskell plutarchInput),
 Arbitrary (AsHaskell plutarchInput),
 Pretty (AsHaskell plutarchOutput),
 Eq (AsHaskell plutarchOutput)) =>
(AsHaskell plutarchInput -> AsHaskell plutarchOutput)
-> (forall (s0 :: S). Term s0 (plutarchInput :--> plutarchOutput))
-> Property
checkHaskellEquivalent @plutarchInput AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a
signum Term s0 (plutarchInput :--> plutarchInput)
forall (s0 :: S). Term s0 (plutarchInput :--> plutarchInput)
forall (a :: S -> Type) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
psignum
    ]

-- Internal

pcountableLaws ::
  forall (a :: S -> Type).
  ( PCountable a
  , Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , Eq (AsHaskell a)
  , Show (AsHaskell a)
  , PLiftable a
  ) =>
  [TestTree]
pcountableLaws :: forall (a :: S -> Type).
(PCountable a, Arbitrary (AsHaskell a), Pretty (AsHaskell a),
 Eq (AsHaskell a), Show (AsHaskell a), PLiftable a) =>
[TestTree]
pcountableLaws =
  [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"x /= psuccessor x" (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x) AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= AsHaskell a
x
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"y < x = psuccessor y <= x" (Property -> TestTree)
-> (((AsHaskell a, AsHaskell a) -> Property) -> Property)
-> ((AsHaskell a, AsHaskell a) -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a) -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a) -> Property) -> TestTree)
-> ((AsHaskell a, AsHaskell a) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y :: AsHaskell a) ->
        (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
y Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x) AsHaskell PBool -> AsHaskell PBool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
y) Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"x < psuccessor y = x <= y" (Property -> TestTree)
-> (((AsHaskell a, AsHaskell a) -> Property) -> Property)
-> ((AsHaskell a, AsHaskell a) -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a, AsHaskell a)
-> ((AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)])
-> ((AsHaskell a, AsHaskell a) -> TestName)
-> ((AsHaskell a, AsHaskell a) -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, AsHaskell a) -> [(AsHaskell a, AsHaskell a)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, AsHaskell a) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, AsHaskell a) -> Property) -> TestTree)
-> ((AsHaskell a, AsHaskell a) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a, AsHaskell a
y :: AsHaskell a) ->
        (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
y)) AsHaskell PBool -> AsHaskell PBool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
y)
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"psuccessorN 1 = psuccessor" (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s (PPositive :--> (a :--> a))
psuccessorN Term s (PPositive :--> (a :--> a))
-> Term s PPositive -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x) AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"psuccessorN n . psuccessorN m = psuccessorN (n + m)" (Property -> TestTree)
-> (((AsHaskell a, Positive, Positive) -> Property) -> Property)
-> ((AsHaskell a, Positive, Positive) -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a, Positive, Positive)
-> ((AsHaskell a, Positive, Positive)
    -> [(AsHaskell a, Positive, Positive)])
-> ((AsHaskell a, Positive, Positive) -> TestName)
-> ((AsHaskell a, Positive, Positive) -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, Positive, Positive)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, Positive, Positive)
-> [(AsHaskell a, Positive, Positive)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, Positive, Positive) -> TestName
forall a. Show a => a -> TestName
show (((AsHaskell a, Positive, Positive) -> Property) -> TestTree)
-> ((AsHaskell a, Positive, Positive) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a, Positive
n :: Positive, Positive
m :: Positive) ->
        (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s (PPositive :--> (a :--> a))
psuccessorN Term s (PPositive :--> (a :--> a))
-> Term s PPositive -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PPositive AsHaskell PPositive
Positive
n Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s (PPositive :--> (a :--> a))
psuccessorN Term s (PPositive :--> (a :--> a))
-> Term s PPositive -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PPositive AsHaskell PPositive
Positive
m Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x))
          AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s (PPositive :--> (a :--> a))
psuccessorN Term s (PPositive :--> (a :--> a))
-> Term s PPositive -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PPositive AsHaskell PPositive
Positive
n Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PPositive AsHaskell PPositive
Positive
m) Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
  ]

penumerableLaws ::
  forall (a :: S -> Type).
  ( PEnumerable a
  , Arbitrary (AsHaskell a)
  , Pretty (AsHaskell a)
  , Eq (AsHaskell a)
  , PLiftable a
  ) =>
  [TestTree]
penumerableLaws :: forall (a :: S -> Type).
(PEnumerable a, Arbitrary (AsHaskell a), Pretty (AsHaskell a),
 Eq (AsHaskell a), PLiftable a) =>
[TestTree]
penumerableLaws =
  [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"ppredecessor . psuccessor = id" (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (a :--> a)
ppredecessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x) AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"psuccessor . ppredecessor = id" (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (a :--> a)
ppredecessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x) AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"ppredecessorN 1 = ppredecessor" (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a) ->
        (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (PPositive :--> (a :--> a))
ppredecessorN Term s (PPositive :--> (a :--> a))
-> Term s PPositive -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x) AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (a :--> a)
ppredecessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"ppredecessorN n . ppredecessorN m = ppredecessorN (n + m)" (Property -> TestTree)
-> (((AsHaskell a, Positive, Positive) -> Property) -> Property)
-> ((AsHaskell a, Positive, Positive) -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a, Positive, Positive)
-> ((AsHaskell a, Positive, Positive)
    -> [(AsHaskell a, Positive, Positive)])
-> ((AsHaskell a, Positive, Positive) -> TestName)
-> ((AsHaskell a, Positive, Positive) -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a, Positive, Positive)
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell a, Positive, Positive)
-> [(AsHaskell a, Positive, Positive)]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell a, Positive, Positive) -> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell a, Positive, Positive) -> Property) -> TestTree)
-> ((AsHaskell a, Positive, Positive) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell a
x :: AsHaskell a, Positive
n :: Positive, Positive
m :: Positive) ->
        (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (PPositive :--> (a :--> a))
ppredecessorN Term s (PPositive :--> (a :--> a))
-> Term s PPositive -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# AsHaskell PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell PPositive
Positive
n Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (PPositive :--> (a :--> a))
ppredecessorN Term s (PPositive :--> (a :--> a))
-> Term s PPositive -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# AsHaskell PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell PPositive
Positive
m Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x))
          AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (PPositive :--> (a :--> a))
ppredecessorN Term s (PPositive :--> (a :--> a))
-> Term s PPositive -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (AsHaskell PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell PPositive
Positive
n Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ AsHaskell PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell PPositive
Positive
m) Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)
  ]

-- pfromData . pdata = id
-- plift . pforgetData . pdata . pconstant = toData
-- plift . pfromData . punsafeCoerce @(PAsData X) . pconstant . toData = id
pisDataLaws ::
  forall (a :: S -> Type).
  ( Arbitrary (AsHaskell a)
  , PLiftable a
  , PIsData a
  , Eq (AsHaskell a)
  , Plutus.ToData (AsHaskell a)
  , Pretty (AsHaskell a)
  ) =>
  String ->
  [TestTree]
pisDataLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), PLiftable a, PIsData a, Eq (AsHaskell a),
 ToData (AsHaskell a), Pretty (AsHaskell a)) =>
TestName -> [TestTree]
pisDataLaws TestName
tyName =
  [ Item [TestTree]
TestTree
fromToProp
  , Item [TestTree]
TestTree
toDataProp
  , Item [TestTree]
TestTree
coerceProp
  ]
  where
    fromToProp :: TestTree
    fromToProp :: TestTree
fromToProp =
      TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pfromData . pdata = id"
        (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow
        ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
          (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s :: S). Term s a) -> forall (s :: S). Term s a
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 a) -> Term s0 (a :--> a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a) -> Term s0 (c :--> a)
plam (Term s0 (PAsData a) -> Term s0 a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s0 (PAsData a) -> Term s0 a)
-> (Term s0 a -> Term s0 (PAsData a)) -> Term s0 a -> Term s0 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s0 a -> Term s0 (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata) Term s0 (a :--> a) -> Term s0 a -> Term s0 a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x)) AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` AsHaskell a
x
    toDataProp :: TestTree
    toDataProp :: TestTree
toDataProp =
      TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"plift . pforgetData . pdata . pconstant = toData"
        (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow
        ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
          (forall (s :: S). Term s PData) -> AsHaskell PData
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (a :--> PData))
-> forall (s0 :: S). Term s0 (a :--> PData)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 a -> Term s0 PData) -> Term s0 (a :--> PData)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 PData) -> Term s0 (c :--> PData)
plam (Term s0 (PAsData a) -> Term s0 PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData (Term s0 (PAsData a) -> Term s0 PData)
-> (Term s0 a -> Term s0 (PAsData a)) -> Term s0 a -> Term s0 PData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s0 a -> Term s0 (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata)) Term s (a :--> PData) -> Term s a -> Term s PData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
x) Data -> Data -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` AsHaskell a -> Data
forall a. ToData a => a -> Data
Plutus.toData AsHaskell a
x
    coerceProp :: TestTree
    coerceProp :: TestTree
coerceProp =
      TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
coerceName
        (Property -> TestTree)
-> ((AsHaskell a -> Property) -> Property)
-> (AsHaskell a -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (AsHaskell a)
-> (AsHaskell a -> [AsHaskell a])
-> (AsHaskell a -> TestName)
-> (AsHaskell a -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell a)
forall a. Arbitrary a => Gen a
arbitrary AsHaskell a -> [AsHaskell a]
forall a. Arbitrary a => a -> [a]
shrink AsHaskell a -> TestName
forall a. Pretty a => a -> TestName
prettyShow
        ((AsHaskell a -> Property) -> TestTree)
-> (AsHaskell a -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(AsHaskell a
x :: AsHaskell a) ->
          (forall (s :: S). Term s a) -> AsHaskell a
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s0 :: S). Term s0 (PData :--> a))
-> forall (s0 :: S). Term s0 (PData :--> a)
forall (p :: S -> Type).
(forall (s0 :: S). Term s0 p) -> forall (s0 :: S). Term s0 p
precompileTerm ((Term s0 PData -> Term s0 a) -> Term s0 (PData :--> a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s0 c -> Term s0 a) -> Term s0 (c :--> a)
plam (Term s0 (PAsData a) -> Term s0 a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s0 (PAsData a) -> Term s0 a)
-> (Term s0 PData -> Term s0 (PAsData a))
-> Term s0 PData
-> Term s0 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce @(PAsData a))) Term s (PData :--> a) -> Term s PData -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PData (AsHaskell a -> Data
forall a. ToData a => a -> Data
Plutus.toData AsHaskell a
x)) AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` AsHaskell a
x
    coerceName :: String
    coerceName :: TestName
coerceName = TestName
"plift . pfromData . punsafeCoerce @(PAsData " TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
tyName TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
") . pconstant . toData = id"

-- Helpers

-- Effectively (,,), but with a 50% chance to generate three copies of the same
-- thing. This ensures transitivity tests aren't vacuously true.
data Triplet (a :: Type)
  = AllSame a
  | AllDifferent a a a
  deriving stock (Triplet a -> Triplet a -> Bool
(Triplet a -> Triplet a -> Bool)
-> (Triplet a -> Triplet a -> Bool) -> Eq (Triplet a)
forall a. Eq a => Triplet a -> Triplet a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Triplet a -> Triplet a -> Bool
== :: Triplet a -> Triplet a -> Bool
$c/= :: forall a. Eq a => Triplet a -> Triplet a -> Bool
/= :: Triplet a -> Triplet a -> Bool
Eq, Int -> Triplet a -> TestName -> TestName
[Triplet a] -> TestName -> TestName
Triplet a -> TestName
(Int -> Triplet a -> TestName -> TestName)
-> (Triplet a -> TestName)
-> ([Triplet a] -> TestName -> TestName)
-> Show (Triplet a)
forall a. Show a => Int -> Triplet a -> TestName -> TestName
forall a. Show a => [Triplet a] -> TestName -> TestName
forall a. Show a => Triplet a -> TestName
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Triplet a -> TestName -> TestName
showsPrec :: Int -> Triplet a -> TestName -> TestName
$cshow :: forall a. Show a => Triplet a -> TestName
show :: Triplet a -> TestName
$cshowList :: forall a. Show a => [Triplet a] -> TestName -> TestName
showList :: [Triplet a] -> TestName -> TestName
Show)

instance Pretty a => Pretty (Triplet a) where
  {-# INLINEABLE pretty #-}
  pretty :: forall ann. Triplet a -> Doc ann
pretty = (a, a, a) -> Doc ann
forall ann. (a, a, a) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ((a, a, a) -> Doc ann)
-> (Triplet a -> (a, a, a)) -> Triplet a -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Triplet a -> (a, a, a)
forall a. Triplet a -> (a, a, a)
toTriple

instance Arbitrary1 Triplet where
  {-# INLINEABLE liftArbitrary #-}
  liftArbitrary :: forall a. Gen a -> Gen (Triplet a)
liftArbitrary Gen a
gen = [Gen (Triplet a)] -> Gen (Triplet a)
forall a. HasCallStack => [Gen a] -> Gen a
oneof [a -> Triplet a
forall a. a -> Triplet a
AllSame (a -> Triplet a) -> Gen a -> Gen (Triplet a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
gen, a -> a -> a -> Triplet a
forall a. a -> a -> a -> Triplet a
AllDifferent (a -> a -> a -> Triplet a) -> Gen a -> Gen (a -> a -> Triplet a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
gen Gen (a -> a -> Triplet a) -> Gen a -> Gen (a -> Triplet a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen a
gen Gen (a -> Triplet a) -> Gen a -> Gen (Triplet a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen a
gen]
  {-# INLINEABLE liftShrink #-}
  liftShrink :: forall a. (a -> [a]) -> Triplet a -> [Triplet a]
liftShrink a -> [a]
shr = \case
    AllSame a
x -> a -> Triplet a
forall a. a -> Triplet a
AllSame (a -> Triplet a) -> [a] -> [Triplet a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [a]
shr a
x
    AllDifferent a
x a
y a
z ->
      (a -> a -> a -> Triplet a
forall a. a -> a -> a -> Triplet a
AllDifferent (a -> a -> a -> Triplet a) -> [a] -> [a -> a -> Triplet a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [a]
shr a
x [a -> a -> Triplet a] -> [a] -> [a -> Triplet a]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> a -> [a]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
y [a -> Triplet a] -> [a] -> [Triplet a]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> a -> [a]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
z)
        [Triplet a] -> [Triplet a] -> [Triplet a]
forall a. [a] -> [a] -> [a]
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (a -> a -> a -> Triplet a
forall a. a -> a -> a -> Triplet a
AllDifferent a
x (a -> a -> Triplet a) -> [a] -> [a -> Triplet a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [a]
shr a
y [a -> Triplet a] -> [a] -> [Triplet a]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> a -> [a]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
z)
        [Triplet a] -> [Triplet a] -> [Triplet a]
forall a. [a] -> [a] -> [a]
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (a -> a -> a -> Triplet a
forall a. a -> a -> a -> Triplet a
AllDifferent a
x a
y (a -> Triplet a) -> [a] -> [Triplet a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [a]
shr a
z)

instance Arbitrary a => Arbitrary (Triplet a) where
  {-# INLINEABLE arbitrary #-}
  arbitrary :: Gen (Triplet a)
arbitrary = Gen a -> Gen (Triplet a)
forall a. Gen a -> Gen (Triplet a)
forall (f :: Type -> Type) a. Arbitrary1 f => Gen a -> Gen (f a)
liftArbitrary Gen a
forall a. Arbitrary a => Gen a
arbitrary
  {-# INLINEABLE shrink #-}
  shrink :: Triplet a -> [Triplet a]
shrink = (a -> [a]) -> Triplet a -> [Triplet a]
forall a. (a -> [a]) -> Triplet a -> [Triplet a]
forall (f :: Type -> Type) a.
Arbitrary1 f =>
(a -> [a]) -> f a -> [f a]
liftShrink a -> [a]
forall a. Arbitrary a => a -> [a]
shrink

toTriple :: forall (a :: Type). Triplet a -> (a, a, a)
toTriple :: forall a. Triplet a -> (a, a, a)
toTriple = \case
  AllSame a
x -> (a
x, a
x, a
x)
  AllDifferent a
x a
y a
z -> (a
x, a
y, a
z)