Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
This module defines functions useful for testing.
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 ()))
- 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 ())))
- 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 ()))
- printSampleProgramAndValue ∷ (uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a, MakeKnown (Term TyName Name uni fun ()) a) ⇒ TermGen a → IO ()
- sampleProgramValueGolden ∷ (uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a, MakeKnown (Term TyName Name uni fun ()) a) ⇒ String → String → TermGen a → IO ()
- 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 ())) → TermGen a → Property
Documentation
data TypeEvalCheckError uni fun Source #
The type of errors that can occur during type-eval checking.
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
data TypeEvalCheckResult uni fun Source #
Type-eval checking of a term results in a value of this type.
TypeEvalCheckResult | |
|
type TypeEvalCheckM uni fun = Either (TypeEvalCheckError uni fun) Source #
The monad type-eval checking runs in.
∷ (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.
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 ()))) Source #
Generate a term 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 ())) Source #
Generate a program using a given generator and check that it's well-typed and evaluates correctly.
printSampleProgramAndValue ∷ (uni ~ DefaultUni, fun ~ DefaultFun, KnownTypeAst TyName uni a, MakeKnown (Term TyName Name uni fun ()) a) ⇒ TermGen a → IO () Source #
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.
sampleProgramValueGolden Source #
∷ (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 () |
∷ (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 |
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.