{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators    #-}

module Evaluation.Builtins.Common
    ( unsafeSplitStructuralOperational
    , evaluateCek
    , evaluateCekNoEmit
    , readKnownCek
    , typecheckAnd
    , typecheckEvaluateCek
    , typecheckEvaluateCekNoEmit
    , typecheckReadKnownCek
    , PlcTerm
    , UplcTerm
    , CekResult (..)
    , evalTerm
    , mkApp1
    , mkApp2
    , ok
    , fails
    , evalOkEq
    , integer
    , bytestring
    , zero
    , one
    , true
    , false
    , cekSuccessFalse
    , cekSuccessTrue
    )
where

import PlutusCore qualified as TPLC
import PlutusCore.Builtin
import PlutusCore.Compiler.Erase qualified as TPLC
import PlutusCore.Default
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.MkPlc (builtin, mkConstant, mkIterAppNoAnn)
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import PlutusCore.TypeCheck
import PlutusPrelude (def)

import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Evaluation.Machine.Cek

import Control.Monad.Except
import Data.Bifunctor
import Data.ByteString (ByteString)
import Data.Text (Text)

import Test.Tasty.QuickCheck (Property, property, (===))

-- | Type check and evaluate a term.
typecheckAnd
    :: ( MonadError (TPLC.Error uni fun ()) m, TPLC.Typecheckable uni fun, GEq uni
       , Closed uni, uni `Everywhere` ExMemoryUsage
       )
    => BuiltinSemanticsVariant fun
    -> (MachineParameters CekMachineCosts fun (CekValue uni fun ()) ->
            UPLC.Term Name uni fun () -> a)
    -> CostingPart uni fun -> TPLC.Term TyName Name uni fun () -> m a
typecheckAnd :: forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Closed uni, Everywhere uni ExMemoryUsage) =>
BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m a
typecheckAnd BuiltinSemanticsVariant fun
semvar MachineParameters CekMachineCosts fun (CekValue uni fun ())
-> Term Name uni fun () -> a
action CostingPart uni fun
costingPart Term TyName Name uni fun ()
term = QuoteT m a -> m a
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
TPLC.runQuoteT (QuoteT m a -> m a) -> QuoteT m a -> m a
forall a b. (a -> b) -> a -> b
$ do
    -- Here we don't use 'getDefTypeCheckConfig', to cover the absurd case where
    -- builtins can change their type according to their 'BuiltinSemanticsVariant'.
    TypeCheckConfig uni fun
tcConfig <- KindCheckConfig -> BuiltinTypes uni fun -> TypeCheckConfig uni fun
forall (uni :: * -> *) fun.
KindCheckConfig -> BuiltinTypes uni fun -> TypeCheckConfig uni fun
TypeCheckConfig KindCheckConfig
defKindCheckConfig (BuiltinTypes uni fun -> TypeCheckConfig uni fun)
-> QuoteT m (BuiltinTypes uni fun)
-> QuoteT m (TypeCheckConfig uni fun)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinSemanticsVariant fun
-> () -> QuoteT m (BuiltinTypes uni fun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
BuiltinSemanticsVariant fun -> ann -> m (BuiltinTypes uni fun)
builtinMeaningsToTypes BuiltinSemanticsVariant fun
semvar ()
    Normalized (Type TyName uni ())
_ <- TypeCheckConfig uni fun
-> Term TyName Name uni fun ()
-> QuoteT m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
TPLC.inferType TypeCheckConfig uni fun
tcConfig Term TyName Name uni fun ()
term
    a -> QuoteT m a
forall a. a -> QuoteT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> QuoteT m a)
-> (Term Name uni fun () -> a)
-> Term Name uni fun ()
-> QuoteT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineParameters CekMachineCosts fun (CekValue uni fun ())
-> Term Name uni fun () -> a
action MachineParameters CekMachineCosts fun (CekValue uni fun ())
runtime (Term Name uni fun () -> QuoteT m a)
-> Term Name uni fun () -> QuoteT m a
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun () -> Term Name uni fun ()
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
TPLC.eraseTerm Term TyName Name uni fun ()
term
    where
      runtime :: MachineParameters CekMachineCosts fun (CekValue uni fun ())
runtime = BuiltinSemanticsVariant fun
-> CostModel
     CekMachineCosts (CostingPart (UniOf (CekValue uni fun ())) fun)
-> MachineParameters CekMachineCosts fun (CekValue uni fun ())
forall (uni :: * -> *) fun builtincosts val machinecosts.
(CostingPart uni fun ~ builtincosts, HasMeaningIn uni val,
 ToBuiltinMeaning uni fun) =>
