-- editorconfig-checker-disable-file
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies     #-}
{-# LANGUAGE TypeOperators    #-}

module Evaluation.Machines
    ( test_machines
    , test_budget
    , test_tallying
    , test_NumberOfStepCounters
    ) where

import PlutusPrelude

import UntypedPlutusCore
import UntypedPlutusCore.Evaluation.Machine.Cek as Cek
import UntypedPlutusCore.Evaluation.Machine.Cek.Internal (NumberOfStepCounters)
import UntypedPlutusCore.Evaluation.Machine.SteppableCek qualified as SCek

import PlutusCore qualified as Plc
import PlutusCore.Builtin
import PlutusCore.Compiler.Erase
import PlutusCore.Default
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as Plc
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.FsTree
import PlutusCore.Generators.Hedgehog.Interesting
import PlutusCore.MkPlc
import PlutusCore.Pretty

import PlutusCore.Examples.Builtins
import PlutusCore.StdLib.Data.Nat qualified as Plc
import PlutusCore.StdLib.Meta
import PlutusCore.StdLib.Meta.Data.Function (etaExpand)

import Data.Proxy (Proxy (..))
import GHC.Exts (fromString)
import GHC.Ix
import GHC.TypeNats (natVal)
import Hedgehog hiding (Size, Var, eval)
import Test.Tasty
import Test.Tasty.Extras
import Test.Tasty.Golden
import Test.Tasty.Hedgehog

testMachine
    :: (uni ~ DefaultUni, fun ~ DefaultFun, PrettyPlc structural)
    => String
    -> (Term Name uni fun () ->
           Either
               (EvaluationException structural operational (Term Name uni fun ()))
               (Term Name uni fun ()))
    -> TestTree
testMachine :: forall (uni :: * -> *) fun structural operational.
(uni ~ DefaultUni, fun ~ DefaultFun, PrettyPlc structural) =>
String
-> (Term Name uni fun ()
    -> Either
         (EvaluationException structural operational (Term Name uni fun ()))
         (Term Name uni fun ()))
-> TestTree
testMachine String
machine Term Name uni fun ()
-> Either
     (EvaluationException structural operational (Term Name uni fun ()))
     (Term Name uni fun ())
eval =
    String -> [TestTree] -> TestTree
testGroup String
machine ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall a.
 KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
 String -> TermGen a -> TestTree)
-> [TestTree]
forall c.
(forall a.
 KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
 String -> TermGen a -> c)
-> [c]
fromInterestingTermGens ((forall a.
  KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
  String -> TermGen a -> TestTree)
 -> [TestTree])
-> (forall a.
    KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
    String -> TermGen a -> TestTree)
-> [TestTree]
forall a b. (a -> b) -> a -> b
$ \String
name TermGen a
genTermOfTbv ->
        String -> PropertyName -> Property -> TestTree
testPropertyNamed String
name (String -> PropertyName
forall a. IsString a => String -> a
fromString String
name) (Property -> TestTree)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestLimit -> Property -> Property
withTests TestLimit
99 (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> TestTree) -> PropertyT IO () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
            TermOf Term TyName Name DefaultUni DefaultFun ()
term a
val <- (TermOf (Term TyName Name DefaultUni DefaultFun ()) a -> String)
-> TermGen a
-> PropertyT
     IO (TermOf (Term TyName Name DefaultUni DefaultFun ()) a)
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith TermOf (Term TyName Name DefaultUni DefaultFun ()) a -> String
forall a. Monoid a => a
mempty TermGen a
genTermOfTbv
            let resExp :: EvaluationResult
  (HeadSpine (Term TyName Name DefaultUni DefaultFun ()))
resExp = forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> EvaluationResult (HeadSpine val)
makeKnownOrFail @_ @(Plc.Term TyName Name DefaultUni DefaultFun ()) a
val
            case Either
  (EvaluationException structural operational (Term Name uni fun ()))
  (Term Name uni fun ())
-> Either
     (ErrorWithCause structural (Term Name uni fun ()))
     (EvaluationResult (Term Name uni fun ()))
