{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Plutarch.Test.QuickCheck (
  PLamArgs,
  PA,
  PB,
  PC,
  punlam',
  punlam,
  fromPFun,
  fromPPartial,
  fromFailingPPartial,
  pexpectFailure,
  haskEquiv',
  haskEquiv,
  shrinkPLift,
  arbitraryPLift,
  PFun (..),
  pattern PFn,
  TestableTerm (..),
  PArbitrary (..),
  pconstantT,
  pliftT,
  uplcEq,
  Equality (..),
  Partiality (..),
  PWrapLam,
  PUnLamHask,
  PLamWrapped,
  FromPFun,
  NotPLam,
  shouldCrash,
  shouldRun,
) where

import Data.Kind (Constraint, Type)
import GHC.TypeLits
import Generics.SOP (All, HPure (hcpure), NP (Nil, (:*)), Proxy (Proxy))
import Plutarch (Config (Config), Script, TracingMode (DoTracing, NoTracing), compile, tracingMode)
import Plutarch.Evaluate (evalScript, evalScriptHuge, evalTerm)
import Plutarch.Lift (DerivePConstantViaNewtype (..), PConstantDecl, PUnsafeLiftDecl (PLifted))
import Plutarch.Num (PNum)
import Plutarch.Prelude (
  ClosedTerm,
  DPTStrat,
  DerivePlutusType,
  Generic,
  PBool,
  PEq,
  PInteger,
  PIsData,
  PLift,
  POpaque,
  POrd,
  PPartialOrd,
  PlutusType,
  PlutusTypeNewtype,
  S,
  Term,
  pcon,
  pconstant,
  pdata,
  plift,
  pto,
  (#),
  (#==),
  type (:-->),
 )
import Plutarch.Show (PShow)
import Plutarch.Test.QuickCheck.Function (
  PFun (..),
  pattern PFn,
 )
import Plutarch.Test.QuickCheck.Helpers (loudEval)
import Plutarch.Test.QuickCheck.Internal (
  FailingTestableTerm (..),
  PArbitrary (..),
  PCoArbitrary (..),
  TestableTerm (..),
  pconstantT,
  pliftT,
 )
import Test.QuickCheck (
  Arbitrary (..),
  Gen,
  Property,
  Testable (property),
  counterexample,
  forAll,
  (.&&.),
 )
import Test.QuickCheck.Poly (A (A), B (B), C (C))

{- | Helper for writing property tests at the Haskell level. Given a 'Script',
 run it with the largest limits possible: if it crashes, pass; otherwise,
 fail and report any logs.

 = Note

 Depending on the logging settings the 'Script' was compiled with, you may not
 get any logs. While we print a warning when this happens, there might have
 just not been any logs to give you in the first place: there's no way to tell
 for sure.

 @since 2.1.5
-}
shouldCrash :: Script -> Property
shouldCrash :: Script -> Property
shouldCrash Script
script =
  let (Either EvalError Script
res, ExBudget
_, [Text]
logs) = Script -> (Either EvalError Script, ExBudget, [Text])
evalScriptHuge Script
script
   in case Either EvalError Script
res of
        Left EvalError
_ -> forall prop. Testable prop => prop -> Property
property Bool
True
        Right Script
_ ->
          forall prop. Testable prop => String -> prop -> Property
counterexample String
"Expected failure, but succeeded instead."
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => [a] -> String
showLogs [Text]
logs)
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => prop -> Property
property
            forall a b. (a -> b) -> a -> b
$ Bool
False

{- | Helper for writing property tests at the Haskell level. Given a 'Script',
 run it with the largest limits possible: if it runs, pass; otherwise, fail
 and report the error, as well as any logs.

 = Note

 Depending on the logging settings the 'Script' was compiled with, you may not
 get any logs. While we print a warning when this happens, there might have
 just not been any logs to give you in the first place: there's no way to tell
 for sure.

 @since 2.1.5
-}
shouldRun :: Script -> Property
shouldRun :: Script -> Property
shouldRun Script
script =
  let (Either EvalError Script
res, ExBudget
_, [Text]
logs) = Script -> (Either EvalError Script, ExBudget, [Text])
evalScriptHuge Script
script
   in case Either EvalError Script
res of
        Left EvalError
err ->
          forall prop. Testable prop => String -> prop -> Property
counterexample String
"Expected success, but failed instead."
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Error: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show EvalError
err)
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => [a] -> String
showLogs [Text]
logs)
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => prop -> Property
property
            forall a b. (a -> b) -> a -> b
$ Bool
False
        Right Script
_ -> forall prop. Testable prop => prop -> Property
property Bool
True

-- Get the type of Haskell TestableTerm function and change Plutarch
-- lambda to PFun if there is one:
-- :k! PLamWrapped (TestableTerm PInteger -> TestableTerm (PInteger :--> PBool) -> TestableTerm PUnit)
-- = TestableTerm PInteger -> PFun PInteger PBool -> TestableTerm PUnit
type family PLamWrapped (h :: Type) :: Type where
  PLamWrapped (TestableTerm (a :--> b) -> c) = PFun a b -> PLamWrapped c
  PLamWrapped (a -> b) = a -> PLamWrapped b
  PLamWrapped a = a

-- Check if given type of TestableTerm is a lambda.
type family IsLam (h :: Type) :: Bool where
  IsLam (TestableTerm (a :--> b) -> c) = 'True
  IsLam _ = 'False

-- Check if given type of Haskell is function or not.
type family IsLast (h :: Type) :: Bool where
  IsLast (_ -> _) = 'False
  IsLast _ = 'True

{- | Ensure given 'PType'('S -> Type') ir not an arrow. This is very useful
     when using ambiguous type variable.

 @since 2.2.0
-}
type NotPLam (p :: S -> Type) = IsLam (TestableTerm p) ~ 'False

-- Helper for type error.
-- Empty constraint when all arguments/return are TestableTerm
-- Type error when there exists some non TestableTerm type.
type family OnlyTestableTerm (h :: Type) :: Constraint where
  OnlyTestableTerm (TestableTerm _ -> a) = OnlyTestableTerm a
  OnlyTestableTerm (TestableTerm _) = ()
  OnlyTestableTerm h =
    TypeError
      ( 'Text "\""
          ':<>: 'ShowType h
          ':<>: 'Text "\" is not in terms of \"TestableTerm\""
          ':$$: 'Text "\tFunction should be only in terms of TestableTerms"
      )

