From ffc06c90914f40acc9de404069daabcdb1ca21ee Mon Sep 17 00:00:00 2001 From: effectfully Date: Fri, 3 Jan 2025 00:01:02 +0100 Subject: [PATCH] [UPLC] [Test] Add scoping tests --- plutus-core/plutus-core.cabal | 16 +++-- .../src/PlutusCore/Check/Scoping.hs | 40 +++++++---- .../src/PlutusCore/Core/Instance/Scoping.hs | 22 +++++- .../src/PlutusIR/Core/Instance/Scoping.hs | 23 ++++-- .../plutus-ir/test/PlutusIR/Scoping/Tests.hs | 2 +- plutus-core/prelude/PlutusPrelude.hs | 9 +++ plutus-core/testlib/PlutusCore/Test.hs | 3 +- .../src/UntypedPlutusCore/Core/Instance.hs | 1 + .../Core/Instance/Scoping.hs | 70 +++++++++++++++++++ .../src/UntypedPlutusCore/Rename/Internal.hs | 13 ++-- .../untyped-plutus-core/test/Generators.hs | 5 +- .../untyped-plutus-core/test/Scoping/Spec.hs | 63 +++++++++++++++++ plutus-core/untyped-plutus-core/test/Spec.hs | 2 + 13 files changed, 236 insertions(+), 33 deletions(-) create mode 100644 plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs create mode 100644 plutus-core/untyped-plutus-core/test/Scoping/Spec.hs diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal index 6c84e1a0d88..12dbfcef0c9 100644 --- a/plutus-core/plutus-core.cabal +++ b/plutus-core/plutus-core.cabal @@ -195,6 +195,7 @@ library UntypedPlutusCore.Check.Scope UntypedPlutusCore.Check.Uniques UntypedPlutusCore.Core + UntypedPlutusCore.Core.Instance.Scoping UntypedPlutusCore.Core.Plated UntypedPlutusCore.Core.Type UntypedPlutusCore.Core.Zip @@ -206,12 +207,19 @@ library UntypedPlutusCore.Evaluation.Machine.SteppableCek UntypedPlutusCore.Evaluation.Machine.SteppableCek.DebugDriver UntypedPlutusCore.Evaluation.Machine.SteppableCek.Internal + UntypedPlutusCore.Mark UntypedPlutusCore.MkUPlc UntypedPlutusCore.Parser UntypedPlutusCore.Purity UntypedPlutusCore.Rename + UntypedPlutusCore.Rename.Internal UntypedPlutusCore.Size UntypedPlutusCore.Transform.CaseOfCase + UntypedPlutusCore.Transform.CaseReduce + UntypedPlutusCore.Transform.Cse + UntypedPlutusCore.Transform.FloatDelay + UntypedPlutusCore.Transform.ForceDelay + UntypedPlutusCore.Transform.Inline UntypedPlutusCore.Transform.Simplifier other-modules: @@ -264,16 +272,9 @@ library UntypedPlutusCore.Evaluation.Machine.Cek.EmitterMode UntypedPlutusCore.Evaluation.Machine.Cek.ExBudgetMode UntypedPlutusCore.Evaluation.Machine.CommonAPI - UntypedPlutusCore.Mark - UntypedPlutusCore.Rename.Internal UntypedPlutusCore.Simplify UntypedPlutusCore.Simplify.Opts UntypedPlutusCore.Subst - UntypedPlutusCore.Transform.CaseReduce - UntypedPlutusCore.Transform.Cse - UntypedPlutusCore.Transform.FloatDelay - UntypedPlutusCore.Transform.ForceDelay - UntypedPlutusCore.Transform.Inline reexported-modules: Data.SatInt hs-source-dirs: @@ -438,6 +439,7 @@ test-suite untyped-plutus-core-test Evaluation.Regressions Flat.Spec Generators + Scoping.Spec Transform.CaseOfCase.Test Transform.Simplify Transform.Simplify.Lib diff --git a/plutus-core/plutus-core/src/PlutusCore/Check/Scoping.hs b/plutus-core/plutus-core/src/PlutusCore/Check/Scoping.hs index 5e040279ddb..ee02fe4a70a 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Check/Scoping.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Check/Scoping.hs @@ -20,6 +20,7 @@ import Data.List.NonEmpty (NonEmpty) import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict as Map import Data.Maybe +import Data.Proxy import Data.Set as Set import Text.Pretty import Text.PrettyBy @@ -66,6 +67,11 @@ to touch any annotations) and collect all the available information: which names which didn't, which appeared etc, simultaneously checking that the names that were supposed to disappear indeed disappeared and the names that were supposed to stay indeed stayed. +Note that to tell that e.g. a binding disappeared it's crucial that the AST node with the appopriate +annotation is itself preserved, only the name changed. If some pass removes the AST node of a +binding that is supposed to be disappear, it won't be accounted for. Which is precisely what we need +for passes like inlining. + Once all this scoping information is collected, we run 'checkScopeInfo' to check that the information is coherent. See its docs for the details on what exactly the checked invariants are. @@ -88,24 +94,24 @@ isSameScope TermName{} TypeName{} = False data Stays = StaysOutOfScopeVariable -- ^ An out-of-scope variable does not get renamed and hence stays. | StaysFreeVariable -- ^ A free variable does not get renamed and hence stays. - deriving stock (Show) + deriving stock (Show, Eq) -- | Changing names. data Disappears = DisappearsBinding -- ^ A binding gets renamed and hence the name that it binds disappears. | DisappearsVariable -- ^ A bound variable gets renamed and hence its name disappears. - deriving stock (Show) + deriving stock (Show, Eq) -- | A name either stays or disappears. data NameAction = Stays Stays | Disappears Disappears - deriving stock (Show) + deriving stock (Show, Eq) data NameAnn = NameAction NameAction ScopedName | NotAName - deriving stock (Show) + deriving stock (Show, Eq) instance Pretty NameAnn where pretty = viaShow @@ -282,6 +288,12 @@ class CollectScopeInfo t where -} collectScopeInfo :: t NameAnn -> ScopeErrorOrInfo +instance EstablishScoping Proxy where + establishScoping _ = pure Proxy + +instance CollectScopeInfo Proxy where + collectScopeInfo _ = mempty + -- See Note [Example of a scoping check]. type Scoping t = (EstablishScoping t, CollectScopeInfo t) @@ -290,7 +302,7 @@ type Scoping t = (EstablishScoping t, CollectScopeInfo t) -- original binder with the annotated sort and its value, but also decorate the reassembled binder -- with one out-of-scope variable and one in-scope one. establishScopingBinder - :: (Reference name value, ToScopedName name, Scoping sort, Scoping value) + :: (Reference name value, ToScopedName name, EstablishScoping sort, EstablishScoping value) => (NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn) -> name -> sort ann @@ -459,19 +471,22 @@ checkScopeInfo bindRem scopeInfo = do -- | The type of errors that the scope checking machinery returns. data ScopeCheckError t = ScopeCheckError - { _input :: !(t NameAnn) -- ^ What got fed to the scoping check pass. - , _output :: !(t NameAnn) -- ^ What got out of it. - , _error :: !ScopeError -- ^ The error returned by the scoping check pass. + { _input :: !(t NameAnn) -- ^ What got fed to the scoping check pass before preparation. + , _prepared :: !(t NameAnn) -- ^ What got fed to the scoping check pass after preparation. + , _output :: !(t NameAnn) -- ^ What got out of it. + , _error :: !ScopeError -- ^ The error returned by the scoping check pass. } deriving stock instance Show (t NameAnn) => Show (ScopeCheckError t) instance PrettyBy config (t NameAnn) => PrettyBy config (ScopeCheckError t) where - prettyBy config (ScopeCheckError input output err) = vsep + prettyBy config (ScopeCheckError input prepared output err) = vsep [ pretty err , "when checking that transformation of" <> hardline , indent 2 $ prettyBy config input <> hardline , "to" <> hardline + , indent 2 $ prettyBy config prepared <> hardline + , "to" <> hardline , indent 2 $ prettyBy config output <> hardline , "is correct" ] @@ -490,8 +505,9 @@ checkRespectsScoping -> t ann -> Either (ScopeCheckError t) () checkRespectsScoping bindRem prep run thing = - first (ScopeCheckError input output) $ + first (ScopeCheckError input prepared output) $ unScopeErrorOrInfo (collectScopeInfo output) >>= checkScopeInfo bindRem where - input = prep . runQuote $ establishScoping thing - output = run input + input = runQuote $ establishScoping thing + prepared = prep input + output = run prepared diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs index 570e000f48a..44c98e76bf6 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs @@ -6,6 +6,8 @@ module PlutusCore.Core.Instance.Scoping () where +import PlutusPrelude + import PlutusCore.Check.Scoping import PlutusCore.Core.Type import PlutusCore.Name.Unique @@ -51,6 +53,10 @@ instance tyname ~ TyName => EstablishScoping (Type tyname uni) where establishScoping (TySOP _ tyls) = TySOP NotAName <$> (traverse . traverse) establishScoping tyls +firstBound :: Term tyname name uni fun ann -> [name] +firstBound (Apply _ (LamAbs _ name _ body) _) = name : firstBound body +firstBound _ = [] + instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name uni fun) where establishScoping (LamAbs _ nameDup ty body) = do name <- freshenName nameDup @@ -58,7 +64,7 @@ instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name un establishScoping (TyAbs _ nameDup kind body) = do name <- freshenTyName nameDup establishScopingBinder TyAbs name kind body - establishScoping (IWrap _ pat arg term) = + establishScoping (IWrap _ pat arg term) = IWrap NotAName <$> establishScoping pat <*> establishScoping arg <*> establishScoping term establishScoping (Apply _ fun arg) = Apply NotAName <$> establishScoping fun <*> establishScoping arg @@ -73,8 +79,18 @@ instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name un establishScoping (Builtin _ bi) = pure $ Builtin NotAName bi establishScoping (Constr _ ty i es) = Constr NotAName <$> establishScoping ty <*> pure i <*> traverse establishScoping es - establishScoping (Case _ ty a es) = - Case NotAName <$> establishScoping ty <*> establishScoping a <*> traverse establishScoping es + establishScoping (Case _ ty a es) = do + esScoped <- traverse establishScoping es + let esScopedPoked = addTheRest $ map (\e -> (e, firstBound e)) esScoped + branchBounds = map (snd . fst) esScopedPoked + referenceInBranch ((branch, _), others) = referenceOutOfScope (map snd others) branch + tyScoped <- establishScoping ty + aScoped <- establishScoping a + -- For each of the branches reference (as out-of-scope) the variables bound in that branch + -- in all the other ones, as well as outside of the whole case-expression. This is to check + -- that none of the transformations leak variables outside of the branch they're bound in. + pure . referenceOutOfScope branchBounds $ + Case NotAName tyScoped aScoped $ map referenceInBranch esScopedPoked instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) where establishScoping (Program _ ver term) = diff --git a/plutus-core/plutus-ir/src/PlutusIR/Core/Instance/Scoping.hs b/plutus-core/plutus-ir/src/PlutusIR/Core/Instance/Scoping.hs index b0ae80cf28d..a99f4fbdbea 100644 --- a/plutus-core/plutus-ir/src/PlutusIR/Core/Instance/Scoping.hs +++ b/plutus-core/plutus-ir/src/PlutusIR/Core/Instance/Scoping.hs @@ -8,16 +8,16 @@ {-# OPTIONS_GHC -Wno-orphans #-} module PlutusIR.Core.Instance.Scoping where +import PlutusPrelude + import PlutusIR.Core.Type import PlutusCore.Check.Scoping import PlutusCore.MkPlc import PlutusCore.Quote -import Data.Foldable -import Data.List.NonEmpty (NonEmpty (..), (<|)) +import Data.List.NonEmpty ((<|)) import Data.List.NonEmpty qualified as NonEmpty -import Data.Traversable instance tyname ~ TyName => Reference TyName (Term tyname name uni fun) where referenceVia reg tyname term = TyInst NotAName term $ TyVar (reg tyname) tyname @@ -219,6 +219,10 @@ registerByRecursivity :: ToScopedName name => Recursivity -> name -> NameAnn registerByRecursivity Rec = registerBound registerByRecursivity NonRec = registerOutOfScope +firstBound :: Term tyname name uni fun ann -> [name] +firstBound (Apply _ (LamAbs _ name _ body) _) = name : firstBound body +firstBound _ = [] + instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name uni fun) where establishScoping (Let _ recy bindingsDup body) = do bindings <- establishScopingBindings (registerByRecursivity recy) bindingsDup @@ -249,7 +253,18 @@ instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name un establishScoping (Constant _ con) = pure $ Constant NotAName con establishScoping (Builtin _ bi) = pure $ Builtin NotAName bi establishScoping (Constr _ ty i es) = Constr NotAName <$> establishScoping ty <*> pure i <*> traverse establishScoping es - establishScoping (Case _ ty arg cs) = Case NotAName <$> establishScoping ty <*> establishScoping arg <*> traverse establishScoping cs + establishScoping (Case _ ty a es) = do + esScoped <- traverse establishScoping es + let esScopedPoked = addTheRest $ map (\e -> (e, firstBound e)) esScoped + branchBounds = map (snd . fst) esScopedPoked + referenceInBranch ((branch, _), others) = referenceOutOfScope (map snd others) branch + tyScoped <- establishScoping ty + aScoped <- establishScoping a + -- For each of the branches reference (as out-of-scope) the variables bound in that branch + -- in all the other ones, as well as outside of the whole case-expression. This is to check + -- that none of the transformations leak variables outside of the branch they're bound in. + pure . referenceOutOfScope branchBounds $ + Case NotAName tyScoped aScoped $ map referenceInBranch esScopedPoked instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) where establishScoping (Program _ v term) = Program NotAName v <$> establishScoping term diff --git a/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs index 67b389cb744..7f25585bb6b 100644 --- a/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs +++ b/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs @@ -30,7 +30,7 @@ test_names :: TestTree test_names = testGroup "names" [ T.test_scopingGood "beta-reduction" genTerm T.BindingRemovalNotOk T.PrerenameYes $ pure . beta - , T.test_scopingGood "case-of-known-constructor" genTerm T.BindingRemovalNotOk T.PrerenameYes $ + , T.test_scopingGood "case-of-known-constructor" genTerm T.BindingRemovalOk T.PrerenameYes $ pure . caseReduce , T.test_scopingGood "commuteFnWithConst" genTerm T.BindingRemovalNotOk T.PrerenameYes $ pure . commuteFnWithConst diff --git a/plutus-core/prelude/PlutusPrelude.hs b/plutus-core/prelude/PlutusPrelude.hs index 09395a0b8a0..1b5b243dd4f 100644 --- a/plutus-core/prelude/PlutusPrelude.hs +++ b/plutus-core/prelude/PlutusPrelude.hs @@ -98,6 +98,7 @@ module PlutusPrelude , distinct , unsafeFromRight , tryError + , addTheRest , modifyError , lowerInitialChar ) where @@ -266,6 +267,14 @@ tryError :: MonadError e m => m a -> m (Either e a) tryError a = (Right <$> a) `catchError` (pure . Left) {-# INLINE tryError #-} +-- | Pair each element of the given list with all the other elements. +-- +-- >>> addTheRest "abcd" +-- [('a',"bcd"),('b',"acd"),('c',"abd"),('d',"abc")] +addTheRest :: [a] -> [(a, [a])] +addTheRest [] = [] +addTheRest (x:xs) = (x, xs) : map (fmap (x :)) (addTheRest xs) + {- A different 'MonadError' analogue to the 'withExceptT' function. Modify the value (and possibly the type) of an error in an @ExceptT@-transformed monad, while stripping the @ExceptT@ layer. diff --git a/plutus-core/testlib/PlutusCore/Test.hs b/plutus-core/testlib/PlutusCore/Test.hs index cf31956bdc1..6d68525dd65 100644 --- a/plutus-core/testlib/PlutusCore/Test.hs +++ b/plutus-core/testlib/PlutusCore/Test.hs @@ -604,7 +604,8 @@ prop_scopingFor :: Property prop_scopingFor gen bindRem preren run = withTests 200 . property $ do prog <- forAllNoShow $ runAstGen gen - let catchEverything = unsafePerformIO . try @SomeException . evaluate + let -- TODO: use @enclosed-exceptions@. + catchEverything = unsafePerformIO . try @SomeException . evaluate prep = runPrerename preren case catchEverything $ checkRespectsScoping bindRem prep (TPLC.runQuote . run) prog of Left exc -> fail $ displayException exc 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 b1437d267fe..c96c4e7f3ca 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance.hs @@ -3,3 +3,4 @@ module UntypedPlutusCore.Core.Instance (module Export) where import UntypedPlutusCore.Core.Instance.Eq () import UntypedPlutusCore.Core.Instance.Flat as Export import UntypedPlutusCore.Core.Instance.Pretty () +import UntypedPlutusCore.Core.Instance.Scoping () diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs new file mode 100644 index 00000000000..043279c2662 --- /dev/null +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs @@ -0,0 +1,70 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} + +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module UntypedPlutusCore.Core.Instance.Scoping () where + +import PlutusPrelude + +import UntypedPlutusCore.Core.Type + +import PlutusCore.Check.Scoping +import PlutusCore.Name.Unique +import PlutusCore.Quote + +import Data.Proxy +import Data.Vector qualified as Vector + +firstBound :: Term name uni fun ann -> [name] +firstBound (Apply _ (LamAbs _ name body) _) = name : firstBound body +firstBound _ = [] + +instance name ~ Name => Reference Name (Term name uni fun) where + referenceVia reg name term = Apply NotAName term $ Var (reg name) name + +instance name ~ Name => EstablishScoping (Term name uni fun) where + establishScoping (LamAbs _ nameDup body) = do + name <- freshenName nameDup + establishScopingBinder (\ann name' _ -> LamAbs ann name') name Proxy body + establishScoping (Delay _ body) = Delay NotAName <$> establishScoping body + establishScoping (Apply _ fun arg) = + Apply NotAName <$> establishScoping fun <*> establishScoping arg + establishScoping (Error _) = pure $ Error NotAName + establishScoping (Force _ term) = Force NotAName <$> establishScoping term + establishScoping (Var _ nameDup) = do + name <- freshenName nameDup + pure $ Var (registerFree name) name + establishScoping (Constant _ con) = pure $ Constant NotAName con + establishScoping (Builtin _ bi) = pure $ Builtin NotAName bi + establishScoping (Constr _ i es) = Constr NotAName <$> pure i <*> traverse establishScoping es + establishScoping (Case _ a es) = do + esScoped <- traverse establishScoping es + let esScopedPoked = addTheRest . map (\e -> (e, firstBound e)) $ Vector.toList esScoped + branchBounds = map (snd . fst) esScopedPoked + referenceInBranch ((branch, _), others) = referenceOutOfScope (map snd others) branch + aScoped <- establishScoping a + -- For each of the branches reference (as out-of-scope) the variables bound in that branch + -- in all the other ones, as well as outside of the whole case-expression. This is to check + -- that none of the transformations leak variables outside of the branch they're bound in. + pure . referenceOutOfScope branchBounds $ + Case NotAName aScoped . Vector.fromList $ map referenceInBranch esScopedPoked + +instance name ~ Name => EstablishScoping (Program name uni fun) where + establishScoping (Program _ ver term) = Program NotAName ver <$> establishScoping term + +instance name ~ Name => CollectScopeInfo (Term name uni fun) where + collectScopeInfo (LamAbs ann name body) = handleSname ann name <> collectScopeInfo body + collectScopeInfo (Delay _ body) = collectScopeInfo body + collectScopeInfo (Apply _ fun arg) = collectScopeInfo fun <> collectScopeInfo arg + collectScopeInfo (Error _) = mempty + collectScopeInfo (Force _ term) = collectScopeInfo term + collectScopeInfo (Var ann name) = handleSname ann name + collectScopeInfo (Constant _ _) = mempty + collectScopeInfo (Builtin _ _) = mempty + collectScopeInfo (Constr _ _ es) = foldMap collectScopeInfo es + collectScopeInfo (Case _ arg cs) = collectScopeInfo arg <> foldMap collectScopeInfo cs + +instance name ~ Name => CollectScopeInfo (Program name uni fun) where + collectScopeInfo (Program _ _ term) = collectScopeInfo term diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs index 5212de3c41b..3389dda5e69 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs @@ -1,6 +1,8 @@ -- | The internal module of the renamer that defines the actual algorithms, -- but not the user-facing API. +{-# LANGUAGE ConstraintKinds #-} + module UntypedPlutusCore.Rename.Internal ( module Export , renameTermM @@ -14,11 +16,14 @@ import PlutusCore.Name.Unique import PlutusCore.Quote import PlutusCore.Rename.Monad as Export +import Control.Monad.Reader (MonadReader) + +type MonadRename m = (MonadQuote m, MonadReader (Renaming TermUnique) m) -- | Rename a 'Term' in the 'RenameM' monad. renameTermM - :: (HasUniques (Term name uni fun ann), MonadQuote m) - => Term name uni fun ann -> ScopedRenameT m (Term name uni fun ann) + :: (MonadRename m, HasUniques (Term name uni fun ann)) + => Term name uni fun ann -> m (Term name uni fun ann) renameTermM (LamAbs ann name body) = withFreshenedName name $ \nameFr -> LamAbs ann nameFr <$> renameTermM body renameTermM (Apply ann fun arg) = Apply ann <$> renameTermM fun <*> renameTermM arg @@ -33,6 +38,6 @@ renameTermM bi@Builtin{} = pure bi -- | Rename a 'Program' in the 'RenameM' monad. renameProgramM - :: (HasUniques (Program name uni fun ann), MonadQuote m) - => Program name uni fun ann -> ScopedRenameT m (Program name uni fun ann) + :: (MonadRename m, HasUniques (Program name uni fun ann)) + => Program name uni fun ann -> m (Program name uni fun ann) renameProgramM (Program ann ver term) = Program ann ver <$> renameTermM term diff --git a/plutus-core/untyped-plutus-core/test/Generators.hs b/plutus-core/untyped-plutus-core/test/Generators.hs index 2d111a9cba0..791ab327c4c 100644 --- a/plutus-core/untyped-plutus-core/test/Generators.hs +++ b/plutus-core/untyped-plutus-core/test/Generators.hs @@ -10,7 +10,7 @@ import PlutusPrelude (display, fold, on, void, zipExact, (&&&)) import PlutusCore (Name, _nameText) import PlutusCore.Annotation -import PlutusCore.Compiler.Erase (eraseProgram) +import PlutusCore.Compiler.Erase (eraseProgram, eraseTerm) import PlutusCore.Default (Closed, DefaultFun, DefaultUni, Everywhere, GEq) import PlutusCore.Error (ParserErrorBundle) import PlutusCore.Generators.Hedgehog (forAllPretty) @@ -70,6 +70,9 @@ compareProgram => Program Name uni fun a -> Program Name uni fun a -> Bool compareProgram (Program _ v t) (Program _ v' t') = v == v' && compareTerm t t' +genTerm :: forall fun. (Bounded fun, Enum fun) => AstGen (Term Name DefaultUni fun ()) +genTerm = fmap eraseTerm AST.genTerm + genProgram :: forall fun. (Bounded fun, Enum fun) => AstGen (Program Name DefaultUni fun ()) genProgram = fmap eraseProgram AST.genProgram diff --git a/plutus-core/untyped-plutus-core/test/Scoping/Spec.hs b/plutus-core/untyped-plutus-core/test/Scoping/Spec.hs new file mode 100644 index 00000000000..bc780a5a70b --- /dev/null +++ b/plutus-core/untyped-plutus-core/test/Scoping/Spec.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE TypeApplications #-} + +module Scoping.Spec where + +import Generators (genProgram, genTerm) + +import UntypedPlutusCore (_soInlineHints, defaultSimplifyOpts) +import UntypedPlutusCore.Mark +import UntypedPlutusCore.Rename.Internal +import UntypedPlutusCore.Transform.CaseOfCase (caseOfCase) +import UntypedPlutusCore.Transform.CaseReduce (caseReduce) +import UntypedPlutusCore.Transform.Cse (cse) +import UntypedPlutusCore.Transform.FloatDelay (floatDelay) +import UntypedPlutusCore.Transform.ForceDelay (forceDelay) +import UntypedPlutusCore.Transform.Inline (inline) +import UntypedPlutusCore.Transform.Simplifier (evalSimplifierT) + +import PlutusCore.Default.Builtins (DefaultFun) +import PlutusCore.Rename +import PlutusCore.Test qualified as T + +import Test.Tasty + +-- See Note [Scoping tests API]. +test_names :: TestTree +test_names = testGroup "names" + [ T.test_scopingGood "renaming" (genProgram @DefaultFun) T.BindingRemovalNotOk T.PrerenameNo + rename + , T.test_scopingSpoilRenamer (genProgram @DefaultFun) markNonFreshProgram + renameProgramM + , T.test_scopingGood "case-of-case" (genTerm @DefaultFun) T.BindingRemovalOk T.PrerenameYes $ + evalSimplifierT . caseOfCase + , -- COKC removes entire branches, some of which are going to contain binders, but we still use + -- 'BindingRemovalNotOk', because the 'EstablishScoping' instance does not attempt to + -- reference bindings from one branch in another one. We could do that, but then we'd be + -- removing not just TODO. + T.test_scopingGood "case-of-known-constructor" + (genTerm @DefaultFun) + T.BindingRemovalOk -- COKC removes branches, which may (and likely do) contain bindings. + T.PrerenameYes + (evalSimplifierT . caseReduce) + , -- CSE creates entirely new names, which isn't supported by the scoping check machinery. + T.test_scopingBad "cse" + (genTerm @DefaultFun) + T.BindingRemovalOk + T.PrerenameYes + (evalSimplifierT . cse maxBound) + , T.test_scopingGood "float-delay" + (genTerm @DefaultFun) + T.BindingRemovalNotOk + T.PrerenameNo + (evalSimplifierT . floatDelay) + , T.test_scopingGood "force-delay" + (genTerm @DefaultFun) + T.BindingRemovalNotOk + T.PrerenameYes + (evalSimplifierT . forceDelay) + , T.test_scopingGood "inline" + (genTerm @DefaultFun) + T.BindingRemovalOk + T.PrerenameYes + (evalSimplifierT . inline True (_soInlineHints defaultSimplifyOpts) maxBound) + ] diff --git a/plutus-core/untyped-plutus-core/test/Spec.hs b/plutus-core/untyped-plutus-core/test/Spec.hs index ae6675c7574..a81a04d0918 100644 --- a/plutus-core/untyped-plutus-core/test/Spec.hs +++ b/plutus-core/untyped-plutus-core/test/Spec.hs @@ -15,6 +15,7 @@ import Evaluation.Machines (test_budget, test_machines, test_tallying) import Evaluation.Regressions (schnorrVerifyRegressions) import Flat.Spec (test_flat) import Generators (test_parsing) +import Scoping.Spec (test_names) import Transform.CaseOfCase.Test (test_caseOfCase) import Transform.Simplify (test_simplify) @@ -40,4 +41,5 @@ main = do , test_flat , schnorrVerifyRegressions , evalOrder + , test_names ]