forall structural operational term a.
Either (EvaluationException structural operational term) a
-> Either (ErrorWithCause structural term) (EvaluationResult a)
splitStructuralOperational (Either
   (EvaluationException structural operational (Term Name uni fun ()))
   (Term Name uni fun ())
 -> Either
      (ErrorWithCause structural (Term Name uni fun ()))
      (EvaluationResult (Term Name uni fun ())))
-> (Term Name uni fun ()
    -> Either
         (EvaluationException structural operational (Term Name uni fun ()))
         (Term Name uni fun ()))
-> Term Name uni fun ()
-> Either
     (ErrorWithCause structural (Term Name uni fun ()))
     (EvaluationResult (Term Name uni fun ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term Name uni fun ()
-> Either
     (EvaluationException structural operational (Term Name uni fun ()))
     (Term Name uni fun ())
eval (Term Name uni fun ()
 -> Either
      (ErrorWithCause structural (Term Name uni fun ()))
      (EvaluationResult (Term Name uni fun ())))
-> Term Name uni fun ()
-> Either
     (ErrorWithCause structural (Term Name uni fun ()))
     (EvaluationResult (Term Name uni fun ()))
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
eraseTerm Term TyName Name uni fun ()
Term TyName Name DefaultUni DefaultFun ()
term of
                Left ErrorWithCause structural (Term Name uni fun ())
err     -> String -> PropertyT IO ()
forall a. String -> PropertyT IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ ErrorWithCause structural (Term Name uni fun ()) -> String
forall a. Show a => a -> String
show ErrorWithCause structural (Term Name uni fun ())
err
                Right EvaluationResult (Term Name uni fun ())
resAct -> (Term Name uni fun () -> HeadSpine (Term Name uni fun ()))
-> EvaluationResult (Term Name uni fun ())
-> EvaluationResult (HeadSpine (Term Name uni fun ()))
forall a b. (a -> b) -> EvaluationResult a -> EvaluationResult b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term Name uni fun () -> HeadSpine (Term Name uni fun ())
forall a. a -> HeadSpine a
HeadOnly EvaluationResult (Term Name uni fun ())
resAct EvaluationResult (HeadSpine (Term Name uni fun ()))
-> EvaluationResult (HeadSpine (Term Name uni fun ()))
-> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== (HeadSpine (Term TyName Name uni fun ())
 -> HeadSpine (Term Name uni fun ()))
-> EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> EvaluationResult (HeadSpine (Term Name uni fun ()))
forall a b. (a -> b) -> EvaluationResult a -> EvaluationResult b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term TyName Name uni fun () -> Term Name uni fun ())
-> HeadSpine (Term TyName Name uni fun ())
-> HeadSpine (Term Name uni fun ())
forall a b. (a -> b) -> HeadSpine a -> HeadSpine b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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
eraseTerm) EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
EvaluationResult
  (HeadSpine (Term TyName Name DefaultUni DefaultFun ()))
resExp

test_machines :: TestTree
test_machines :: TestTree
test_machines =
    String -> [TestTree] -> TestTree
testGroup String
"machines"
        [ String
-> (Term Name DefaultUni DefaultFun ()
    -> Either
         (CekEvaluationException Name DefaultUni DefaultFun)
         (Term Name DefaultUni DefaultFun ()))
-> TestTree
forall (uni :: * -> *) fun structural operational.
(uni ~ DefaultUni, fun ~ DefaultFun, PrettyPlc structural) =>
String
-> (Term Name uni fun ()
    -> Either
         (EvaluationException structural operational (Term Name uni fun ()))
         (Term Name uni fun ()))
-> TestTree
testMachine String
"CEK" ((Term Name DefaultUni DefaultFun ()
  -> Either
       (CekEvaluationException Name DefaultUni DefaultFun)
       (Term Name DefaultUni DefaultFun ()))
 -> TestTree)
-> (Term Name DefaultUni DefaultFun ()
    -> Either
         (CekEvaluationException Name DefaultUni DefaultFun)
         (Term Name DefaultUni DefaultFun ()))
-> TestTree
forall a b. (a -> b) -> a -> b
$ MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException Name DefaultUni DefaultFun)
     (Term Name DefaultUni DefaultFun ())
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 ())
Cek.evaluateCekNoEmit MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
forall ann.
Typeable ann =>
MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
Plc.defaultCekParametersForTesting
        , String