BuiltinSemanticsVariant fun
-> CostModel machinecosts builtincosts
-> MachineParameters machinecosts fun val
mkMachineParameters BuiltinSemanticsVariant fun
semvar (CostModel
   CekMachineCosts (CostingPart (UniOf (CekValue uni fun ())) fun)
 -> MachineParameters CekMachineCosts fun (CekValue uni fun ()))
-> CostModel
     CekMachineCosts (CostingPart (UniOf (CekValue uni fun ())) fun)
-> MachineParameters CekMachineCosts fun (CekValue uni fun ())
forall a b. (a -> b) -> a -> b
$
                -- FIXME: make sure we have the the correct cost model for the semantics variant.
                   CekMachineCosts
-> CostingPart (UniOf (CekValue uni fun ())) fun
-> CostModel
     CekMachineCosts (CostingPart (UniOf (CekValue uni fun ())) fun)
forall machinecosts builtincosts.
machinecosts -> builtincosts -> CostModel machinecosts builtincosts
CostModel CekMachineCosts
defaultCekMachineCostsForTesting CostingPart uni fun
CostingPart (UniOf (CekValue uni fun ())) fun
costingPart

-- | Type check and evaluate a term, logging enabled.
typecheckEvaluateCek
    :: ( MonadError (TPLC.Error uni fun ()) m, TPLC.Typecheckable uni fun, GEq uni
       , uni `Everywhere` ExMemoryUsage, PrettyUni uni, Pretty fun
       )
    => BuiltinSemanticsVariant fun
    -> CostingPart uni fun
    -> TPLC.Term TyName Name uni fun ()
    -> m (EvaluationResult (UPLC.Term Name uni fun ()), [Text])
typecheckEvaluateCek :: forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
typecheckEvaluateCek BuiltinSemanticsVariant fun
semvar =
    BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun ()
    -> (EvaluationResult (Term Name uni fun ()), [Text]))
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Closed uni, Everywhere uni ExMemoryUsage) =>
BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m a
typecheckAnd BuiltinSemanticsVariant fun
semvar ((MachineParameters CekMachineCosts fun (CekValue uni fun ())
  -> Term Name uni fun ()
  -> (EvaluationResult (Term Name uni fun ()), [Text]))
 -> CostingPart uni fun
 -> Term TyName Name uni fun ()
 -> m (EvaluationResult (Term Name uni fun ()), [Text]))
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun ()
    -> (EvaluationResult (Term Name uni fun ()), [Text]))
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
forall a b. (a -> b) -> a -> b
$ \MachineParameters CekMachineCosts fun (CekValue uni fun ())
params ->
        (Either
   (EvaluationException
      (MachineError fun) CekUserError (Term Name uni fun ()))
   (Term Name uni fun ())
 -> EvaluationResult (Term Name uni fun ()))
-> (Either
      (EvaluationException
         (MachineError fun) CekUserError (Term Name uni fun ()))
      (Term Name uni fun ()),
    [Text])
-> (EvaluationResult (Term Name uni fun ()), [Text])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Either
  (EvaluationException
     (MachineError fun) CekUserError (Term Name uni fun ()))
  (Term Name uni fun ())
-> EvaluationResult (Term Name uni fun ())
forall structural term operational a.
(PrettyPlc structural, PrettyPlc term, Typeable structural,
 Typeable term) =>
Either (EvaluationException structural operational term) a
-> EvaluationResult a
unsafeSplitStructuralOperational ((Either
    (EvaluationException
       (MachineError fun) CekUserError (Term Name uni fun ()))
    (Term Name uni fun ()),
  [Text])
 -> (EvaluationResult (Term Name uni fun ()), [Text]))
-> (Term Name uni fun ()
    -> (Either
          (EvaluationException
             (MachineError fun) CekUserError (Term Name uni fun ()))
          (Term Name uni fun ()),
        [Text]))
-> Term Name uni fun ()
-> (EvaluationResult (Term Name uni fun ()), [Text])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EmitterMode uni fun
-> MachineParameters CekMachineCosts fun (CekValue uni fun ())
-> Term Name uni fun ()
-> (Either
      (EvaluationException
         (MachineError fun) CekUserError (Term Name uni fun ()))
      (Term Name uni fun ()),
    [Text])
forall (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
EmitterMode uni fun
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    [Text])
evaluateCek EmitterMode uni fun
forall (uni :: * -> *) fun. EmitterMode uni fun
logEmitter MachineParameters CekMachineCosts fun (CekValue uni fun ())
params