-- | Wraps TestableTerm lambda to `PFun` for function generation and shrinking.
class PWrapLam' (h :: Type) (lam :: Bool) (last :: Bool) where
  pwrapLam' :: h -> PLamWrapped h

instance
  forall (a :: Type) (b :: Type) (pa :: S -> Type) (pb :: S -> Type).
  ( TestableTerm (pa :--> pb) ~ a
  , PWrapLam' b (IsLam b) (IsLast b)
  , PLamWrapped (a -> b) ~ (PFun pa pb -> PLamWrapped b)
  , PLift pa
  , PLift pb
  ) =>
  PWrapLam' (a -> b) 'True 'False
  where
  pwrapLam' :: (a -> b) -> PLamWrapped (a -> b)
pwrapLam' a -> b
f (PFn forall (s :: S). Term s (pa :--> pb)
pf) = forall h (lam :: Bool) (last :: Bool).
PWrapLam' h lam last =>
h -> PLamWrapped h
pwrapLam' @b @(IsLam b) @(IsLast b) forall a b. (a -> b) -> a -> b
$ a -> b
f (forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall (s :: S). Term s (pa :--> pb)
pf)

instance
  forall (a :: Type) (b :: Type).
  ( PWrapLam' b (IsLam b) (IsLast b)
  , PLamWrapped (a -> b) ~ (a -> PLamWrapped b)
  ) =>
  PWrapLam' (a -> b) 'False 'False
  where
  pwrapLam' :: (a -> b) -> PLamWrapped (a -> b)
pwrapLam' a -> b
f a
x = forall h (lam :: Bool) (last :: Bool).
PWrapLam' h lam last =>
h -> PLamWrapped h
pwrapLam' @b @(IsLam b) @(IsLast b) forall a b. (a -> b) -> a -> b
$ a -> b
f a
x

instance
  forall (a :: Type).
  (PLamWrapped a ~ a) =>
  PWrapLam' a 'False 'True
  where
  pwrapLam' :: a -> PLamWrapped a
pwrapLam' = forall a. a -> a
id

{- | Constraint for `PWrapLam'` that will give a better type error message.

 @since 2.1.0
-}
type PWrapLam (h :: Type) = (PWrapLam' h (IsLam h) (IsLast h), OnlyTestableTerm h)

{- | Replace any TestableTerm that is a lambda with `PFun` for generation and
     shrinking. It will ignore lambda on the return as it should not be
     generated.

= Note
`TestableTerm`s that are Plutarc function means @TestableTerm (a :--> b)@.

 @since 2.1.0
-}
pwrapLam ::
  forall (h :: Type).
  PWrapLam h =>
  h ->
  PLamWrapped h
pwrapLam :: forall h. PWrapLam h => h -> PLamWrapped h
pwrapLam = forall h (lam :: Bool) (last :: Bool).
PWrapLam' h lam last =>
h -> PLamWrapped h
pwrapLam' @h @(IsLam h) @(IsLast h)

-- Get the type of Haskell Testable function from given Plutarch Function.
-- It requires the final return type and the actual function type, both in PType.
--
-- This typeclass is not exhaustive: it will not reduce when provided final return
-- type is not an actual return type of Plutarch function.
type family PUnLamHask (fin :: S -> Type) (p :: S -> Type) :: Type where
  PUnLamHask a a = TestableTerm a
  PUnLamHask fin ((a :--> b) :--> c) =
    TestableTerm (a :--> b) -> PUnLamHask fin c
  PUnLamHask fin (a :--> b) = TestableTerm a -> PUnLamHask fin b

-- Helper for type error.
-- This will give a type error when final return type given does not match
-- that of the actual function.
type family CheckReturn (fin :: S -> Type) (p :: S -> Type) :: Constraint where
  CheckReturn a a = ()
  CheckReturn fin ((a :--> b) :--> c) = CheckReturn fin c
  CheckReturn fin (a :--> b) = CheckReturn fin b
  CheckReturn a b =
    ( a ~ b
    , TypeError
        ( 'Text "Return type does not match:"
            ':$$: 'Text "\tExpected \""
              ':<>: 'ShowType a
              ':<>: 'Text "\" but given function returns \""
              ':<>: 'ShowType b
              ':<>: 'Text "\""
        )
    )

type family IsFinal (fin :: S -> Type) (p :: S -> Type) :: Bool where
  IsFinal a a = 'True
  IsFinal _ _ = 'False

{- | Brings Plutarch function into Haskell given the final return type.
     It will wrap each arguments and the return type with `TestableTerm`.

 @since 2.1.0
-}
class PUnLam' (fin :: S -> Type) (p :: S -> Type) (end :: Bool) where
  pUnLam' :: (forall s. Term s p) -> PUnLamHask fin p

instance
  forall (fin :: S -> Type) (pa :: S -> Type) (pb :: S -> Type).
  ( PUnLam' fin pb (IsFinal fin pb)
  , PUnLamHask fin (pa :--> pb) ~ (TestableTerm pa -> PUnLamHask fin pb)
  ) =>
  PUnLam' fin (pa :--> pb) 'False
  where
  pUnLam' :: (forall (s :: S). Term s (pa :--> pb))
-> PUnLamHask fin (pa :--> pb)
pUnLam' forall (s :: S). Term s (pa :--> pb)
f (TestableTerm forall (s :: S). Term s pa
y) = forall (fin :: PType) (p :: PType) (end :: Bool).
PUnLam' fin p end =>
(forall (s :: S). Term s p) -> PUnLamHask fin p
pUnLam' @fin @pb @(IsFinal fin pb) (forall (s :: S). Term s (pa :--> pb)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s pa
y)

instance PUnLam' fin fin 'True where
  pUnLam' :: (forall (s :: S). Term s fin) -> PUnLamHask fin fin
pUnLam' = forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm

