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

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

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

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

@since WIP
-}
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
  ]

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

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

@since WIP
-}
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)
    ]

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

Same as above

@since WIP
-}
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)
    ]

-- | @since WIP
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)) -- it'll get wrapped in PAsData so not top level
    , 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
    ]

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

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

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

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

-- Internal

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

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

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

-- ptryFrom should successfully parse a toData of a type
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

-- This is an ugly kludge because PValue doesn't have a direct PData conversion,
-- and bringing one in would break too much other stuff to be worth it.
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

-- Same as before
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

-- Helpers

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

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

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

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

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