{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}

module Evaluation.Builtins.MakeRead
    ( test_makeRead
    ) where

import PlutusCore qualified as TPLC
import PlutusCore.Builtin
import PlutusCore.Default
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as TPLC
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result
import PlutusCore.MkPlc hiding (error)
import PlutusCore.Pretty
import PlutusCore.StdLib.Data.Unit
import PlutusPrelude

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 Data.Text (Text)

-- | 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
makeRead :: forall a.
(MakeKnown (Term TyName Name DefaultUni DefaultFun ()) a,
 ReadKnown (Term Name DefaultUni DefaultFun ()) a) =>
a -> EvaluationResult a
makeRead a
x = do
  HeadSpine (Term TyName Name DefaultUni DefaultFun ())
fXsTerm <- forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> EvaluationResult (HeadSpine val)
makeKnownOrFail @_ @(TPLC.Term TyName Name DefaultUni DefaultFun ()) a
x
  case Either
  (EvaluationException
     (MachineError DefaultFun)
     CekUserError
     (Term Name DefaultUni DefaultFun ()))
  a
-> Either
     (ErrorWithCause
        (MachineError DefaultFun) (Term Name DefaultUni DefaultFun ()))
     (EvaluationResult a)
forall structural operational term a.
Either (EvaluationException structural operational term) a
-> Either (ErrorWithCause structural term) (EvaluationResult a)
splitStructuralOperational (Either
   (EvaluationException
      (MachineError DefaultFun)
      CekUserError
      (Term Name DefaultUni DefaultFun ()))
   a
 -> Either
      (ErrorWithCause
         (MachineError DefaultFun) (Term Name DefaultUni DefaultFun ()))
      (EvaluationResult a))
-> Either
     (Error DefaultUni DefaultFun ())
     (Either
        (EvaluationException
           (MachineError DefaultFun)
           CekUserError
           (Term Name DefaultUni DefaultFun ()))
        a)
