Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Test] [Builtin] Polish 'MakeRead' tests #6202

Merged
merged 1 commit into from
Jun 12, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -20,38 +20,29 @@ import UntypedPlutusCore as UPLC (Name, Term, TyName)

import Evaluation.Builtins.Common

import Data.String (fromString)
import Hedgehog hiding (Size, Var)
import Hedgehog.Gen qualified as Gen
import Hedgehog.Range qualified as Range
import Test.Tasty
import Test.Tasty.Hedgehog
import Test.Tasty.HUnit

import Data.Text (Text)

-- | Convert a Haskell value to a PLC term and then convert back to a Haskell value
-- of a different type.
readMakeHetero
:: ( MakeKnown (TPLC.Term TyName Name DefaultUni DefaultFun ()) a
, ReadKnown (UPLC.Term Name DefaultUni DefaultFun ()) b
)
=> a -> EvaluationResult b
readMakeHetero x = do
xTerm <- makeKnownOrFail @_ @(TPLC.Term TyName Name DefaultUni DefaultFun ()) x
case extractEvaluationResult <$> typecheckReadKnownCek def
TPLC.defaultBuiltinCostModelForTesting xTerm of
Left err -> error $ "Type error" ++ displayPlcCondensedErrorClassic err
Right (Left err) -> error $ "Evaluation error: " ++ show err
Right (Right res) -> res

-- | Convert a Haskell value to a PLC term and then convert back to a Haskell value
-- of the same type.
readMake
-- | Lift a Haskell value into a PLC term, evaluate it and unlift the result back to the original
-- Haskell value.
makeRead
:: ( MakeKnown (TPLC.Term TyName Name DefaultUni DefaultFun ()) a
, ReadKnown (UPLC.Term Name DefaultUni DefaultFun ()) a
)
=> a -> EvaluationResult a
readMake = readMakeHetero
makeRead x = do
xTerm <- makeKnownOrFail @_ @(TPLC.Term TyName Name DefaultUni DefaultFun ()) x
case extractEvaluationResult <$> typecheckReadKnownCek def
TPLC.defaultBuiltinCostModelForTesting xTerm of
Left err -> error $ "Type error" ++ displayPlcCondensedErrorClassic err
Right (Left err) -> error $ "Evaluation error: " ++ show err
Right (Right res) -> res

builtinRoundtrip
:: ( MakeKnown (TPLC.Term TyName Name DefaultUni DefaultFun ()) a
Expand All @@ -61,7 +52,7 @@ builtinRoundtrip
=> Gen a -> Property
builtinRoundtrip genX = property $ do
x <- forAll genX
case readMake x of
case makeRead x of
EvaluationFailure -> fail "EvaluationFailure"
EvaluationSuccess x' -> x === x'

Expand All @@ -70,42 +61,29 @@ test_textRoundtrip =
testPropertyNamed "textRoundtrip" "textRoundtrip" . builtinRoundtrip $
Gen.text (Range.linear 0 20) Gen.unicode

-- | Generate a bunch of 'text's, put each of them into a 'Term', apply a builtin over
-- each of these terms such that being evaluated it calls a Haskell function that appends a char to
-- the contents of an external 'IORef' and assemble all the resulting terms together in a single
-- term where all characters are passed to lambdas and ignored, so that only 'unitval' is returned
-- in the end.
-- After evaluation of the CEK machine finishes, read the 'IORef' and check that you got the exact
-- same sequence of 'text's that was originally generated.
-- Calls 'unsafePerformIO' internally while evaluating the term, because the CEK machine can only
-- handle pure things and 'unsafePerformIO' is the way to pretend an effectful thing is pure.
test_collectText :: TestTree
test_collectText = testPropertyNamed "collectText" "collectText" . property $ do
-- | Generate a bunch of 'text's, put each of them into a 'Term' and apply the @Trace@ builtin over
-- each of these terms and assemble all the resulting terms together in a single term where all
-- characters are passed to lambdas and ignored, so that only 'unitval' is returned in the end.
--
-- After evaluation of the CEK machine finishes, check that the logs contains the exact same
-- sequence of 'text's that was originally generated.
test_collectText :: BuiltinSemanticsVariant DefaultFun -> TestTree
test_collectText semVar = testPropertyNamed (show semVar) (fromString $ show semVar) . property $ do
strs <- forAll . Gen.list (Range.linear 0 10) $ Gen.text (Range.linear 0 20) Gen.unicode
let step arg rest = mkIterAppNoAnn (tyInst () (builtin () Trace) unit)
[ mkConstant @Text @DefaultUni () arg
, rest
]
term = foldr step unitval (reverse strs)
-- FIXME: semantic variant?
strs' <- case typecheckEvaluateCek def TPLC.defaultBuiltinCostModelForTesting term of
strs' <- case typecheckEvaluateCek semVar TPLC.defaultBuiltinCostModelForTesting term of
Left _ -> failure
Right (EvaluationFailure, _) -> failure
Right (EvaluationSuccess _, strs') -> return strs'
strs === strs'

test_noticeEvaluationFailure :: TestTree
test_noticeEvaluationFailure =
testCase "noticeEvaluationFailure" . assertBool "'EvaluationFailure' ignored" $
isEvaluationFailure $ do
_ <- readMake True
_ <- readMakeHetero @(EvaluationResult ()) @() EvaluationFailure
readMake ("a"::Text)

test_makeRead :: TestTree
test_makeRead =
testGroup "makeRead"
[ test_textRoundtrip
, test_collectText
, test_noticeEvaluationFailure
, testGroup "collectText" $ map test_collectText enumerate
]
Loading