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

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

import Control.Applicative ((<|>))
import Data.Kind (Type)
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
        ( ClosedTerm (a :--> (a :--> (a :--> PBool)))
-> ClosedTerm (a :--> (a :--> (a :--> PBool)))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> (a :--> PBool)))
plam ((Term s a -> Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> (a :--> PBool))))
-> (Term s a -> Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> (a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 Term s a
arg3 -> (Term s a
arg1 Term s a -> Term s a -> Term s 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 s a
arg2 Term s a -> Term s a -> Term s 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 s a
arg3)) 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
arg1 Term s a -> Term s a -> Term s 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 s a
arg2) Term s a -> Term s a -> Term s 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 s 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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> (Term s a
arg1 Term s a -> Term s a -> Term s 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 s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PMonoid a => Term s a
pmempty) 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
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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> (Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PMonoid a => Term s a
pmempty Term s a -> Term s a -> Term s 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 s a
arg1) 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
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 (ClosedTerm (a :--> (a :--> PBool))
-> ClosedTerm (a :--> (a :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> PBool))
plam ((Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> PBool)))
-> (Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 -> (Term s a
arg1 Term s a -> Term s a -> Term s 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 s a
arg2) 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
arg2 Term s a -> Term s a -> Term s 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 s 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
          ( ClosedTerm (a :--> (a :--> (a :--> PBool)))
-> ClosedTerm (a :--> (a :--> (a :--> PBool)))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> (a :--> PBool)))
plam ((Term s a -> Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> (a :--> PBool))))
-> (Term s a -> Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> (a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 Term s a
arg3 -> ((Term s a
arg1 Term s a -> Term s a -> Term s 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 s a
arg2) Term s a -> Term s a -> Term s 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 s a
arg3) 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
arg1 Term s a -> Term s a -> Term s 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 s a
arg2 Term s a -> Term s a -> Term s 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 s 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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> (Term s a
arg1 Term s a -> Term s a -> Term s 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 s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero) 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
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 (ClosedTerm (PPositive :--> PBool)
-> ClosedTerm (PPositive :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s PPositive -> Term s PBool) -> Term s (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 s c -> Term s PBool) -> Term s (c :--> PBool)
plam ((Term s PPositive -> Term s PBool)
 -> Term s (PPositive :--> PBool))
-> (Term s PPositive -> Term s PBool)
-> Term s (PPositive :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
arg1 -> Term s a -> Term s PPositive -> Term s 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 s PPositive
arg1 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
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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> ((Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate 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
arg1) Term s a -> Term s a -> Term s 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 s a
arg1) 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
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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate 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).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate 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
arg1) 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
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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> (Term s a
arg1 Term s a -> Term s a -> Term s 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 s a
arg1) 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
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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate 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
arg1) 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
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero Term s a -> Term s a -> Term s 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 s 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
          ( ClosedTerm (a :--> (a :--> PBool))
-> ClosedTerm (a :--> (a :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> PBool))
plam ((Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> PBool)))
-> (Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 -> (Term s a
arg1 Term s a -> Term s a -> Term s 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 s a
arg2) 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
arg1 Term s a -> Term s a -> Term s 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 s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate 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
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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> Term s a
arg1 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
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
            ( ClosedTerm (a :--> (a :--> (a :--> PBool)))
-> ClosedTerm (a :--> (a :--> (a :--> PBool)))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> (a :--> PBool)))
plam ((Term s a -> Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> (a :--> PBool))))
-> (Term s a -> Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> (a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 Term s a
arg3 -> (Term s a
arg1 Term s a -> Term s a -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s a
arg2) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s a
arg2 Term s a -> Term s a -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s a
arg3) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s a
arg1 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
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
        ( ClosedTerm (a :--> (a :--> PBool))
-> ClosedTerm (a :--> (a :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> PBool))
plam ((Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> PBool)))
-> (Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 -> (Term s a
arg1 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
arg2) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s a
arg2 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
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 (ClosedTerm (a :--> PBool) -> ClosedTerm (a :--> PBool)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((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 -> Term s PBool) -> Term s (a :--> PBool))
-> (Term s a -> Term s PBool) -> Term s (a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 -> Term s (PBool :--> PBool)
forall (s :: S). Term s (PBool :--> PBool)
pnot Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s a
arg1 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
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
        ( ClosedTerm (a :--> (a :--> (a :--> PBool)))
-> ClosedTerm (a :--> (a :--> (a :--> PBool)))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> (a :--> PBool)))
plam ((Term s a -> Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> (a :--> PBool))))
-> (Term s a -> Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> (a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 Term s a
arg3 -> (Term s a
arg1 Term s a -> Term s a -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#>= Term s a
arg2) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s a
arg2 Term s a -> Term s a -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#>= Term s a
arg3) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s a
arg1 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
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
        ( ClosedTerm (a :--> (a :--> PBool))
-> ClosedTerm (a :--> (a :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> PBool))
plam ((Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> PBool)))
-> (Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 -> (Term s a
arg1 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
arg2) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s a
arg2 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
arg1) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s a
arg1 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
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 (ClosedTerm (a :--> (a :--> PBool))
-> ClosedTerm (a :--> (a :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> PBool))
plam ((Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> PBool)))
-> (Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 -> Term s a
arg1 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
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
          ( ClosedTerm (a :--> (a :--> PBool))
-> ClosedTerm (a :--> (a :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a -> Term s PBool)
-> Term s (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 s c -> Term s a -> Term s PBool)
-> Term s (c :--> (a :--> PBool))
plam ((Term s a -> Term s a -> Term s PBool)
 -> Term s (a :--> (a :--> PBool)))
-> (Term s a -> Term s a -> Term s PBool)
-> Term s (a :--> (a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
arg1 Term s a
arg2 -> (Term s a
arg1 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
arg2) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s a
arg1 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
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
  ]

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

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
"PValue" ([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.PValue V1.Unsorted V1.NoGuarantees) TestName
"PValue"
    , forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), Eq (AsHaskell a),
 PLiftable a, Show (AsHaskell a)) =>
[TestTree]
checkPLiftableLaws @(V1.PValue V1.Unsorted V1.NoGuarantees)
    ]

{- | 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.PMap V1.Unsorted 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.PMap V1.Unsorted 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)
-> ClosedTerm (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)
-> ClosedTerm
     (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput))
-> Property
checkHaskellEquivalent2 (forall a. Eq a => a -> a -> Bool
(==) @(AsHaskell plutarchInput)) (ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm (ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
 -> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool)))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s plutarchInput -> Term s plutarchInput -> Term s PBool)
-> Term s (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 s c -> Term s plutarchInput -> Term s PBool)
-> Term s (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)
-> ClosedTerm (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)
-> ClosedTerm
     (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput))
-> Property
checkHaskellEquivalent2 (forall a. Ord a => a -> a -> Bool
(<) @(AsHaskell plutarchInput)) (ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm (ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
 -> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool)))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s plutarchInput -> Term s plutarchInput -> Term s PBool)