-> (Term Name DefaultUni DefaultFun ()
    -> Either
         (CekEvaluationException Name DefaultUni DefaultFun)
         (Term Name DefaultUni DefaultFun ()))
-> TestTree
forall (uni :: * -> *) fun structural operational.
(uni ~ DefaultUni, fun ~ DefaultFun, PrettyPlc structural) =>
String
-> (Term Name uni fun ()
    -> Either
         (EvaluationException structural operational (Term Name uni fun ()))
         (Term Name uni fun ()))
-> TestTree
testMachine String
"SteppableCEK" ((Term Name DefaultUni DefaultFun ()
  -> Either
       (CekEvaluationException Name DefaultUni DefaultFun)
       (Term Name DefaultUni DefaultFun ()))
 -> TestTree)
-> (Term Name DefaultUni DefaultFun ()
    -> Either
         (CekEvaluationException Name DefaultUni DefaultFun)
         (Term Name DefaultUni DefaultFun ()))
-> TestTree
forall a b. (a -> b) -> a -> b
$ MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException Name DefaultUni DefaultFun)
     (Term Name DefaultUni DefaultFun ())
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 ())
SCek.evaluateCekNoEmit MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
forall ann.
Typeable ann =>
MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
Plc.defaultCekParametersForTesting
        ]

testBudget
    :: (Ix fun, Show fun, Hashable fun, Pretty fun, Typeable fun)
    => BuiltinsRuntime fun (CekValue DefaultUni fun ())
    -> TestName
    -> Term Name DefaultUni fun ()
    -> TestNested
testBudget :: forall fun.
(Ix fun, Show fun, Hashable fun, Pretty fun, Typeable fun) =>
BuiltinsRuntime fun (CekValue DefaultUni fun ())
-> String -> Term Name DefaultUni fun () -> TestNested
testBudget BuiltinsRuntime fun (CekValue DefaultUni fun ())
runtime String
name Term Name DefaultUni fun ()
term =
                       String -> String -> Text -> TestNested
nestedGoldenVsText
    String
name
    String
