-- editorconfig-checker-disable-file
-- | This module defines types and functions related to "type-eval checking".

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE TemplateHaskell        #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

module PlutusCore.Generators.Hedgehog.TypeEvalCheck
    ( TypeEvalCheckError (..)
    , TypeEvalCheckResult (..)
    , TypeEvalCheckM
    , typeEvalCheckBy
    , unsafeTypeEvalCheck
    ) where

import PlutusPrelude

import PlutusCore.Generators.Hedgehog.TypedBuiltinGen
import PlutusCore.Generators.Hedgehog.Utils

import PlutusCore
import PlutusCore.Builtin
import PlutusCore.Evaluation.Machine.Ck
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Normalize
import PlutusCore.Pretty

import Control.Lens.TH
import Control.Monad.Except
import Data.Proxy
import Data.String
import Prettyprinter

{- Note [Type-eval checking]
We generate terms along with values they are supposed to evaluate to. Before evaluating a term,
we type check it. Then we evaluate the term and check whether the expected result matches with
the actual one. Thus "type-eval checking".
-}

-- | The type of errors that can occur during type-eval checking.
data TypeEvalCheckError uni fun
    = TypeEvalCheckErrorIllFormed !(Error uni fun ())
    | TypeEvalCheckErrorIllTyped
          !(Normalized (Type TyName uni ()))
          !(Normalized (Type TyName uni ()))
    | TypeEvalCheckErrorException !String
    | TypeEvalCheckErrorIllEvaled
          !(EvaluationResult (HeadSpine (Term TyName Name uni fun ())))
          !(EvaluationResult (Term TyName Name uni fun ()))
      -- ^ The former is an expected result of evaluation, the latter -- is an actual one.
makeClassyPrisms ''TypeEvalCheckError

instance ann ~ () => AsError (TypeEvalCheckError uni fun) uni fun ann where
    _Error :: Prism' (TypeEvalCheckError uni fun) (Error uni fun ann)
_Error = p (Error uni fun ()) (f (Error uni fun ()))
-> p (TypeEvalCheckError uni fun) (f (TypeEvalCheckError uni fun))
forall r (uni :: * -> *) fun.
AsTypeEvalCheckError r uni fun =>
Prism' r (Error uni fun ())
Prism' (TypeEvalCheckError uni fun) (Error uni fun ())
_TypeEvalCheckErrorIllFormed (p (Error uni fun ()) (f (Error uni fun ()))
 -> p (TypeEvalCheckError uni fun) (f (TypeEvalCheckError uni fun)))
-> (p (Error uni fun ann) (f (Error uni fun ann))
    -> p (Error uni fun ()) (f (Error uni fun ())))
-> p (Error uni fun ann) (f (Error uni fun ann))
-> p (TypeEvalCheckError uni fun) (f (TypeEvalCheckError uni fun))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Error uni fun ann) (f (Error uni fun ann))
-> p (Error uni fun ()) (f (Error uni fun ()))
forall r (uni :: * -> *) fun ann.
AsError r uni fun ann =>
Prism' r (Error uni fun ann)
Prism' (Error uni fun ()) (Error uni fun ann)
_Error

instance ann ~ () => AsTypeError (TypeEvalCheckError uni fun) (Term TyName Name uni fun ann) uni fun ann where
    _TypeError :: Prism'
  (TypeEvalCheckError uni fun)
  (TypeError (Term TyName Name uni fun ann) uni fun ann)
_TypeError = p (Error uni fun ()) (f (Error uni fun ()))
-> p (TypeEvalCheckError uni fun) (f (TypeEvalCheckError uni fun))
forall r (uni :: * -> *) fun.
AsTypeEvalCheckError r uni fun =>
Prism' r (Error uni fun ())
Prism' (TypeEvalCheckError uni fun) (Error uni fun ())
_TypeEvalCheckErrorIllFormed (p (Error uni fun ()) (f (Error uni fun ()))
 -> p (TypeEvalCheckError uni fun) (f (TypeEvalCheckError uni fun)))
-> (p (TypeError (Term TyName Name uni fun ann) uni fun ann)
      (f (TypeError (Term TyName Name uni fun ann) uni fun ann))
    -> p (Error uni fun ()) (f (Error uni fun ())))
-> p (TypeError (Term TyName Name uni fun ann) uni fun ann)
     (f (TypeError (Term TyName Name uni fun ann) uni fun ann))
-> p (TypeEvalCheckError uni fun) (f (TypeEvalCheckError uni fun))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (TypeError (Term TyName Name uni fun ann) uni fun ann)
  (f (TypeError (Term TyName Name uni fun ann) uni fun ann))
-> p (Error uni fun ()) (f (Error uni fun ()))
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism'
  (Error uni fun ())
  (TypeError (Term TyName Name uni fun ann) uni fun ann)