{- | Constraint for `punlam`-related functions.

 @since 2.1.0
-}
type PUnLam fin p = (PUnLam' fin p (IsFinal fin p), CheckReturn fin p)

{- | Bring Plutarch function into the Haskell level with each Plutarch
     types wrapped in the `TestableTerm`.

 @since 2.1.0
-}
punlam' ::
  forall (fin :: S -> Type) (p :: S -> Type).
  PUnLam fin p =>
  (forall s. Term s p) ->
  PUnLamHask fin p
punlam' :: forall (fin :: PType) (p :: PType).
PUnLam fin p =>
(forall (s :: S). Term s p) -> PUnLamHask fin p
punlam' = forall (fin :: PType) (p :: PType) (end :: Bool).
PUnLam' fin p end =>
(forall (s :: S). Term s p) -> PUnLamHask fin p
pUnLam' @fin @p @(IsFinal fin p)

{- | Same as @punlam'@ but evaluates the given Plutarch function before
     the conversion. It will throw an error if evaluation fails.

 @since 2.1.0
-}
punlam ::
  forall (fin :: S -> Type) (p :: S -> Type).
  PUnLam fin p =>
  (forall s. Term s p) ->
  PUnLamHask fin p
punlam :: forall (fin :: PType) (p :: PType).
PUnLam fin p =>
(forall (s :: S). Term s p) -> PUnLamHask fin p
punlam forall (s :: S). Term s p
pf = forall (fin :: PType) (p :: PType).
PUnLam fin p =>
(forall (s :: S). Term s p) -> PUnLamHask fin p
punlam' @fin (forall (p :: PType). ClosedTerm p -> ClosedTerm p
loudEval forall (s :: S). Term s p
pf)

{- | Constraint for 'fromPFun'.

 @since 2.2.0
-}
type FromPFun (end :: S -> Type) (a :: S -> Type) =
  ( PUnLam end a
  , PWrapLam (PUnLamHask end a)
  )

{- | "Converts a Plutarch function into a Haskell function on
     'TestableTerm's, then wraps functions into 'PFun' as
     necessary. The result will be 'Quickcheck-compatible' if all
     Plutarch types used have 'PArbitrary' instances."

 @since 2.0.0
-}
fromPFun ::
  forall (p :: S -> Type).
  FromPFun PBool p =>
  ClosedTerm p ->
  PLamWrapped (PUnLamHask PBool p)
fromPFun :: forall (p :: PType).
FromPFun PBool p =>
ClosedTerm p -> PLamWrapped (PUnLamHask PBool p)
fromPFun ClosedTerm p
pf = forall h. PWrapLam h => h -> PLamWrapped h
pwrapLam forall a b. (a -> b) -> a -> b
$ forall (fin :: PType) (p :: PType).
PUnLam fin p =>
(forall (s :: S). Term s p) -> PUnLamHask fin p
punlam @PBool ClosedTerm p
pf

{- | Same as 'fromPFun' but it expects 'POpaque' as the return type. It is
     helpful testing partial functions like 'PValidator'.

 @since 2.1.6
-}
fromPPartial ::
  forall (p :: S -> Type).
  FromPFun POpaque p =>
  ClosedTerm p ->
  PLamWrapped (PUnLamHask POpaque p)
fromPPartial :: forall (p :: PType).
FromPFun POpaque p =>
ClosedTerm p -> PLamWrapped (PUnLamHask POpaque p)
fromPPartial ClosedTerm p
pf = forall h. PWrapLam h => h -> PLamWrapped h
pwrapLam forall a b. (a -> b) -> a -> b
$ forall (fin :: PType) (p :: PType).
PUnLam fin p =>
(forall (s :: S). Term s p) -> PUnLamHask fin p
punlam @POpaque ClosedTerm p
pf

-- Makes return type 'FailingTestableTerm' to make QC look for fails instead
-- of successes.
type family PExpectingFail (a :: Type) where
  PExpectingFail (TestableTerm a) = FailingTestableTerm a
  PExpectingFail (TestableTerm a -> b) = TestableTerm a -> PExpectingFail b

class PExpectFailure' (a :: Type) (last :: Bool) where
  pexpectFailure' :: a -> PExpectingFail a

instance PExpectFailure' (TestableTerm a) 'True where
  pexpectFailure' :: TestableTerm a -> PExpectingFail (TestableTerm a)
pexpectFailure' = forall (a :: PType). TestableTerm a -> FailingTestableTerm a
FailingTestableTerm

instance
  forall (a :: Type) (b :: Type).
  ( PExpectFailure' b (IsLast b)
  , PExpectingFail (a -> b) ~ (a -> PExpectingFail b)
  ) =>
  PExpectFailure' (a -> b) 'False
  where
  pexpectFailure' :: (a -> b) -> PExpectingFail (a -> b)
pexpectFailure' a -> b
f a
x = forall a (last :: Bool).
PExpectFailure' a last =>
a -> PExpectingFail a
pexpectFailure' @b @(IsLast b) forall a b. (a -> b) -> a -> b
$ a -> b
f a
x