".uplc"
    (Doc Any -> Text
forall ann. Doc ann -> Text
forall str ann. Render str => Doc ann -> str
render
      (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ (Either
   (CekEvaluationException Name DefaultUni fun)
   (Term Name DefaultUni fun ()),
 TallyingSt fun)
-> Doc Any
forall a ann. PrettyPlc a => a -> Doc ann
prettyPlcReadable
      ((Either
    (CekEvaluationException Name DefaultUni fun)
    (Term Name DefaultUni fun ()),
  TallyingSt fun)
 -> Doc Any)
-> (Either
      (CekEvaluationException Name DefaultUni fun)
      (Term Name DefaultUni fun ()),
    TallyingSt fun)
-> Doc Any
forall a b. (a -> b) -> a -> b
$ MachineParameters CekMachineCosts fun (CekValue DefaultUni fun ())
-> ExBudgetMode (TallyingSt fun) DefaultUni fun
-> Term Name DefaultUni fun ()
-> (Either
      (CekEvaluationException Name DefaultUni fun)
      (Term Name DefaultUni fun ()),
    TallyingSt fun)
forall (uni :: * -> *) fun ann cost.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
runCekNoEmit
        (CekMachineCosts
-> BuiltinsRuntime fun (CekValue DefaultUni fun ())
-> MachineParameters
     CekMachineCosts fun (CekValue DefaultUni fun ())
forall machinecosts fun val.
machinecosts
-> BuiltinsRuntime fun val
-> MachineParameters machinecosts fun val
MachineParameters CekMachineCosts
Plc.defaultCekMachineCostsForTesting BuiltinsRuntime fun (CekValue DefaultUni fun ())
runtime)
        ExBudgetMode (TallyingSt fun) DefaultUni fun
forall fun (uni :: * -> *).
Hashable fun =>
ExBudgetMode (TallyingSt fun) uni fun
Cek.tallying Term Name DefaultUni fun ()
term)

bunchOfFibs :: PlcFolderContents DefaultUni DefaultFun
bunchOfFibs :: PlcFolderContents DefaultUni DefaultFun
bunchOfFibs = [FsTree (PlcEntity DefaultUni DefaultFun)]
-> PlcFolderContents DefaultUni DefaultFun
forall a. [FsTree a] -> FolderContents a
FolderContents [String
-> [FsTree (PlcEntity DefaultUni DefaultFun)]
-> FsTree (PlcEntity DefaultUni DefaultFun)
forall a. String -> [FsTree a] -> FsTree a
treeFolderContents String
"Fib" ([FsTree (PlcEntity DefaultUni DefaultFun)]
 -> FsTree (PlcEntity DefaultUni DefaultFun))
-> [FsTree (PlcEntity DefaultUni DefaultFun)]
-> FsTree (PlcEntity DefaultUni DefaultFun)
forall a b. (a -> b) -> a -> b
$ (Integer -> FsTree (PlcEntity DefaultUni DefaultFun))
-> [Integer] -> [FsTree (PlcEntity DefaultUni DefaultFun)]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> FsTree (PlcEntity DefaultUni DefaultFun)
fibFile [Integer
1..Integer
3]] where
    fibFile :: Integer -> FsTree (PlcEntity DefaultUni DefaultFun)
fibFile Integer
i = String
-> Term TyName Name DefaultUni DefaultFun ()
-> FsTree (PlcEntity DefaultUni DefaultFun)
forall (uni :: * -> *) fun.
String -> Term TyName Name uni fun () -> PlcFsTree uni fun
plcTermFile (Integer -> String
forall a. Show a => a -> String
show Integer
i) (Integer -> Term TyName Name DefaultUni DefaultFun ()
naiveFib Integer
i)

-- | To check how a sequence of calls to a built-in @id@ affects budgeting when a (relatively)
-- big AST is threaded through them.
bunchOfIdNats :: PlcFolderContents DefaultUni ExtensionFun
bunchOfIdNats :: PlcFolderContents DefaultUni ExtensionFun
bunchOfIdNats =
    [FsTree (PlcEntity DefaultUni ExtensionFun)]
-> PlcFolderContents DefaultUni ExtensionFun
forall a. [FsTree a] -> FolderContents a
FolderContents [String
-> [FsTree (PlcEntity DefaultUni ExtensionFun)]
-> FsTree (PlcEntity DefaultUni ExtensionFun)
forall a. String -> [FsTree a] -> FsTree a
treeFolderContents String
"IdNat" ([FsTree (PlcEntity DefaultUni ExtensionFun)]
 -> FsTree (PlcEntity DefaultUni ExtensionFun))
-> [FsTree (PlcEntity DefaultUni ExtensionFun)]
-> FsTree (PlcEntity DefaultUni ExtensionFun)
forall a b. (a -> b) -> a -> b
$ (Int -> FsTree (PlcEntity DefaultUni ExtensionFun))
-> [Int] -> [FsTree (PlcEntity DefaultUni ExtensionFun)]
forall a b. (a -> b) -> [a] -> [b]
map Int -> FsTree (PlcEntity DefaultUni ExtensionFun)
idNatFile [Int
0 :: Int, Int
3.. Int
9]] where
        idNatFile :: Int -> FsTree (PlcEntity DefaultUni ExtensionFun)
idNatFile Int
i = String
-> Term TyName Name DefaultUni ExtensionFun ()
-> FsTree (PlcEntity DefaultUni ExtensionFun)
forall (uni :: * -> *) fun.
String -> Term TyName Name uni fun () -> PlcFsTree uni fun
plcTermFile (Int -> String
forall a. Show a => a -> String
show Int
i) (Term TyName Name DefaultUni ExtensionFun ()
-> Int -> Term TyName Name DefaultUni ExtensionFun ()
forall {t} {term :: * -> *} {uni :: * -> *}.
(Num t, Eq t, TermLike term TyName Name uni ExtensionFun) =>
term () -> t -> term ()
idNat Term TyName Name DefaultUni ExtensionFun ()
id0 Int
i)
        -- > id0 = foldNat {nat} succ zero
        id0 :: Term TyName Name DefaultUni ExtensionFun ()
id0 = Term TyName Name DefaultUni ExtensionFun ()
-> [Term TyName Name DefaultUni ExtensionFun ()]
-> Term TyName Name DefaultUni ExtensionFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Term TyName Name DefaultUni ExtensionFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni ExtensionFun ()
forall ann.
ann
-> Term TyName Name DefaultUni ExtensionFun ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni ExtensionFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () Term TyName Name DefaultUni ExtensionFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Plc.foldNat (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni ExtensionFun ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni ExtensionFun ()
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.natTy) [Term TyName Name DefaultUni ExtensionFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Plc.succ, Term TyName Name DefaultUni ExtensionFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Plc.zero]

        idNat :: term () -> t -> term ()
idNat term ()
idN t
0 = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () term ()
idN (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ Integer -> term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term ()
metaIntegerToNat Integer
10
        idNat term ()
idN t
n = term () -> t -> term ()
idNat term ()
idN' (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) where
            -- Intentionally not eta-expanding the call to @idN'@, so that it gets forced during
            -- evaluation, which causes @idN@ to get forced, which on the first iteration causes
            -- @id0@ to get forced, which gives us a sufficiently big AST.
            -- > idN' = id {nat -> nat} idN
            idN' :: term ()
idN' = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> ExtensionFun -> term ()
forall ann. ann -> ExtensionFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () ExtensionFun
Id) (Type TyName uni () -> term ()) -> Type TyName uni () -> term ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
Plc.TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.natTy Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.natTy) term ()
idN