_TypeError

-- | Type-eval checking of a term results in a value of this type.
data TypeEvalCheckResult uni fun = TypeEvalCheckResult
    { forall (uni :: * -> *) fun.
TypeEvalCheckResult uni fun -> Normalized (Type TyName uni ())
_termCheckResultType  :: Normalized (Type TyName uni ())
      -- ^ The type of the term.
    , forall (uni :: * -> *) fun.
TypeEvalCheckResult uni fun
-> EvaluationResult (Term TyName Name uni fun ())
_termCheckResultValue :: EvaluationResult (Term TyName Name uni fun ())
      -- ^ The result of evaluation of the term.
    }

instance ( PrettyBy config (Type TyName uni ())
         , PrettyBy config (Term TyName Name uni fun ())
         , PrettyBy config (HeadSpine (Term TyName Name uni fun ()))
         , PrettyBy config (Error uni fun ())
         ) => PrettyBy config (TypeEvalCheckError uni fun) where
    prettyBy :: forall ann. config -> TypeEvalCheckError uni fun -> Doc ann
prettyBy config
config (TypeEvalCheckErrorIllFormed Error uni fun ()
err)             =
        Doc ann
"The term is ill-formed:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> config -> Error uni fun () -> Doc ann
forall ann. config -> Error uni fun () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config Error uni fun ()
err
    prettyBy config
config (TypeEvalCheckErrorIllTyped Normalized (Type TyName uni ())
expected Normalized (Type TyName uni ())
actual) =
        Doc ann
"The expected type:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> config -> Normalized (Type TyName uni ()) -> Doc ann
forall ann. config -> Normalized (Type TyName uni ()) -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config Normalized (Type TyName uni ())
expected Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<>
        Doc ann
"doesn't match with the actual type:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> config -> Normalized (Type TyName uni ()) -> Doc ann
forall ann. config -> Normalized (Type TyName uni ()) -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config Normalized (Type TyName uni ())
actual
    prettyBy config
_      (TypeEvalCheckErrorException String
err)             =
        Doc ann
"An exception occurred:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall a. IsString a => String -> a
fromString String
err
    prettyBy config
config (TypeEvalCheckErrorIllEvaled EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
expected EvaluationResult (Term TyName Name uni fun ())
actual) =
        Doc ann
"The expected value:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> config
-> EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> Doc ann
forall ann.
config
-> EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
expected Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<>
        Doc ann
"doesn't match with the actual value:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> config -> EvaluationResult (Term TyName Name uni fun ()) -> Doc ann
forall ann.
config -> EvaluationResult (Term TyName Name uni fun ()) -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config EvaluationResult (Term TyName Name uni fun ())
actual

-- | The monad type-eval checking runs in.
type TypeEvalCheckM uni fun = Either (TypeEvalCheckError uni fun)

