-- | This module defines functions useful for testing.

{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}

module PlutusCore.Generators.Hedgehog.Test
    ( TypeEvalCheckError (..)
    , TypeEvalCheckResult (..)
    , TypeEvalCheckM
    , typeEvalCheckBy
    , unsafeTypeEvalCheck
    , getSampleTermValue
    , getSampleProgramAndValue
    , printSampleProgramAndValue
    , sampleProgramValueGolden
    , propEvaluate
    ) where

import PlutusPrelude (ShowPretty (..))

import PlutusCore.Generators.Hedgehog.Interesting
import PlutusCore.Generators.Hedgehog.TypeEvalCheck
import PlutusCore.Generators.Hedgehog.Utils

import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Default
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result
import PlutusCore.Name.Unique
import PlutusCore.Pretty

import Control.Monad ((>=>))
import Data.Functor ((<&>))
import Data.Text.IO qualified as Text
import Hedgehog hiding (Size, Var, eval)
import Hedgehog.Gen qualified as Gen
import System.FilePath ((</>))

-- | Generate a term using a given generator and check that it's well-typed and evaluates correctly.
getSampleTermValue
    :: ( uni ~ DefaultUni, fun ~ DefaultFun
       , KnownTypeAst TyName uni a, MakeKnown (Term TyName Name uni fun ()) a
       )
    => TermGen a
    -> IO (TermOf (Term TyName Name uni fun ()) (EvaluationResult (Term TyName Name uni fun ())))
getSampleTermValue :: forall (uni :: * -> *) fun a.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a) =>
TermGen a
-> IO
     (TermOf
        (Term TyName Name uni fun ())
        (EvaluationResult (Term TyName Name uni fun ())))
getSampleTermValue TermGen a
genTerm = Gen
  (TermOf
     (Term TyName Name uni fun ())
     (EvaluationResult (Term TyName Name uni fun ())))
-> IO
     (TermOf
        (Term TyName Name uni fun ())
        (EvaluationResult (Term TyName Name uni fun ())))
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Gen.sample (Gen
   (TermOf
      (Term TyName Name uni fun ())
      (EvaluationResult (Term TyName Name uni fun ())))
 -> IO
      (TermOf
         (Term TyName Name uni fun ())
         (EvaluationResult (Term TyName Name uni fun ()))))
-> Gen
     (TermOf
        (Term TyName Name uni fun ())
        (EvaluationResult (Term TyName Name uni fun ())))
-> IO
     (TermOf
        (Term TyName Name uni fun ())
        (EvaluationResult (Term TyName Name uni fun ())))
forall a b. (a -> b) -> a -> b
$ TermOf (Term TyName Name uni fun ()) a
-> TermOf
     (Term TyName Name uni fun ())
     (EvaluationResult (Term TyName Name uni fun ()))
forall (uni :: * -> *) fun a.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a) =>
TermOf (Term TyName Name uni fun ()) a
-> TermOf
     (Term TyName Name uni fun ())
     (EvaluationResult (Term TyName Name uni fun ()))
unsafeTypeEvalCheck (TermOf (Term TyName Name uni fun ()) a
 -> TermOf
      (Term TyName Name uni fun ())
      (EvaluationResult (Term TyName Name uni fun ())))
-> GenT Identity (TermOf (Term TyName Name uni fun ()) a)
-> Gen
     (TermOf
        (Term TyName Name uni fun ())
        (EvaluationResult (Term TyName Name uni fun ())))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity (TermOf (Term TyName Name uni fun ()) a)
TermGen a
genTerm

-- | Generate a program using a given generator and check that it's well-typed and evaluates
-- correctly.
getSampleProgramAndValue
    :: ( uni ~ DefaultUni, fun ~ DefaultFun
       , KnownTypeAst TyName uni a, MakeKnown (Term TyName Name uni fun ()) a
       )
    => TermGen a
    -> IO (Program TyName Name uni fun (), EvaluationResult (Term TyName Name uni fun ()))
getSampleProgramAndValue :: forall (uni :: * -> *) fun a.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a) =>
TermGen a
-> IO
     (Program TyName Name uni fun (),
      EvaluationResult (Term TyName Name uni fun ()))
getSampleProgramAndValue TermGen a
genTerm =
    TermGen a
-> IO
     (TermOf
        (Term TyName Name uni fun ())
        (EvaluationResult (Term TyName Name uni fun ())))
forall (uni :: * -> *) fun a.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a) =>
TermGen a
-> IO
     (TermOf
        (Term TyName Name uni fun ())
        (EvaluationResult (Term TyName Name uni fun ())))
getSampleTermValue TermGen a
genTerm IO
  (TermOf
     (Term TyName Name uni fun ())
     (EvaluationResult (Term TyName Name uni fun ())))