-- | Same as 'bunchOfIdNats' except uses the built-in @ifThenElse@.
bunchOfIfThenElseNats :: PlcFolderContents DefaultUni DefaultFun
bunchOfIfThenElseNats :: PlcFolderContents DefaultUni DefaultFun
bunchOfIfThenElseNats =
    [FsTree (PlcEntity DefaultUni DefaultFun)]
-> PlcFolderContents DefaultUni DefaultFun
forall a. [FsTree a] -> FolderContents a
FolderContents [String
-> [FsTree (PlcEntity DefaultUni DefaultFun)]
-> FsTree (PlcEntity DefaultUni DefaultFun)
forall a. String -> [FsTree a] -> FsTree a
treeFolderContents String
"IfThenElse" ([FsTree (PlcEntity DefaultUni DefaultFun)]
 -> FsTree (PlcEntity DefaultUni DefaultFun))
-> [FsTree (PlcEntity DefaultUni DefaultFun)]
-> FsTree (PlcEntity DefaultUni DefaultFun)
forall a b. (a -> b) -> a -> b
$ (Int -> FsTree (PlcEntity DefaultUni DefaultFun))
-> [Int] -> [FsTree (PlcEntity DefaultUni DefaultFun)]
forall a b. (a -> b) -> [a] -> [b]
map Int -> FsTree (PlcEntity DefaultUni DefaultFun)
ifThenElseNatFile [Int
0 :: Int, Int
1.. Int
5]] where
        ifThenElseNatFile :: Int -> FsTree (PlcEntity DefaultUni DefaultFun)