type PExpectFailure a = (PExpectFailure' a (IsLast a))

{- | Mark testable function to expect failing case. Unlike `expectFailure` from
     QC, this will *not* abort after encountering one failing. Instead, it will
     run for all cases and make sure all cases fail. This can accept any
     Plutarch types.

 @since 2.1.6
-}
pexpectFailure ::
  forall (a :: Type).
  PExpectFailure a =>
  a ->
  PExpectingFail a
pexpectFailure :: forall a. PExpectFailure a => a -> PExpectingFail a
pexpectFailure =
  forall a (last :: Bool).
PExpectFailure' a last =>
a -> PExpectingFail a
pexpectFailure' @a @(IsLast a)

{- | Same as 'fromPPartial' but it test for failure instead of successes.

 @since 2.1.6
-}
fromFailingPPartial ::
  forall (p :: S -> Type).
  ( PUnLam POpaque p
  , PWrapLam (PUnLamHask POpaque p)
  , PExpectFailure (PLamWrapped (PUnLamHask POpaque p))
  ) =>
  ClosedTerm p ->
  PExpectingFail (PLamWrapped (PUnLamHask POpaque p))
fromFailingPPartial :: forall (p :: PType).
(PUnLam POpaque p, PWrapLam (PUnLamHask POpaque p),
 PExpectFailure (PLamWrapped (PUnLamHask POpaque p))) =>
ClosedTerm p -> PExpectingFail (PLamWrapped (PUnLamHask POpaque p))
fromFailingPPartial ClosedTerm p
pf = forall a. PExpectFailure a => a -> PExpectingFail a
pexpectFailure forall a b. (a -> b) -> a -> b
$ forall h. PWrapLam h => h -> PLamWrapped h
pwrapLam forall a b. (a -> b) -> a -> b
$ forall (fin :: PType) (p :: PType).
PUnLam fin p =>
(forall (s :: S). Term s p) -> PUnLamHask fin p
punlam @POpaque ClosedTerm p
pf

{- | Ways an Plutarch terms can be compared.
     @OnPEq@ uses Plutarch `PEq` instance to compare give terms. This
     means two terms with different UPLC representations can be
     considered equal when `PEq` instance defines so.
     @OnUPLC@ uses compiled and evaluated raw UPLC to compare two
     terms. It is useful comparing Terms that forgot their types--
     `POpqaue`.

 @since 2.1.0
-}
data Equality
  = OnPEq
  | OnPData
  | OnBoth
  deriving stock (Equality -> Equality -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Equality -> Equality -> Bool
$c/= :: Equality -> Equality -> Bool
== :: Equality -> Equality -> Bool
$c== :: Equality -> Equality -> Bool
Eq, Int -> Equality -> ShowS
[Equality] -> ShowS
Equality -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Equality] -> ShowS
$cshowList :: [Equality] -> ShowS
show :: Equality -> String
$cshow :: Equality -> String
showsPrec :: Int -> Equality -> ShowS
$cshowsPrec :: Int -> Equality -> ShowS
Show)

{- | Partiality of the comparison. @ByPartial@ will have some
     performance disadventages.

 @since 2.1.0
-}
data Partiality
  = ByComplete
  | ByPartial

{- | Extracts all @TestableTerm@s from give Plutarch function.

 @since 2.0.0
-}
type family PLamArgs (p :: S -> Type) :: [Type] where
  PLamArgs (a :--> b) = TestableTerm a : PLamArgs b
  PLamArgs _ = '[]

{- | Make property by directly comparing behavior of Plutarch function
     to Haskell counterpart.  This function will expect all Plutarch
     types to be `plift`able and `pshow`able.  With given TestableTerm
     generator, it will generate value for each arguments. Then, it
     will apply generated value and lifted value to Plutarch and
     haskell function. Once all arguments are applied, It will check
     the equality of results.

     There are few options provided by @HaskEquiv@. It allows users to
     use specific comparison methods: @OnPEq@, @OnPData@, @OnBoth@.
     @OnPEq@ uses Plutarch typeclass @PEq@ to compare two resulting
     outcomes(one from Plutarch function, other from Haskell function).
     @OnPData@ compares the raw `Data`s from two functions. @OnBoth@
     conjoins @OnPEq@ and @OnPData@.

     Users can also specify partiality of provided function:
     @ByComplete@ and @ByPartial@. @ByPartial@ will allow Haskell
     functions to expect a failure in Plutarch functions. Maybe return
     is expected from the Haskell function; @Nothing@ will represent
     the case where Plutarch function fails. @ByComplete@ expects
     Plutarch function to not fail. It will consider failure on
     evaluation as a failure. @ByPartial@ will be slightly less
     performant than @ByComplete@, so it is recommended to use
     @ByComplete@ when possible.

 @since 2.0.0
-}
class
  (PLamArgs p ~ args) =>
  HaskEquiv
    (e :: Equality)
    (par :: Partiality)
    (h :: Type)
    (p :: S -> Type)
    (args :: [Type])
  where
  haskEquiv :: h -> TestableTerm p -> NP Gen args -> Property

