Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.Generators.Hedgehog.TypeEvalCheck

Description

This module defines types and functions related to "type-eval checking".

Synopsis

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 ()))
data TypeEvalCheckResult uni fun = TypeEvalCheckResult {
- _termCheckResultType ∷ Normalized (Type TyName uni ())
- _termCheckResultValue ∷ EvaluationResult (Term TyName Name uni fun ())
}
type TypeEvalCheckM uni fun = Either (TypeEvalCheckError uni fun)
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 ())) → TermOf (Term TyName Name uni fun ()) a → TypeEvalCheckM uni fun (TermOf (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun))
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 ()))

Documentation

data TypeEvalCheckError uni fun Source #

The type of errors that can occur during type-eval checking.

Constructors

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.

Instances

Instances details

(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) Source #
Instance details Defined in PlutusCore.Generators.Hedgehog.TypeEvalCheck Methods prettyBy ∷ config → TypeEvalCheckError uni fun → Doc ann Source # prettyListBy ∷ config → [TypeEvalCheckError uni fun] → Doc ann Source #
ann ~ () ⇒ AsError (TypeEvalCheckError uni fun) uni fun ann Source #
Instance details Defined in PlutusCore.Generators.Hedgehog.TypeEvalCheck Methods _Error ∷ Prism' (TypeEvalCheckError uni fun) (Error uni fun ann) Source # _ParseErrorE ∷ Prism' (TypeEvalCheckError uni fun) ParserErrorBundle Source # _UniqueCoherencyErrorE ∷ Prism' (TypeEvalCheckError uni fun) (UniqueError ann) Source # _TypeErrorE ∷ Prism' (TypeEvalCheckError uni fun) (TypeError (Term TyName Name uni fun ()) uni fun ann) Source # _NormCheckErrorE ∷ Prism' (TypeEvalCheckError uni fun) (NormCheckError TyName Name uni fun ann) Source # _FreeVariableErrorE ∷ Prism' (TypeEvalCheckError uni fun) FreeVariableError Source #
ann ~ () ⇒ AsTypeError (TypeEvalCheckError uni fun) (Term TyName Name uni fun ann) uni fun ann Source #
Instance details Defined in PlutusCore.Generators.Hedgehog.TypeEvalCheck Methods _TypeError ∷ Prism' (TypeEvalCheckError uni fun) (TypeError (Term TyName Name uni fun ann) uni fun ann) Source # _KindMismatch ∷ Prism' (TypeEvalCheckError uni fun) (ann, Type TyName uni (), ExpectedShapeOr (Kind ()), Kind ()) Source # _TypeMismatch ∷ Prism' (TypeEvalCheckError uni fun) (ann, Term TyName Name uni fun ann, ExpectedShapeOr (Type TyName uni ()), Normalized (Type TyName uni ())) Source # _TyNameMismatch ∷ Prism' (TypeEvalCheckError uni fun) (ann, TyName, TyName) Source # _NameMismatch ∷ Prism' (TypeEvalCheckError uni fun) (ann, Name, Name) Source # _FreeTypeVariableE ∷ Prism' (TypeEvalCheckError uni fun) (ann, TyName) Source # _FreeVariableE ∷ Prism' (TypeEvalCheckError uni fun) (ann, Name) Source # _UnknownBuiltinFunctionE ∷ Prism' (TypeEvalCheckError uni fun) (ann, fun) Source #

data TypeEvalCheckResult uni fun Source #

Type-eval checking of a term results in a value of this type.

Constructors

TypeEvalCheckResult
Fields _termCheckResultType ∷ Normalized (Type TyName uni ()) The type of the term. _termCheckResultValue ∷ EvaluationResult (Term TyName Name uni fun ()) The result of evaluation of the term.

type TypeEvalCheckM uni fun = Either (TypeEvalCheckError uni fun) Source #

The monad type-eval checking runs in.

typeEvalCheckBy Source #

Arguments

∷ (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))

Type check and evaluate a term and check that the expected result is equal to the actual one.

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 ())) Source #

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.