-> (TermOf
      (Term TyName Name uni fun ())
      (EvaluationResult (Term TyName Name uni fun ()))
    -> (Program TyName Name uni fun (),
        EvaluationResult (Term TyName Name uni fun ())))
-> IO
     (Program TyName Name uni fun (),
      EvaluationResult (Term TyName Name uni fun ()))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(TermOf Term TyName Name uni fun ()
term EvaluationResult (Term TyName Name uni fun ())
result) ->
        (()
-> Version
-> Term TyName Name uni fun ()
-> Program TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program () Version
latestVersion Term TyName Name uni fun ()
term, EvaluationResult (Term TyName Name uni fun ())
result)

-- | Generate a program using a given generator, check that it's well-typed and evaluates correctly
-- and pretty-print it to stdout using the default pretty-printing mode.
printSampleProgramAndValue
    :: ( uni ~ DefaultUni, fun ~ DefaultFun
       , KnownTypeAst TyName uni a, MakeKnown (Term TyName Name uni fun ()) a
       )
    => TermGen a -> IO ()
printSampleProgramAndValue :: forall (uni :: * -> *) fun a.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a) =>
TermGen a -> IO ()
printSampleProgramAndValue =
    TermGen a
-> IO
     (Program TyName Name DefaultUni DefaultFun (),
      EvaluationResult (Term TyName Name DefaultUni DefaultFun ()))
forall (uni :: * -> *) fun a.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a) =>
TermGen a
-> IO
     (Program TyName Name uni fun (),
      EvaluationResult (Term TyName Name uni fun ()))
getSampleProgramAndValue (TermGen a
 -> IO
      (Program TyName Name DefaultUni DefaultFun (),
       EvaluationResult (Term TyName Name DefaultUni DefaultFun ())))
-> ((Program TyName Name DefaultUni DefaultFun (),
     EvaluationResult (Term TyName Name DefaultUni DefaultFun ()))
    -> IO ())
-> TermGen a
-> IO ()
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \(Program TyName Name DefaultUni DefaultFun ()
program, EvaluationResult (Term TyName Name DefaultUni DefaultFun ())
value) -> do
        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Program TyName Name DefaultUni DefaultFun () -> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlc Program TyName Name DefaultUni DefaultFun ()
program
        String -> IO ()
putStrLn String
""
        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ EvaluationResult (Term TyName Name DefaultUni DefaultFun ())
-> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlc EvaluationResult (Term TyName Name DefaultUni DefaultFun ())
value

-- | Generate a pair of files: @<folder>.<name>.plc@ and @<folder>.<name>.plc.golden@.
-- The first file contains a term generated by a term generator (wrapped in 'Program'),
-- the second file contains the result of evaluation of the term.
sampleProgramValueGolden
    :: ( uni ~ DefaultUni, fun ~ DefaultFun
       , KnownTypeAst TyName uni a, MakeKnown (Term TyName Name uni fun ()) a
       )
    => String     -- ^ @folder@
    -> String     -- ^ @name@
    -> TermGen a  -- ^ A term generator.
    -> IO ()
sampleProgramValueGolden :: forall (uni :: * -> *) fun a.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a) =>
String -> String -> TermGen a -> IO ()
sampleProgramValueGolden String
folder String
name TermGen a
genTerm = do
    let filePlc :: String
filePlc       = String
folder String -> String -> String
</> (String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".plc")
        filePlcGolden :: String
filePlcGolden = String
folder String -> String -> String
</> (String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".plc.golden")
    (Program TyName Name DefaultUni DefaultFun ()
program, EvaluationResult (Term TyName Name DefaultUni DefaultFun ())
value) <- TermGen a
-> IO
     (Program TyName Name DefaultUni DefaultFun (),
      EvaluationResult (Term TyName Name DefaultUni DefaultFun ()))
forall (uni :: * -> *) fun a.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a) =>
TermGen a
-> IO
     (Program TyName Name uni fun (),
      EvaluationResult (Term TyName Name uni fun ()))
getSampleProgramAndValue TermGen a
genTerm
    String -> Text -> IO ()
