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

module Plutarch.Test.Laws (
  checkLedgerPropertiesValue,
  checkLedgerPropertiesAssocMap,
  checkLedgerProperties,
  checkLedgerPropertiesPCountable,
  checkLedgerPropertiesPEnumerable,
  checkHaskellOrdEquivalent,
  checkHaskellNumEquivalent,
  checkHaskellIntegralEquivalent,
  checkPLiftableLaws,
) where

import Plutarch.Builtin (pforgetData)
import Plutarch.Enum (PCountable (psuccessor, psuccessorN), PEnumerable (ppredecessor, ppredecessorN))
import Plutarch.Internal.Lift (PLiftable (fromPlutarch, fromPlutarchRepr, toPlutarch, toPlutarchRepr))
import Plutarch.LedgerApi.V1 qualified as V1
import Plutarch.Num (PNum (pabs, pnegate, psignum, (#*), (#+), (#-)))
import Plutarch.Positive (PPositive, Positive)
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)
import Test.QuickCheck (
  Arbitrary (arbitrary, shrink),
  NonZero (getNonZero),
  forAllShrinkShow,
  (=/=),
  (===),
 )
import Test.Tasty (TestName, TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Type.Reflection (Typeable, typeRep)

{- | 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 -> Type) s a)
-> Either LiftError (AsHaskell a)
fromPlutarch @a (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> PLifted @(S -> Type) 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
  , PPartialOrd 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,
 PPartialOrd 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).
PPartialOrd 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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
(#<=) @plutarchInput))
    ]

-- | @since WIP
checkHaskellIntegralEquivalent ::
  forall (plutarchInput :: S -> Type).
  ( PLiftable plutarchInput
  , Pretty (AsHaskell plutarchInput)
  , Arbitrary (AsHaskell plutarchInput)
  , Typeable (AsHaskell plutarchInput)
  , Integral (AsHaskell plutarchInput)
  , Typeable plutarchInput
  , PIntegral plutarchInput
  ) =>
  TestTree
checkHaskellIntegralEquivalent :: forall (plutarchInput :: S -> Type).
(PLiftable plutarchInput, Pretty (AsHaskell plutarchInput),
 Arbitrary (AsHaskell plutarchInput),
 Typeable @Type (AsHaskell plutarchInput),
 Integral (AsHaskell plutarchInput),
 Typeable @(S -> Type) plutarchInput, PIntegral plutarchInput) =>
TestTree
checkHaskellIntegralEquivalent =
  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
"Integral"
        , TestName
Item [TestName]
" <-> "
        , forall k (a :: k). Typeable @k a => TestName -> TestName
instanceOfType @(S -> Type) @plutarchInput TestName
"PIntegral"
        ]
    )
    [ forall (plutarchInput :: S -> Type).
(Arbitrary (AsHaskell plutarchInput),
 Pretty (AsHaskell plutarchInput), Eq (AsHaskell plutarchInput),
 PLiftable plutarchInput, Num (AsHaskell plutarchInput)) =>
TestName
-> (AsHaskell plutarchInput
    -> AsHaskell plutarchInput -> AsHaskell plutarchInput)
-> ClosedTerm
     (plutarchInput :--> (plutarchInput :--> plutarchInput))
-> TestTree
testIntegralEquivalent @plutarchInput TestName
"div = pdiv" AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Integral a => a -> a -> a
div Term s (plutarchInput :--> (plutarchInput :--> plutarchInput))
ClosedTerm (plutarchInput :--> (plutarchInput :--> plutarchInput))
forall (a :: S -> Type) (s :: S).
PIntegral a =>
Term s (a :--> (a :--> a))
pdiv
    , forall (plutarchInput :: S -> Type).
(Arbitrary (AsHaskell plutarchInput),
 Pretty (AsHaskell plutarchInput), Eq (AsHaskell plutarchInput),
 PLiftable plutarchInput, Num (AsHaskell plutarchInput)) =>
TestName
-> (AsHaskell plutarchInput
    -> AsHaskell plutarchInput -> AsHaskell plutarchInput)
-> ClosedTerm
     (plutarchInput :--> (plutarchInput :--> plutarchInput))
-> TestTree
testIntegralEquivalent @plutarchInput TestName
"mod = pmod" AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Integral a => a -> a -> a
mod Term s (plutarchInput :--> (plutarchInput :--> plutarchInput))
ClosedTerm (plutarchInput :--> (plutarchInput :--> plutarchInput))
forall (a :: S -> Type) (s :: S).
PIntegral a =>
Term s (a :--> (a :--> a))
pmod
    , forall (plutarchInput :: S -> Type).
(Arbitrary (AsHaskell plutarchInput),
 Pretty (AsHaskell plutarchInput), Eq (AsHaskell plutarchInput),
 PLiftable plutarchInput, Num (AsHaskell plutarchInput)) =>
TestName
-> (AsHaskell plutarchInput
    -> AsHaskell plutarchInput -> AsHaskell plutarchInput)
-> ClosedTerm
     (plutarchInput :--> (plutarchInput :--> plutarchInput))
-> TestTree
testIntegralEquivalent @plutarchInput TestName
"quot = pquot" AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Integral a => a -> a -> a
quot Term s (plutarchInput :--> (plutarchInput :--> plutarchInput))
ClosedTerm (plutarchInput :--> (plutarchInput :--> plutarchInput))
forall (a :: S -> Type) (s :: S).
PIntegral a =>
Term s (a :--> (a :--> a))
pquot
    , forall (plutarchInput :: S -> Type).
(Arbitrary (AsHaskell plutarchInput),
 Pretty (AsHaskell plutarchInput), Eq (AsHaskell plutarchInput),
 PLiftable plutarchInput, Num (AsHaskell plutarchInput)) =>
TestName
-> (AsHaskell plutarchInput
    -> AsHaskell plutarchInput -> AsHaskell plutarchInput)
-> ClosedTerm
     (plutarchInput :--> (plutarchInput :--> plutarchInput))
-> TestTree
testIntegralEquivalent @plutarchInput TestName
"rem = prem" AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
forall a. Integral a => a -> a -> a
rem Term s (plutarchInput :--> (plutarchInput :--> plutarchInput))
ClosedTerm (plutarchInput :--> (plutarchInput :--> plutarchInput))
forall (a :: S -> Type) (s :: S).
PIntegral a =>
Term s (a :--> (a :--> a))
prem
    ]