-- | @since 2.1.0
instance
  forall
    (e :: Equality)
    (par :: Partiality)
    (ha :: Type)
    (hb :: Type)
    (pa :: S -> Type)
    (pb :: S -> Type)
    (hbArgs :: [Type]).
  ( PLamArgs pb ~ hbArgs
  , HaskEquiv e par hb pb hbArgs
  , PLifted pa ~ ha
  , PLift pa
  , PShow pa
  ) =>
  HaskEquiv e par (ha -> hb) (pa :--> pb) (TestableTerm pa ': hbArgs)
  where
  haskEquiv :: (ha -> hb)
-> TestableTerm (pa :--> pb)
-> NP Gen (TestableTerm pa : hbArgs)
-> Property
haskEquiv ha -> hb
h (TestableTerm forall (s :: S). Term s (pa :--> pb)
p) (Gen x
g :* NP Gen xs
gs) =
    forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen x
g forall a b. (a -> b) -> a -> b
$ \(TestableTerm forall (s :: S). Term s pa
x) -> forall (e :: Equality) (par :: Partiality) h (p :: PType)
       (args :: [*]).
HaskEquiv e par h p args =>
h -> TestableTerm p -> NP Gen args -> Property
haskEquiv @e @par (ha -> hb
h forall a b. (a -> b) -> a -> b
$ forall (p :: PType).
(HasCallStack, PLift p) =>
ClosedTerm p -> PLifted p
plift forall (s :: S). Term s pa
x) (forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s (pa :--> pb)
p forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s pa
x) NP Gen xs
gs

instance
  forall (e :: Equality) (p :: S -> Type) (h :: Type).
  (HaskEquiv e 'ByComplete h p '[]) =>
  HaskEquiv e 'ByPartial (Maybe h) p '[]
  where
  haskEquiv :: Maybe h -> TestableTerm p -> NP Gen '[] -> Property
haskEquiv Maybe h
h (TestableTerm forall (s :: S). Term s p
p) NP Gen '[]
_ =
    case forall (a :: PType).
Config
-> ClosedTerm a
-> Either Text (Either EvalError (ClosedTerm a), ExBudget, [Text])
evalTerm (Config {$sel:tracingMode:Config :: TracingMode
tracingMode = TracingMode
DoTracing}) forall (s :: S). Term s p
p of
      Left Text
err -> String -> Property
failWith forall a b. (a -> b) -> a -> b
$ String
"Plutarch compilation failed.\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Text
err
      Right (Left EvalError
err, ExBudget
_, [Text]
t) ->
        case Maybe h
h of
          Just h
_ -> String -> Property
failWith forall a b. (a -> b) -> a -> b
$ String
"Haskell expected success, but Plutarch evaluation failed.\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show EvalError
err forall a. Semigroup a => a -> a -> a
<> String
"\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show [Text]
t
          Maybe h
Nothing -> forall prop. Testable prop => prop -> Property
property Bool
True
      Right (Right forall (s :: S). Term s p
p', ExBudget
_, [Text]
t) ->
        case Maybe h
h of
          Just h
h' -> forall (e :: Equality) (par :: Partiality) h (p :: PType)
       (args :: [*]).
HaskEquiv e par h p args =>
h -> TestableTerm p -> NP Gen args -> Property
haskEquiv @e @'ByComplete h
h' (forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall (s :: S). Term s p
p') forall {k} (a :: k -> *). NP a '[]
Nil
          Maybe h
Nothing -> String -> Property
failWith forall a b. (a -> b) -> a -> b
$ String
"Haskell expected failure, but Plutarch succeed.\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show [Text]
t

-- | @since 2.1.0
instance
  forall (p :: S -> Type) (h :: Type).
  (PLamArgs p ~ '[], PLift p, PLifted p ~ h, PEq p) =>
  HaskEquiv 'OnPEq 'ByComplete h p '[]
  where
  haskEquiv :: h -> TestableTerm p -> NP Gen '[] -> Property
haskEquiv h
h (TestableTerm forall (s :: S). Term s p
p) NP Gen '[]
_ =
    forall prop. Testable prop => String -> prop -> Property
counterexample String
"Comparison by PEq Failed" forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
        forall (p :: PType).
(HasCallStack, PLift p) =>
ClosedTerm p -> PLifted p
plift forall a b. (a -> b) -> a -> b
$
          forall (s :: S). Term s p
p forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant h
h

-- | @since 2.1.0
instance
  forall (p :: S -> Type) (h :: Type).
  (PLamArgs p ~ '[], PLift p, PLifted p ~ h, PIsData p) =>
  HaskEquiv 'OnPData 'ByComplete h p '[]
  where
  haskEquiv :: h -> TestableTerm p -> NP Gen '[] -> Property
haskEquiv h
h (TestableTerm forall (s :: S). Term s p
p) NP Gen '[]
_ =
    forall prop. Testable prop => String -> prop -> Property
counterexample String
"Comparison by PData Failed" forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
        forall (p :: PType).
(HasCallStack, PLift p) =>
ClosedTerm p -> PLifted p
plift (forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata forall (s :: S). Term s p
p forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant h
h))

-- | @since 2.1.0
instance
  forall (p :: S -> Type) (h :: Type).
  (PLamArgs p ~ '[], PLift p, PLifted p ~ h, PIsData p, PEq p) =>
  HaskEquiv 'OnBoth 'ByComplete h p '[]
  where
  haskEquiv :: h -> TestableTerm p -> NP Gen '[] -> Property
haskEquiv h
h TestableTerm p
p NP Gen '[]
_ =
    forall (e :: Equality) (par :: Partiality) h (p :: PType)
       (args :: [*]).
HaskEquiv e par h p args =>
h -> TestableTerm p -> NP Gen args -> Property
haskEquiv @'OnPEq @'ByComplete h
h TestableTerm p
p forall {k} (a :: k -> *). NP a '[]
Nil
      forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. forall (e :: Equality) (par :: Partiality) h (p :: PType)
       (args :: [*]).
HaskEquiv e par h p args =>
h -> TestableTerm p -> NP Gen args -> Property
haskEquiv @'OnPData @'ByComplete h
h TestableTerm p
p forall {k} (a :: k -> *). NP a '[]
Nil

{- | Simplified version of `haskEquiv`. It will use arbitrary instead of
     asking custom generators.

 @since 2.0.0
-}
haskEquiv' ::
  forall (e :: Equality) (par :: Partiality) (h :: Type) (p :: S -> Type) (args :: [Type]).
  ( HaskEquiv e par h p args
  , All Arbitrary args
  ) =>
  h ->
  (forall s. Term s p) ->
  Property
haskEquiv' :: forall (e :: Equality) (par :: Partiality) h (p :: PType)
       (args :: [*]).
(HaskEquiv e par h p args, All Arbitrary args) =>
h -> (forall (s :: S). Term s p) -> Property
haskEquiv' h
h forall (s :: S). Term s p
p =
  forall (e :: Equality) (par :: Partiality) h (p :: PType)
       (args :: [*]).
HaskEquiv e par h p args =>
h -> TestableTerm p -> NP Gen args -> Property
haskEquiv @e @par h
h (forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall (s :: S). Term s p
p) forall a b. (a -> b) -> a -> b
$
    forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure (forall {k} (t :: k). Proxy t
Proxy @Arbitrary) forall a. Arbitrary a => Gen a
arbitrary

{- | Compares evaluated UPLC

 @since 2.0.1
-}
uplcEq ::
  forall (a :: S -> Type) (b :: S -> Type).
  TestableTerm a ->
  TestableTerm b ->
  Property
uplcEq :: forall (a :: PType) (b :: PType).
TestableTerm a -> TestableTerm b -> Property
uplcEq TestableTerm a
x TestableTerm b
y = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> Property
failWith forall prop. Testable prop => prop -> Property
property Either String Bool
go
  where
    go :: Either String Bool
go = do
      Script
x' <- forall {a :: PType}. TestableTerm a -> Either String Script
eval TestableTerm a
x
      Script
y' <- forall {a :: PType}. TestableTerm a -> Either String Script
eval TestableTerm b
y
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Script
x' forall a. Eq a => a -> a -> Bool
== Script
y'
    eval :: TestableTerm a -> Either String Script
eval (TestableTerm forall (s :: S). Term s a
t) =
      case forall (a :: PType). Config -> ClosedTerm a -> Either Text Script
compile (Config {$sel:tracingMode:Config :: TracingMode
tracingMode = TracingMode
NoTracing}) forall (s :: S). Term s a
t of
        Left Text
err -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"Term compilation failed:\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Text
err
        Right Script
s' ->
          case Script -> (Either EvalError Script, ExBudget, [Text])
evalScript Script
s' of
            (Right Script
s, ExBudget
_, [Text]
_) -> forall a b. b -> Either a b
Right Script
s
            (Left EvalError
err, ExBudget
_, [Text]
_) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"Term evaluation failed:\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show EvalError
err

{- | Placeholder for a polymorphic type. Plutarch equivalence of QuickCheck's
  `A`.

 @since 2.0.0
-}
newtype PA (s :: S)
  = PA (Term s PInteger)
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x. Rep (PA s) x -> PA s
forall (s :: S) x. PA s -> Rep (PA s) x
$cto :: forall (s :: S) x. Rep (PA s) x -> PA s
$cfrom :: forall (s :: S) x. PA s -> Rep (PA s) x
Generic)
  deriving anyclass (forall (s :: S). PA s -> Term s (PInner PA)
forall (s :: S) (b :: PType).
Term s (PInner PA) -> (PA s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PA) -> (PA s -> Term s b) -> Term s b
$cpmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PA) -> (PA s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PA s -> Term s (PInner PA)
$cpcon' :: forall (s :: S). PA s -> Term s (PInner PA)
PlutusType, forall (s :: S). Term s (PAsData PA) -> Term s PA
forall (s :: S). Term s PA -> Term s PData
forall (a :: PType).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
pdataImpl :: forall (s :: S). Term s PA -> Term s PData
$cpdataImpl :: forall (s :: S). Term s PA -> Term s PData
pfromDataImpl :: forall (s :: S). Term s (PAsData PA) -> Term s PA
$cpfromDataImpl :: forall (s :: S). Term s (PAsData PA) -> Term s PA
PIsData, forall (s :: S). Term s PA -> Term s PA -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
#== :: forall (s :: S). Term s PA -> Term s PA -> Term s PBool
$c#== :: forall (s :: S). Term s PA -> Term s PA -> Term s PBool
PEq, PEq PA
forall (s :: S). Term s PA -> Term s PA -> Term s PBool
forall (t :: PType).
PEq t
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> PPartialOrd t
#< :: forall (s :: S). Term s PA -> Term s PA -> Term s PBool
$c#< :: forall (s :: S). Term s PA -> Term s PA -> Term s PBool
#<= :: forall (s :: S). Term s PA -> Term s PA -> Term s PBool
$c#<= :: forall (s :: S). Term s PA -> Term s PA -> Term s PBool
PPartialOrd, PPartialOrd PA
forall (t :: PType). PPartialOrd t -> POrd t
POrd, forall (s :: S). Bool -> Term s PA -> Term s PString
forall (t :: PType).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
pshow' :: forall (s :: S). Bool -> Term s PA -> Term s PString
$cpshow' :: forall (s :: S). Bool -> Term s PA -> Term s PString
PShow, forall (s :: S). Term s (PA :--> PA)
forall (s :: S). Integer -> Term s PA
forall (s :: S). Term s PA -> Term s PA -> Term s PA
forall (a :: PType).
(forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Integer -> Term s a)
-> PNum a
pfromInteger :: forall (s :: S). Integer -> Term s PA
$cpfromInteger :: forall (s :: S). Integer -> Term s PA
psignum :: forall (s :: S). Term s (PA :--> PA)
$cpsignum :: forall (s :: S). Term s (PA :--> PA)
pabs :: forall (s :: S). Term s (PA :--> PA)
$cpabs :: forall (s :: S). Term s (PA :--> PA)
pnegate :: forall (s :: S). Term s (PA :--> PA)
$cpnegate :: forall (s :: S). Term s (PA :--> PA)
#* :: forall (s :: S). Term s PA -> Term s PA -> Term s PA
$c#* :: forall (s :: S). Term s PA -> Term s PA -> Term s PA
#- :: forall (s :: S). Term s PA -> Term s PA -> Term s PA
$c#- :: forall (s :: S). Term s PA -> Term s PA -> Term s PA
#+ :: forall (s :: S). Term s PA -> Term s PA -> Term s PA
$c#+ :: forall (s :: S). Term s PA -> Term s PA -> Term s PA
PNum)

-- | @since 2.0.0
instance DerivePlutusType PA where type DPTStrat _ = PlutusTypeNewtype

-- | @since 2.0.0
instance PUnsafeLiftDecl PA where type PLifted PA = A

-- | @since 2.0.0
deriving via
  (DerivePConstantViaNewtype A PA PInteger)
  instance
    PConstantDecl A

-- | @since 2.0.0
instance PArbitrary PA where
  parbitrary :: Gen (TestableTerm PA)
parbitrary = do
    (TestableTerm forall (s :: S). Term s PInteger
x) <- forall (a :: PType). PArbitrary a => Gen (TestableTerm a)
parbitrary
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PA s
PA forall (s :: S). Term s PInteger
x

  pshrink :: TestableTerm PA -> [TestableTerm PA]
pshrink (TestableTerm forall (s :: S). Term s PA
x) =
    let f :: TestableTerm PInteger -> TestableTerm PA
f (TestableTerm forall (s :: S). Term s PInteger
y) = forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PA s
PA forall (s :: S). Term s PInteger
y
     in TestableTerm PInteger -> TestableTerm PA
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => a -> [a]
shrink (forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (s :: S). Term s PA
x)

-- | @since 2.0.0
instance PCoArbitrary PA where
  pcoarbitrary :: forall b. TestableTerm PA -> Gen b -> Gen b
pcoarbitrary (TestableTerm forall (s :: S). Term s PA
x) = forall (a :: PType) b.
PCoArbitrary a =>
TestableTerm a -> Gen b -> Gen b
pcoarbitrary forall a b. (a -> b) -> a -> b
$ forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (s :: S). Term s PA
x

{- | Same as `PA`.

 @since 2.0.0
-}
newtype PB (s :: S)
  = PB (Term s PInteger)
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x. Rep (PB s) x -> PB s
forall (s :: S) x. PB s -> Rep (PB s) x
$cto :: forall (s :: S) x. Rep (PB s) x -> PB s
$cfrom :: forall (s :: S) x. PB s -> Rep (PB s) x
Generic)
  deriving anyclass (forall (s :: S). PB s -> Term s (PInner PB)
forall (s :: S) (b :: PType).
Term s (PInner PB) -> (PB s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PB) -> (PB s -> Term s b) -> Term s b
$cpmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PB) -> (PB s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PB s -> Term s (PInner PB)
$cpcon' :: forall (s :: S). PB s -> Term s (PInner PB)
PlutusType, forall (s :: S). Term s (PAsData PB) -> Term s PB
forall (s :: S). Term s PB -> Term s PData
forall (a :: PType).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
pdataImpl :: forall (s :: S). Term s PB -> Term s PData
$cpdataImpl :: forall (s :: S). Term s PB -> Term s PData
pfromDataImpl :: forall (s :: S). Term s (PAsData PB) -> Term s PB
$cpfromDataImpl :: forall (s :: S). Term s (PAsData PB) -> Term s PB
PIsData, forall (s :: S). Term s PB -> Term s PB -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
#== :: forall (s :: S). Term s PB -> Term s PB -> Term s PBool
$c#== :: forall (s :: S). Term s PB -> Term s PB -> Term s PBool
PEq, PEq PB
forall (s :: S). Term s PB -> Term s PB -> Term s PBool
forall (t :: PType).
PEq t
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> PPartialOrd t
#< :: forall (s :: S). Term s PB -> Term s PB -> Term s PBool
$c#< :: forall (s :: S). Term s PB -> Term s PB -> Term s PBool
#<= :: forall (s :: S). Term s PB -> Term s PB -> Term s PBool
$c#<= :: forall (s :: S). Term s PB -> Term s PB -> Term s PBool
PPartialOrd, PPartialOrd PB
forall (t :: PType). PPartialOrd t -> POrd t
POrd, forall (s :: S). Bool -> Term s PB -> Term s PString
forall (t :: PType).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
pshow' :: forall (s :: S). Bool -> Term s PB -> Term s PString
$cpshow' :: forall (s :: S). Bool -> Term s PB -> Term s PString
PShow, forall (s :: S). Term s (PB :--> PB)
forall (s :: S). Integer -> Term s PB
forall (s :: S). Term s PB -> Term s PB -> Term s PB
forall (a :: PType).
(forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Integer -> Term s a)
-> PNum a
pfromInteger :: forall (s :: S). Integer -> Term s PB
$cpfromInteger :: forall (s :: S). Integer -> Term s PB
psignum :: forall (s :: S). Term s (PB :--> PB)
$cpsignum :: forall (s :: S). Term s (PB :--> PB)
pabs :: forall (s :: S). Term s (PB :--> PB)
$cpabs :: forall (s :: S). Term s (PB :--> PB)
pnegate :: forall (s :: S). Term s (PB :--> PB)
$cpnegate :: forall (s :: S). Term s (PB :--> PB)
#* :: forall (s :: S). Term s PB -> Term s PB -> Term s PB
$c#* :: forall (s :: S). Term s PB -> Term s PB -> Term s PB
#- :: forall (s :: S). Term s PB -> Term s PB -> Term s PB
$c#- :: forall (s :: S). Term s PB -> Term s PB -> Term s PB
#+ :: forall (s :: S). Term s PB -> Term s PB -> Term s PB
$c#+ :: forall (s :: S). Term s PB -> Term s PB -> Term s PB
PNum)

-- | @since 2.0.0
instance DerivePlutusType PB where type DPTStrat _ = PlutusTypeNewtype

-- | @since 2.0.0
instance PUnsafeLiftDecl PB where type PLifted PB = B

-- | @since 2.0.0
deriving via
  (DerivePConstantViaNewtype B PB PInteger)
  instance
    PConstantDecl B

-- | @since 2.0.0
instance PArbitrary PB where
  parbitrary :: Gen (TestableTerm PB)
parbitrary = do
    (TestableTerm forall (s :: S). Term s PInteger
x) <- forall (a :: PType). PArbitrary a => Gen (TestableTerm a)
parbitrary
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PB s
PB forall (s :: S). Term s PInteger
x

  pshrink :: TestableTerm PB -> [TestableTerm PB]
pshrink (TestableTerm forall (s :: S). Term s PB
x) =
    let f :: TestableTerm PInteger -> TestableTerm PB
f (TestableTerm forall (s :: S). Term s PInteger
y) = forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PB s
PB forall (s :: S). Term s PInteger
y
     in TestableTerm PInteger -> TestableTerm PB
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => a -> [a]
shrink (forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (s :: S). Term s PB
x)

-- | @since 2.0.0
instance PCoArbitrary PB where
  pcoarbitrary :: forall b. TestableTerm PB -> Gen b -> Gen b
pcoarbitrary (TestableTerm forall (s :: S). Term s PB
x) = forall (a :: PType) b.
PCoArbitrary a =>
TestableTerm a -> Gen b -> Gen b
pcoarbitrary forall a b. (a -> b) -> a -> b
$ forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (s :: S). Term s PB
x

{- | Same as `PA`.

 @since 2.0.0
-}
newtype PC (s :: S)
  = PC (Term s PInteger)
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x. Rep (PC s) x -> PC s
forall (s :: S) x. PC s -> Rep (PC s) x
$cto :: forall (s :: S) x. Rep (PC s) x -> PC s
$cfrom :: forall (s :: S) x. PC s -> Rep (PC s) x
Generic)
  deriving anyclass (forall (s :: S). PC s -> Term s (PInner PC)
forall (s :: S) (b :: PType).
Term s (PInner PC) -> (PC s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PC) -> (PC s -> Term s b) -> Term s b
$cpmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PC) -> (PC s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PC s -> Term s (PInner PC)
$cpcon' :: forall (s :: S). PC s -> Term s (PInner PC)
PlutusType, forall (s :: S). Term s (PAsData PC) -> Term s PC
forall (s :: S). Term s PC -> Term s PData
forall (a :: PType).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
pdataImpl :: forall (s :: S). Term s PC -> Term s PData
$cpdataImpl :: forall (s :: S). Term s PC -> Term s PData
pfromDataImpl :: forall (s :: S). Term s (PAsData PC) -> Term s PC
$cpfromDataImpl :: forall (s :: S). Term s (PAsData PC) -> Term s PC
PIsData, forall (s :: S). Term s PC -> Term s PC -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
#== :: forall (s :: S). Term s PC -> Term s PC -> Term s PBool
$c#== :: forall (s :: S). Term s PC -> Term s PC -> Term s PBool
PEq, PEq PC
forall (s :: S). Term s PC -> Term s PC -> Term s PBool
forall (t :: PType).
PEq t
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> PPartialOrd t
#< :: forall (s :: S). Term s PC -> Term s PC -> Term s PBool
$c#< :: forall (s :: S). Term s PC -> Term s PC -> Term s PBool
#<= :: forall (s :: S). Term s PC -> Term s PC -> Term s PBool
$c#<= :: forall (s :: S). Term s PC -> Term s PC -> Term s PBool
PPartialOrd, PPartialOrd PC
forall (t :: PType). PPartialOrd t -> POrd t
POrd, forall (s :: S). Bool -> Term s PC -> Term s PString
forall (t :: PType).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
pshow' :: forall (s :: S). Bool -> Term s PC -> Term s PString
$cpshow' :: forall (s :: S). Bool -> Term s PC -> Term s PString
PShow, forall (s :: S). Term s (PC :--> PC)
forall (s :: S). Integer -> Term s PC
forall (s :: S). Term s PC -> Term s PC -> Term s PC
forall (a :: PType).
(forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s a -> Term s a -> Term s a)
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a))
-> (forall (s :: S). Integer -> Term s a)
-> PNum a
pfromInteger :: forall (s :: S). Integer -> Term s PC
$cpfromInteger :: forall (s :: S). Integer -> Term s PC
psignum :: forall (s :: S). Term s (PC :--> PC)
$cpsignum :: forall (s :: S). Term s (PC :--> PC)
pabs :: forall (s :: S). Term s (PC :--> PC)
$cpabs :: forall (s :: S). Term s (PC :--> PC)
pnegate :: forall (s :: S). Term s (PC :--> PC)
$cpnegate :: forall (s :: S). Term s (PC :--> PC)
#* :: forall (s :: S). Term s PC -> Term s PC -> Term s PC
$c#* :: forall (s :: S). Term s PC -> Term s PC -> Term s PC
#- :: forall (s :: S). Term s PC -> Term s PC -> Term s PC
$c#- :: forall (s :: S). Term s PC -> Term s PC -> Term s PC
#+ :: forall (s :: S). Term s PC -> Term s PC -> Term s PC
$c#+ :: forall (s :: S). Term s PC -> Term s PC -> Term s PC
PNum)

