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

-- | This module defines functions useful for testing.
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
".golden.plc")
  (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 (Term TyName Name uni fun ())
expected EvaluationResult (Term TyName Name uni fun ())
actual) ->
      -- Ditto.
      EvaluationResult (Term TyName Name uni fun ())
-> ShowPretty (EvaluationResult (Term TyName Name uni fun ()))
forall a. a -> ShowPretty a
ShowPretty EvaluationResult (Term TyName Name uni fun ())
expected ShowPretty (EvaluationResult (Term TyName Name uni fun ()))
-> ShowPretty (EvaluationResult (Term TyName Name uni fun ()))
-> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== EvaluationResult (Term TyName Name uni fun ())
-> ShowPretty (EvaluationResult (Term TyName Name uni fun ()))
forall a. a -> ShowPretty a
ShowPretty 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 ()