ifThenElseNatFile Int
i = String
-> Term TyName Name DefaultUni DefaultFun ()
-> FsTree (PlcEntity DefaultUni DefaultFun)
forall (uni :: * -> *) fun.
String -> Term TyName Name uni fun () -> PlcFsTree uni fun
plcTermFile (Int -> String
forall a. Show a => a -> String
show Int
i) (Term TyName Name DefaultUni DefaultFun ()
-> Int -> Term TyName Name DefaultUni DefaultFun ()
forall {t} {term :: * -> *} {uni :: * -> *}.
(TermLike term TyName Name uni DefaultFun, Contains uni Bool,
 Integral t) =>
term () -> t -> term ()
ifThenElseNat Term TyName Name DefaultUni DefaultFun ()
id0 Int
i)
        -- > id0 = foldNat {nat} succ zero
        id0 :: Term TyName Name DefaultUni DefaultFun ()
id0 = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Plc.foldNat Type TyName DefaultUni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.natTy) [Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Plc.succ, Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Plc.zero]

        ifThenElseNat :: term () -> t -> term ()
ifThenElseNat term ()
idN t
0 = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () term ()
idN (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ Integer -> term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term ()
metaIntegerToNat Integer
10
        ifThenElseNat term ()
idN t
n = term () -> t -> term ()
ifThenElseNat term ()
idN' (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) where
            -- Eta-expanding @idN'@ so that all of the if-then-else-s don't get evaluated --
            -- only those that are on the actual execution path.
            -- > idN' = \(n : nat) -> ifThenElse {nat -> nat} ($(even n)) idN idN n
            idN' :: term ()
idN'

                = Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname (uni :: * -> *) fun.
TermLike term tyname Name uni fun =>
Type tyname uni () -> term () -> term ()
etaExpand Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.natTy
                (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
IfThenElse) (Type TyName uni () -> term ()) -> Type TyName uni () -> term ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
Plc.TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.natTy Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.natTy)
                    [() -> Bool -> term ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () (Bool -> term ()) -> Bool -> term ()
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. Integral a => a -> Bool
even t
n, term ()
idN, term ()
idN]

test_budget :: TestTree
test_budget :: TestTree
test_budget
    -- Error diffs are very big
    = SizeCutoff -> TestTree -> TestTree
forall v. IsOption v => v -> TestTree -> TestTree
localOption (Int64 -> SizeCutoff
SizeCutoff Int64
1000000)
    (TestTree -> TestTree)
-> ([TestNested] -> TestTree) -> [TestNested] -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [TestNested] -> TestTree
runTestNested [String
"untyped-plutus-core", String
"test", String
"Evaluation", String
"Machines", String
"Budget"]
    ([TestNested] -> TestTree) -> [TestNested] -> TestTree
forall a b. (a -> b) -> a -> b
$ [[TestNested]] -> [TestNested]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ BuiltinsRuntime DefaultFun (CekValue DefaultUni DefaultFun ())
-> PlcFolderContents DefaultUni DefaultFun -> [TestNested]
forall {fun}.
(Ix fun, Show fun, Hashable fun, Pretty fun, Typeable fun) =>
BuiltinsRuntime fun (CekValue DefaultUni fun ())
-> PlcFolderContents DefaultUni fun -> [TestNested]
folder BuiltinsRuntime DefaultFun (CekValue DefaultUni DefaultFun ())
forall term.
HasMeaningIn DefaultUni term =>
BuiltinsRuntime DefaultFun term
Plc.defaultBuiltinsRuntimeForTesting PlcFolderContents DefaultUni DefaultFun
bunchOfFibs
        , BuiltinsRuntime ExtensionFun (CekValue DefaultUni ExtensionFun ())