-- | @since 2.0.0
instance DerivePlutusType PC where type DPTStrat _ = PlutusTypeNewtype

-- | @since 2.0.0
instance PUnsafeLiftDecl PC where type PLifted PC = C

-- | @since 2.0.0
deriving via
  (DerivePConstantViaNewtype C PC PInteger)
  instance
    PConstantDecl C

-- | @since 2.0.0
instance PArbitrary PC where
  parbitrary :: Gen (TestableTerm PC)
parbitrary = do
    (TestableTerm forall (s :: S). Term s PInteger
x) <- forall (a :: PType). PArbitrary a => Gen (TestableTerm a)
parbitrary
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PC s
PC forall (s :: S). Term s PInteger
x

  pshrink :: TestableTerm PC -> [TestableTerm PC]
pshrink (TestableTerm forall (s :: S). Term s PC
x) =
    let f :: TestableTerm PInteger -> TestableTerm PC
f (TestableTerm forall (s :: S). Term s PInteger
y) = forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PC s
PC forall (s :: S). Term s PInteger
y
     in TestableTerm PInteger -> TestableTerm PC
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => a -> [a]
shrink (forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (s :: S). Term s PC
x)

-- | @since 2.0.0
instance PCoArbitrary PC where
  pcoarbitrary :: forall b. TestableTerm PC -> Gen b -> Gen b