-- | Type check and evaluate a term, logging disabled.
typecheckEvaluateCekNoEmit
    :: ( MonadError (TPLC.Error uni fun ()) m, TPLC.Typecheckable uni fun, GEq uni
       , uni `Everywhere` ExMemoryUsage, PrettyUni uni, Pretty fun
       )
    => BuiltinSemanticsVariant fun
    -> CostingPart uni fun
    -> TPLC.Term TyName Name uni fun ()
    -> m (EvaluationResult (UPLC.Term Name uni fun ()))
typecheckEvaluateCekNoEmit :: forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()))
typecheckEvaluateCekNoEmit BuiltinSemanticsVariant fun
semvar =
    BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> EvaluationResult (Term Name uni fun ()))
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()))
forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Closed uni, Everywhere uni ExMemoryUsage) =>
BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m a
typecheckAnd BuiltinSemanticsVariant fun
semvar ((MachineParameters CekMachineCosts fun (CekValue uni fun ())
  -> Term Name uni fun () -> EvaluationResult (Term Name uni fun ()))
 -> CostingPart uni fun
 -> Term TyName Name uni fun ()
 -> m (EvaluationResult (Term Name uni fun ())))
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> EvaluationResult (Term Name uni fun ()))
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()))
forall a b. (a -> b) -> a -> b
$ \MachineParameters CekMachineCosts fun (CekValue uni fun ())
params ->
        Either
  (EvaluationException
     (MachineError fun) CekUserError (Term Name uni fun ()))
  (Term Name uni fun ())
-> EvaluationResult (Term Name uni fun ())
forall structural term operational a.
(PrettyPlc structural, PrettyPlc term, Typeable structural,
 Typeable term) =>
Either (EvaluationException structural operational term) a
-> EvaluationResult a
unsafeSplitStructuralOperational (Either
   (EvaluationException
      (MachineError fun) CekUserError (Term Name uni fun ()))
   (Term Name uni fun ())
 -> EvaluationResult (Term Name uni fun ()))
-> (Term Name uni fun ()
    -> Either
         (EvaluationException
            (MachineError fun) CekUserError (Term Name uni fun ()))
         (Term Name uni fun ()))
-> Term Name uni fun ()
-> EvaluationResult (Term Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineParameters CekMachineCosts fun (CekValue uni fun ())
-> Term Name uni fun ()
-> Either
     (EvaluationException
        (MachineError fun) CekUserError (Term Name uni fun ()))
     (Term Name uni fun ())
forall (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
evaluateCekNoEmit MachineParameters CekMachineCosts fun (CekValue uni fun ())
params

-- | Type check and convert a Plutus Core term to a Haskell value.
typecheckReadKnownCek
    :: ( MonadError (TPLC.Error uni fun ()) m, TPLC.Typecheckable uni fun, GEq uni
       , uni `Everywhere` ExMemoryUsage, PrettyUni uni, Pretty fun
       , ReadKnown (UPLC.Term Name uni fun ()) a
       )
    => BuiltinSemanticsVariant fun
    -> CostingPart uni fun
    -> TPLC.Term TyName Name uni fun ()
    -> m (Either (CekEvaluationException Name uni fun) a)
typecheckReadKnownCek :: forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun,
 ReadKnown (Term Name uni fun ()) a) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (Either (CekEvaluationException Name uni fun) a)
typecheckReadKnownCek BuiltinSemanticsVariant fun
semvar =
    BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun ()
    -> Either (CekEvaluationException Name uni fun) a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (Either (CekEvaluationException Name uni fun) a)
forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Closed uni, Everywhere uni ExMemoryUsage) =>
BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m a
typecheckAnd BuiltinSemanticsVariant fun
semvar MachineParameters CekMachineCosts fun (CekValue uni fun ())
-> Term Name uni fun ()
-> Either (CekEvaluationException Name uni fun) a
forall (uni :: * -> *) fun a ann.
(ThrowableBuiltins uni fun, ReadKnown (Term Name uni fun ()) a) =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either (CekEvaluationException Name uni fun) a
readKnownCek


-- TPLC/UPLC utilities

type PlcTerm  = TPLC.Term TPLC.TyName TPLC.Name TPLC.DefaultUni TPLC.DefaultFun ()
type PlcError = TPLC.Error TPLC.DefaultUni TPLC.DefaultFun ()
type UplcTerm = UPLC.Term TPLC.Name TPLC.DefaultUni TPLC.DefaultFun ()

