Skip to content

Commit

Permalink
fixup! Test case demostrates that CaseOfCase UPLC transform doesn't p…
Browse files Browse the repository at this point in the history
…reserve program semantics.
  • Loading branch information
Unisay committed May 8, 2024
1 parent c70a7f1 commit f79ed35
Show file tree
Hide file tree
Showing 8 changed files with 88 additions and 30 deletions.
4 changes: 2 additions & 2 deletions plutus-benchmark/nofib/test/9.6/knights10-4x4.budget.golden
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
({cpu: 2339861234
| mem: 7524812})
({cpu: 2340321234
| mem: 7526812})
2 changes: 1 addition & 1 deletion plutus-benchmark/nofib/test/9.6/knights10-4x4.size.golden
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1995
1998
2 changes: 1 addition & 1 deletion plutus-core/plutus-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,7 @@ library
UntypedPlutusCore.Parser
UntypedPlutusCore.Purity
UntypedPlutusCore.Rename
UntypedPlutusCore.Transform.CaseOfCase

other-modules:
Data.Aeson.Flatten
Expand Down Expand Up @@ -261,7 +262,6 @@ library
UntypedPlutusCore.Simplify.Opts
UntypedPlutusCore.Size
UntypedPlutusCore.Subst
UntypedPlutusCore.Transform.CaseOfCase
UntypedPlutusCore.Transform.CaseReduce
UntypedPlutusCore.Transform.Cse
UntypedPlutusCore.Transform.FloatDelay
Expand Down
Original file line number Diff line number Diff line change
@@ -1 +1,7 @@
(force ifThenElse b_0 1 2)
[
[
[ (force (builtin ifThenElse)) b_0 ]
(case (constr 0) (con integer 1) (con integer 2))
]
(case (constr 1) (con integer 1) (con integer 2))
]
Original file line number Diff line number Diff line change
@@ -1 +1,5 @@
(case (force ifThenElse b_0 t_1 (constr 1 [])) [1, 2])
(case
[ [ [ (force (builtin ifThenElse)) b_0 ] t_1 ] (constr 1) ]
(con integer 1)
(con integer 2)
)
Original file line number Diff line number Diff line change
@@ -1 +1,7 @@
(force ifThenElse b_0 (f_3 x_1 xs_2) 2)
[
[
[ (force (builtin ifThenElse)) b_0 ]
(case (constr 0 x_1 xs_2) f_3 (con integer 2))
]
(case (constr 1) f_3 (con integer 2))
]
81 changes: 58 additions & 23 deletions plutus-core/untyped-plutus-core/test/Transform/CaseOfCase/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@

module Transform.CaseOfCase.Test where

import Data.ByteString.Lazy qualified as BSL
import Data.Text.Encoding (encodeUtf8)
import Data.Vector qualified as V
import PlutusCore qualified as PLC
import PlutusCore.Evaluation.Machine.BuiltinCostModel (BuiltinCostModel)
Expand All @@ -12,25 +14,27 @@ import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultBuiltinCostMode
import PlutusCore.Evaluation.Machine.MachineParameters (CostModel (..), MachineParameters,
mkMachineParameters)
import PlutusCore.MkPlc (mkConstant, mkIterApp)
import PlutusCore.Quote (freshName, runQuote, runQuoteT)
import PlutusCore.Pretty
import PlutusCore.Quote (freshName, runQuote)
import PlutusPrelude (Default (def))
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Golden (goldenVsString)
import Test.Tasty.HUnit (testCase, (@?=))
import Transform.Simplify.Lib (goldenVsSimplified)
import UntypedPlutusCore (DefaultFun, DefaultUni, Name, Term (..), defaultSimplifyOpts,
simplifyTerm)
import UntypedPlutusCore (DefaultFun, DefaultUni, Name, Term (..))
import UntypedPlutusCore.Core qualified as UPLC
import UntypedPlutusCore.Evaluation.Machine.Cek (CekMachineCosts, CekValue, EvaluationResult (..),
noEmitter, unsafeEvaluateCek)
import UntypedPlutusCore.Transform.CaseOfCase (caseOfCase)

test_caseOfCase :: TestTree
test_caseOfCase =
testGroup
"CaseOfCase"
[ goldenVsSimplified "CaseOfCase/1" caseOfCase1
, goldenVsSimplified "CaseOfCase/2" caseOfCase2
, goldenVsSimplified "CaseOfCase/3" caseOfCase3
, caseOfCaseWithError
[ goldenVsSimplified "1" caseOfCase1
, goldenVsSimplified "2" caseOfCase2
, goldenVsSimplified "3" caseOfCase3
, goldenVsSimplified "withError" caseOfCaseWithError
, testCaseOfCaseWithError
]

caseOfCase1 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
Expand Down Expand Up @@ -73,23 +77,44 @@ caseOfCase3 = runQuote do
alts = V.fromList [altTrue, altFalse]
pure $ Case () (mkIterApp ite [((), Var () b), ((), true), ((), false)]) alts

caseOfCaseWithError :: TestTree
{- |
@
case (force ifThenElse) True True False of
True -> ()
False -> _|_
@
Evaluates to `()` because the first case alternative is selected.
(The _|_ is not evaluated because case alternatives are evaluated lazily).
After the `CaseOfCase` transformation the program should evaluate to `()` as well.
@
force ((force ifThenElse) True (delay ()) (delay _|_))
@
-}
caseOfCaseWithError :: Term Name DefaultUni DefaultFun ()
caseOfCaseWithError =
Case
()
( mkIterApp
(Force () (Builtin () PLC.IfThenElse))
[ ((), mkConstant @Bool () True)
, ((), Constr () 0 []) -- True
, ((), Constr () 1 []) -- False
]
)
(V.fromList [mkConstant @() () (), Error ()])

testCaseOfCaseWithError :: TestTree
testCaseOfCaseWithError =
testCase "Transformation doesn't evaluate error eagerly" do
let
originalTerm =
Case
()
( mkIterApp
(Force () (Builtin () PLC.IfThenElse))
[ ((), mkConstant @Bool () True)
, ((), Constr () 0 []) -- True
, ((), Constr () 1 []) -- False
]
)
(V.fromList [mkConstant @() () (), Error ()])
simplifiedTerm <- runQuoteT $ simplifyTerm defaultSimplifyOpts def originalTerm
evaluateUplc simplifiedTerm @?= evaluateUplc originalTerm
let simplifiedTerm = caseOfCase caseOfCaseWithError
evaluateUplc simplifiedTerm @?= evaluateUplc caseOfCaseWithError

----------------------------------------------------------------------------------------------------
-- Helper functions --------------------------------------------------------------------------------

evaluateUplc
:: UPLC.Term Name DefaultUni DefaultFun ()
Expand All @@ -101,3 +126,13 @@ evaluateUplc = fst <$> unsafeEvaluateCek noEmitter machineParameters
machineParameters
:: MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ()) =
mkMachineParameters def costModel

goldenVsSimplified :: String -> Term Name PLC.DefaultUni PLC.DefaultFun () -> TestTree
goldenVsSimplified name =
goldenVsString name ("untyped-plutus-core/test/Transform/CaseOfCase/" ++ name ++ ".uplc.golden")
. pure
. BSL.fromStrict
. encodeUtf8
. render
. prettyClassicDebug
. caseOfCase
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[
[
[ (force (builtin ifThenElse)) (con bool True) ]
(case (constr 0) (con unit ()) (error))
]
(case (constr 1) (con unit ()) (error))
]

0 comments on commit f79ed35

Please sign in to comment.