-> PlcFolderContents DefaultUni ExtensionFun -> [TestNested]
forall {fun}.
(Ix fun, Show fun, Hashable fun, Pretty fun, Typeable fun) =>
BuiltinsRuntime fun (CekValue DefaultUni fun ())
-> PlcFolderContents DefaultUni fun -> [TestNested]
folder (BuiltinSemanticsVariant ExtensionFun
-> ()
-> BuiltinsRuntime
     ExtensionFun (CekValue DefaultUni ExtensionFun ())
forall cost (uni :: * -> *) fun val.
(cost ~ CostingPart uni fun, ToBuiltinMeaning uni fun,
 HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun -> cost -> BuiltinsRuntime fun val
toBuiltinsRuntime BuiltinSemanticsVariant ExtensionFun
forall a. Default a => a
def ()) PlcFolderContents DefaultUni ExtensionFun
bunchOfIdNats
        , BuiltinsRuntime DefaultFun (CekValue DefaultUni DefaultFun ())
-> PlcFolderContents DefaultUni DefaultFun -> [TestNested]
forall {fun}.
(Ix fun, Show fun, Hashable fun, Pretty fun, Typeable fun) =>
BuiltinsRuntime fun (CekValue DefaultUni fun ())
-> PlcFolderContents DefaultUni fun -> [TestNested]
folder BuiltinsRuntime DefaultFun (CekValue DefaultUni DefaultFun ())
forall term.
HasMeaningIn DefaultUni term =>
BuiltinsRuntime DefaultFun term
Plc.defaultBuiltinsRuntimeForTesting PlcFolderContents DefaultUni DefaultFun
bunchOfIfThenElseNats
        ]
  where
    folder :: BuiltinsRuntime fun (CekValue DefaultUni fun ())
-> PlcFolderContents DefaultUni fun -> [TestNested]
folder BuiltinsRuntime fun (CekValue DefaultUni fun ())
runtime =
        (String -> [TestNested] -> TestNested)
-> (String -> Type TyName DefaultUni () -> TestNested)
-> (String -> Term TyName Name DefaultUni fun () -> TestNested)
-> PlcFolderContents DefaultUni fun
-> [TestNested]
forall b (uni :: * -> *) fun.
(String -> [b] -> b)
-> (String -> Type TyName uni () -> b)
-> (String -> Term TyName Name uni fun () -> b)
-> PlcFolderContents uni fun
-> [b]
foldPlcFolderContents String -> [TestNested] -> TestNested
testNested String -> Type TyName DefaultUni () -> TestNested
forall a. Monoid a => a
mempty (\String
name -> BuiltinsRuntime fun (CekValue DefaultUni fun ())
-> String -> Term Name DefaultUni fun () -> TestNested
forall fun.
(Ix fun, Show fun, Hashable fun, Pretty fun, Typeable fun) =>
BuiltinsRuntime fun (CekValue DefaultUni fun ())
-> String -> Term Name DefaultUni fun () -> TestNested
testBudget BuiltinsRuntime fun (CekValue DefaultUni fun ())
runtime String
name (Term Name DefaultUni fun () -> TestNested)
-> (Term TyName Name DefaultUni fun ()
    -> Term Name DefaultUni fun ())
-> Term TyName Name DefaultUni fun ()
-> TestNested
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm)

testTallying :: TestName -> Term Name DefaultUni DefaultFun () -> TestNested
testTallying :: String -> Term Name DefaultUni DefaultFun () -> TestNested
testTallying String
name Term Name DefaultUni DefaultFun ()
term =
                       String -> String -> Text -> TestNested
nestedGoldenVsText
    String
name
    String