-> Term s (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 s c -> Term s plutarchInput -> Term s PBool)
-> Term s (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)
-> ClosedTerm (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)
-> ClosedTerm
     (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput))
-> Property
checkHaskellEquivalent2 (forall a. Ord a => a -> a -> Bool
(<=) @(AsHaskell plutarchInput)) (ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm (ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
 -> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool)))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
-> ClosedTerm (plutarchInput :--> (plutarchInput :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s plutarchInput -> Term s plutarchInput -> Term s PBool)
-> Term s (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 s c -> Term s plutarchInput -> Term s PBool)
-> Term s (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)
-> ClosedTerm
     (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput))
-> Property
checkHaskellEquivalent2 @plutarchInput AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a -> a
(+) ((Term s plutarchInput
 -> Term s plutarchInput -> Term s plutarchInput)
-> Term s (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 s c -> Term s plutarchInput -> Term s plutarchInput)
-> Term s (c :--> (plutarchInput :--> plutarchInput))
plam Term s plutarchInput
-> Term s plutarchInput -> Term s 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)
-> ClosedTerm
     (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput))
-> Property
checkHaskellEquivalent2 @plutarchInput AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a -> a
(-) ((Term s plutarchInput
 -> Term s plutarchInput -> Term s plutarchInput)
-> Term s (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 s c -> Term s plutarchInput -> Term s plutarchInput)
-> Term s (c :--> (plutarchInput :--> plutarchInput))
plam Term s plutarchInput
-> Term s plutarchInput -> Term s 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)
-> ClosedTerm
     (plutarchInput1 :--> (plutarchInput2 :--> plutarchOutput))
-> Property
checkHaskellEquivalent2 @plutarchInput AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a -> a
(*) ((Term s plutarchInput
 -> Term s plutarchInput -> Term s plutarchInput)
-> Term s (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 s c -> Term s plutarchInput -> Term s plutarchInput)
-> Term s (c :--> (plutarchInput :--> plutarchInput))
plam Term s plutarchInput
-> Term s plutarchInput -> Term s 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)
-> ClosedTerm (plutarchInput :--> plutarchOutput) -> Property
checkHaskellEquivalent @plutarchInput AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a
negate Term s (plutarchInput :--> plutarchInput)
ClosedTerm (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)
-> ClosedTerm (plutarchInput :--> plutarchOutput) -> Property
checkHaskellEquivalent @plutarchInput AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a
abs Term s (plutarchInput :--> plutarchInput)
ClosedTerm (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)
-> ClosedTerm (plutarchInput :--> plutarchOutput) -> Property
checkHaskellEquivalent @plutarchInput AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Num a => a -> a
signum Term s (plutarchInput :--> plutarchInput)
ClosedTerm (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). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s a) -> Term s (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 s c -> Term s a) -> Term s (c :--> a)
plam (Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData a) -> Term s a)
-> (Term s a -> Term s (PAsData a)) -> Term s a -> Term s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata) 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` 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 (ClosedTerm (a :--> PData) -> ClosedTerm (a :--> PData)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s a -> Term s PData) -> Term s (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 s c -> Term s PData) -> Term s (c :--> PData)
plam (Term s (PAsData a) -> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData a) -> Term s PData)
-> (Term s a -> Term s (PAsData a)) -> Term s a -> Term s PData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (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 (ClosedTerm (PData :--> a) -> ClosedTerm (PData :--> a)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s PData -> Term s a) -> Term s (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 s c -> Term s a) -> Term s (c :--> a)
plam (Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData a) -> Term s a)
-> (Term s PData -> Term s (PAsData a)) -> Term s PData -> Term s 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)