-> Either
     (Error DefaultUni DefaultFun ())
     (Either
        (ErrorWithCause
           (MachineError DefaultFun) (Term Name DefaultUni DefaultFun ()))
        (EvaluationResult a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (Either
        (EvaluationException
           (MachineError DefaultFun)
           CekUserError
           (Term Name DefaultUni DefaultFun ()))
        a)
forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun,
 ReadKnown (Term Name uni fun ()) a) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (Either (CekEvaluationException Name uni fun) a)
typecheckReadKnownCek BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def
    BuiltinCostModel
CostingPart DefaultUni DefaultFun
TPLC.defaultBuiltinCostModelForTesting (HeadSpine (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
HeadSpine (term ()) -> term ()
headSpineToTerm HeadSpine (Term TyName Name DefaultUni DefaultFun ())
fXsTerm) of
      Left Error DefaultUni DefaultFun ()
err          -> [Char] -> EvaluationResult a
forall a. HasCallStack => [Char] -> a
error ([Char] -> EvaluationResult a) -> [Char] -> EvaluationResult a
forall a b. (a -> b) -> a -> b
$ [Char]
"Type error" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Error DefaultUni DefaultFun () -> [Char]
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlcCondensedErrorClassic Error DefaultUni DefaultFun ()
err
      Right (Left ErrorWithCause
  (MachineError DefaultFun) (Term Name DefaultUni DefaultFun ())
err)  -> [Char] -> EvaluationResult a
forall a. HasCallStack => [Char] -> a
error ([Char] -> EvaluationResult a) -> [Char] -> EvaluationResult a
forall a b. (a -> b) -> a -> b
$ [Char]
"Evaluation error: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ErrorWithCause
  (MachineError DefaultFun) (Term Name DefaultUni DefaultFun ())
-> [Char]
forall a. Show a => a -> [Char]
show ErrorWithCause
  (MachineError DefaultFun) (Term Name DefaultUni DefaultFun ())
err
      Right (Right EvaluationResult a
res) -> EvaluationResult a
res

builtinRoundtrip
    :: ( MakeKnown (TPLC.Term TyName Name DefaultUni DefaultFun ()) a
       , ReadKnown (UPLC.Term Name DefaultUni DefaultFun ()) a
       , Show a, Eq a
       )
    => Gen a -> Property
builtinRoundtrip :: forall a.
(MakeKnown (Term TyName Name DefaultUni DefaultFun ()) a,
 ReadKnown (Term Name DefaultUni DefaultFun ()) a, Show a, Eq a) =>
Gen a -> Property
builtinRoundtrip Gen a
genX = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    a
x <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
genX
    case a -> EvaluationResult a
forall a.
(MakeKnown (Term TyName Name DefaultUni DefaultFun ()) a,
 ReadKnown (Term Name DefaultUni DefaultFun ()) a) =>
a -> EvaluationResult a
makeRead a
x of
        EvaluationResult a
EvaluationFailure    -> [Char] -> PropertyT IO ()
forall a. [Char] -> PropertyT IO a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"EvaluationFailure"
        EvaluationSuccess a
x' -> a
x a -> a -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== a
x'

test_textRoundtrip :: TestTree
test_textRoundtrip :: TestTree
test_textRoundtrip =
    [Char] -> PropertyName -> Property -> TestTree
testPropertyNamed [Char]
"textRoundtrip" PropertyName
"textRoundtrip" (Property -> TestTree)
-> (Gen Text -> Property) -> Gen Text -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen Text -> Property
forall a.
(MakeKnown (Term TyName Name DefaultUni DefaultFun ()) a,
 ReadKnown (Term Name DefaultUni DefaultFun ()) a, Show a, Eq a) =>
Gen a -> Property
builtinRoundtrip (Gen Text -> TestTree) -> Gen Text -> TestTree
forall a b. (a -> b) -> a -> b
$
        Range Int -> GenT Identity Char -> Gen Text
forall (m :: * -> *). MonadGen m => Range Int -> m Char -> m Text
Gen.text (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
0 Int
20) GenT Identity Char
forall (m :: * -> *). MonadGen m => m Char
Gen.unicode

-- | 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 :: BuiltinSemanticsVariant DefaultFun -> TestTree
test_collectText BuiltinSemanticsVariant DefaultFun
semVar = [Char] -> PropertyName -> Property -> TestTree
testPropertyNamed (BuiltinSemanticsVariant DefaultFun -> [Char]
forall a. Show a => a -> [Char]
show BuiltinSemanticsVariant DefaultFun
semVar) ([Char] -> PropertyName
forall a. IsString a => [Char] -> a
fromString ([Char] -> PropertyName) -> [Char] -> PropertyName
forall a b. (a -> b) -> a -> b
$ BuiltinSemanticsVariant DefaultFun -> [Char]
forall a. Show a => a -> [Char]
show BuiltinSemanticsVariant DefaultFun
semVar) (Property -> TestTree)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> TestTree) -> PropertyT IO () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
    [Text]
strs <- Gen [Text] -> PropertyT IO [Text]
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen [Text] -> PropertyT IO [Text])
-> (Gen Text -> Gen [Text]) -> Gen Text -> PropertyT IO [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Int -> Gen Text -> Gen [Text]
forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Gen.list (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
0 Int
10) (Gen Text -> PropertyT IO [Text])
-> Gen Text -> PropertyT IO [Text]
forall a b. (a -> b) -> a -> b
$ Range Int -> GenT Identity Char -> Gen Text
forall (m :: * -> *). MonadGen m => Range Int -> m Char -> m Text
Gen.text (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
0 Int
20) GenT Identity Char
forall (m :: * -> *). MonadGen m => m Char
Gen.unicode
    let step :: Text -> term () -> term ()
step Text
arg term ()
rest = term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> term () -> Type tyname DefaultUni () -> term ()
forall ann.
ann -> term ann -> Type tyname DefaultUni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
Trace) Type tyname DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text @DefaultUni () Text
arg
            , term ()
rest
            ]
        term :: Term TyName Name DefaultUni DefaultFun ()
term = (Text
 -> Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> [Text]
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Text
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall {term :: * -> *} {tyname} {name}.
TermLike term tyname name DefaultUni DefaultFun =>
Text -> term () -> term ()
step Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
strs)
    [Text]
strs' <- case BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
typecheckEvaluateCek BuiltinSemanticsVariant DefaultFun
semVar BuiltinCostModel
CostingPart DefaultUni DefaultFun
TPLC.defaultBuiltinCostModelForTesting Term TyName Name DefaultUni DefaultFun ()
term of
        Left Error DefaultUni DefaultFun ()
_                             -> PropertyT IO [Text]
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
        Right (EvaluationResult (Term Name DefaultUni DefaultFun ())
EvaluationFailure, [Text]
_)       -> PropertyT IO [Text]
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
        Right (EvaluationSuccess Term Name DefaultUni DefaultFun ()
_, [Text]
strs') -> [Text] -> PropertyT IO [Text]
forall a. a -> PropertyT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Text]
strs'
    [Text]
strs [Text] -> [Text] -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== [Text]
strs'

test_makeRead :: TestTree
test_makeRead :: TestTree
test_makeRead =
    [Char] -> [TestTree] -> TestTree
testGroup [Char]
"makeRead"
        [ TestTree
test_textRoundtrip
        , [Char] -> [TestTree] -> TestTree
testGroup [Char]
"collectText" ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ (BuiltinSemanticsVariant DefaultFun -> TestTree)
-> [BuiltinSemanticsVariant DefaultFun] -> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
map BuiltinSemanticsVariant DefaultFun -> TestTree
test_collectText [BuiltinSemanticsVariant DefaultFun]
forall a. (Enum a, Bounded a) => [a]
enumerate
        ]