{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Plutarch.Test.Laws (
checkLedgerPropertiesValue,
checkLedgerPropertiesAssocMap,
checkLedgerProperties,
checkLedgerPropertiesPCountable,
checkLedgerPropertiesPEnumerable,
checkHaskellOrdEquivalent,
checkHaskellNumEquivalent,
checkPLiftableLaws,
checkPOrdLaws,
) 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 qualified as PLA
import PlutusLedgerApi.V1.Orphans ()
import PlutusTx.AssocMap qualified as AssocMap
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)
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)
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)
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
)
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
"fromPlutarch . toPlutarch = 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 =>
(forall (s :: S). PLifted s a) -> Either LiftError (AsHaskell a)
fromPlutarch @a (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> PLifted s a
toPlutarch @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
"fromPlutarchRepr . toPlutarchRepr = Just"
(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 -> Maybe (AsHaskell a)
fromPlutarchRepr @a (forall (a :: S -> Type). PLiftable a => AsHaskell a -> PlutusRepr a
toPlutarchRepr @a AsHaskell a
x) Maybe (AsHaskell a) -> Maybe (AsHaskell a) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== AsHaskell a -> Maybe (AsHaskell a)
forall a. a -> Maybe a
Just 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
]
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"
, [TestTree]
Item [[TestTree]]
ptryFromLawsValue
, 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)
]
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"
, [TestTree]
Item [[TestTree]]
ptryFromLawsAssocMap
, 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)
]
checkLedgerProperties ::
forall (a :: S -> Type).
( Typeable a
, PLiftable a
, PTryFrom PData 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, PTryFrom PData 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))
, forall (a :: S -> Type).
(Arbitrary (AsHaskell a), PLiftable a, Eq (AsHaskell a),
PTryFrom PData a, ToData (AsHaskell a), Pretty (AsHaskell a)) =>
[TestTree]
ptryFromLaws @a
, forall (a :: S -> Type).
(Arbitrary (AsHaskell a), Pretty (AsHaskell a), Eq (AsHaskell a),
PLiftable a, Show (AsHaskell a)) =>
[TestTree]
checkPLiftableLaws @a
]
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)
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)
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
]
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)
]
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"
ptryFromLaws ::
forall (a :: S -> Type).
( Arbitrary (AsHaskell a)
, PLiftable a
, Eq (AsHaskell a)
, PTryFrom PData a
, Plutus.ToData (AsHaskell a)
, Pretty (AsHaskell a)
) =>
[TestTree]
ptryFromLaws :: forall (a :: S -> Type).
(Arbitrary (AsHaskell a), PLiftable a, Eq (AsHaskell a),
PTryFrom PData a, ToData (AsHaskell a), Pretty (AsHaskell a)) =>
[TestTree]
ptryFromLaws = [Item [TestTree]
TestTree
pDataAgreementProp]
where
pDataAgreementProp :: TestTree
pDataAgreementProp :: TestTree
pDataAgreementProp = TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"can parse toData of original"
(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 PData -> Term s a) -> Term s (PData :--> a))
-> (Term s PData -> Term s a) -> Term s (PData :--> a)
forall a b. (a -> b) -> a -> b
$ \Term s PData
d -> forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @a Term s PData
d (Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a
forall a b. (a, b) -> a
fst) 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 PData -> Term s PData)
-> (AsHaskell a -> AsHaskell PData) -> AsHaskell a -> Term s PData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsHaskell a -> Data
AsHaskell a -> AsHaskell PData
forall a. ToData a => a -> Data
Plutus.toData (AsHaskell a -> Term s PData) -> AsHaskell a -> Term s PData
forall a b. (a -> b) -> a -> b
$ AsHaskell a
x))
AsHaskell a -> AsHaskell a -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` AsHaskell a
x
ptryFromLawsValue :: [TestTree]
ptryFromLawsValue :: [TestTree]
ptryFromLawsValue = [Item [TestTree]
TestTree
pDataAgreementProp]
where
pDataAgreementProp :: TestTree
pDataAgreementProp :: TestTree
pDataAgreementProp = TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"can parse toData of original"
(Property -> TestTree)
-> ((Value -> Property) -> Property)
-> (Value -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen Value
-> (Value -> [Value])
-> (Value -> TestName)
-> (Value -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen Value
forall a. Arbitrary a => Gen a
arbitrary Value -> [Value]
forall a. Arbitrary a => a -> [a]
shrink Value -> TestName
forall a. Pretty a => a -> TestName
prettyShow
((Value -> Property) -> TestTree)
-> (Value -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(Value
v :: PLA.Value) ->
(forall (s :: S). Term s (PValue 'Unsorted 'NoGuarantees))
-> AsHaskell (PValue 'Unsorted 'NoGuarantees)
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (ClosedTerm (PData :--> PValue 'Unsorted 'NoGuarantees)
-> ClosedTerm (PData :--> PValue 'Unsorted 'NoGuarantees)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s PData -> Term s (PValue 'Unsorted 'NoGuarantees))
-> Term s (PData :--> PValue 'Unsorted 'NoGuarantees)
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 (PValue 'Unsorted 'NoGuarantees))
-> Term s (c :--> PValue 'Unsorted 'NoGuarantees)
plam ((Term s PData -> Term s (PValue 'Unsorted 'NoGuarantees))
-> Term s (PData :--> PValue 'Unsorted 'NoGuarantees))
-> (Term s PData -> Term s (PValue 'Unsorted 'NoGuarantees))
-> Term s (PData :--> PValue 'Unsorted 'NoGuarantees)
forall a b. (a -> b) -> a -> b
$ \Term s PData
d -> Term s (PAsData (PValue 'Unsorted 'NoGuarantees))
-> Term s (PValue 'Unsorted 'NoGuarantees)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PValue 'Unsorted 'NoGuarantees))
-> Term s (PValue 'Unsorted 'NoGuarantees))
-> (((Term s (PAsData (PValue 'Unsorted 'NoGuarantees)),
Reduce
(PTryFromExcess
PData (PAsData (PValue 'Unsorted 'NoGuarantees)) s))
-> Term s (PAsData (PValue 'Unsorted 'NoGuarantees)))
-> Term s (PAsData (PValue 'Unsorted 'NoGuarantees)))
-> ((Term s (PAsData (PValue 'Unsorted 'NoGuarantees)),
Reduce
(PTryFromExcess
PData (PAsData (PValue 'Unsorted 'NoGuarantees)) s))
-> Term s (PAsData (PValue 'Unsorted 'NoGuarantees)))
-> Term s (PValue 'Unsorted 'NoGuarantees)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData (V1.PValue V1.Unsorted V1.NoGuarantees)) Term s PData
d (((Term s (PAsData (PValue 'Unsorted 'NoGuarantees)),
Reduce
(PTryFromExcess
PData (PAsData (PValue 'Unsorted 'NoGuarantees)) s))
-> Term s (PAsData (PValue 'Unsorted 'NoGuarantees)))
-> Term s (PValue 'Unsorted 'NoGuarantees))
-> ((Term s (PAsData (PValue 'Unsorted 'NoGuarantees)),
Reduce
(PTryFromExcess
PData (PAsData (PValue 'Unsorted 'NoGuarantees)) s))
-> Term s (PAsData (PValue 'Unsorted 'NoGuarantees)))
-> Term s (PValue 'Unsorted 'NoGuarantees)
forall a b. (a -> b) -> a -> b
$ (Term s (PAsData (PValue 'Unsorted 'NoGuarantees)),
Reduce
(PTryFromExcess
PData (PAsData (PValue 'Unsorted 'NoGuarantees)) s))
-> Term s (PAsData (PValue 'Unsorted 'NoGuarantees))
forall a b. (a, b) -> a
fst) Term s (PData :--> PValue 'Unsorted 'NoGuarantees)
-> Term s PData -> Term s (PValue 'Unsorted 'NoGuarantees)
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 (Value -> Data
forall a. ToData a => a -> Data
Plutus.toData Value
v))
Value -> Value -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` Value
v
ptryFromLawsAssocMap :: [TestTree]
ptryFromLawsAssocMap :: [TestTree]
ptryFromLawsAssocMap = [Item [TestTree]
TestTree
pDataAgreementProp]
where
pDataAgreementProp :: TestTree
pDataAgreementProp :: TestTree
pDataAgreementProp = TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"can parse toData of original"
(Property -> TestTree)
-> ((Map Integer Integer -> Property) -> Property)
-> (Map Integer Integer -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (Map Integer Integer)
-> (Map Integer Integer -> [Map Integer Integer])
-> (Map Integer Integer -> TestName)
-> (Map Integer Integer -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (Map Integer Integer)
forall a. Arbitrary a => Gen a
arbitrary Map Integer Integer -> [Map Integer Integer]
forall a. Arbitrary a => a -> [a]
shrink Map Integer Integer -> TestName
forall a. Pretty a => a -> TestName
prettyShow
((Map Integer Integer -> Property) -> TestTree)
-> (Map Integer Integer -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(Map Integer Integer
v :: AssocMap.Map Integer Integer) ->
(forall (s :: S). Term s (PMap 'Unsorted PInteger PInteger))
-> AsHaskell (PMap 'Unsorted PInteger PInteger)
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (ClosedTerm (PData :--> PMap 'Unsorted PInteger PInteger)
-> ClosedTerm (PData :--> PMap 'Unsorted PInteger PInteger)
forall (p :: S -> Type). ClosedTerm p -> ClosedTerm p
precompileTerm ((Term s PData -> Term s (PMap 'Unsorted PInteger PInteger))
-> Term s (PData :--> PMap 'Unsorted PInteger PInteger)
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 (PMap 'Unsorted PInteger PInteger))
-> Term s (c :--> PMap 'Unsorted PInteger PInteger)
plam ((Term s PData -> Term s (PMap 'Unsorted PInteger PInteger))
-> Term s (PData :--> PMap 'Unsorted PInteger PInteger))
-> (Term s PData -> Term s (PMap 'Unsorted PInteger PInteger))
-> Term s (PData :--> PMap 'Unsorted PInteger PInteger)
forall a b. (a -> b) -> a -> b
$ \Term s PData
d -> Term s (PAsData (PMap 'Unsorted PInteger PInteger))
-> Term s (PMap 'Unsorted PInteger PInteger)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PMap 'Unsorted PInteger PInteger))
-> Term s (PMap 'Unsorted PInteger PInteger))
-> (((Term s (PAsData (PMap 'Unsorted PInteger PInteger)),
Reduce
(PTryFromExcess
PData (PAsData (PMap 'Unsorted PInteger PInteger)) s))
-> Term s (PAsData (PMap 'Unsorted PInteger PInteger)))
-> Term s (PAsData (PMap 'Unsorted PInteger PInteger)))
-> ((Term s (PAsData (PMap 'Unsorted PInteger PInteger)),
Reduce
(PTryFromExcess
PData (PAsData (PMap 'Unsorted PInteger PInteger)) s))
-> Term s (PAsData (PMap 'Unsorted PInteger PInteger)))
-> Term s (PMap 'Unsorted PInteger PInteger)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData (V1.PMap V1.Unsorted PInteger PInteger)) Term s PData
d (((Term s (PAsData (PMap 'Unsorted PInteger PInteger)),
Reduce
(PTryFromExcess
PData (PAsData (PMap 'Unsorted PInteger PInteger)) s))
-> Term s (PAsData (PMap 'Unsorted PInteger PInteger)))
-> Term s (PMap 'Unsorted PInteger PInteger))
-> ((Term s (PAsData (PMap 'Unsorted PInteger PInteger)),
Reduce
(PTryFromExcess
PData (PAsData (PMap 'Unsorted PInteger PInteger)) s))
-> Term s (PAsData (PMap 'Unsorted PInteger PInteger)))
-> Term s (PMap 'Unsorted PInteger PInteger)
forall a b. (a -> b) -> a -> b
$ (Term s (PAsData (PMap 'Unsorted PInteger PInteger)),
Reduce
(PTryFromExcess
PData (PAsData (PMap 'Unsorted PInteger PInteger)) s))
-> Term s (PAsData (PMap 'Unsorted PInteger PInteger))
forall a b. (a, b) -> a
fst) Term s (PData :--> PMap 'Unsorted PInteger PInteger)
-> Term s PData -> Term s (PMap 'Unsorted PInteger PInteger)
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 (Map Integer Integer -> Data
forall a. ToData a => a -> Data
Plutus.toData Map Integer Integer
v))
Map Integer Integer -> Map Integer Integer -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` Map Integer Integer
v
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)