-- See Note [Type-eval checking].
-- | Type check and evaluate a term and check that the expected result is equal to the actual one.
typeEvalCheckBy
    :: ( 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.
    -> TermOf (Term TyName Name uni fun ()) a
    -> TypeEvalCheckM uni fun (TermOf (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun))
typeEvalCheckBy :: 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 ()
term (a
x :: a)) = Term TyName Name uni fun ()
-> TypeEvalCheckResult uni fun
-> TermOf
     (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun)
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name uni fun ()
term (TypeEvalCheckResult uni fun
 -> TermOf
      (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun))
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
-> Either
     (TypeEvalCheckError uni fun)
     (TermOf
        (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    let tyExpected :: Normalized (Type TyName uni ())
tyExpected = Quote (Normalized (Type TyName uni ()))
-> Normalized (Type TyName uni ())
forall a. Quote a -> a
runQuote (Quote (Normalized (Type TyName uni ()))
 -> Normalized (Type TyName uni ()))
-> (Type TyName uni () -> Quote (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type TyName uni () -> Quote (Normalized (Type TyName uni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType (Type TyName uni () -> Normalized (Type TyName uni ()))
-> Type TyName uni () -> Normalized (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ Proxy a -> Type TyName uni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
        valExpected :: EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
valExpected = a -> EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> EvaluationResult (HeadSpine val)
makeKnownOrFail a
x
    Normalized (Type TyName uni ())
tyActual <- QuoteT
  (Either (TypeEvalCheckError uni fun))
  (Normalized (Type TyName uni ()))
-> Either
     (TypeEvalCheckError uni fun) (Normalized (Type TyName uni ()))
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT
   (Either (TypeEvalCheckError uni fun))
   (Normalized (Type TyName uni ()))
 -> Either
      (TypeEvalCheckError uni fun) (Normalized (Type TyName uni ())))
-> QuoteT
     (Either (TypeEvalCheckError uni fun))
     (Normalized (Type TyName uni ()))
-> Either
     (TypeEvalCheckError uni fun) (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ do
        TypeCheckConfig uni fun
config <- ()
-> QuoteT
     (Either (TypeEvalCheckError uni fun)) (TypeCheckConfig uni fun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
getDefTypeCheckConfig ()
        TypeCheckConfig uni fun
-> Term TyName Name uni fun ()
-> QuoteT
     (Either (TypeEvalCheckError uni fun))
     (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
inferType TypeCheckConfig uni fun
config Term TyName Name uni fun ()
term
    if Normalized (Type TyName uni ())
tyExpected Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ()) -> Bool
forall a. Eq a => a -> a -> Bool
== Normalized (Type TyName uni ())
tyActual
        then case Either
  (EvaluationException
     structural operational (Term TyName Name uni fun ()))
  (Term TyName Name uni fun ())
-> Either
     (ErrorWithCause structural (Term TyName Name uni fun ()))
     (EvaluationResult (Term TyName Name uni fun ()))
forall structural operational term a.
Either (EvaluationException structural operational term) a
-> Either (ErrorWithCause structural term) (EvaluationResult a)
splitStructuralOperational (Either
   (EvaluationException
      structural operational (Term TyName Name uni fun ()))
   (Term TyName Name uni fun ())
 -> Either
      (ErrorWithCause structural (Term TyName Name uni fun ()))
      (EvaluationResult (Term TyName Name uni fun ())))
-> Either
     (EvaluationException
        structural operational (Term TyName Name uni fun ()))
     (Term TyName Name uni fun ())
-> Either
     (ErrorWithCause structural (Term TyName Name uni fun ()))
     (EvaluationResult (Term TyName Name uni fun ()))
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
-> Either
     (EvaluationException
        structural operational (Term TyName Name uni fun ()))
     (Term TyName Name uni fun ())
eval Term TyName Name uni fun ()
term of
                Right EvaluationResult (Term TyName Name uni fun ())
valActual ->
                    if EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
valExpected EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> Bool
forall a. Eq a => a -> a -> Bool
== (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 ())
valActual
                        then TypeEvalCheckResult uni fun
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
forall a. a -> Either (TypeEvalCheckError uni fun) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeEvalCheckResult uni fun
 -> Either
      (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun))
-> TypeEvalCheckResult uni fun
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
forall a b. (a -> b) -> a -> b
$ Normalized (Type TyName uni ())
-> EvaluationResult (Term TyName Name uni fun ())
-> TypeEvalCheckResult uni fun
forall (uni :: * -> *) fun.
Normalized (Type TyName uni ())
-> EvaluationResult (Term TyName Name uni fun ())
-> TypeEvalCheckResult uni fun
TypeEvalCheckResult Normalized (Type TyName uni ())
tyExpected EvaluationResult (Term TyName Name uni fun ())
valActual
                        else TypeEvalCheckError uni fun
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
forall a.
TypeEvalCheckError uni fun -> Either (TypeEvalCheckError uni fun) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeEvalCheckError uni fun
 -> Either
      (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun))
-> TypeEvalCheckError uni fun
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
forall a b. (a -> b) -> a -> b
$ EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> EvaluationResult (Term TyName Name uni fun ())
-> TypeEvalCheckError uni fun
forall (uni :: * -> *) fun.
EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
-> EvaluationResult (Term TyName Name uni fun ())
-> TypeEvalCheckError uni fun
TypeEvalCheckErrorIllEvaled EvaluationResult (HeadSpine (Term TyName Name uni fun ()))
valExpected EvaluationResult (Term TyName Name uni fun ())
valActual
                Left ErrorWithCause structural (Term TyName Name uni fun ())
exc        -> TypeEvalCheckError DefaultUni DefaultFun
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
forall a.
TypeEvalCheckError DefaultUni DefaultFun
-> Either (TypeEvalCheckError uni fun) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeEvalCheckError DefaultUni DefaultFun
 -> Either
      (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun))
-> TypeEvalCheckError DefaultUni DefaultFun
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
forall a b. (a -> b) -> a -> b
$ String -> TypeEvalCheckError DefaultUni DefaultFun
forall (uni :: * -> *) fun. String -> TypeEvalCheckError uni fun
TypeEvalCheckErrorException (String -> TypeEvalCheckError DefaultUni DefaultFun)
-> String -> TypeEvalCheckError DefaultUni DefaultFun
forall a b. (a -> b) -> a -> b
$ ErrorWithCause structural (Term TyName Name uni fun ()) -> String
forall a. Show a => a -> String
show ErrorWithCause structural (Term TyName Name uni fun ())
exc
        else TypeEvalCheckError uni DefaultFun
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
forall a.
TypeEvalCheckError uni DefaultFun
-> Either (TypeEvalCheckError uni fun) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeEvalCheckError uni DefaultFun
 -> Either
      (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun))
-> TypeEvalCheckError uni DefaultFun
-> Either
     (TypeEvalCheckError uni fun) (TypeEvalCheckResult uni fun)
forall a b. (a -> b) -> a -> b
$ Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeEvalCheckError uni DefaultFun
forall (uni :: * -> *) fun.
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ()) -> TypeEvalCheckError uni fun
TypeEvalCheckErrorIllTyped Normalized (Type TyName uni ())
tyExpected Normalized (Type TyName uni ())
tyActual

-- | Type check and evaluate a term and check that the expected result is equal to the actual one.
-- Throw an error in case something goes wrong.
unsafeTypeEvalCheck
    :: ( 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 :: 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
termOfTbv = do
    let errOrRes :: TypeEvalCheckM
  uni
  DefaultFun
  (TermOf
     (Term TyName Name uni DefaultFun ())
     (TypeEvalCheckResult uni DefaultFun))
errOrRes = (Term TyName Name uni DefaultFun ()
 -> Either
      (EvaluationException
         (MachineError DefaultFun)
         CkUserError
         (Term TyName Name uni DefaultFun ()))
      (Term TyName Name uni DefaultFun ()))
-> TermOf (Term TyName Name uni DefaultFun ()) a
-> TypeEvalCheckM
     uni
     DefaultFun
     (TermOf
        (Term TyName Name uni DefaultFun ())
        (TypeEvalCheckResult uni DefaultFun))
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 (BuiltinsRuntime DefaultFun (CkValue uni DefaultFun)
-> Term TyName Name uni DefaultFun ()
-> Either
     (EvaluationException
        (MachineError DefaultFun)
        CkUserError
        (Term TyName Name uni DefaultFun ()))
     (Term TyName Name uni DefaultFun ())
forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either
     (CkEvaluationException uni fun) (Term TyName Name uni fun ())
evaluateCkNoEmit BuiltinsRuntime DefaultFun (CkValue uni DefaultFun)
forall term.
HasMeaningIn DefaultUni term =>
BuiltinsRuntime DefaultFun term
defaultBuiltinsRuntimeForTesting) TermOf (Term TyName Name uni fun ()) a
TermOf (Term TyName Name uni DefaultFun ()) a
termOfTbv
    case TypeEvalCheckM
  uni
  DefaultFun
  (TermOf
     (Term TyName Name uni DefaultFun ())
     (TypeEvalCheckResult uni DefaultFun))
errOrRes of
        Left TypeEvalCheckError uni DefaultFun
err         -> String
-> TermOf
     (Term TyName Name uni fun ())
     (EvaluationResult (Term TyName Name uni fun ()))
forall a. HasCallStack => String -> a
error (String
 -> TermOf
      (Term TyName Name uni fun ())
      (EvaluationResult (Term TyName Name uni fun ())))
-> String
-> TermOf
     (Term TyName Name uni fun ())
     (EvaluationResult (Term TyName Name uni fun ()))
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ TypeEvalCheckError uni DefaultFun -> String
forall err. PrettyPlc err => err -> String
prettyPlcErrorString TypeEvalCheckError uni DefaultFun
err
            , String
"\nin\n"
            , Doc Any -> String
forall ann. Doc ann -> String
forall str ann. Render str => Doc ann -> str
render (Doc Any -> String)
-> (Term TyName Name uni fun () -> Doc Any)
-> Term TyName Name uni fun ()
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun () -> Doc Any
forall a ann. PrettyPlc a => a -> Doc ann
prettyPlcClassicSimple (Term TyName Name uni fun () -> String)
-> Term TyName Name uni fun () -> String
forall a b. (a -> b) -> a -> b
$ TermOf (Term TyName Name uni fun ()) a
-> Term TyName Name uni fun ()
forall term a. TermOf term a -> term
_termOfTerm TermOf (Term TyName Name uni fun ()) a
termOfTbv
            ]
        Right TermOf
  (Term TyName Name uni DefaultFun ())
  (TypeEvalCheckResult uni DefaultFun)
termOfTecr -> TypeEvalCheckResult uni fun
-> EvaluationResult (Term TyName Name uni fun ())
forall (uni :: * -> *) fun.
TypeEvalCheckResult uni fun
-> EvaluationResult (Term TyName Name uni fun ())
_termCheckResultValue (TypeEvalCheckResult uni fun
 -> EvaluationResult (Term TyName Name uni fun ()))
-> TermOf
     (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun)
-> TermOf
     (Term TyName Name uni fun ())
     (EvaluationResult (Term TyName Name uni fun ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermOf (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun)
TermOf
  (Term TyName Name uni DefaultFun ())
  (TypeEvalCheckResult uni DefaultFun)
termOfTecr