".uplc"
    (Doc Any -> Text
forall ann. Doc ann -> Text
forall str ann. Render str => Doc ann -> str
render (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ (Either
   (CekEvaluationException Name DefaultUni DefaultFun)
   (Term Name DefaultUni DefaultFun ()),
 TallyingSt DefaultFun)
-> Doc Any
forall a ann. PrettyPlc a => a -> Doc ann
prettyPlcReadable ((Either
    (CekEvaluationException Name DefaultUni DefaultFun)
    (Term Name DefaultUni DefaultFun ()),
  TallyingSt DefaultFun)
 -> Doc Any)
-> (Either
      (CekEvaluationException Name DefaultUni DefaultFun)
      (Term Name DefaultUni DefaultFun ()),
    TallyingSt DefaultFun)
-> Doc Any
forall a b. (a -> b) -> a -> b
$ MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
-> ExBudgetMode (TallyingSt DefaultFun) DefaultUni DefaultFun
-> Term Name DefaultUni DefaultFun ()
-> (Either
      (CekEvaluationException Name DefaultUni DefaultFun)
      (Term Name DefaultUni DefaultFun ()),
    TallyingSt DefaultFun)
forall (uni :: * -> *) fun ann cost.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
runCekNoEmit MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
forall ann.
Typeable ann =>
MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
Plc.defaultCekParametersForTesting ExBudgetMode (TallyingSt DefaultFun) DefaultUni DefaultFun
forall fun (uni :: * -> *).
Hashable fun =>
ExBudgetMode (TallyingSt fun) uni fun
Cek.tallying Term Name DefaultUni DefaultFun ()
term)

test_tallying :: TestTree
test_tallying :: TestTree
test_tallying =
    -- Error diffs are very big
    SizeCutoff -> TestTree -> TestTree
forall v. IsOption v => v -> TestTree -> TestTree
localOption (Int64 -> SizeCutoff
SizeCutoff Int64
1000000)
        (TestTree -> TestTree)
-> (PlcFolderContents DefaultUni DefaultFun -> TestTree)
-> PlcFolderContents DefaultUni DefaultFun
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [TestNested] -> TestTree
runTestNested [String
"untyped-plutus-core", String
"test", String
"Evaluation", String
"Machines", String
"Tallying"]
        ([TestNested] -> TestTree)
-> (PlcFolderContents DefaultUni DefaultFun -> [TestNested])
-> PlcFolderContents DefaultUni DefaultFun
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [TestNested] -> TestNested)
-> (String -> Type TyName DefaultUni () -> TestNested)
-> (String
    -> Term TyName Name DefaultUni DefaultFun () -> TestNested)
-> PlcFolderContents DefaultUni DefaultFun
-> [TestNested]
forall b (uni :: * -> *) fun.
(String -> [b] -> b)
-> (String -> Type TyName uni () -> b)
-> (String -> Term TyName Name uni fun () -> b)
-> PlcFolderContents uni fun
-> [b]
foldPlcFolderContents String -> [TestNested] -> TestNested
testNested String -> Type TyName DefaultUni () -> TestNested
forall a. Monoid a => a
mempty (\String
name -> String -> Term Name DefaultUni DefaultFun () -> TestNested
testTallying String
name (Term Name DefaultUni DefaultFun () -> TestNested)
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> TestNested
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm)
        (PlcFolderContents DefaultUni DefaultFun -> TestTree)
-> PlcFolderContents DefaultUni DefaultFun -> TestTree
forall a b. (a -> b) -> a -> b
$ PlcFolderContents DefaultUni DefaultFun
bunchOfFibs

test_NumberOfStepCounters :: TestTree
test_NumberOfStepCounters :: TestTree
test_NumberOfStepCounters =
    [String] -> TestNested -> TestTree
runTestNestedM [String
"untyped-plutus-core", String
"test", String
"Evaluation", String
"Machines"] (TestNested -> TestTree) -> TestNested -> TestTree
forall a b. (a -> b) -> a -> b
$ do
        String -> String -> Doc Any -> TestNested
forall ann. String -> String -> Doc ann -> TestNested
nestedGoldenVsDoc String
"NumberOfStepCounters" String
"" (Doc Any -> TestNested)
-> (Proxy 9 -> Doc Any) -> Proxy 9 -> TestNested
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Doc Any
forall ann. Natural -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Natural -> Doc Any) -> (Proxy 9 -> Natural) -> Proxy 9 -> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy 9 -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy 9 -> TestNested) -> Proxy 9 -> TestNested
forall a b. (a -> b) -> a -> b
$ forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @NumberOfStepCounters
        String -> String -> Doc Any -> TestNested
forall ann. String -> String -> Doc ann -> TestNested
nestedGoldenVsDoc String
"NumberOfStepCounters" String
"" (Doc Any -> TestNested)
-> ([StepKind] -> Doc Any) -> [StepKind] -> TestNested
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Doc Any
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Int -> Doc Any) -> ([StepKind] -> Int) -> [StepKind] -> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [StepKind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([StepKind] -> TestNested) -> [StepKind] -> TestNested
forall a b. (a -> b) -> a -> b
$ forall a. (Enum a, Bounded a) => [a]
enumerate @StepKind