checkHaskellNumEquivalent ::
  forall (plutarchInput :: S -> Type).
  ( PLiftable plutarchInput
  , Pretty (AsHaskell plutarchInput)
  , Arbitrary (AsHaskell plutarchInput)
  , Eq (AsHaskell plutarchInput)
  , Typeable (AsHaskell plutarchInput)
  , Num (AsHaskell plutarchInput)
  , Typeable plutarchInput
  , PNum 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,
 PNum 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).
PNum 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).
PNum 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).
PNum 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). PNum 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). PNum 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). PNum a => Term s (a :--> a)
psignum
    ]

-- Internal

-- | @since WIP
testIntegralEquivalent ::
  forall (plutarchInput :: S -> Type).
  ( Arbitrary (AsHaskell plutarchInput)
  , Pretty (AsHaskell plutarchInput)
  , Eq (AsHaskell plutarchInput)
  , PLiftable plutarchInput
  , Num (AsHaskell plutarchInput)
  ) =>
  TestName ->
  (AsHaskell plutarchInput -> AsHaskell plutarchInput -> AsHaskell plutarchInput) ->
  ClosedTerm (plutarchInput :--> plutarchInput :--> plutarchInput) ->
  TestTree
testIntegralEquivalent :: forall (plutarchInput :: S -> Type).
(Arbitrary (AsHaskell plutarchInput),
 Pretty (AsHaskell plutarchInput), Eq (AsHaskell plutarchInput),
 PLiftable plutarchInput, Num (AsHaskell plutarchInput)) =>
TestName
-> (AsHaskell plutarchInput
    -> AsHaskell plutarchInput -> AsHaskell plutarchInput)
-> ClosedTerm
     (plutarchInput :--> (plutarchInput :--> plutarchInput))
-> TestTree
testIntegralEquivalent TestName
name AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
goHaskell ClosedTerm (plutarchInput :--> (plutarchInput :--> plutarchInput))
goPlutarch =
  TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
name (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    Gen (AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
-> ((AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
    -> [(AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))])
-> ((AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
    -> TestName)
-> ((AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
    -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> TestName) -> (a -> prop) -> Property
forAllShrinkShow Gen (AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
forall a. Arbitrary a => Gen a
arbitrary (AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
-> [(AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))]
forall a. Arbitrary a => a -> [a]
shrink (AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
-> TestName
forall a. Pretty a => a -> TestName
prettyShow (((AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
  -> Property)
 -> Property)
-> ((AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput))
    -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$
      \(AsHaskell plutarchInput
input1 :: AsHaskell plutarchInput, NonZero (AsHaskell plutarchInput)
input2 :: NonZero (AsHaskell plutarchInput)) ->
        AsHaskell plutarchInput
-> AsHaskell plutarchInput -> AsHaskell plutarchInput
goHaskell AsHaskell plutarchInput
input1 (NonZero (AsHaskell plutarchInput) -> AsHaskell plutarchInput
forall a. NonZero a -> a
getNonZero NonZero (AsHaskell plutarchInput)
input2)
          AsHaskell plutarchInput -> AsHaskell plutarchInput -> Property
forall a. (Eq a, Pretty a) => a -> a -> Property
`prettyEquals` (forall (s :: S). Term s plutarchInput) -> AsHaskell plutarchInput
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift (Term s (plutarchInput :--> (plutarchInput :--> plutarchInput))
ClosedTerm (plutarchInput :--> (plutarchInput :--> plutarchInput))
goPlutarch Term s (plutarchInput :--> (plutarchInput :--> plutarchInput))
-> Term s plutarchInput
-> Term s (plutarchInput :--> plutarchInput)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# AsHaskell plutarchInput -> Term s plutarchInput
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell plutarchInput
input1 Term s (plutarchInput :--> plutarchInput)
-> Term s plutarchInput -> Term s plutarchInput
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# AsHaskell plutarchInput -> Term s plutarchInput
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant (NonZero (AsHaskell plutarchInput) -> AsHaskell plutarchInput
forall a. NonZero a -> a
getNonZero NonZero (AsHaskell plutarchInput)
input2))

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).
PPartialOrd 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).
PPartialOrd 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).
PPartialOrd 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).
PPartialOrd 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
1 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 a. Num a => a -> a -> 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
1 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 a. Num a => a -> a -> 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 (s :: S) (a :: S -> Type) (b :: S -> Type).
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