From c950d18a741eb5970aa8f2584bf30418a4fc2145 Mon Sep 17 00:00:00 2001 From: Nikolaos Bezirgiannis Date: Mon, 20 Dec 2021 16:21:12 +0100 Subject: [PATCH] SCP-2973: Switch CEK to NamedDeBruijn, keeping test interface unchanged --- .hlint.yaml | 2 + .../.plan.nix/plutus-benchmark.nix | 1 + .../.plan.nix/plutus-core.nix | 3 + .../.plan.nix/plutus-tx.nix | 1 - .../.plan.nix/plutus-benchmark.nix | 1 + .../.plan.nix/plutus-core.nix | 3 + .../.plan.nix/plutus-tx.nix | 1 - .../.plan.nix/plutus-benchmark.nix | 1 + .../.plan.nix/plutus-core.nix | 3 + .../.plan.nix/plutus-tx.nix | 1 - plutus-benchmark/cek-calibration/Main.hs | 3 +- plutus-benchmark/plutus-benchmark.cabal | 1 + plutus-benchmark/validation/Bench.hs | 2 +- plutus-core/common/PlcTestUtils.hs | 12 +- plutus-core/executables/Common.hs | 13 +- plutus-core/executables/plc/Main.hs | 4 +- plutus-core/executables/uplc/Main.hs | 7 +- .../PlutusCore/Generators/NEAT/Spec.hs | 2 +- .../index-envs/src/Data/DeBruijnEnv.hs | 7 +- plutus-core/plutus-core.cabal | 9 +- plutus-core/plutus-core/src/PlutusCore.hs | 6 +- .../src/PlutusCore/Core/Instance.hs | 2 +- .../src/PlutusCore/Core/Instance/Eq.hs | 43 +++++-- .../plutus-core/src/PlutusCore/Core/Type.hs | 14 ++- .../plutus-core/src/PlutusCore/DeBruijn.hs | 46 +------ .../src/PlutusCore/DeBruijn/Internal.hs | 18 ++- .../plutus-core/src/PlutusCore/Error.hs | 3 +- .../plutus-core/src/PlutusCore/Flat.hs | 2 +- plutus-core/plutus-ir/test/TestLib.hs | 4 +- .../test/datatypes/listMatchEval.golden | 2 +- .../plutus-ir/test/recursion/even3Eval.golden | 2 +- .../src/UntypedPlutusCore/Core/Instance.hs | 2 +- .../src/UntypedPlutusCore/Core/Instance/Eq.hs | 25 +++- .../src/UntypedPlutusCore/Core/Type.hs | 19 ++- .../src/UntypedPlutusCore/DeBruijn.hs | 36 +----- .../Evaluation/Machine/Cek.hs | 73 +++++++++-- .../Evaluation/Machine/Cek/ExBudgetMode.hs | 2 +- .../Evaluation/Machine/Cek/Internal.hs | 118 ++++++++++-------- .../UntypedPlutusCore/Transform/Simplify.hs | 4 - .../untyped-plutus-core/test/DeBruijn/Spec.hs | 18 +-- .../test/Evaluation/Builtins/Common.hs | 2 +- .../Evaluation/Golden/closure.uplc.golden | 2 +- plutus-errors/src/Errors/TH/GenDocs.hs | 2 +- plutus-ledger-api/src/Plutus/V1/Ledger/Api.hs | 18 +-- .../src/Plutus/V1/Ledger/Scripts.hs | 27 ++-- plutus-ledger-api/test/Spec/Eval.hs | 38 +++--- plutus-metatheory/src/Main.lagda | 21 ++-- plutus-metatheory/src/Raw.hs | 12 +- plutus-metatheory/src/Untyped.hs | 9 +- plutus-tx-plugin/src/PlutusTx/Plugin.hs | 2 +- plutus-tx-plugin/test/Budget/Lib.hs | 6 +- .../test/IsData/bytestring.plc.golden | 2 +- plutus-tx-plugin/test/IsData/int.plc.golden | 2 +- plutus-tx-plugin/test/IsData/list.plc.golden | 2 +- plutus-tx-plugin/test/IsData/mono.plc.golden | 2 +- .../test/IsData/nested.plc.golden | 2 +- plutus-tx-plugin/test/IsData/poly.plc.golden | 2 +- .../test/IsData/record.plc.golden | 2 +- plutus-tx-plugin/test/IsData/tuple.plc.golden | 2 +- .../test/IsData/tupleInterop.plc.golden | 2 +- plutus-tx-plugin/test/IsData/unit.plc.golden | 2 +- .../test/IsData/unitInterop.plc.golden | 2 +- .../test/IsData/unsafeTupleInterop.plc.golden | 2 +- plutus-tx-plugin/test/Lib.hs | 9 +- .../test/Lift/boolInterop.plc.golden | 2 +- .../recursive/sameEmptyRoseEval.plc.golden | 30 ++--- .../Functions/recursive/even3.plc.golden | 2 +- .../Functions/recursive/even4.plc.golden | 2 +- .../Plugin/Laziness/joinErrorEval.plc.golden | 2 +- .../Plugin/Primitives/andApply.plc.golden | 2 +- .../Primitives/deconstructData2.plc.golden | 18 +-- .../Primitives/deconstructData3.plc.golden | 14 +-- .../Primitives/equalsByteString.plc.golden | 2 +- .../Plugin/Primitives/equalsString.plc.golden | 2 +- .../Plugin/Primitives/intEqApply.plc.golden | 2 +- .../Plugin/Primitives/ltByteString.plc.golden | 2 +- .../Plugin/Primitives/matchData1.plc.golden | 4 +- plutus-tx-plugin/test/TH/all.plc.golden | 2 +- plutus-tx/plutus-tx.cabal | 1 - plutus-tx/src/PlutusTx/Evaluation.hs | 51 -------- plutus-tx/src/PlutusTx/Lift.hs | 2 +- 81 files changed, 420 insertions(+), 408 deletions(-) delete mode 100644 plutus-tx/src/PlutusTx/Evaluation.hs diff --git a/.hlint.yaml b/.hlint.yaml index c0c8da5749c..20f1d737380 100644 --- a/.hlint.yaml +++ b/.hlint.yaml @@ -23,3 +23,5 @@ - fixity: infixr 3 *** - fixity: infixr 3 &&& - fixity: infixr 1 <=< +# first is too lazy, see: https://github.com/input-output-hk/plutus/issues/3876 +- ignore: {name: Use first, within: [UntypedPlutusCore.Evaluation.Machine.Cek]} diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-benchmark.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-benchmark.nix index d2d05d26755..608bee1fe40 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-benchmark.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-benchmark.nix @@ -212,6 +212,7 @@ (hsPkgs."plutus-tx-plugin" or (errorHandler.buildDepError "plutus-tx-plugin")) (hsPkgs."criterion" or (errorHandler.buildDepError "criterion")) (hsPkgs."mtl" or (errorHandler.buildDepError "mtl")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; hsSourceDirs = [ "cek-calibration" ]; diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix index 0a709c884b3..aabd7fda47a 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix @@ -101,6 +101,7 @@ (hsPkgs."witherable" or (errorHandler.buildDepError "witherable")) (hsPkgs."word-array" or (errorHandler.buildDepError "word-array")) (hsPkgs."cardano-crypto-class" or (errorHandler.buildDepError "cardano-crypto-class")) + (hsPkgs."plutus-core".components.sublibs.index-envs or (errorHandler.buildDepError "plutus-core:index-envs")) ]; build-tools = [ (hsPkgs.buildPackages.alex.components.exes.alex or (pkgs.buildPackages.alex or (errorHandler.buildToolDepError "alex:alex"))) @@ -344,6 +345,7 @@ (hsPkgs."prettyprinter" or (errorHandler.buildDepError "prettyprinter")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."transformers" or (errorHandler.buildDepError "transformers")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; modules = [ "Common" "Parsers" ]; @@ -365,6 +367,7 @@ (hsPkgs."split" or (errorHandler.buildDepError "split")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."transformers" or (errorHandler.buildDepError "transformers")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; modules = [ "Common" "Parsers" ]; diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-tx.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-tx.nix index ac4f824c748..740e947d50f 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-tx.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-tx.nix @@ -61,7 +61,6 @@ "PlutusTx/Coverage" "PlutusTx/TH" "PlutusTx/Prelude" - "PlutusTx/Evaluation" "PlutusTx/Applicative" "PlutusTx/Base" "PlutusTx/Bool" diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-benchmark.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-benchmark.nix index d2d05d26755..608bee1fe40 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-benchmark.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-benchmark.nix @@ -212,6 +212,7 @@ (hsPkgs."plutus-tx-plugin" or (errorHandler.buildDepError "plutus-tx-plugin")) (hsPkgs."criterion" or (errorHandler.buildDepError "criterion")) (hsPkgs."mtl" or (errorHandler.buildDepError "mtl")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; hsSourceDirs = [ "cek-calibration" ]; diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix index 0a709c884b3..aabd7fda47a 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix @@ -101,6 +101,7 @@ (hsPkgs."witherable" or (errorHandler.buildDepError "witherable")) (hsPkgs."word-array" or (errorHandler.buildDepError "word-array")) (hsPkgs."cardano-crypto-class" or (errorHandler.buildDepError "cardano-crypto-class")) + (hsPkgs."plutus-core".components.sublibs.index-envs or (errorHandler.buildDepError "plutus-core:index-envs")) ]; build-tools = [ (hsPkgs.buildPackages.alex.components.exes.alex or (pkgs.buildPackages.alex or (errorHandler.buildToolDepError "alex:alex"))) @@ -344,6 +345,7 @@ (hsPkgs."prettyprinter" or (errorHandler.buildDepError "prettyprinter")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."transformers" or (errorHandler.buildDepError "transformers")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; modules = [ "Common" "Parsers" ]; @@ -365,6 +367,7 @@ (hsPkgs."split" or (errorHandler.buildDepError "split")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."transformers" or (errorHandler.buildDepError "transformers")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; modules = [ "Common" "Parsers" ]; diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-tx.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-tx.nix index ac4f824c748..740e947d50f 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-tx.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-tx.nix @@ -61,7 +61,6 @@ "PlutusTx/Coverage" "PlutusTx/TH" "PlutusTx/Prelude" - "PlutusTx/Evaluation" "PlutusTx/Applicative" "PlutusTx/Base" "PlutusTx/Bool" diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-benchmark.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-benchmark.nix index d2d05d26755..608bee1fe40 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-benchmark.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-benchmark.nix @@ -212,6 +212,7 @@ (hsPkgs."plutus-tx-plugin" or (errorHandler.buildDepError "plutus-tx-plugin")) (hsPkgs."criterion" or (errorHandler.buildDepError "criterion")) (hsPkgs."mtl" or (errorHandler.buildDepError "mtl")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; hsSourceDirs = [ "cek-calibration" ]; diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix index 0a709c884b3..aabd7fda47a 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix @@ -101,6 +101,7 @@ (hsPkgs."witherable" or (errorHandler.buildDepError "witherable")) (hsPkgs."word-array" or (errorHandler.buildDepError "word-array")) (hsPkgs."cardano-crypto-class" or (errorHandler.buildDepError "cardano-crypto-class")) + (hsPkgs."plutus-core".components.sublibs.index-envs or (errorHandler.buildDepError "plutus-core:index-envs")) ]; build-tools = [ (hsPkgs.buildPackages.alex.components.exes.alex or (pkgs.buildPackages.alex or (errorHandler.buildToolDepError "alex:alex"))) @@ -344,6 +345,7 @@ (hsPkgs."prettyprinter" or (errorHandler.buildDepError "prettyprinter")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."transformers" or (errorHandler.buildDepError "transformers")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; modules = [ "Common" "Parsers" ]; @@ -365,6 +367,7 @@ (hsPkgs."split" or (errorHandler.buildDepError "split")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."transformers" or (errorHandler.buildDepError "transformers")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) ]; buildable = true; modules = [ "Common" "Parsers" ]; diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-tx.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-tx.nix index ac4f824c748..740e947d50f 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-tx.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-tx.nix @@ -61,7 +61,6 @@ "PlutusTx/Coverage" "PlutusTx/TH" "PlutusTx/Prelude" - "PlutusTx/Evaluation" "PlutusTx/Applicative" "PlutusTx/Base" "PlutusTx/Bool" diff --git a/plutus-benchmark/cek-calibration/Main.hs b/plutus-benchmark/cek-calibration/Main.hs index 58e785a48c4..a1fb507b6fc 100644 --- a/plutus-benchmark/cek-calibration/Main.hs +++ b/plutus-benchmark/cek-calibration/Main.hs @@ -24,6 +24,7 @@ import UntypedPlutusCore as UPLC import UntypedPlutusCore.Evaluation.Machine.Cek import Control.Exception +import Control.Lens import Control.Monad.Except import Criterion.Main import Criterion.Types qualified as C @@ -80,7 +81,7 @@ mkListBMs ns = bgroup "List" [mkListBM n | n <- ns] writePlc :: UPLC.Program NamedDeBruijn DefaultUni DefaultFun () -> Haskell.IO () writePlc p = - case runExcept @UPLC.FreeVariableError $ runQuoteT $ UPLC.unDeBruijnProgram p of + case runExcept @UPLC.FreeVariableError $ runQuoteT $ traverseOf UPLC.progTerm UPLC.unDeBruijnTerm p of Left e -> throw e Right p' -> Haskell.print . PP.prettyPlcClassicDebug $ p' diff --git a/plutus-benchmark/plutus-benchmark.cabal b/plutus-benchmark/plutus-benchmark.cabal index 37d31b6ee77..cd26efc25ce 100644 --- a/plutus-benchmark/plutus-benchmark.cabal +++ b/plutus-benchmark/plutus-benchmark.cabal @@ -248,3 +248,4 @@ benchmark cek-calibration , plutus-tx-plugin -any , criterion >= 1.5.9.0 , mtl -any + , lens -any diff --git a/plutus-benchmark/validation/Bench.hs b/plutus-benchmark/validation/Bench.hs index a0e4b5cda5e..d06c3345a5e 100644 --- a/plutus-benchmark/validation/Bench.hs +++ b/plutus-benchmark/validation/Bench.hs @@ -79,7 +79,7 @@ loadFlat file = do case unflat contents of Left e -> errorWithoutStackTrace $ "Flat deserialisation failure for " ++ file ++ ": " ++ show e Right prog -> do - let t = unDeBruijnAnonTerm $ UPLC.toTerm prog + let t = unDeBruijnAnonTerm $ UPLC._progTerm prog return $! force t -- `force` to try to ensure that deserialiation is not included in benchmarking time. diff --git a/plutus-core/common/PlcTestUtils.hs b/plutus-core/common/PlcTestUtils.hs index 224cce52621..a9b4c555fa0 100644 --- a/plutus-core/common/PlcTestUtils.hs +++ b/plutus-core/common/PlcTestUtils.hs @@ -57,7 +57,7 @@ import UntypedPlutusCore qualified as UPLC import UntypedPlutusCore.Evaluation.Machine.Cek qualified as UPLC import Control.Exception -import Control.Lens.Combinators (_2) +import Control.Lens import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State @@ -112,7 +112,7 @@ instance ToUPlc (UPLC.Program TPLC.Name uni fun ()) uni fun where toUPlc = pure instance ToUPlc (UPLC.Program UPLC.NamedDeBruijn uni fun ()) uni fun where - toUPlc p = withExceptT @_ @FreeVariableError toException $ TPLC.runQuoteT $ UPLC.unDeBruijnProgram p + toUPlc p = withExceptT @_ @FreeVariableError toException $ TPLC.runQuoteT $ traverseOf UPLC.progTerm UPLC.unDeBruijnTerm p pureTry :: Exception e => a -> Either e a pureTry = unsafePerformIO . try . evaluate @@ -180,28 +180,28 @@ goldenTPlc => String -> a -> TestNested goldenTPlc name value = nestedGoldenVsDocM name $ ppThrow $ do p <- toTPlc value - withExceptT @_ @FreeVariableError toException $ deBruijnProgram p + withExceptT @_ @FreeVariableError toException $ traverseOf TPLC.progTerm deBruijnTerm p goldenTPlcCatch :: ToTPlc a DefaultUni TPLC.DefaultFun => String -> a -> TestNested goldenTPlcCatch name value = nestedGoldenVsDocM name $ ppCatch $ do p <- toTPlc value - withExceptT @_ @FreeVariableError toException $ deBruijnProgram p + withExceptT @_ @FreeVariableError toException $ traverseOf TPLC.progTerm deBruijnTerm p goldenUPlc :: ToUPlc a DefaultUni TPLC.DefaultFun => String -> a -> TestNested goldenUPlc name value = nestedGoldenVsDocM name $ ppThrow $ do p <- toUPlc value - withExceptT @_ @FreeVariableError toException $ UPLC.deBruijnProgram p + withExceptT @_ @FreeVariableError toException $ traverseOf UPLC.progTerm UPLC.deBruijnTerm p goldenUPlcCatch :: ToUPlc a DefaultUni TPLC.DefaultFun => String -> a -> TestNested goldenUPlcCatch name value = nestedGoldenVsDocM name $ ppCatch $ do p <- toUPlc value - withExceptT @_ @FreeVariableError toException $ UPLC.deBruijnProgram p + withExceptT @_ @FreeVariableError toException $ traverseOf UPLC.progTerm UPLC.deBruijnTerm p goldenTEval :: ToTPlc a DefaultUni TPLC.DefaultFun diff --git a/plutus-core/executables/Common.hs b/plutus-core/executables/Common.hs index 87b6ca1a5d6..56553760bbc 100644 --- a/plutus-core/executables/Common.hs +++ b/plutus-core/executables/Common.hs @@ -34,6 +34,7 @@ import UntypedPlutusCore.Evaluation.Machine.Cek qualified as Cek import UntypedPlutusCore.Parser qualified as UPLC (parseProgram) import Control.DeepSeq (NFData, rnf) +import Control.Lens hiding (ix, op) import Control.Monad.Except import Data.Aeson qualified as Aeson import Data.Bifunctor (second) @@ -123,16 +124,16 @@ typedDeBruijnNotSupportedError = -- | Convert an untyped program to one where the 'name' type is de Bruijn indices. toDeBruijn :: UplcProg ann -> IO (UPLC.Program UPLC.DeBruijn PLC.DefaultUni PLC.DefaultFun ann) toDeBruijn prog = - case runExcept @UPLC.FreeVariableError (UPLC.deBruijnProgram prog) of + case runExcept @UPLC.FreeVariableError $ traverseOf UPLC.progTerm UPLC.deBruijnTerm prog of Left e -> errorWithoutStackTrace $ show e Right p -> return $ UPLC.programMapNames (\(UPLC.NamedDeBruijn _ ix) -> UPLC.DeBruijn ix) p -- | Convert an untyped program to one where the 'name' type is textual names with de Bruijn indices. toNamedDeBruijn :: UplcProg ann -> IO (UPLC.Program UPLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun ann) toNamedDeBruijn prog = - case runExcept @UPLC.FreeVariableError (UPLC.deBruijnProgram prog) of + case runExcept @UPLC.FreeVariableError $ traverseOf UPLC.progTerm UPLC.deBruijnTerm prog of Left e -> errorWithoutStackTrace $ show e - Right p -> return $ UPLC.programMapNames (\(UPLC.NamedDeBruijn v ix) -> UPLC.NamedDeBruijn v ix) p + Right p -> return p ---------------- Printing budgets and costs ---------------- @@ -249,7 +250,7 @@ instance Show Format where data ConvertOptions = ConvertOptions Input Format Output Format PrintMode data PrintOptions = PrintOptions Input PrintMode -data ExampleOptions = ExampleOptions ExampleMode +newtype ExampleOptions = ExampleOptions ExampleMode data ApplyOptions = ApplyOptions Files Format Output Format PrintMode helpText :: @@ -320,7 +321,7 @@ type UntypedProgramDeBruijn ann = UPLC.Program UPLC.NamedDeBruijn PLC.DefaultUni -- with a Unique for disambiguation). Again, we don't support typed programs. fromDeBruijn :: UntypedProgramDeBruijn ann -> IO (UplcProg ann) fromDeBruijn prog = do - case PLC.runQuote $ runExceptT @UPLC.FreeVariableError $ UPLC.unDeBruijnProgram prog of + case PLC.runQuote $ runExceptT @UPLC.FreeVariableError $ traverseOf UPLC.progTerm UPLC.unDeBruijnTerm prog of Left e -> errorWithoutStackTrace $ show e Right p -> return p @@ -344,7 +345,7 @@ loadUplcASTfromFlat flatMode inp = do Named -> handleResult $ unflat input DeBruijn -> do deserialised <- handleResult $ unflat input - let namedProgram = UPLC.programMapNames (\(UPLC.DeBruijn ix) -> UPLC.NamedDeBruijn "v" ix) deserialised + let namedProgram = UPLC.programMapNames UPLC.fakeNameDeBruijn deserialised fromDeBruijn namedProgram NamedDeBruijn -> do deserialised <- handleResult $ unflat input diff --git a/plutus-core/executables/plc/Main.hs b/plutus-core/executables/plc/Main.hs index 1a9d3f6015c..c4522f3aa1c 100644 --- a/plutus-core/executables/plc/Main.hs +++ b/plutus-core/executables/plc/Main.hs @@ -11,11 +11,11 @@ import PlutusCore.Pretty qualified as PP import UntypedPlutusCore qualified as UPLC (eraseProgram) -import Data.Function ((&)) import Data.Functor (void) import Data.Text.IO qualified as T import Control.DeepSeq (rnf) +import Control.Lens import Options.Applicative import System.Exit (exitSuccess) @@ -129,7 +129,7 @@ runEval :: EvalOptions -> IO () runEval (EvalOptions inp ifmt printMode timingMode) = do prog <- getProgram ifmt inp let evaluate = Ck.evaluateCkNoEmit PLC.defaultBuiltinsRuntime - term = void . PLC.toTerm $ prog + term = void $ prog ^. PLC.progTerm !_ = rnf term -- Force evaluation of body to ensure that we're not timing parsing/deserialisation. -- The parser apparently returns a fully-evaluated AST, but let's be on the safe side. diff --git a/plutus-core/executables/uplc/Main.hs b/plutus-core/executables/uplc/Main.hs index 41b72441c96..581b609c1ea 100644 --- a/plutus-core/executables/uplc/Main.hs +++ b/plutus-core/executables/uplc/Main.hs @@ -21,6 +21,7 @@ import UntypedPlutusCore qualified as UPLC import UntypedPlutusCore.Evaluation.Machine.Cek qualified as Cek import Control.DeepSeq (NFData, rnf) +import Control.Lens import Options.Applicative import System.Exit (exitFailure) import System.IO (hPrint, stderr) @@ -35,7 +36,7 @@ uplcInfoCommand = plutus uplcHelpText data BudgetMode = Silent | Verbose SomeBudgetMode -data SomeBudgetMode = forall cost. (Eq cost, NFData cost, PrintBudgetState cost) => SomeBudgetMode (Cek.ExBudgetMode cost PLC.DefaultUni PLC.DefaultFun) +data SomeBudgetMode = forall cost. (Eq cost, NFData cost, PrintBudgetState cost, Monoid cost) => SomeBudgetMode (Cek.ExBudgetMode cost PLC.DefaultUni PLC.DefaultFun) data EvalOptions = EvalOptions Input Format PrintMode BudgetMode TraceMode Output TimingMode CekModel @@ -156,7 +157,7 @@ runApply :: ApplyOptions -> IO () runApply (ApplyOptions inputfiles ifmt outp ofmt mode) = do scripts <- mapM ((getProgram ifmt :: Input -> IO (UplcProg PLC.AlexPosn)) . FileInput) inputfiles let appliedScript = - case map (\case p -> () <$ p) scripts of + case void <$> scripts of [] -> errorWithoutStackTrace "No input files" progAndargs -> foldl1 UPLC.applyProgram progAndargs writeProgram outp ofmt mode appliedScript @@ -166,7 +167,7 @@ runApply (ApplyOptions inputfiles ifmt outp ofmt mode) = do runEval :: EvalOptions -> IO () runEval (EvalOptions inp ifmt printMode budgetMode traceMode outputMode timingMode cekModel) = do prog <- getProgram ifmt inp - let term = void . UPLC.toTerm $ prog + let term = void $ prog ^. UPLC.progTerm !_ = rnf term cekparams = case cekModel of Default -> PLC.defaultCekParameters -- AST nodes are charged according to the default cost model diff --git a/plutus-core/generators/PlutusCore/Generators/NEAT/Spec.hs b/plutus-core/generators/PlutusCore/Generators/NEAT/Spec.hs index a47d9b58823..858fba03b30 100644 --- a/plutus-core/generators/PlutusCore/Generators/NEAT/Spec.hs +++ b/plutus-core/generators/PlutusCore/Generators/NEAT/Spec.hs @@ -254,7 +254,7 @@ data TestFail | AgdaErrorP () | FVErrorP FreeVariableError | CkP (CkEvaluationException DefaultUni DefaultFun) - | UCekP (U.CekEvaluationException DefaultUni DefaultFun) + | UCekP (U.CekEvaluationException Name DefaultUni DefaultFun) | Ctrex Ctrex data Ctrex diff --git a/plutus-core/index-envs/src/Data/DeBruijnEnv.hs b/plutus-core/index-envs/src/Data/DeBruijnEnv.hs index e2b07f8cd29..aafb43d9567 100644 --- a/plutus-core/index-envs/src/Data/DeBruijnEnv.hs +++ b/plutus-core/index-envs/src/Data/DeBruijnEnv.hs @@ -38,7 +38,8 @@ instance DeBruijnEnv (BRAL.RAList a) where unsafeIndex = BRAL.index -- | A sequence implemented by a map from "levels" to values and a counter giving the "current" level. -data RelativizedMap a = RelativizedMap (IM.IntMap a) {-# UNPACK #-} !Int +data RelativizedMap a = RelativizedMap (IM.IntMap a) {-# UNPACK #-} !Word + deriving Show instance DeBruijnEnv (RelativizedMap a) where type Element (RelativizedMap a) = a @@ -46,9 +47,9 @@ instance DeBruijnEnv (RelativizedMap a) where {-# INLINABLE empty #-} empty = RelativizedMap mempty 0 {-# INLINABLE cons #-} - cons a (RelativizedMap im l) = RelativizedMap (IM.insert l a im) (l+1) + cons a (RelativizedMap im l) = RelativizedMap (IM.insert (fromIntegral l) a im) (l+1) {-# INLINABLE index #-} - index (RelativizedMap im l) w = IM.lookup (l - fromIntegral w) im + index (RelativizedMap im l) w = IM.lookup (fromIntegral l - fromIntegral w) im instance DeBruijnEnv (RAL.RAList a) where type Element (RAL.RAList a) = a diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal index 1b2872d92a9..afeb92108ac 100644 --- a/plutus-core/plutus-core.cabal +++ b/plutus-core/plutus-core.cabal @@ -318,7 +318,8 @@ library unordered-containers -any, witherable -any, word-array -any, - cardano-crypto-class -any + cardano-crypto-class -any, + index-envs test-suite satint-test import: lang @@ -447,7 +448,8 @@ executable plc optparse-applicative -any, prettyprinter -any, text -any, - transformers -any + transformers -any, + lens -any executable uplc import: lang @@ -469,7 +471,8 @@ executable uplc prettyprinter -any, split -any, text -any, - transformers -any + transformers -any, + lens -any executable pir import: lang diff --git a/plutus-core/plutus-core/src/PlutusCore.hs b/plutus-core/plutus-core/src/PlutusCore.hs index c79d56bd15e..ba6731ee297 100644 --- a/plutus-core/plutus-core/src/PlutusCore.hs +++ b/plutus-core/plutus-core/src/PlutusCore.hs @@ -55,7 +55,6 @@ module PlutusCore , Normalized (..) , defaultVersion , allKeywords - , toTerm , termAnn , typeAnn , tyVarDeclAnn @@ -67,13 +66,14 @@ module PlutusCore , tyDeclAnn , tyDeclType , tyDeclKind + , progAnn + , progVer + , progTerm , mapFun -- * DeBruijn representation , DeBruijn (..) , NamedDeBruijn (..) - , deBruijnProgram , deBruijnTerm - , unDeBruijnProgram , unDeBruijnTerm -- * Lexer , AlexPosn (..) diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Instance.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Instance.hs index 49e392ac8d6..cc24bbc0ddf 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Core/Instance.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Core/Instance.hs @@ -1,6 +1,6 @@ module PlutusCore.Core.Instance (module Export) where -import PlutusCore.Core.Instance.Eq as Export +import PlutusCore.Core.Instance.Eq () import PlutusCore.Core.Instance.Pretty () import PlutusCore.Core.Instance.Recursive as Export import PlutusCore.Core.Instance.Scoping () diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs index 1af985f23cb..84fda979616 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs @@ -2,35 +2,58 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -module PlutusCore.Core.Instance.Eq - ( eqTypeM - , eqTermM - ) where +module PlutusCore.Core.Instance.Eq () where import PlutusPrelude import PlutusCore.Core.Type +import PlutusCore.DeBruijn import PlutusCore.Eq import PlutusCore.Name import PlutusCore.Rename.Monad import Universe -instance (HasUniques (Type tyname uni ann), GEq uni, Eq ann) => Eq (Type tyname uni ann) where +instance (GEq uni, Eq ann) => Eq (Type TyName uni ann) where ty1 == ty2 = runEqRename @TypeRenaming $ eqTypeM ty1 ty2 instance - ( HasUniques (Term tyname name uni fun ann) - , GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann - ) => Eq (Term tyname name uni fun ann) where + ( GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann + ) => Eq (Term TyName Name uni fun ann) where term1 == term2 = runEqRename $ eqTermM term1 term2 +-- Simple Structural Equality of a `Term NamedDeBruijn`. This implies three things: +-- b) We do not do equality "modulo starting index". E.g. `LamAbs 0 (Var 0) /= LamAbs 1 (Var 1)`. +-- c) We do not do equality ""modulo annotations". +-- Note that we ignore the name part in case of the nameddebruijn +-- If a user wants to ignore annotations he must prior do `void <$> term`, to throw away any annotations. +deriving instance + (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) => + Eq (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) + +deriving instance + (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) => + Eq (Term TyDeBruijn DeBruijn uni fun ann) + +deriving instance + (GEq uni, Closed uni, uni `Everywhere` Eq, Eq ann) => + Eq (Type NamedTyDeBruijn uni ann) + +deriving instance + (GEq uni, Closed uni, uni `Everywhere` Eq, Eq ann) => + Eq (Type TyDeBruijn uni ann) + +deriving instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann, + Eq (Term tyname name uni fun ann) + ) => Eq (Program tyname name uni fun ann) + type EqRenameOf ren a = HasUniques a => a -> a -> EqRename ren -- See Note [Modulo alpha]. @@ -127,7 +150,3 @@ eqTermM TyInst{} _ = empty eqTermM Var{} _ = empty eqTermM Constant{} _ = empty eqTermM Builtin{} _ = empty - -deriving instance (HasUniques (Term tyname name uni fun ann) - , GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann - ) => Eq (Program tyname name uni fun ann) diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Type.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Type.hs index 32de2fd3e55..3f894417b50 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Core/Type.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Core/Type.hs @@ -27,7 +27,6 @@ module PlutusCore.Core.Type , Binder (..) , defaultVersion -- * Helper functions - , toTerm , termAnn , typeAnn , mapFun @@ -40,6 +39,9 @@ module PlutusCore.Core.Type , tyDeclAnn , tyDeclType , tyDeclKind + , progAnn + , progVer + , progTerm ) where @@ -91,8 +93,13 @@ data Version ann deriving (Eq, Show, Functor, Generic, NFData, Hashable) -- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language. -data Program tyname name uni fun ann = Program ann (Version ann) (Term tyname name uni fun ann) +data Program tyname name uni fun ann = Program + { _progAnn :: ann + , _progVer :: Version ann + , _progTerm :: Term tyname name uni fun ann + } deriving (Show, Functor, Generic, NFData, Hashable) +makeLenses ''Program -- | Extract the universe from a type. type family UniOf a :: GHC.Type -> GHC.Type @@ -153,9 +160,6 @@ type instance HasUniques (Program tyname name uni fun ann) = defaultVersion :: ann -> Version ann defaultVersion ann = Version ann 1 0 0 -toTerm :: Program tyname name uni fun ann -> Term tyname name uni fun ann -toTerm (Program _ _ term) = term - typeAnn :: Type tyname uni ann -> ann typeAnn (TyVar ann _ ) = ann typeAnn (TyFun ann _ _ ) = ann diff --git a/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs b/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs index 664cf2b0b7f..1bb2c01d7b6 100644 --- a/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs +++ b/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs @@ -17,23 +17,20 @@ module PlutusCore.DeBruijn , fakeNameDeBruijn , deBruijnTy , deBruijnTerm - , deBruijnProgram , unDeBruijnTy , unDeBruijnTerm - , unDeBruijnProgram -- * unsafe api, use with care , deBruijnTyWith , deBruijnTermWith - , deBruijnProgramWith , unDeBruijnTyWith , unDeBruijnTermWith - , unDeBruijnProgramWith , freeIndexAsConsistentLevel + , deBruijnInitIndex ) where import PlutusCore.DeBruijn.Internal -import PlutusCore.Core +import PlutusCore.Core.Type import PlutusCore.Name import PlutusCore.Quote @@ -65,14 +62,6 @@ unDeBruijnTermWith -> m (Term TyName Name uni fun ann) unDeBruijnTermWith = (runDeBruijnT .) . unDeBruijnTermWithM --- | Takes a "handler" function to execute when encountering free variables. -unDeBruijnProgramWith - :: MonadQuote m - => (Index -> ReaderT Levels m Unique) - -> Program NamedTyDeBruijn NamedDeBruijn uni fun ann - -> m (Program TyName Name uni fun ann) -unDeBruijnProgramWith h (Program ann ver term) = Program ann ver <$> unDeBruijnTermWith h term - -- | Convert a 'Type' with 'NamedTyDeBruijn's into a 'Type' with 'TyName's. -- Will throw an error if a free variable is encountered. unDeBruijnTy @@ -87,14 +76,6 @@ unDeBruijnTerm => Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Term TyName Name uni fun ann) unDeBruijnTerm = unDeBruijnTermWith freeIndexThrow --- | Convert a 'Program' with 'NamedTyDeBruijn's and 'NamedDeBruijn's into a 'Program' with 'TyName's and 'Name's. --- Will throw an error if a free variable is encountered. -unDeBruijnProgram - :: (MonadQuote m, AsFreeVariableError e, MonadError e m) - => Program NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Program TyName Name uni fun ann) -unDeBruijnProgram = unDeBruijnProgramWith freeIndexThrow - - -- | Convert a 'Type' with 'TyName's into a 'Type' with 'NamedTyDeBruijn's. -- Will throw an error if a free variable is encountered. deBruijnTy @@ -109,13 +90,6 @@ deBruijnTerm => Term TyName Name uni fun ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) deBruijnTerm = deBruijnTermWith freeUniqueThrow --- | Convert a 'Program' with 'TyName's and 'Name's into a 'Program' with 'NamedTyDeBruijn's and 'NamedDeBruijn's. --- Will throw an error if a free variable is encountered. -deBruijnProgram - :: (AsFreeVariableError e, MonadError e m) - => Program TyName Name uni fun ann -> m (Program NamedTyDeBruijn NamedDeBruijn uni fun ann) -deBruijnProgram = deBruijnProgramWith freeUniqueThrow - deBruijnTermWith :: Monad m => (Unique -> ReaderT Levels m Index) @@ -130,14 +104,6 @@ deBruijnTyWith -> m (Type NamedTyDeBruijn uni ann) deBruijnTyWith = (runDeBruijnT .) . deBruijnTyWithM -deBruijnProgramWith - :: Monad m - => (Unique -> ReaderT Levels m Index) - -> Program TyName Name uni fun ann - -> m (Program NamedTyDeBruijn NamedDeBruijn uni fun ann) -deBruijnProgramWith h (Program ann ver term) = Program ann ver <$> deBruijnTermWith h term - - {- Note [De Bruijn conversion and recursion schemes] These are quite repetitive, but we can't use a catamorphism for this, because we are not only altering the recursive type, but also the name type parameters. @@ -216,12 +182,12 @@ unDeBruijnTyWithM h = go TyForall ann tn k ty -> -- See NOTE: [DeBruijn indices of Binders] declareBinder $ do - tn' <- deBruijnToTyName h $ set index 0 tn + tn' <- deBruijnToTyName h $ set index deBruijnInitIndex tn withScope $ TyForall ann tn' k <$> go ty TyLam ann tn k ty -> -- See NOTE: [DeBruijn indices of Binders] declareBinder $ do - tn' <- deBruijnToTyName h $ set index 0 tn + tn' <- deBruijnToTyName h $ set index deBruijnInitIndex tn withScope $ TyLam ann tn' k <$> go ty -- boring recursive cases TyFun ann i o -> TyFun ann <$> go i <*> go o @@ -249,12 +215,12 @@ unDeBruijnTermWithM h = go TyAbs ann tn k t -> -- See NOTE: [DeBruijn indices of Binders] declareBinder $ do - tn' <- deBruijnToTyName h $ set index 0 tn + tn' <- deBruijnToTyName h $ set index deBruijnInitIndex tn withScope $ TyAbs ann tn' k <$> go t LamAbs ann n ty t -> -- See NOTE: [DeBruijn indices of Binders] declareBinder $ do - n' <- deBruijnToName h $ set index 0 n + n' <- deBruijnToName h $ set index deBruijnInitIndex n withScope $ LamAbs ann n' <$> goT ty <*> go t -- boring recursive cases Apply ann t1 t2 -> Apply ann <$> go t1 <*> go t2 diff --git a/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs b/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs index 9f0630de2b9..2f11fdbed03 100644 --- a/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs +++ b/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs @@ -7,6 +7,7 @@ -- | Support for using de Bruijn indices for term and type names. module PlutusCore.DeBruijn.Internal ( Index (..) + , HasIndex (..) , DeBruijn (..) , NamedDeBruijn (..) , TyDeBruijn (..) @@ -30,8 +31,8 @@ module PlutusCore.DeBruijn.Internal , freeIndexThrow , freeIndexAsConsistentLevel , freeUniqueThrow - , HasIndex (..) , runDeBruijnT + , deBruijnInitIndex ) where import PlutusCore.Name @@ -62,20 +63,30 @@ newtype Index = Index Natural deriving newtype (Show, Num, Enum, Real, Integral, Eq, Ord, Pretty) deriving anyclass NFData +-- | The LamAbs index (for debruijn indices) and the starting level of DeBruijn monad +deBruijnInitIndex :: Index +deBruijnInitIndex = 0 + -- | A term name as a de Bruijn index. data NamedDeBruijn = NamedDeBruijn { ndbnString :: T.Text, ndbnIndex :: Index } deriving (Show, Generic) deriving anyclass NFData +instance Eq NamedDeBruijn where + -- ignoring actual names and only relying solely on debruijn indices + (NamedDeBruijn _ ix1) == (NamedDeBruijn _ ix2) = ix1 == ix2 + -- | A term name as a de Bruijn index, without the name string. newtype DeBruijn = DeBruijn { dbnIndex :: Index } - deriving (Show, Generic) + deriving (Show, Generic, Eq) deriving anyclass NFData -- | A type name as a de Bruijn index. newtype NamedTyDeBruijn = NamedTyDeBruijn NamedDeBruijn deriving stock (Show, Generic) deriving newtype (PrettyBy config) + -- ignoring actual names and only relying solely on debruijn indices + deriving Eq via NamedDeBruijn deriving anyclass NFData instance Wrapped NamedTyDeBruijn @@ -83,6 +94,7 @@ instance Wrapped NamedTyDeBruijn newtype TyDeBruijn = TyDeBruijn DeBruijn deriving stock (Show, Generic) deriving newtype (PrettyBy config) + deriving Eq via DeBruijn deriving anyclass NFData instance Wrapped TyDeBruijn @@ -295,4 +307,4 @@ ixToLevel :: Level -> Index -> Level ixToLevel (Level current) ixAST = Level $ current - fromIntegral ixAST runDeBruijnT :: ReaderT Levels m a -> m a -runDeBruijnT = flip runReaderT (Levels 0 BM.empty) +runDeBruijnT = flip runReaderT (Levels (Level $ fromIntegral deBruijnInitIndex) BM.empty) diff --git a/plutus-core/plutus-core/src/PlutusCore/Error.hs b/plutus-core/plutus-core/src/PlutusCore/Error.hs index f8890ef2567..5256af4473b 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Error.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Error.hs @@ -80,7 +80,8 @@ data NormCheckError tyname name uni fun ann | BadTerm ann (Term tyname name uni fun ann) T.Text deriving (Show, Functor, Generic, NFData) deriving instance - ( HasUniques (Term tyname name uni fun ann) + ( Eq (Term tyname name uni fun ann) + , Eq (Type tyname uni ann) , GEq uni, Closed uni, uni `Everywhere` Eq , Eq fun, Eq ann ) => Eq (NormCheckError tyname name uni fun ann) diff --git a/plutus-core/plutus-core/src/PlutusCore/Flat.hs b/plutus-core/plutus-core/src/PlutusCore/Flat.hs index df71b1e7533..89f7b5c4707 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Flat.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Flat.hs @@ -336,7 +336,7 @@ instance Flat NamedTyDeBruijn where instance Flat (Binder DeBruijn) where size _ = id -- zero cost encode _ = mempty - decode = pure $ Binder (DeBruijn 0) + decode = pure $ Binder $ DeBruijn deBruijnInitIndex -- (Binder TyDeBruin) could similarly have a flat instance, but we don't need it. diff --git a/plutus-core/plutus-ir/test/TestLib.hs b/plutus-core/plutus-ir/test/TestLib.hs index cea250f3c3f..1300818c5c1 100644 --- a/plutus-core/plutus-ir/test/TestLib.hs +++ b/plutus-core/plutus-ir/test/TestLib.hs @@ -106,14 +106,14 @@ goldenPlcFromPir :: Parser SourcePos a -> String -> TestNested goldenPlcFromPir = goldenPirM (\ast -> ppThrow $ do p <- toTPlc ast - withExceptT @_ @PLC.FreeVariableError toException $ PLC.deBruijnProgram p) + withExceptT @_ @PLC.FreeVariableError toException $ traverseOf PLC.progTerm PLC.deBruijnTerm p) goldenPlcFromPirCatch :: ToTPlc a PLC.DefaultUni PLC.DefaultFun => Parser SourcePos a -> String -> TestNested goldenPlcFromPirCatch = goldenPirM (\ast -> ppCatch $ do p <- toTPlc ast - withExceptT @_ @PLC.FreeVariableError toException $ PLC.deBruijnProgram p) + withExceptT @_ @PLC.FreeVariableError toException $ traverseOf PLC.progTerm PLC.deBruijnTerm p) goldenEvalPir :: ToUPlc a PLC.DefaultUni PLC.DefaultFun => diff --git a/plutus-core/plutus-ir/test/datatypes/listMatchEval.golden b/plutus-core/plutus-ir/test/datatypes/listMatchEval.golden index 8fa31e0cf57..5d050430f86 100644 --- a/plutus-core/plutus-ir/test/datatypes/listMatchEval.golden +++ b/plutus-core/plutus-ir/test/datatypes/listMatchEval.golden @@ -1 +1 @@ -(delay (lam x_85 x_85)) \ No newline at end of file +(delay (lam x_0 x_0)) \ No newline at end of file diff --git a/plutus-core/plutus-ir/test/recursion/even3Eval.golden b/plutus-core/plutus-ir/test/recursion/even3Eval.golden index 17b4fe70d3c..4e8ddacc956 100644 --- a/plutus-core/plutus-ir/test/recursion/even3Eval.golden +++ b/plutus-core/plutus-ir/test/recursion/even3Eval.golden @@ -1 +1 @@ -(delay (lam case_True_228 (lam case_False_229 case_False_229))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_False_1))) \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance.hs index 15d98b4bd5c..5fad798cd63 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance.hs @@ -1,5 +1,5 @@ module UntypedPlutusCore.Core.Instance (module Export) where -import UntypedPlutusCore.Core.Instance.Eq as Export +import UntypedPlutusCore.Core.Instance.Eq () import UntypedPlutusCore.Core.Instance.Pretty () import UntypedPlutusCore.Core.Instance.Recursive as Export diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Eq.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Eq.hs index 815a9344c21..596ce381c59 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Eq.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Eq.hs @@ -1,24 +1,43 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -module UntypedPlutusCore.Core.Instance.Eq where +module UntypedPlutusCore.Core.Instance.Eq () where import PlutusPrelude import UntypedPlutusCore.Core.Type +import PlutusCore.DeBruijn import PlutusCore.Eq import PlutusCore.Name import PlutusCore.Rename.Monad import Universe -instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, HasUnique name TermUnique, Eq ann) => - Eq (Term name uni fun ann) where +instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) => + Eq (Term Name uni fun ann) where term1 == term2 = runEqRename $ eqTermM term1 term2 +-- Simple Structural Equality of a `Term NamedDeBruijn`. This implies three things: +-- a) We ignore the name part of the nameddebruijn +-- b) We do not do equality "modulo init index, see deBruijnInitIndex". E.g. `LamAbs 0 (Var 0) /= LamAbs 1 (Var 1)`. +-- c) We do not do equality ""modulo annotations". +-- If a user wants to ignore annotations he must prior do `void <$> term`, to throw away any annotations. +deriving instance + (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) => + Eq (Term NamedDeBruijn uni fun ann) + +deriving instance + (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) => + Eq (Term DeBruijn uni fun ann) + +deriving instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann, + Eq (Term name uni fun ann) + ) => Eq (Program name uni fun ann) + -- | Check equality of two 'Term's. eqTermM :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann, HasUnique name TermUnique) diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs index 26bab7fa1b3..e8a7c96f398 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} @@ -12,18 +13,21 @@ module UntypedPlutusCore.Core.Type , TPLC.Binder (..) , Term (..) , Program (..) - , toTerm , bindFunM , bindFun , mapFun , termAnn , erase , eraseProgram + , progAnn + , progVer + , progTerm ) where import Data.Functor.Identity import PlutusPrelude +import Control.Lens import PlutusCore.Constant qualified as TPLC import PlutusCore.Core qualified as TPLC import PlutusCore.MkPlc @@ -55,7 +59,7 @@ once per program, so it's not too big a deal if it doesn't get a tag. The latter two are due to the fact that we don't have value restriction in Typed Plutus Core and hence a computation can be stuck expecting only a single type argument for the computation -to become unstuck. Therefore we can't just silently remove type abstractions and instantions and +to become unstuck. Therefore we can't just silently remove type abstractions and instantiations and need to replace them with something else that also blocks evaluation (in order for the semantics of an erased program to match with the semantics of the original typed one). 'Delay' and 'Force' serve exactly this purpose. @@ -77,9 +81,15 @@ data Term name uni fun ann deriving anyclass (NFData) -- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language. -data Program name uni fun ann = Program ann (TPLC.Version ann) (Term name uni fun ann) +-- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language. +data Program name uni fun ann = Program + { _progAnn :: ann + , _progVer :: TPLC.Version ann + , _progTerm :: Term name uni fun ann + } deriving stock (Show, Functor, Generic) deriving anyclass (NFData) +makeLenses ''Program type instance TPLC.UniOf (Term name uni fun ann) = uni @@ -105,9 +115,6 @@ instance TPLC.FromConstant (Term name uni fun ()) where type instance TPLC.HasUniques (Term name uni fun ann) = TPLC.HasUnique name TPLC.TermUnique type instance TPLC.HasUniques (Program name uni fun ann) = TPLC.HasUniques (Term name uni fun ann) -toTerm :: Program name uni fun ann -> Term name uni fun ann -toTerm (Program _ _ term) = term - -- | Return the outermost annotation of a 'Term'. termAnn :: Term name uni fun ann -> ann termAnn (Constant ann _) = ann diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs index 2c42d079d9e..ee091ce5a75 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs @@ -11,17 +11,14 @@ module UntypedPlutusCore.DeBruijn , FreeVariableError (..) , AsFreeVariableError (..) , deBruijnTerm - , deBruijnProgram , unDeBruijnTerm - , unDeBruijnProgram , unNameDeBruijn , fakeNameDeBruijn -- * unsafe api, use with care , deBruijnTermWith - , deBruijnProgramWith , unDeBruijnTermWith - , unDeBruijnProgramWith , freeIndexAsConsistentLevel + , deBruijnInitIndex ) where import PlutusCore.DeBruijn.Internal @@ -45,21 +42,6 @@ deBruijnTerm => Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann) deBruijnTerm = deBruijnTermWith freeUniqueThrow --- | Convert a 'Program' with Name's into a 'Program' with 'DeBruijn's. --- Will throw an error if a free variable is encountered. -deBruijnProgram - :: (AsFreeVariableError e, MonadError e m) - => Program Name uni fun ann -> m (Program NamedDeBruijn uni fun ann) -deBruijnProgram = deBruijnProgramWith freeUniqueThrow - --- | Takes a "handler" function to execute when encountering free variables. -deBruijnProgramWith - :: Monad m - => (Unique -> ReaderT Levels m Index) - -> Program Name uni fun ann - -> m (Program NamedDeBruijn uni fun ann) -deBruijnProgramWith h (Program ann ver term) = Program ann ver <$> deBruijnTermWith h term - -- | Convert a 'Term' with 'DeBruijn's into a 'Term' with 'Name's. -- Will throw an error if a free variable is encountered. unDeBruijnTerm @@ -67,21 +49,7 @@ unDeBruijnTerm => Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann) unDeBruijnTerm = unDeBruijnTermWith freeIndexThrow --- | Convert a 'Program' with 'DeBruijn's into a 'Program' with 'Name's. --- Will throw an error if a free variable is encountered. -unDeBruijnProgram - :: (MonadQuote m, AsFreeVariableError e, MonadError e m) - => Program NamedDeBruijn uni fun ann -> m (Program Name uni fun ann) -unDeBruijnProgram = unDeBruijnProgramWith freeIndexThrow - -- | Takes a "handler" function to execute when encountering free variables. -unDeBruijnProgramWith - :: MonadQuote m - => (Index -> ReaderT Levels m Unique) - -> Program NamedDeBruijn uni fun ann - -> m (Program Name uni fun ann) -unDeBruijnProgramWith h (Program ann ver term) = Program ann ver <$> unDeBruijnTermWith h term - deBruijnTermWith :: Monad m => (Unique -> ReaderT Levels m Index) @@ -135,7 +103,7 @@ unDeBruijnTermWithM h = go LamAbs ann n t -> -- See NOTE: [DeBruijn indices of Binders] declareBinder $ do - n' <- deBruijnToName h $ set index 0 n + n' <- deBruijnToName h $ set index deBruijnInitIndex n withScope $ LamAbs ann n' <$> go t -- boring recursive cases Apply ann t1 t2 -> Apply ann <$> go t1 <*> go t2 diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs index 225f06a096b..0a73fa8ace9 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs @@ -8,6 +8,7 @@ module UntypedPlutusCore.Evaluation.Machine.Cek ( -- * Running the machine runCek + , runCekDeBruijn , runCekNoEmit , unsafeRunCekNoEmit , evaluateCek @@ -47,24 +48,30 @@ module UntypedPlutusCore.Evaluation.Machine.Cek , readKnownCek , Hashable , PrettyUni + , unDeBruijnResult ) where import PlutusPrelude import UntypedPlutusCore.Core +import UntypedPlutusCore.DeBruijn import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts import UntypedPlutusCore.Evaluation.Machine.Cek.EmitterMode import UntypedPlutusCore.Evaluation.Machine.Cek.ExBudgetMode import UntypedPlutusCore.Evaluation.Machine.Cek.Internal +import Control.Monad.Except +import Control.Monad.State import PlutusCore.Constant import PlutusCore.Evaluation.Machine.ExMemory import PlutusCore.Evaluation.Machine.Exception import PlutusCore.Evaluation.Machine.MachineParameters import PlutusCore.Name import PlutusCore.Pretty +import PlutusCore.Quote +import Data.Bifunctor import Data.Ix (Ix) import Data.Text (Text) import Universe @@ -80,16 +87,42 @@ allow one to specify an 'ExBudgetMode'. I.e. such functions are only for fully e (and possibly returning logs). See also haddocks of 'enormousBudget'. -} +-- | Evaluate a term using the CEK machine with logging enabled and keep track of costing. +-- A wrapper around the internal runCek to debruijn input and undebruijn output. +-- TODO: remove once we expose a direct debruijn api. +runCek + :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun, Monoid cost) + => MachineParameters CekMachineCosts CekValue uni fun + -> ExBudgetMode cost uni fun + -> EmitterMode uni fun + -> Term Name uni fun () + -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost, [Text]) +runCek params mode emitMode term = + -- translating input + case runExcept @FreeVariableError $ deBruijnTerm term of + Left _ -> (error "freevarI", mempty, mempty) + Right dbt -> do + -- Don't use 'let': https://github.com/input-output-hk/plutus/issues/3876 + case runCekDeBruijn params mode emitMode dbt of + -- translating back the output + (res, cost', emit) -> (unDeBruijnResult res, cost', emit) + -- | Evaluate a term using the CEK machine with logging disabled and keep track of costing. runCekNoEmit - :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun) + :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun, Monoid cost) => MachineParameters CekMachineCosts CekValue uni fun -> ExBudgetMode cost uni fun -> Term Name uni fun () - -> (Either (CekEvaluationException uni fun) (Term Name uni fun ()), cost) + -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost) runCekNoEmit params mode term = - case runCek params mode noEmitter term of - (errOrRes, cost', _) -> (errOrRes, cost') + -- translating input + case runExcept @FreeVariableError $ deBruijnTerm term of + Left _ -> (error "freevarI", mempty) + Right dbt -> do + -- Don't use 'let': https://github.com/input-output-hk/plutus/issues/3876 + case runCekDeBruijn params mode noEmitter dbt of + -- translating back the output + (res, cost', _) -> (unDeBruijnResult res, cost') -- | Unsafely evaluate a term using the CEK machine with logging disabled and keep track of costing. -- May throw a 'CekMachineException'. @@ -97,6 +130,7 @@ unsafeRunCekNoEmit :: ( GShow uni, Typeable uni , Closed uni, uni `EverywhereAll` '[ExMemoryUsage, PrettyConst] , Ix fun, Pretty fun, Typeable fun + , Monoid cost ) => MachineParameters CekMachineCosts CekValue uni fun -> ExBudgetMode cost uni fun @@ -112,17 +146,23 @@ evaluateCek => EmitterMode uni fun -> MachineParameters CekMachineCosts CekValue uni fun -> Term Name uni fun () - -> (Either (CekEvaluationException uni fun) (Term Name uni fun ()), [Text]) + -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), [Text]) evaluateCek emitMode params term = - case runCek params restrictingEnormous emitMode term of - (errOrRes, _, logs) -> (errOrRes, logs) + -- translating input + case runExcept @FreeVariableError $ deBruijnTerm term of + Left _ -> (error "freevarI", mempty) + Right dbt -> + -- Don't use 'let': https://github.com/input-output-hk/plutus/issues/3876 + case runCekDeBruijn params restrictingEnormous emitMode dbt of + -- translating back the output + (res, _, logs) -> (unDeBruijnResult res, logs) -- | Evaluate a term using the CEK machine with logging disabled. evaluateCekNoEmit :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun) => MachineParameters CekMachineCosts CekValue uni fun -> Term Name uni fun () - -> Either (CekEvaluationException uni fun) (Term Name uni fun ()) + -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ()) evaluateCekNoEmit params = fst . runCekNoEmit params restrictingEnormous -- | Evaluate a term using the CEK machine with logging enabled. May throw a 'CekMachineException'. @@ -158,5 +198,20 @@ readKnownCek ) => MachineParameters CekMachineCosts CekValue uni fun -> Term Name uni fun () - -> Either (CekEvaluationException uni fun) a + -> Either (CekEvaluationException Name uni fun) a readKnownCek params = evaluateCekNoEmit params >=> readKnownSelf + +-- | Temporary wrapper for keeping tests the same +-- *GRACEFULLY* undebruijnifies: a) the error-cause-term (if it exists) or b) the success value-term. +-- 'Graceful' means that the (a) && (b) undebruijnifications do not throw an error upon a free variable encounter. +-- TODO: remove when we have direct debruijn api +unDeBruijnResult :: Either (CekEvaluationException NamedDeBruijn uni fun) (Term NamedDeBruijn uni fun ()) + -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ()) +unDeBruijnResult = bimap (fmap gracefulUnDeBruijn) gracefulUnDeBruijn + where + -- free debruijn indices will be turned to free, consistent uniques + gracefulUnDeBruijn :: Term NamedDeBruijn uni fun () -> Term Name uni fun () + gracefulUnDeBruijn t = runQuote + . flip evalStateT mempty + $ unDeBruijnTermWith freeIndexAsConsistentLevel t + diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/ExBudgetMode.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/ExBudgetMode.hs index bd6e33ac151..6618591fcc7 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/ExBudgetMode.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/ExBudgetMode.hs @@ -104,7 +104,7 @@ tallying = newtype RestrictingSt = RestrictingSt ExRestrictingBudget deriving stock (Eq, Show) - deriving newtype (NFData) + deriving newtype (Semigroup, Monoid, NFData) deriving anyclass (PrettyBy config) instance Pretty RestrictingSt where diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs index 735648b706f..4da4af30c74 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs @@ -44,7 +44,7 @@ module UntypedPlutusCore.Evaluation.Machine.Cek.Internal , StepKind(..) , PrettyUni , extractEvaluationResult - , runCek + , runCekDeBruijn ) where @@ -52,15 +52,15 @@ import ErrorCode import PlutusPrelude import UntypedPlutusCore.Core -import UntypedPlutusCore.Subst +import Data.DeBruijnEnv as Env import PlutusCore.Constant +import PlutusCore.DeBruijn import PlutusCore.Evaluation.Machine.ExBudget import PlutusCore.Evaluation.Machine.ExMemory import PlutusCore.Evaluation.Machine.Exception import PlutusCore.Evaluation.Machine.MachineParameters import PlutusCore.Evaluation.Result -import PlutusCore.Name import PlutusCore.Pretty import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCosts (..)) @@ -70,12 +70,12 @@ import Control.Monad.Catch import Control.Monad.Except import Control.Monad.ST import Control.Monad.ST.Unsafe -import Data.Array +import Data.Array hiding (index) import Data.Hashable (Hashable) import Data.Kind qualified as GHC import Data.Semigroup (stimes) import Data.Text (Text) -import Data.Word64Array.Word8 +import Data.Word64Array.Word8 hiding (Index) import Prettyprinter import Universe @@ -184,13 +184,13 @@ instance Show (BuiltinRuntime (CekValue uni fun)) where data CekValue uni fun = -- This bang gave us a 1-2% speed-up at the time of writing. VCon !(Some (ValueOf uni)) - | VDelay (Term Name uni fun ()) !(CekValEnv uni fun) - | VLamAbs Name (Term Name uni fun ()) !(CekValEnv uni fun) + | VDelay (Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun) + | VLamAbs NamedDeBruijn (Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun) | VBuiltin -- A partial builtin application, accumulating arguments for eventual full application. !fun -- So that we know, for what builtin we're calculating the cost. -- TODO: any chance we could sneak this into 'BuiltinRuntime' -- where we have a partially instantiated costing function anyway? - (Term Name uni fun ()) -- This must be lazy. It represents the partial application of the + (Term NamedDeBruijn uni fun ()) -- This must be lazy. It represents the partial application of the -- builtin function that we're going to run when it's fully saturated. -- We need the 'Term' to be able to return it in case full saturation -- is never achieved and a partial application needs to be returned @@ -203,7 +203,7 @@ data CekValue uni fun = -- Check the docs of 'BuiltinRuntime' for details. deriving (Show) -type CekValEnv uni fun = UniqueMap TermUnique (CekValue uni fun) +type CekValEnv uni fun = RelativizedMap (CekValue uni fun) -- | The CEK machine is parameterized over a @spendBudget@ function. This makes the budgeting machinery extensible -- and allows us to separate budgeting logic from evaluation logic and avoid branching on the union @@ -349,8 +349,9 @@ newtype CekM uni fun s a = CekM } deriving newtype (Functor, Applicative, Monad) -- | The CEK machine-specific 'EvaluationException'. -type CekEvaluationException uni fun = - EvaluationException CekUserError (MachineError fun) (Term Name uni fun ()) +-- TODO: unparameterize the `name` when we move to direct-debruijn api +type CekEvaluationException name uni fun = + EvaluationException CekUserError (MachineError fun) (Term name uni fun ()) -- | The set of constraints we need to be able to print things in universes, which we need in order to throw exceptions. type PrettyUni uni fun = (GShow uni, Closed uni, Pretty fun, Typeable uni, Typeable fun, Everywhere uni PrettyConst) @@ -392,7 +393,7 @@ throwingDischarged -> CekM uni fun s x throwingDischarged l t = throwingWithCause l t . Just . dischargeCekValue -instance PrettyUni uni fun => MonadError (CekEvaluationException uni fun) (CekM uni fun s) where +instance PrettyUni uni fun => MonadError (CekEvaluationException NamedDeBruijn uni fun) (CekM uni fun s) where -- See Note [Throwing exceptions in ST]. throwError = CekM . throwM @@ -431,28 +432,50 @@ spendBudgetCek = let (CekBudgetSpender spend) = ?cekBudgetSpender in spend -- see Note [Scoping]. -- | Instantiate all the free variables of a term by looking them up in an environment. -- Mutually recursive with dischargeCekVal. -dischargeCekValEnv :: CekValEnv uni fun -> Term Name uni fun () -> Term Name uni fun () -dischargeCekValEnv !valEnv = - -- We recursively discharge the environments of Cek values, but we will gradually end up doing - -- this to terms which have no free variables remaining, at which point we won't call this - -- substitution function any more and so we will terminate. - termSubstFreeNames $ \name -> do - val <- lookupName name valEnv - Just $ dischargeCekValue val +dischargeCekValEnv :: forall uni fun. CekValEnv uni fun -> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun () +dischargeCekValEnv valEnv@(RelativizedMap _ curLvl) = go 0 + where + -- The lamCnt is just a counter that measures how many lambda-abstractions + -- we have descended in the `go` loop. + go :: Word -> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun () + go !lamCnt = \case + LamAbs ann name body -> LamAbs ann name $ go (lamCnt+1) body + var@(Var _ (NamedDeBruijn _ ndbnIx)) -> let ix = fromIntegral ndbnIx :: Word in + if lamCnt >= ix + -- the index n is less-than-or-equal than the number of lambdas we have descended + -- this means that n points to a bound variable, so we don't discharge it. + then var + else + -- index relative to (as seen from the point of view of) the environment + let envIx = ix - lamCnt + in if envIx > curLvl + -- if the relative index is larger than current level, it means + -- that the variable is free, since we don't have such a large key stored in the env + then var + -- Although we call unsafeIndex, it must be safe, since we made the prior check that we are less-than-equal + -- to the current level. In other words, all keys less-than-equal to the current level are guaranteed to exist in the env. + else + dischargeCekValue $ valEnv `Env.unsafeIndex` envIx + Apply ann fun arg -> Apply ann (go lamCnt fun) $ go lamCnt arg + Delay ann term -> Delay ann $ go lamCnt term + Force ann term -> Force ann $ go lamCnt term + t -> t -- | Convert a 'CekValue' into a 'Term' by replacing all bound variables with the terms -- they're bound to (which themselves have to be obtain by recursively discharging values). -dischargeCekValue :: CekValue uni fun -> Term Name uni fun () +dischargeCekValue :: CekValue uni fun -> Term NamedDeBruijn uni fun () dischargeCekValue = \case - VCon val -> Constant () val - VDelay body env -> dischargeCekValEnv env $ Delay () body + VCon val -> Constant () val + VDelay body env -> dischargeCekValEnv env $ Delay () body -- 'computeCek' turns @LamAbs _ name body@ into @VLamAbs name body env@ where @env@ is an -- argument of 'computeCek' and hence we need to start discharging outside of the reassembled -- lambda, otherwise @name@ could clash with the names that we have in @env@. - VLamAbs name body env -> dischargeCekValEnv env $ LamAbs () name body + VLamAbs (NamedDeBruijn n _ix) body env -> + -- The index on the binder is meaningless, we put `0` by convention, see 'Binder'. + dischargeCekValEnv env $ LamAbs () (NamedDeBruijn n deBruijnInitIndex) body -- We only discharge a value when (a) it's being returned by the machine, -- or (b) it's needed for an error message. - VBuiltin _ term env _ -> dischargeCekValEnv env term + VBuiltin _ term env _ -> dischargeCekValEnv env term instance (Closed uni, GShow uni, uni `Everywhere` PrettyConst, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun) where @@ -475,7 +498,7 @@ we can match on context and the top frame in a single, strict pattern match. -} data Context uni fun = FrameApplyFun !(CekValue uni fun) !(Context uni fun) -- ^ @[V _]@ - | FrameApplyArg !(CekValEnv uni fun) (Term Name uni fun ()) !(Context uni fun) -- ^ @[_ N]@ + | FrameApplyArg !(CekValEnv uni fun) (Term NamedDeBruijn uni fun ()) !(Context uni fun) -- ^ @[_ N]@ | FrameForce !(Context uni fun) -- ^ @(force _)@ | NoFrame deriving (Show) @@ -500,7 +523,7 @@ runCekM -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> (forall s. GivenCekReqs uni fun s => CekM uni fun s a) - -> (Either (CekEvaluationException uni fun) a, cost, [Text]) + -> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost, [Text]) runCekM (MachineParameters costs runtime) (ExBudgetMode getExBudgetInfo) (EmitterMode getEmitterMode) a = runST $ do ExBudgetInfo{_exBudgetModeSpender, _exBudgetModeGetFinal, _exBudgetModeGetCumulative} <- getExBudgetInfo CekEmitterInfo{_cekEmitterInfoEmit, _cekEmitterInfoGetFinal} <- getEmitterMode _exBudgetModeGetCumulative @@ -515,15 +538,10 @@ runCekM (MachineParameters costs runtime) (ExBudgetMode getExBudgetInfo) (Emitte logs <- _cekEmitterInfoGetFinal pure (errOrRes, st, logs) --- | Extend an environment with a variable name, the value the variable stands for --- and the environment the value is defined in. -extendEnv :: Name -> CekValue uni fun -> CekValEnv uni fun -> CekValEnv uni fun -extendEnv = insertByName - -- | Look up a variable name in the environment. -lookupVarName :: forall uni fun s . (PrettyUni uni fun) => Name -> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun) -lookupVarName varName varEnv = - case lookupName varName varEnv of +lookupVarName :: forall uni fun s . (PrettyUni uni fun) => NamedDeBruijn -> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun) +lookupVarName varName@(NamedDeBruijn _ varIx) varEnv = + case varEnv `Env.index` fromIntegral varIx of Nothing -> throwingWithCause _MachineError OpenTermEvaluatedMachineError $ Just var where var = Var () varName Just val -> pure val @@ -534,7 +552,7 @@ lookupVarName varName varEnv = evalBuiltinApp :: (GivenCekReqs uni fun s, PrettyUni uni fun) => fun - -> Term Name uni fun () + -> Term NamedDeBruijn uni fun () -> CekValEnv uni fun -> BuiltinRuntime (CekValue uni fun) -> CekM uni fun s (CekValue uni fun) @@ -552,8 +570,8 @@ enterComputeCek . (Ix fun, PrettyUni uni fun, GivenCekReqs uni fun s, uni `Everywhere` ExMemoryUsage) => Context uni fun -> CekValEnv uni fun - -> Term Name uni fun () - -> CekM uni fun s (Term Name uni fun ()) + -> Term NamedDeBruijn uni fun () + -> CekM uni fun s (Term NamedDeBruijn uni fun ()) enterComputeCek = computeCek (toWordArray 0) where -- | The computing part of the CEK machine. -- Either @@ -565,8 +583,8 @@ enterComputeCek = computeCek (toWordArray 0) where :: WordArray -> Context uni fun -> CekValEnv uni fun - -> Term Name uni fun () - -> CekM uni fun s (Term Name uni fun ()) + -> Term NamedDeBruijn uni fun () + -> CekM uni fun s (Term NamedDeBruijn uni fun ()) -- s ; ρ ▻ {L A} ↦ s , {_ A} ; ρ ▻ L computeCek !unbudgetedSteps !ctx !env (Var _ varName) = do !unbudgetedSteps' <- stepAndMaybeSpend BVar unbudgetedSteps @@ -613,7 +631,7 @@ enterComputeCek = computeCek (toWordArray 0) where :: WordArray -> Context uni fun -> CekValue uni fun - -> CekM uni fun s (Term Name uni fun ()) + -> CekM uni fun s (Term NamedDeBruijn uni fun ()) --- Instantiate all the free variable of the resulting term in case there are any. -- . ◅ V ↦ [] V returnCek !unbudgetedSteps NoFrame val = do @@ -639,7 +657,7 @@ enterComputeCek = computeCek (toWordArray 0) where :: WordArray -> Context uni fun -> CekValue uni fun - -> CekM uni fun s (Term Name uni fun ()) + -> CekM uni fun s (Term NamedDeBruijn uni fun ()) forceEvaluate !unbudgetedSteps !ctx (VDelay body env) = computeCek unbudgetedSteps ctx env body forceEvaluate !unbudgetedSteps !ctx (VBuiltin fun term env (BuiltinRuntime sch f exF)) = do let term' = Force () term @@ -670,9 +688,9 @@ enterComputeCek = computeCek (toWordArray 0) where -> Context uni fun -> CekValue uni fun -- lhs of application -> CekValue uni fun -- rhs of application - -> CekM uni fun s (Term Name uni fun ()) - applyEvaluate !unbudgetedSteps !ctx (VLamAbs name body env) arg = - computeCek unbudgetedSteps ctx (extendEnv name arg env) body + -> CekM uni fun s (Term NamedDeBruijn uni fun ()) + applyEvaluate !unbudgetedSteps !ctx (VLamAbs _ body env) arg = + computeCek unbudgetedSteps ctx (Env.cons arg env) body -- Annotating @f@ and @exF@ with bangs gave us some speed-up, but only until we added a bang to -- 'VCon'. After that the bangs here were making things a tiny bit slower and so we removed them. applyEvaluate !unbudgetedSteps !ctx (VBuiltin fun term env (BuiltinRuntime sch f exF)) arg = do @@ -720,14 +738,14 @@ enterComputeCek = computeCek (toWordArray 0) where -- See Note [Compilation peculiarities]. -- | Evaluate a term using the CEK machine and keep track of costing, logging is optional. -runCek +runCekDeBruijn :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun) => MachineParameters CekMachineCosts CekValue uni fun -> ExBudgetMode cost uni fun -> EmitterMode uni fun - -> Term Name uni fun () - -> (Either (CekEvaluationException uni fun) (Term Name uni fun ()), cost, [Text]) -runCek params mode emitMode term = + -> Term NamedDeBruijn uni fun () + -> (Either (CekEvaluationException NamedDeBruijn uni fun) (Term NamedDeBruijn uni fun ()), cost, [Text]) +runCekDeBruijn params mode emitMode term = runCekM params mode emitMode $ do spendBudgetCek BStartup (cekStartupCost ?cekCosts) - enterComputeCek NoFrame mempty term + enterComputeCek NoFrame Env.empty term diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Simplify.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Simplify.hs index f8f9e1cd998..74beefa1f5b 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Simplify.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Simplify.hs @@ -2,16 +2,12 @@ -- | Very basic simplifications on UPLC. module UntypedPlutusCore.Transform.Simplify ( simplifyTerm - , simplifyProgram ) where import UntypedPlutusCore.Core import Control.Lens (transformOf) -simplifyProgram :: Program name uni fun a -> Program name uni fun a -simplifyProgram (Program a v t) = Program a v $ simplifyTerm t - simplifyTerm :: Term name uni fun a -> Term name uni fun a simplifyTerm = transformOf termSubterms processTerm diff --git a/plutus-core/untyped-plutus-core/test/DeBruijn/Spec.hs b/plutus-core/untyped-plutus-core/test/DeBruijn/Spec.hs index 0e2f326bb90..1ed9e44e9b3 100644 --- a/plutus-core/untyped-plutus-core/test/DeBruijn/Spec.hs +++ b/plutus-core/untyped-plutus-core/test/DeBruijn/Spec.hs @@ -6,6 +6,7 @@ import Common import Control.Monad.Except import Control.Monad.State import Data.Semigroup +import PlutusCore (defaultVersion) import PlutusCore.Default import PlutusCore.Error import PlutusCore.MkPlc @@ -14,9 +15,9 @@ import PlutusCore.Quote import Test.Tasty import UntypedPlutusCore as UPLC --- Note: The point of these tests is that --- binders with wrong indices will be undebruinified successfully, whereas --- variables with wrong indices (e.g. out of scope) will fail. +-- Note: This tests two things during undebruijnification: +-- 1) binders with wrong indices will be undebruinified successfully +-- 2) variables with wrong indices (e.g. out of scope) will fail to undebruijnify -- (lam x_0 x_1) okId0 :: UPLC.Term DeBruijn DefaultUni DefaultFun () @@ -90,13 +91,14 @@ test_debruijn = runTestNestedIn ["untyped-plutus-core","test"] $ ] ] where - actThrow = prettyPlcClassicDebug . runExcept @(Error DefaultUni DefaultFun ()) . runQuoteT . unDeBruijnProgram . mkProg + actThrow = prettyPlcClassicDebug . runExcept @(Error DefaultUni DefaultFun ()) . runQuoteT . progTerm unDeBruijnTerm . mkProg - actGrace = prettyPlcClassicDebug . runExcept @(Error DefaultUni DefaultFun ()) . runQuoteT - . flip evalStateT mempty - . unDeBruijnProgramWith freeIndexAsConsistentLevel . mkProg + actGrace = prettyPlcClassicDebug . runExcept @(Error DefaultUni DefaultFun ()) + . runQuoteT + . flip evalStateT mempty + . progTerm (unDeBruijnTermWith freeIndexAsConsistentLevel) . mkProg - mkProg = programMapNames fakeNameDeBruijn . Program () (Version () 1 0 0) + mkProg = Program () (defaultVersion ()) . termMapNames fakeNameDeBruijn tests = [("okId0", okId0) ,("okId99", okId99) diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Common.hs b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Common.hs index a6e54dfaa57..46598a90adf 100644 --- a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Common.hs +++ b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Common.hs @@ -60,5 +60,5 @@ typecheckReadKnownCek ) => MachineParameters CekMachineCosts CekValue uni fun -> TPLC.Term TyName Name uni fun () - -> m (Either (CekEvaluationException uni fun) a) + -> m (Either (CekEvaluationException Name uni fun) a) typecheckReadKnownCek = typecheckAnd readKnownCek diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/closure.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/closure.uplc.golden index 9d17ef9a5a4..c37c65ee4b3 100644 --- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/closure.uplc.golden +++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/closure.uplc.golden @@ -1 +1 @@ -(Right (lam j_1 (con integer 1))) \ No newline at end of file +(Right (lam j_0 (con integer 1))) \ No newline at end of file diff --git a/plutus-errors/src/Errors/TH/GenDocs.hs b/plutus-errors/src/Errors/TH/GenDocs.hs index 4667c986a5d..90a108c9a24 100644 --- a/plutus-errors/src/Errors/TH/GenDocs.hs +++ b/plutus-errors/src/Errors/TH/GenDocs.hs @@ -15,7 +15,7 @@ import Prettyprinter qualified as PP genDocs :: Q [TH.Dec] genDocs = let allCodes = $(genCodes allErrors) in case findDuplicates allCodes of - [] -> pure $ fmap mkTySyn (zip allErrors allCodes) + [] -> pure $ fmap mkTySyn (sortOn snd $ zip allErrors allCodes) -- Fail at compile time if duplicate error codes are found. dups -> fail $ "ErrorCode instances have some duplicate error-code numbers: " ++ (show $ PP.pretty dups) diff --git a/plutus-ledger-api/src/Plutus/V1/Ledger/Api.hs b/plutus-ledger-api/src/Plutus/V1/Ledger/Api.hs index dbf9c5cd4f7..08578a42377 100644 --- a/plutus-ledger-api/src/Plutus/V1/Ledger/Api.hs +++ b/plutus-ledger-api/src/Plutus/V1/Ledger/Api.hs @@ -124,8 +124,7 @@ import Plutus.V1.Ledger.Credential import Plutus.V1.Ledger.Crypto import Plutus.V1.Ledger.DCert import Plutus.V1.Ledger.Interval hiding (singleton) -import Plutus.V1.Ledger.Scripts hiding (mkTermToEvaluate) -import Plutus.V1.Ledger.Scripts qualified as Scripts +import Plutus.V1.Ledger.Scripts as Scripts import Plutus.V1.Ledger.Time import Plutus.V1.Ledger.TxId import Plutus.V1.Ledger.Value @@ -178,7 +177,7 @@ type SerializedScript = ShortByteString -- | Errors that can be thrown when evaluating a Plutus script. data EvaluationError = - CekError (UPLC.CekEvaluationException PLC.DefaultUni PLC.DefaultFun) -- ^ An error from the evaluator itself + CekError (UPLC.CekEvaluationException PLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun) -- ^ An error from the evaluator itself | DeBruijnError PLC.FreeVariableError -- ^ An error in the pre-evaluation step of converting from de-Bruijn indices | CodecError CBOR.DeserialiseFailure -- ^ A serialisation error | IncompatibleVersionError (PLC.Version ()) -- ^ An error indicating a version tag that we don't support @@ -194,12 +193,15 @@ instance Pretty EvaluationError where pretty CostModelParameterMismatch = "Cost model parameters were not as we expected" -- | Shared helper for the evaluation functions, deserializes the 'SerializedScript' , applies it to its arguments, and un-deBruijn-ifies it. -mkTermToEvaluate :: (MonadError EvaluationError m) => SerializedScript -> [PLC.Data] -> m (UPLC.Term UPLC.Name PLC.DefaultUni PLC.DefaultFun ()) +mkTermToEvaluate :: (MonadError EvaluationError m) => SerializedScript -> [PLC.Data] -> m (UPLC.Term UPLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun ()) mkTermToEvaluate bs args = do s@(Script (UPLC.Program _ v _)) <- liftEither $ first CodecError $ CBOR.deserialiseOrFail $ fromStrict $ fromShort bs unless (v == PLC.defaultVersion ()) $ throwError $ IncompatibleVersionError v - UPLC.Program _ _ t <- liftEither $ first DeBruijnError $ Scripts.mkTermToEvaluate (Scripts.applyArguments s args) - pure t + let t = UPLC._progTerm $ unScript $ Scripts.applyArguments s args + -- add fake names to keep the api working on NamedDeBruijn + pure $ UPLC.termMapNames UPLC.fakeNameDeBruijn t + + -- | Evaluates a script, with a cost model and a budget that restricts how many -- resources it can use according to the cost model. Also returns the budget that @@ -221,7 +223,7 @@ evaluateScriptRestricting verbose cmdata budget p args = swap $ runWriter @LogOu Nothing -> throwError CostModelParameterMismatch let (res, UPLC.RestrictingSt (PLC.ExRestrictingBudget final), logs) = - UPLC.runCek + UPLC.runCekDeBruijn (toMachineParameters model) (UPLC.restricting $ PLC.ExRestrictingBudget budget) (if verbose == Verbose then UPLC.logEmitter else UPLC.noEmitter) @@ -248,7 +250,7 @@ evaluateScriptCounting verbose cmdata p args = swap $ runWriter @LogOutput $ run Nothing -> throwError CostModelParameterMismatch let (res, UPLC.CountingSt final, logs) = - UPLC.runCek + UPLC.runCekDeBruijn (toMachineParameters model) UPLC.counting (if verbose == Verbose then UPLC.logEmitter else UPLC.noEmitter) diff --git a/plutus-ledger-api/src/Plutus/V1/Ledger/Scripts.hs b/plutus-ledger-api/src/Plutus/V1/Ledger/Scripts.hs index 32e1995dd70..325cebb7cfe 100644 --- a/plutus-ledger-api/src/Plutus/V1/Ledger/Scripts.hs +++ b/plutus-ledger-api/src/Plutus/V1/Ledger/Scripts.hs @@ -33,7 +33,6 @@ module Plutus.V1.Ledger.Scripts( applyValidator, applyMintingPolicyScript, applyStakeValidatorScript, - mkTermToEvaluate, applyArguments, -- * Script wrappers mkValidatorScript, @@ -65,7 +64,7 @@ import Prelude qualified as Haskell import Codec.CBOR.Decoding (decodeBytes) import Codec.Serialise (Serialise, decode, encode, serialise) import Control.DeepSeq (NFData) -import Control.Monad.Except (MonadError, runExceptT, throwError) +import Control.Monad.Except (MonadError, throwError) import Data.Aeson (FromJSON, FromJSONKey, ToJSON, ToJSONKey) import Data.Aeson qualified as JSON import Data.Aeson.Extras qualified as JSON @@ -80,13 +79,12 @@ import Plutus.V1.Ledger.Bytes (LedgerBytes (..)) import Plutus.V1.Ledger.Orphans () import PlutusCore qualified as PLC import PlutusCore.Data qualified as PLC -import PlutusCore.DeBruijn qualified as PLC import PlutusCore.Evaluation.Machine.ExBudget qualified as PLC +import PlutusCore.Evaluation.Machine.Exception (ErrorWithCause (..), EvaluationError (..)) import PlutusCore.MkPlc qualified as PLC import PlutusTx (CompiledCode, FromData (..), ToData (..), UnsafeFromData (..), getPlc, makeLift) import PlutusTx.Builtins as Builtins import PlutusTx.Builtins.Internal as BI -import PlutusTx.Evaluation (ErrorWithCause (..), EvaluationError (..), evaluateCekTrace) import PlutusTx.Prelude import Prettyprinter import Prettyprinter.Extras @@ -174,7 +172,6 @@ fromPlc (UPLC.Program a v t) = data ScriptError = EvaluationError [Text] Haskell.String -- ^ Expected behavior of the engine (e.g. user-provided error) | EvaluationException Haskell.String Haskell.String -- ^ Unexpected behavior of the engine (a bug) - | MalformedScript Haskell.String -- ^ Script is wrong in some way deriving (Haskell.Show, Haskell.Eq, Generic, NFData) deriving anyclass (ToJSON, FromJSON) @@ -184,38 +181,28 @@ applyArguments (Script (UPLC.Program a v t)) args = applied = PLC.mkIterApp () t termArgs in Script (UPLC.Program a v applied) -mkTermToEvaluate :: Script -> Either PLC.FreeVariableError (UPLC.Program UPLC.Name PLC.DefaultUni PLC.DefaultFun ()) -mkTermToEvaluate (Script (UPLC.Program a v t)) = - -- TODO: evaluate the nameless debruijn program directly - let named = UPLC.termMapNames PLC.fakeNameDeBruijn t - namedProgram = UPLC.Program a v named - in PLC.runQuote $ runExceptT @PLC.FreeVariableError $ UPLC.unDeBruijnProgram namedProgram - -- | Evaluate a script, returning the trace log. evaluateScript :: forall m . (MonadError ScriptError m) => Script -> m (PLC.ExBudget, [Text]) evaluateScript s = do - p <- case mkTermToEvaluate s of - Right p -> Haskell.return p - Left e -> throwError $ MalformedScript $ Haskell.show e - let (logOut, UPLC.TallyingSt _ budget, result) = evaluateCekTrace p + let t = UPLC.termMapNames UPLC.fakeNameDeBruijn $ UPLC._progTerm $ unScript s + (result, UPLC.TallyingSt _ budget, logOut) = UPLC.runCekDeBruijn PLC.defaultCekParameters UPLC.tallying UPLC.logEmitter t case result of - Right _ -> Haskell.pure () + Right _ -> Haskell.pure (budget, logOut) Left errWithCause@(ErrorWithCause err cause) -> throwError $ case err of InternalEvaluationError internalEvalError -> EvaluationException (Haskell.show errWithCause) (PLC.show internalEvalError) UserEvaluationError evalError -> EvaluationError logOut (mkError evalError cause) -- TODO fix this error channel fuckery - Haskell.pure (budget, logOut) -- | Create an error message from the contents of an ErrorWithCause. -- If the cause of an error is a `Just t` where `t = b v0 v1 .. vn` for some builtin `b` then -- the error will be a "BuiltinEvaluationFailure" otherwise it will be `PLC.show evalError` -mkError :: UPLC.CekUserError -> Maybe (UPLC.Term UPLC.Name PLC.DefaultUni PLC.DefaultFun ()) -> String +mkError :: UPLC.CekUserError -> Maybe (UPLC.Term UPLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun ()) -> String mkError evalError Nothing = PLC.show evalError mkError evalError (Just t) = case findBuiltin t of Just b -> "BuiltinEvaluationFailure of " ++ Haskell.show b Nothing -> PLC.show evalError where - findBuiltin :: UPLC.Term UPLC.Name PLC.DefaultUni PLC.DefaultFun () -> Maybe PLC.DefaultFun + findBuiltin :: UPLC.Term UPLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun () -> Maybe PLC.DefaultFun findBuiltin t = case t of UPLC.Apply _ t _ -> findBuiltin t UPLC.Builtin _ fun -> Just fun diff --git a/plutus-ledger-api/test/Spec/Eval.hs b/plutus-ledger-api/test/Spec/Eval.hs index 15150ee3064..cf697bb97c9 100644 --- a/plutus-ledger-api/test/Spec/Eval.hs +++ b/plutus-ledger-api/test/Spec/Eval.hs @@ -24,6 +24,7 @@ For this test-suite we write the programs directly in the UPLC AST, bypassing the GHC typechecker & compiler, the PIR typechecker & compiler and the PLC typechecker. The reason is that users can submit such hand-crafted code, and we want to test how it behaves. Because this is part of our API, we have to be careful not to change the behaviour of even weird untypeable programs. +In particular, We test both the offline part (Scripts module) and the online part (API module). -} -- (delay outOfScope) @@ -66,7 +67,7 @@ outITELazy = mkIterApp () ] -- [(force (builtin ifThenElse)) (con bool True) (con bool True) (con unit ())] --- Note that the branches have **different** types. +-- Note that the branches have **different** types. The machine cannot catch such a type error. illITEStrict :: UPLC.Term DeBruijn DefaultUni DefaultFun () illITEStrict = mkIterApp () (Force () (Builtin () IfThenElse)) @@ -76,7 +77,7 @@ illITEStrict = mkIterApp () ] -- [(force (builtin ifThenElse)) (con bool True) (lam x (con bool True)) (lam x (con unit ()))] --- The branches are *lazy*. Note that the branches have **different** types. +-- The branches are *lazy*. Note that the branches have **different** types. The machine cannot catch such a type error. illITELazy :: UPLC.Term DeBruijn DefaultUni DefaultFun () illITELazy = mkIterApp () (Force () (Builtin () IfThenElse)) @@ -113,42 +114,36 @@ illOverApp = mkIterApp () testOffline :: TestNested testOffline = pure . testCase "offline" $ do - eval outDelay @?= False - eval outLam @?= False - eval outConst @?= False + eval outDelay @?= True + eval outLam @?= True + eval outConst @?= True eval outITEStrict @?= False - eval outITELazy @?= False + eval outITELazy @?= True + eval illITEStrict @?= True + eval illITELazy @?= True eval illAdd @?= False eval illOverSat @?= False eval illOverApp @?= False - -- some ill-typed expressions cannot be caught by the machine - eval illITEStrict @?= True - eval illITELazy @?= True where eval :: UPLC.Term DeBruijn DefaultUni DefaultFun () -> Bool - eval = isRight . runExcept . evaluateScript . Script . mkProg + eval = isRight . runExcept . Scripts.evaluateScript . Script . mkProg {-| Evaluates scripts as they will be evaluated on-chain, by using the evaluation function we provide for the ledger. Notably, this goes via serializing and deserializing the program, so we can see any errors that might arise from that. -Currently, this includes de Bruijn conversion, but this will go away once we change the evaluator to operate -on de Bruijn indices directly. -currently behaves similar to offlineEvalExternal, because any out-of-scope errors will be caught by -the undebruinification step of mkTermToEvaluate. Subject to change by direct debruijn branch. -} testOnline :: TestNested testOnline = pure . testCase "online" $ do - eval outDelay @?= False - eval outLam @?= False - eval outConst @?= False + eval outDelay @?= True + eval outLam @?= True + eval outConst @?= True eval outITEStrict @?= False - eval outITELazy @?= False + eval outITELazy @?= True + eval illITEStrict @?= True + eval illITELazy @?= True eval illAdd @?= False eval illOverSat @?= False eval illOverApp @?= False - -- some ill-typed expressions cannot be caught by the machine - eval illITEStrict @?= True - eval illITELazy @?= True where eval :: UPLC.Term DeBruijn DefaultUni DefaultFun () -> Bool eval t = @@ -161,7 +156,6 @@ tests = runTestNestedIn ["plutus-ledger-api"] $ testNested "eval" [ testOffline , testOnline - -- TODO: implement testOfflineInternal for cek-debruijn branch using Cek.Internal, to show that also no out-of-scope will be caught ] diff --git a/plutus-metatheory/src/Main.lagda b/plutus-metatheory/src/Main.lagda index abb39688d5a..28d0fdf4e79 100644 --- a/plutus-metatheory/src/Main.lagda +++ b/plutus-metatheory/src/Main.lagda @@ -147,15 +147,16 @@ postulate {-# COMPILE GHC unconvTy = unconvT 0 #-} {-# COMPILE GHC unconvTm = unconv 0 #-} {-# FOREIGN GHC import Data.Bifunctor #-} +{-# FOREIGN GHC import Data.Functor #-} {-# COMPILE GHC ParseError = type ParseError () #-} -{-# COMPILE GHC parse = first (() <$) . runQuote . runExceptT . parseProgram #-} -{-# COMPILE GHC parseU = first (() <$) . runQuote . runExceptT . U.parseProgram #-} -{-# COMPILE GHC parseTm = first (() <$) . runQuote. runExceptT . parseTerm #-} -{-# COMPILE GHC parseTy = first (() <$) . runQuote . runExceptT . parseType #-} -{-# COMPILE GHC deBruijnify = second (() <$) . runExcept . deBruijnProgram #-} -{-# COMPILE GHC deBruijnifyTm = second (() <$) . runExcept . deBruijnTerm #-} -{-# COMPILE GHC deBruijnifyTy = second (() <$) . runExcept . deBruijnTy #-} +{-# COMPILE GHC parse = first void . runQuote . runExceptT . parseProgram #-} +{-# COMPILE GHC parseU = first void . runQuote . runExceptT . U.parseProgram #-} +{-# COMPILE GHC parseTm = first void . runQuote. runExceptT . parseTerm #-} +{-# COMPILE GHC parseTy = first void . runQuote . runExceptT . parseType #-} +{-# COMPILE GHC deBruijnify = \ (Program ann ver tm) -> second (void . Program ann ver) . runExcept $ deBruijnTerm tm #-} +{-# COMPILE GHC deBruijnifyTm = second void . runExcept . deBruijnTerm #-} +{-# COMPILE GHC deBruijnifyTy = second void . runExcept . deBruijnTy #-} {-# FOREIGN GHC import PlutusCore #-} {-# COMPILE GHC ProgramN = type PlutusCore.Program TyName Name DefaultUni DefaultFun PlutusCore.Lexer.AlexPosn #-} {-# COMPILE GHC Program = type PlutusCore.Program NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun () #-} @@ -169,9 +170,9 @@ postulate {-# COMPILE GHC ProgramU = type U.Program NamedDeBruijn DefaultUni DefaultFun () #-} {-# COMPILE GHC TermNU = type U.Term Name DefaultUni DefaultFun PlutusCore.Lexer.AlexPosn #-} {-# COMPILE GHC TermU = type U.Term NamedDeBruijn DefaultUni DefaultFun () #-} -{-# COMPILE GHC deBruijnifyU = second (() <$) . runExcept . U.deBruijnProgram #-} -{-# COMPILE GHC deBruijnifyTmU = second (() <$) . runExcept . U.deBruijnTerm #-} -{-# COMPILE GHC parseTmU = first (() <$) . runQuote. runExceptT . U.parseTerm #-} +{-# COMPILE GHC deBruijnifyU = \ (U.Program ann ver tm) -> second (void . U.Program ann ver) . runExcept $ U.deBruijnTerm tm #-} +{-# COMPILE GHC deBruijnifyTmU = second void . runExcept . U.deBruijnTerm #-} +{-# COMPILE GHC parseTmU = first void . runQuote. runExceptT . U.parseTerm #-} {-# COMPILE GHC convTmU = U.conv #-} {-# COMPILE GHC unconvTmU = U.uconv 0 #-} diff --git a/plutus-metatheory/src/Raw.hs b/plutus-metatheory/src/Raw.hs index c20be876b1f..d227a8e6f36 100644 --- a/plutus-metatheory/src/Raw.hs +++ b/plutus-metatheory/src/Raw.hs @@ -6,8 +6,6 @@ {-# LANGUAGE TypeApplications #-} module Raw where -import GHC.Natural - import Data.ByteString as BS import Data.Text qualified as T import PlutusCore @@ -52,7 +50,7 @@ data RTerm = RVar Integer deriving Show unIndex :: Index -> Integer -unIndex (Index n) = naturalToInteger n +unIndex (Index n) = toInteger n convP :: Program NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm convP (Program _ _ t) = conv t @@ -92,15 +90,15 @@ conv (IWrap _ ty1 ty2 t) = RWrap (convT ty1) (convT ty2) (conv t) conv (Error _ _A) = RError (convT _A) varTm :: Int -> NamedDeBruijn -varTm i = NamedDeBruijn (T.pack [tmnames !! i]) (Index (naturalFromInteger 0)) +varTm i = NamedDeBruijn (T.pack [tmnames !! i]) deBruijnInitIndex varTy :: Int -> NamedDeBruijn -varTy i = NamedDeBruijn (T.pack [tynames !! i]) (Index (naturalFromInteger 0)) +varTy i = NamedDeBruijn (T.pack [tynames !! i]) deBruijnInitIndex -- this should take a level and render levels as names unconvT :: Int -> RType -> Type NamedTyDeBruijn DefaultUni () unconvT i (RTyVar x) = - TyVar () (NamedTyDeBruijn (NamedDeBruijn (T.pack [tynames !! (i - fromIntegral x)]) (Index (naturalFromInteger x)))) + TyVar () (NamedTyDeBruijn (NamedDeBruijn (T.pack [tynames !! (i - fromIntegral x)]) (Index (fromInteger x)))) unconvT i (RTyFun t u) = TyFun () (unconvT i t) (unconvT i u) unconvT i (RTyPi k t) = TyForall () (NamedTyDeBruijn (varTy i)) k (unconvT (i+1) t) @@ -144,7 +142,7 @@ tynames = ['A' .. 'Z'] unconv :: Int -> RTerm -> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun () unconv i (RVar x) = - Var () (NamedDeBruijn (T.pack [tmnames !! (i - fromIntegral x )]) (Index (naturalFromInteger x))) + Var () (NamedDeBruijn (T.pack [tmnames !! (i - fromInteger x )]) (Index (fromInteger x))) unconv i (RTLambda k tm) = TyAbs () (NamedTyDeBruijn (varTy i)) k (unconv (i+1) tm) unconv i (RTApp t ty) = TyInst () (unconv i t) (unconvT i ty) unconv i (RLambda ty tm) = LamAbs () (varTm i) (unconvT (i+1) ty) (unconv (i+1) tm) diff --git a/plutus-metatheory/src/Untyped.hs b/plutus-metatheory/src/Untyped.hs index 634965931c7..138851fbbb4 100644 --- a/plutus-metatheory/src/Untyped.hs +++ b/plutus-metatheory/src/Untyped.hs @@ -8,7 +8,6 @@ import UntypedPlutusCore import Data.ByteString as BS import Data.Text as T -import GHC.Natural import Universe @@ -25,7 +24,7 @@ data UTerm = UVar Integer deriving Show unIndex :: Index -> Integer -unIndex (Index n) = naturalToInteger n +unIndex (Index n) = toInteger n convP :: Program NamedDeBruijn DefaultUni DefaultFun a -> UTerm convP (Program _ _ t) = conv t @@ -45,11 +44,11 @@ tmnames = ['a' .. 'z'] uconv :: Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun () uconv i (UVar x) = Var () - (NamedDeBruijn (T.pack [tmnames !! (i - 1 - fromIntegral x)]) - (Index (naturalFromInteger x))) + (NamedDeBruijn (T.pack [tmnames !! (i - 1 - fromInteger x)]) + (Index (fromInteger x))) uconv i (ULambda t) = LamAbs () - (NamedDeBruijn (T.pack [tmnames !! i]) (Index 0)) + (NamedDeBruijn (T.pack [tmnames !! i]) deBruijnInitIndex) (uconv (i+1) t) uconv i (UApp t u) = Apply () (uconv i t) (uconv i u) uconv i (UCon c) = Constant () c diff --git a/plutus-tx-plugin/src/PlutusTx/Plugin.hs b/plutus-tx-plugin/src/PlutusTx/Plugin.hs index 9e478e12308..8c2b04ebe2b 100644 --- a/plutus-tx-plugin/src/PlutusTx/Plugin.hs +++ b/plutus-tx-plugin/src/PlutusTx/Plugin.hs @@ -416,7 +416,7 @@ runCompiler moduleName opts expr = do when (poDoTypecheck opts) . void $ liftExcept $ PLC.typecheckPipeline plcTcConfig plcP - uplcP <- liftExcept $ UPLC.deBruijnProgram $ UPLC.simplifyProgram $ UPLC.eraseProgram plcP + uplcP <- liftExcept $ traverseOf UPLC.progTerm (UPLC.deBruijnTerm . UPLC.simplifyTerm) $ UPLC.eraseProgram plcP when (poDumpUPlc opts) . liftIO $ dumpFlat uplcP "untyped PLC program" (moduleName ++ ".uplc.flat") pure (spirP, uplcP) diff --git a/plutus-tx-plugin/test/Budget/Lib.hs b/plutus-tx-plugin/test/Budget/Lib.hs index 9da8db43fcf..242b2a60f92 100644 --- a/plutus-tx-plugin/test/Budget/Lib.hs +++ b/plutus-tx-plugin/test/Budget/Lib.hs @@ -12,10 +12,10 @@ import Common import PlutusCore qualified as PLC import PlutusCore.Evaluation.Machine.ExBudget qualified as PLC import PlutusTx.Code (CompiledCode, getPlc) -import PlutusTx.Evaluation qualified as PlutusTx import UntypedPlutusCore qualified as UPLC import UntypedPlutusCore.Evaluation.Machine.Cek qualified as UPLC +import Control.Lens import Control.Monad.Except (runExceptT) import Control.Monad.Reader qualified as Reader import Data.Text qualified as Text @@ -35,10 +35,10 @@ measureBudget :: CompiledCode a -> Maybe PLC.ExBudget measureBudget compiledCode = let programE = PLC.runQuote $ runExceptT @PLC.FreeVariableError - $ UPLC.unDeBruijnProgram + $ traverseOf UPLC.progTerm UPLC.unDeBruijnTerm $ getPlc compiledCode in case programE of Left _ -> Nothing Right program -> - let (_, UPLC.TallyingSt _ budget, _) = PlutusTx.evaluateCekTrace program + let (_, UPLC.TallyingSt _ budget) = UPLC.runCekNoEmit PLC.defaultCekParameters UPLC.tallying $ program ^. UPLC.progTerm in Just budget diff --git a/plutus-tx-plugin/test/IsData/bytestring.plc.golden b/plutus-tx-plugin/test/IsData/bytestring.plc.golden index 5f8d817475c..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/bytestring.plc.golden +++ b/plutus-tx-plugin/test/IsData/bytestring.plc.golden @@ -1 +1 @@ -(delay (lam case_True_98 (lam case_False_99 case_True_98))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/int.plc.golden b/plutus-tx-plugin/test/IsData/int.plc.golden index 016160b8140..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/int.plc.golden +++ b/plutus-tx-plugin/test/IsData/int.plc.golden @@ -1 +1 @@ -(delay (lam case_True_45 (lam case_False_46 case_True_45))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/list.plc.golden b/plutus-tx-plugin/test/IsData/list.plc.golden index b1d33437a89..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/list.plc.golden +++ b/plutus-tx-plugin/test/IsData/list.plc.golden @@ -1 +1 @@ -(delay (lam case_True_134 (lam case_False_135 case_True_134))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/mono.plc.golden b/plutus-tx-plugin/test/IsData/mono.plc.golden index 8bdf6bc9da5..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/mono.plc.golden +++ b/plutus-tx-plugin/test/IsData/mono.plc.golden @@ -1 +1 @@ -(delay (lam case_True_158 (lam case_False_159 case_True_158))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/nested.plc.golden b/plutus-tx-plugin/test/IsData/nested.plc.golden index 5715078a2f9..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/nested.plc.golden +++ b/plutus-tx-plugin/test/IsData/nested.plc.golden @@ -1 +1 @@ -(delay (lam case_True_209 (lam case_False_210 case_True_209))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/poly.plc.golden b/plutus-tx-plugin/test/IsData/poly.plc.golden index 8bdf6bc9da5..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/poly.plc.golden +++ b/plutus-tx-plugin/test/IsData/poly.plc.golden @@ -1 +1 @@ -(delay (lam case_True_158 (lam case_False_159 case_True_158))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/record.plc.golden b/plutus-tx-plugin/test/IsData/record.plc.golden index f2e86ac8b57..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/record.plc.golden +++ b/plutus-tx-plugin/test/IsData/record.plc.golden @@ -1 +1 @@ -(delay (lam case_True_115 (lam case_False_116 case_True_115))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/tuple.plc.golden b/plutus-tx-plugin/test/IsData/tuple.plc.golden index 53fab77af8a..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/tuple.plc.golden +++ b/plutus-tx-plugin/test/IsData/tuple.plc.golden @@ -1 +1 @@ -(delay (lam case_True_127 (lam case_False_128 case_True_127))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/tupleInterop.plc.golden b/plutus-tx-plugin/test/IsData/tupleInterop.plc.golden index b1cd88a5347..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/tupleInterop.plc.golden +++ b/plutus-tx-plugin/test/IsData/tupleInterop.plc.golden @@ -1 +1 @@ -(delay (lam case_True_86 (lam case_False_87 case_True_86))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/unit.plc.golden b/plutus-tx-plugin/test/IsData/unit.plc.golden index 7a37e5bf42b..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/unit.plc.golden +++ b/plutus-tx-plugin/test/IsData/unit.plc.golden @@ -1 +1 @@ -(delay (lam case_True_66 (lam case_False_67 case_True_66))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/unitInterop.plc.golden b/plutus-tx-plugin/test/IsData/unitInterop.plc.golden index c7bca7ce82e..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/unitInterop.plc.golden +++ b/plutus-tx-plugin/test/IsData/unitInterop.plc.golden @@ -1 +1 @@ -(delay (lam case_True_47 (lam case_False_48 case_True_47))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/IsData/unsafeTupleInterop.plc.golden b/plutus-tx-plugin/test/IsData/unsafeTupleInterop.plc.golden index 9f42bc9cd20..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/IsData/unsafeTupleInterop.plc.golden +++ b/plutus-tx-plugin/test/IsData/unsafeTupleInterop.plc.golden @@ -1 +1 @@ -(delay (lam case_True_57 (lam case_False_58 case_True_57))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Lib.hs b/plutus-tx-plugin/test/Lib.hs index 76040c0fb05..2b28148d2bd 100644 --- a/plutus-tx-plugin/test/Lib.hs +++ b/plutus-tx-plugin/test/Lib.hs @@ -12,21 +12,20 @@ module Lib where import Common import Control.Exception -import Control.Lens.Combinators (_1) +import Control.Lens import Control.Monad.Except import Data.Text (Text) import Flat (Flat) import PlcTestUtils -import PlutusPrelude (view) import PlutusTx.Code -import PlutusTx.Evaluation import PlutusCore qualified as PLC import PlutusCore.Pretty import UntypedPlutusCore qualified as UPLC +import UntypedPlutusCore.Evaluation.Machine.Cek instance (PLC.Closed uni, uni `PLC.Everywhere` Flat, uni `PLC.Everywhere` PrettyConst, PLC.GShow uni, Pretty fun, Flat fun) => ToUPlc (CompiledCodeIn uni fun a) uni fun where @@ -43,7 +42,7 @@ runPlcCek :: ToUPlc a PLC.DefaultUni PLC.DefaultFun => [a] -> ExceptT SomeExcept runPlcCek values = do ps <- traverse toUPlc values let p = foldl1 UPLC.applyProgram ps - either (throwError . SomeException) pure $ evaluateCek p + either (throwError . SomeException) pure $ evaluateCekNoEmit PLC.defaultCekParameters (p ^. UPLC.progTerm) runPlcCekTrace :: ToUPlc a PLC.DefaultUni PLC.DefaultFun => @@ -52,7 +51,7 @@ runPlcCekTrace :: runPlcCekTrace values = do ps <- traverse toUPlc values let p = foldl1 UPLC.applyProgram ps - let (logOut, TallyingSt tally _, result) = evaluateCekTrace p + let (result, TallyingSt tally _, logOut) = runCek PLC.defaultCekParameters tallying logEmitter (p ^. UPLC.progTerm) res <- either (throwError . SomeException) pure result pure (logOut, tally, res) diff --git a/plutus-tx-plugin/test/Lift/boolInterop.plc.golden b/plutus-tx-plugin/test/Lift/boolInterop.plc.golden index 0073de28c06..599b9fbb75a 100644 --- a/plutus-tx-plugin/test/Lift/boolInterop.plc.golden +++ b/plutus-tx-plugin/test/Lift/boolInterop.plc.golden @@ -1,3 +1,3 @@ (delay - (lam case_GHC_Types_True_3 (lam case_GHC_Types_False_4 case_GHC_Types_True_3)) + (lam case_GHC_Types_True_0 (lam case_GHC_Types_False_1 case_GHC_Types_True_0)) ) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Data/recursive/sameEmptyRoseEval.plc.golden b/plutus-tx-plugin/test/Plugin/Data/recursive/sameEmptyRoseEval.plc.golden index 56a9954b060..40c84a70ead 100644 --- a/plutus-tx-plugin/test/Plugin/Data/recursive/sameEmptyRoseEval.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Data/recursive/sameEmptyRoseEval.plc.golden @@ -1,47 +1,47 @@ (delay (lam - case_EmptyRose_23 + case_EmptyRose_0 [ - case_EmptyRose_23 + case_EmptyRose_0 (delay (lam - case_Nil_29 + case_Nil_1 (lam - case_Cons_30 + case_Cons_2 [ [ - case_Cons_30 + case_Cons_2 (delay (lam - case_EmptyRose_23 + case_EmptyRose_3 [ - case_EmptyRose_23 - (delay (lam case_Nil_25 (lam case_Cons_26 case_Nil_25))) + case_EmptyRose_3 + (delay (lam case_Nil_4 (lam case_Cons_5 case_Nil_4))) ] ) ) ] (delay (lam - case_Nil_29 + case_Nil_6 (lam - case_Cons_30 + case_Cons_7 [ [ - case_Cons_30 + case_Cons_7 (delay (lam - case_EmptyRose_23 + case_EmptyRose_8 [ - case_EmptyRose_23 + case_EmptyRose_8 (delay - (lam case_Nil_25 (lam case_Cons_26 case_Nil_25)) + (lam case_Nil_9 (lam case_Cons_10 case_Nil_9)) ) ] ) ) ] - (delay (lam case_Nil_25 (lam case_Cons_26 case_Nil_25))) + (delay (lam case_Nil_11 (lam case_Cons_12 case_Nil_11))) ] ) ) diff --git a/plutus-tx-plugin/test/Plugin/Functions/recursive/even3.plc.golden b/plutus-tx-plugin/test/Plugin/Functions/recursive/even3.plc.golden index c5963aff0a3..4e8ddacc956 100644 --- a/plutus-tx-plugin/test/Plugin/Functions/recursive/even3.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Functions/recursive/even3.plc.golden @@ -1 +1 @@ -(delay (lam case_True_22 (lam case_False_23 case_False_23))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_False_1))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Functions/recursive/even4.plc.golden b/plutus-tx-plugin/test/Plugin/Functions/recursive/even4.plc.golden index e311b89b76e..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/Plugin/Functions/recursive/even4.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Functions/recursive/even4.plc.golden @@ -1 +1 @@ -(delay (lam case_True_20 (lam case_False_21 case_True_20))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Laziness/joinErrorEval.plc.golden b/plutus-tx-plugin/test/Plugin/Laziness/joinErrorEval.plc.golden index 6b49ddbb6de..18d200a63c0 100644 --- a/plutus-tx-plugin/test/Plugin/Laziness/joinErrorEval.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Laziness/joinErrorEval.plc.golden @@ -1 +1 @@ -(delay (lam case_Unit_12 case_Unit_12)) \ No newline at end of file +(delay (lam case_Unit_0 case_Unit_0)) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Primitives/andApply.plc.golden b/plutus-tx-plugin/test/Plugin/Primitives/andApply.plc.golden index 77985e07002..4e8ddacc956 100644 --- a/plutus-tx-plugin/test/Plugin/Primitives/andApply.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Primitives/andApply.plc.golden @@ -1 +1 @@ -(delay (lam case_True_5 (lam case_False_6 case_False_6))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_False_1))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Primitives/deconstructData2.plc.golden b/plutus-tx-plugin/test/Plugin/Primitives/deconstructData2.plc.golden index c87a2f170bf..37465936f5f 100644 --- a/plutus-tx-plugin/test/Plugin/Primitives/deconstructData2.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Primitives/deconstructData2.plc.golden @@ -1,23 +1,23 @@ (delay (lam - case_Tuple2_62 + case_Tuple2_0 [ - [ case_Tuple2_62 (con integer 1) ] + [ case_Tuple2_0 (con integer 1) ] (delay (lam - case_Nil_53 + case_Nil_1 (lam - case_Cons_54 + case_Cons_2 [ - [ case_Cons_54 (con integer 2) ] + [ case_Cons_2 (con integer 2) ] (delay (lam - case_Nil_53 + case_Nil_3 (lam - case_Cons_54 + case_Cons_4 [ - [ case_Cons_54 (con integer 3) ] - (delay (lam case_Nil_49 (lam case_Cons_50 case_Nil_49))) + [ case_Cons_4 (con integer 3) ] + (delay (lam case_Nil_5 (lam case_Cons_6 case_Nil_5))) ] ) ) diff --git a/plutus-tx-plugin/test/Plugin/Primitives/deconstructData3.plc.golden b/plutus-tx-plugin/test/Plugin/Primitives/deconstructData3.plc.golden index 2b572019fea..05361d45742 100644 --- a/plutus-tx-plugin/test/Plugin/Primitives/deconstructData3.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Primitives/deconstructData3.plc.golden @@ -1,18 +1,18 @@ (delay (lam - case_Nil_23 + case_Nil_0 (lam - case_Cons_24 + case_Cons_1 [ - [ case_Cons_24 (con data #02) ] + [ case_Cons_1 (con data #02) ] (delay (lam - case_Nil_23 + case_Nil_2 (lam - case_Cons_24 + case_Cons_3 [ - [ case_Cons_24 (con data #03) ] - (delay (lam case_Nil_19 (lam case_Cons_20 case_Nil_19))) + [ case_Cons_3 (con data #03) ] + (delay (lam case_Nil_4 (lam case_Cons_5 case_Nil_4))) ] ) ) diff --git a/plutus-tx-plugin/test/Plugin/Primitives/equalsByteString.plc.golden b/plutus-tx-plugin/test/Plugin/Primitives/equalsByteString.plc.golden index 4cc44bd5750..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/Plugin/Primitives/equalsByteString.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Primitives/equalsByteString.plc.golden @@ -1 +1 @@ -(delay (lam case_True_8 (lam case_False_9 case_True_8))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Primitives/equalsString.plc.golden b/plutus-tx-plugin/test/Plugin/Primitives/equalsString.plc.golden index 4cc44bd5750..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/Plugin/Primitives/equalsString.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Primitives/equalsString.plc.golden @@ -1 +1 @@ -(delay (lam case_True_8 (lam case_False_9 case_True_8))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Primitives/intEqApply.plc.golden b/plutus-tx-plugin/test/Plugin/Primitives/intEqApply.plc.golden index 4cc44bd5750..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/Plugin/Primitives/intEqApply.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Primitives/intEqApply.plc.golden @@ -1 +1 @@ -(delay (lam case_True_8 (lam case_False_9 case_True_8))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Primitives/ltByteString.plc.golden b/plutus-tx-plugin/test/Plugin/Primitives/ltByteString.plc.golden index 4cc44bd5750..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/Plugin/Primitives/ltByteString.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Primitives/ltByteString.plc.golden @@ -1 +1 @@ -(delay (lam case_True_8 (lam case_False_9 case_True_8))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Plugin/Primitives/matchData1.plc.golden b/plutus-tx-plugin/test/Plugin/Primitives/matchData1.plc.golden index 46a6c78df6a..754b98667ac 100644 --- a/plutus-tx-plugin/test/Plugin/Primitives/matchData1.plc.golden +++ b/plutus-tx-plugin/test/Plugin/Primitives/matchData1.plc.golden @@ -1,3 +1 @@ -(delay - (lam case_Just_77 (lam case_Nothing_78 [ case_Just_77 (con integer 1) ])) -) \ No newline at end of file +(delay (lam case_Just_0 (lam case_Nothing_1 [ case_Just_0 (con integer 1) ]))) \ No newline at end of file diff --git a/plutus-tx-plugin/test/TH/all.plc.golden b/plutus-tx-plugin/test/TH/all.plc.golden index 2b33f9071d8..177eccb7bb0 100644 --- a/plutus-tx-plugin/test/TH/all.plc.golden +++ b/plutus-tx-plugin/test/TH/all.plc.golden @@ -1 +1 @@ -(delay (lam case_True_37 (lam case_False_38 case_True_37))) \ No newline at end of file +(delay (lam case_True_0 (lam case_False_1 case_True_0))) \ No newline at end of file diff --git a/plutus-tx/plutus-tx.cabal b/plutus-tx/plutus-tx.cabal index 86f62303af3..c760600eb37 100644 --- a/plutus-tx/plutus-tx.cabal +++ b/plutus-tx/plutus-tx.cabal @@ -40,7 +40,6 @@ library PlutusTx.Coverage PlutusTx.TH PlutusTx.Prelude - PlutusTx.Evaluation PlutusTx.Applicative PlutusTx.Base PlutusTx.Bool diff --git a/plutus-tx/src/PlutusTx/Evaluation.hs b/plutus-tx/src/PlutusTx/Evaluation.hs deleted file mode 100644 index 67221f7a3a1..00000000000 --- a/plutus-tx/src/PlutusTx/Evaluation.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} - -module PlutusTx.Evaluation - ( evaluateCek - , unsafeEvaluateCek - , evaluateCekTrace - , ErrorWithCause(..) - , EvaluationError(..) - , CekExTally - , TallyingSt(..) - , CekEvaluationException - ) -where - -import PlutusCore qualified as PLC -import PlutusCore.Default -import PlutusCore.Name - -import UntypedPlutusCore -import UntypedPlutusCore.Evaluation.Machine.Cek hiding (evaluateCek, unsafeEvaluateCek) -import UntypedPlutusCore.Evaluation.Machine.Cek qualified as Cek - -import Data.Text (Text) - --- We do not use qualified import because the whole module contains off-chain code -import Prelude as Haskell - --- | Evaluate a program in the CEK machine with the usual text dynamic builtins. -evaluateCek - :: (uni ~ DefaultUni, fun ~ DefaultFun) - => Program Name uni fun () -> Either (CekEvaluationException uni fun) (Term Name uni fun ()) -evaluateCek (Program _ _ t) = Cek.evaluateCekNoEmit PLC.defaultCekParameters t - --- | Evaluate a program in the CEK machine with the usual text dynamic builtins. May throw. -unsafeEvaluateCek - :: (uni ~ DefaultUni, fun ~ DefaultFun) - => Program Name uni fun () -> EvaluationResult (Term Name uni fun ()) -unsafeEvaluateCek (Program _ _ t) = Cek.unsafeEvaluateCekNoEmit PLC.defaultCekParameters t - --- | Evaluate a program in the CEK machine with the usual text dynamic builtins and tracing, additionally --- returning the trace output. -evaluateCekTrace - :: (uni ~ DefaultUni, fun ~ DefaultFun) - => Program Name uni fun () - -> ([Text], TallyingSt fun, Either (CekEvaluationException uni fun) (Term Name uni fun ())) -evaluateCekTrace (Program _ _ t) = - case runCek PLC.defaultCekParameters Cek.tallying Cek.logEmitter t of - (errOrRes, st, logs) -> (logs, st, errOrRes) diff --git a/plutus-tx/src/PlutusTx/Lift.hs b/plutus-tx/src/PlutusTx/Lift.hs index 4602dd56152..a2707e6f883 100644 --- a/plutus-tx/src/PlutusTx/Lift.hs +++ b/plutus-tx/src/PlutusTx/Lift.hs @@ -197,5 +197,5 @@ typeCode typeCode p prog@(PLC.Program _ _ term) = do _ <- typeCheckAgainst p term let erased = UPLC.eraseProgram prog - db <- UPLC.deBruijnProgram $ UPLC.simplifyProgram erased + db <- traverseOf UPLC.progTerm (UPLC.deBruijnTerm . UPLC.simplifyTerm) erased pure $ DeserializedCode db Nothing mempty