pcoarbitrary (TestableTerm forall (s :: S). Term s PC
x) = forall (a :: PType) b.
PCoArbitrary a =>
TestableTerm a -> Gen b -> Gen b
pcoarbitrary forall a b. (a -> b) -> a -> b
$ forall (a :: PType). (forall (s :: S). Term s a) -> TestableTerm a
TestableTerm forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (s :: S). Term s PC
x

{- | This shinker 'simplifies' the underlying Plutarch representation. When
     shrinking a list, this shinker is always preferable.

 @since 2.0.0
-}
shrinkPLift ::
  forall (a :: S -> Type).
  ( PLift a
  , Arbitrary (PLifted a)
  ) =>
  TestableTerm a ->
  [TestableTerm a]
shrinkPLift :: forall (a :: PType).
(PLift a, Arbitrary (PLifted a)) =>
TestableTerm a -> [TestableTerm a]
shrinkPLift = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {p :: PType} {h}.
(PLift p, PLifted p ~ h) =>
h -> TestableTerm p
pconstantT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Arbitrary a => a -> [a]
shrink forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {p :: PType} {h}.
(PLift p, PLifted p ~ h) =>
TestableTerm p -> h
pliftT

{- | This generator uses the `Arbitrary` instance of a Haskell representation to
     make a value and lift it into Plutarch.

 @since 2.0.0
-}
arbitraryPLift ::
  forall (a :: S -> Type).
  ( PLift a
  , Arbitrary (PLifted a)
  ) =>
  Gen (TestableTerm a)
arbitraryPLift :: forall (a :: PType).
(PLift a, Arbitrary (PLifted a)) =>
Gen (TestableTerm a)
arbitraryPLift = forall {p :: PType} {h}.
(PLift p, PLifted p ~ h) =>
h -> TestableTerm p
pconstantT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

-- Utilities
failWith :: String -> Property
failWith :: String -> Property
failWith String
err = forall prop. Testable prop => String -> prop -> Property
counterexample String
err forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
False

showLogs :: forall (a :: Type). (Show a) => [a] -> String
showLogs :: forall a. Show a => [a] -> String
showLogs = \case
  [] -> String
"No logs found. Did you forget to compile with tracing on?"
  [a]
logs -> forall a. Show a => a -> String
show [a]
logs