-- Possible CEK evluation results, flattened out
data CekResult =
    TypeCheckError PlcError
  | CekError
  | CekSuccess UplcTerm
    deriving stock (CekResult -> CekResult -> Bool
(CekResult -> CekResult -> Bool)
-> (CekResult -> CekResult -> Bool) -> Eq CekResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CekResult -> CekResult -> Bool
== :: CekResult -> CekResult -> Bool
$c/= :: CekResult -> CekResult -> Bool
/= :: CekResult -> CekResult -> Bool
Eq, Int -> CekResult -> ShowS
[CekResult] -> ShowS
CekResult -> String
(Int -> CekResult -> ShowS)
-> (CekResult -> String)
-> ([CekResult] -> ShowS)
-> Show CekResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CekResult -> ShowS
showsPrec :: Int -> CekResult -> ShowS
$cshow :: CekResult -> String
show :: CekResult -> String
$cshowList :: [CekResult] -> ShowS
showList :: [CekResult] -> ShowS
Show)

evalTerm :: PlcTerm -> CekResult
evalTerm :: PlcTerm -> CekResult
evalTerm PlcTerm
term =
    case BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> PlcTerm
-> Either
     (Error DefaultUni DefaultFun ()) (EvaluationResult UplcTerm)
forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()))
typecheckEvaluateCekNoEmit BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def BuiltinCostModel
CostingPart DefaultUni DefaultFun
defaultBuiltinCostModelForTesting PlcTerm
term
    of Left Error DefaultUni DefaultFun ()
e -> Error DefaultUni DefaultFun () -> CekResult
TypeCheckError Error DefaultUni DefaultFun ()
e
       Right EvaluationResult UplcTerm
x  ->
           case EvaluationResult UplcTerm
x of
             EvaluationResult UplcTerm
TPLC.EvaluationFailure   -> CekResult
CekError
             TPLC.EvaluationSuccess UplcTerm
s -> UplcTerm -> CekResult
CekSuccess UplcTerm
s

integer :: Integer -> PlcTerm
integer :: Integer -> PlcTerm
integer = () -> Integer -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant ()

zero :: PlcTerm
zero :: PlcTerm
zero = Integer -> PlcTerm
integer Integer
0

one :: PlcTerm
one :: PlcTerm
one = Integer -> PlcTerm
integer Integer
1

bytestring :: ByteString -> PlcTerm
bytestring :: ByteString -> PlcTerm
bytestring = () -> ByteString -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant ()

true :: PlcTerm
true :: PlcTerm
true = () -> Bool -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Bool
True

false :: PlcTerm
false :: PlcTerm
false = () -> Bool -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Bool
False

cekSuccessFalse :: CekResult
cekSuccessFalse :: CekResult
cekSuccessFalse = UplcTerm -> CekResult
CekSuccess (UplcTerm -> CekResult) -> UplcTerm -> CekResult
forall a b. (a -> b) -> a -> b
$ () -> Bool -> UplcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Bool
False

cekSuccessTrue :: CekResult
cekSuccessTrue :: CekResult
cekSuccessTrue = UplcTerm -> CekResult
CekSuccess (UplcTerm -> CekResult) -> UplcTerm -> CekResult
forall a b. (a -> b) -> a -> b
$ () -> Bool -> UplcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Bool
True

mkApp1 :: TPLC.DefaultFun -> PlcTerm -> PlcTerm
mkApp1 :: DefaultFun -> PlcTerm -> PlcTerm
mkApp1 DefaultFun
b PlcTerm
x = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
b) [PlcTerm
x]

mkApp2 :: TPLC.DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 :: DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
b PlcTerm
x PlcTerm
y = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
b) [PlcTerm
x,PlcTerm
y]

-- QuickCheck utilities

-- | Term evaluates successfully
ok :: PlcTerm -> Property
ok :: PlcTerm -> Property
ok PlcTerm
t = Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
       case PlcTerm -> CekResult
evalTerm PlcTerm
t of
         CekSuccess UplcTerm
_ -> Bool
True
         CekResult
_            -> Bool
False

-- | Term fails to evaluate successfully
fails :: PlcTerm -> Property
fails :: PlcTerm -> Property
fails PlcTerm
t = PlcTerm -> CekResult
evalTerm PlcTerm
t CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
CekError

-- Check that two terms evaluate successfully and return the same result
evalOkEq :: PlcTerm -> PlcTerm -> Property
evalOkEq :: PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2 =
    case PlcTerm -> CekResult
evalTerm PlcTerm
t1 of
      r :: CekResult
r@(CekSuccess UplcTerm
_) -> CekResult
r CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== PlcTerm -> CekResult
evalTerm PlcTerm
t2
      CekResult
_                -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False