Text.writeFile String
filePlc       (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Program TyName Name DefaultUni DefaultFun () -> Text
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlc Program TyName Name DefaultUni DefaultFun ()
program
    String -> Text -> IO ()
Text.writeFile String
filePlcGolden (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ EvaluationResult (Term TyName Name DefaultUni DefaultFun ())
-> Text
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlc EvaluationResult (Term TyName Name DefaultUni DefaultFun ())
value

-- | A property-based testing procedure for evaluators.
-- Checks whether a term generated along with the value it's supposed to compute to
-- indeed computes to that value according to the provided evaluate.
propEvaluate
    :: ( uni ~ DefaultUni, fun ~ DefaultFun
       , KnownTypeAst TyName uni a, MakeKnown (Term TyName Name uni fun ()) a
       , PrettyPlc structural
       )
    => (Term TyName Name uni fun () ->
           Either
            (EvaluationException structural operational (Term TyName Name uni fun ()))
            (Term TyName Name uni fun ()))
       -- ^ An evaluator.
    -> TermGen a  -- ^ A term/value generator.
    -> Property
propEvaluate :: forall (uni :: * -> *) fun a structural operational.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a, PrettyPlc structural) =>
(Term TyName Name uni fun ()
 -> Either
      (EvaluationException
         structural operational (Term TyName Name uni fun ()))
      (Term TyName Name uni fun ()))
-> TermGen a -> Property
propEvaluate Term TyName Name uni fun ()
-> Either
     (EvaluationException
        structural operational (Term TyName Name uni fun ()))
     (Term TyName Name uni fun ())
eval TermGen a
genTermOfTbv = TestLimit -> Property -> Property
withTests TestLimit
200 (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    TermOf (Term TyName Name DefaultUni DefaultFun ()) a
termOfTbv <- TermGen a
-> PropertyT
     IO (TermOf (Term TyName Name DefaultUni DefaultFun ()) a)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyT m a
forAllNoShow TermGen a
genTermOfTbv
    case (Term TyName Name uni fun ()
 -> Either
      (EvaluationException
         structural operational (Term TyName Name uni fun ()))
      (Term TyName Name uni fun ()))
-> TermOf (Term TyName Name uni fun ()) a
-> TypeEvalCheckM
     uni
     fun
     (TermOf
        (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun))
forall (uni :: * -> *) fun a structural operational.
(uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a,
 MakeKnown (Term TyName Name uni fun ()) a, PrettyPlc structural) =>
(Term TyName Name uni fun ()
 -> Either
      (EvaluationException
         structural operational (Term TyName Name uni fun ()))
      (Term TyName Name uni fun ()))
-> TermOf (Term TyName Name uni fun ()) a
-> TypeEvalCheckM
     uni
     fun
     (TermOf
        (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun))
typeEvalCheckBy Term TyName Name uni fun ()
-> Either
     (EvaluationException
        structural operational (Term TyName Name uni fun ()))
     (Term TyName Name uni fun ())
eval TermOf (Term TyName Name uni fun ()) a
TermOf (Term TyName Name DefaultUni DefaultFun ()) a
termOfTbv of
        Left (TypeEvalCheckErrorIllFormed Error uni fun ()
err)             -> String -> PropertyT IO ()
forall a. String -> PropertyT IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ Error uni fun () -> String
forall err. PrettyPlc err => err -> String
prettyPlcErrorString Error uni fun ()
err
        Left (TypeEvalCheckErrorIllTyped Normalized (Type TyName uni ())
expected Normalized (Type TyName uni ())
actual)  ->
            -- We know that these two are distinct, but there is no nice way we
            -- can report this via 'hedgehog' except by comparing them here again.
            Normalized (Type TyName uni ())
-> ShowPretty (Normalized (Type TyName uni ()))
forall a. a -> ShowPretty a
ShowPretty Normalized (Type TyName uni ())
expected ShowPretty (Normalized (Type TyName uni ()))
-> ShowPretty (Normalized (Type TyName uni ())) -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== Normalized (Type TyName uni ())
-> ShowPretty (Normalized (Type TyName uni ()))
forall a. a -> ShowPretty a
ShowPretty Normalized (Type TyName uni ())
actual
        Left (TypeEvalCheckErrorException String
err)             -> String -> PropertyT IO ()
forall a. String -> PropertyT IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
        Left (TypeEvalCheckErrorIllEvaled EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
expected EvaluationResult (Term TyName Name uni fun ())
actual) ->
            -- Ditto.
            EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> ShowPretty
     (EvaluationResult (HeadSpine (Term TyName Name uni fun ())))
forall a. a -> ShowPretty a
ShowPretty EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
expected ShowPretty
  (EvaluationResult (HeadSpine (Term TyName Name uni fun ())))
-> ShowPretty
     (EvaluationResult (HeadSpine (Term TyName Name uni fun ())))
-> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> ShowPretty
     (EvaluationResult (HeadSpine (Term TyName Name uni fun ())))
forall a. a -> ShowPretty a
ShowPretty ((Term TyName Name uni fun ()
 -> HeadSpine (Term TyName Name uni fun ()))
-> EvaluationResult (Term TyName Name uni fun ())
-> EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
forall a b. (a -> b) -> EvaluationResult a -> EvaluationResult b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term TyName Name uni fun ()
-> HeadSpine (Term TyName Name uni fun ())
forall a. a -> HeadSpine a
HeadOnly EvaluationResult (Term TyName Name uni fun ())
actual)
        Right TermOf (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun)
_                                            -> () -> PropertyT IO ()
forall a. a -> PropertyT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()