{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module PlutusCore.Generators.NEAT.Spec
( tests
, Options (..)
, TestFail (..)
, bigTest
, packAssertion
, tynames
, names
, throwCtrex
, Ctrex (..)
, handleError
, handleUError
, GenDepth (..)
, GenMode (..)
) where
import PlutusCore
import PlutusCore.Compiler.Erase
import PlutusCore.Evaluation.Machine.Ck
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
import PlutusCore.Generators.NEAT.Common
import PlutusCore.Generators.NEAT.Term
import PlutusCore.Normalize
import PlutusCore.Pretty
import UntypedPlutusCore qualified as U
import UntypedPlutusCore.Evaluation.Machine.Cek qualified as U
import Control.Monad (unless)
import Control.Monad.Except (ExceptT, catchError, liftEither, runExceptT, throwError, withExceptT)
import Control.Search (Enumerable (..), Options (..), search')
import Data.Maybe
import Data.Stream qualified as Stream
import Data.Tagged
import Data.Text qualified as Text
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.Options
import Text.Printf
newtype GenDepth = GenDepth {GenDepth -> Int
unGenDepth :: Int}
deriving newtype (ReadPrec [GenDepth]
ReadPrec GenDepth
Int -> ReadS GenDepth
ReadS [GenDepth]
(Int -> ReadS GenDepth)
-> ReadS [GenDepth]
-> ReadPrec GenDepth
-> ReadPrec [GenDepth]
-> Read GenDepth
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS GenDepth
readsPrec :: Int -> ReadS GenDepth
$creadList :: ReadS [GenDepth]
readList :: ReadS [GenDepth]
$creadPrec :: ReadPrec GenDepth
readPrec :: ReadPrec GenDepth
$creadListPrec :: ReadPrec [GenDepth]
readListPrec :: ReadPrec [GenDepth]
Read, GenDepth -> GenDepth -> Bool
(GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> Bool) -> Eq GenDepth
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GenDepth -> GenDepth -> Bool
== :: GenDepth -> GenDepth -> Bool
$c/= :: GenDepth -> GenDepth -> Bool
/= :: GenDepth -> GenDepth -> Bool
Eq, Eq GenDepth
Eq GenDepth =>
(GenDepth -> GenDepth -> Ordering)
-> (GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> GenDepth)
-> (GenDepth -> GenDepth -> GenDepth)
-> Ord GenDepth
GenDepth -> GenDepth -> Bool
GenDepth -> GenDepth -> Ordering
GenDepth -> GenDepth -> GenDepth
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: GenDepth -> GenDepth -> Ordering
compare :: GenDepth -> GenDepth -> Ordering
$c< :: GenDepth -> GenDepth -> Bool
< :: GenDepth -> GenDepth -> Bool
$c<= :: GenDepth -> GenDepth -> Bool
<= :: GenDepth -> GenDepth -> Bool
$c> :: GenDepth -> GenDepth -> Bool
> :: GenDepth -> GenDepth -> Bool
$c>= :: GenDepth -> GenDepth -> Bool
>= :: GenDepth -> GenDepth -> Bool
$cmax :: GenDepth -> GenDepth -> GenDepth
max :: GenDepth -> GenDepth -> GenDepth
$cmin :: GenDepth -> GenDepth -> GenDepth
min :: GenDepth -> GenDepth -> GenDepth
Ord)
newtype GenMode = GenMode {GenMode -> Options
unGenMode :: Options}
deriving newtype (ReadPrec [GenMode]
ReadPrec GenMode
Int -> ReadS GenMode
ReadS [GenMode]
(Int -> ReadS GenMode)
-> ReadS [GenMode]
-> ReadPrec GenMode
-> ReadPrec [GenMode]
-> Read GenMode
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS GenMode
readsPrec :: Int -> ReadS GenMode
$creadList :: ReadS [GenMode]
readList :: ReadS [GenMode]
$creadPrec :: ReadPrec GenMode
readPrec :: ReadPrec GenMode
$creadListPrec :: ReadPrec [GenMode]
readListPrec :: ReadPrec [GenMode]
Read)
instance IsOption GenDepth where
defaultValue :: GenDepth
defaultValue = Int -> GenDepth
GenDepth Int
20
parseValue :: String -> Maybe GenDepth
parseValue = String -> Maybe GenDepth
forall a. Read a => String -> Maybe a
safeRead
optionName :: Tagged GenDepth String
optionName = forall {k} (s :: k) b. b -> Tagged s b
forall s b. b -> Tagged s b
Tagged @GenDepth String
"gen-depth"
optionHelp :: Tagged GenDepth String
optionHelp = forall {k} (s :: k) b. b -> Tagged s b
forall s b. b -> Tagged s b
Tagged @GenDepth String
"Gen depth"
instance IsOption GenMode where
defaultValue :: GenMode
defaultValue = Options -> GenMode
GenMode Options
OF
parseValue :: String -> Maybe GenMode
parseValue = String -> Maybe GenMode
forall a. Read a => String -> Maybe a
safeRead
optionName :: Tagged GenMode String
optionName = forall {k} (s :: k) b. b -> Tagged s b
forall s b. b -> Tagged s b
Tagged @GenMode String
"gen-mode"
optionHelp :: Tagged GenMode String
optionHelp = forall {k} (s :: k) b. b -> Tagged s b
forall s b. b -> Tagged s b
Tagged @GenMode String
"Gen Mode"
tests :: TestTree
tests :: TestTree
tests =
String -> [TestTree] -> TestTree
testGroup String
"NEAT"
[ (GenDepth -> GenDepth) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (GenDepth -> GenDepth -> GenDepth
forall a. Ord a => a -> a -> a
min (GenDepth -> GenDepth -> GenDepth)
-> GenDepth -> GenDepth -> GenDepth
forall a b. (a -> b) -> a -> b
$ Int -> GenDepth
GenDepth Int
10) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
String
-> Kind () -> (Kind () -> ClosedTypeG -> Assertion) -> TestTree
forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
"normalization commutes with conversion from generated types"
(() -> Kind ()
forall ann. ann -> Kind ann
Type ())
((Kind () -> ClosedTypeG -> ExceptT TestFail Quote ())
-> Kind () -> ClosedTypeG -> Assertion
forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion Kind () -> ClosedTypeG -> ExceptT TestFail Quote ()
prop_normalizeConvertCommuteTypes)
, (GenDepth -> GenDepth) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (GenDepth -> GenDepth -> GenDepth
forall a. Ord a => a -> a -> a
min (GenDepth -> GenDepth -> GenDepth)
-> GenDepth -> GenDepth -> GenDepth
forall a b. (a -> b) -> a -> b
$ Int -> GenDepth
GenDepth Int
12) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
String
-> Kind ()
-> (Kind () -> Normalized ClosedTypeG -> Assertion)
-> TestTree
forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
"normal types cannot reduce"
(() -> Kind ()
forall ann. ann -> Kind ann
Type ())
((Kind () -> Normalized ClosedTypeG -> ExceptT TestFail Quote ())
-> Kind () -> Normalized ClosedTypeG -> Assertion
forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion Kind () -> Normalized ClosedTypeG -> ExceptT TestFail Quote ()
prop_normalTypesCannotReduce)
, (GenDepth -> GenDepth) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (GenDepth -> GenDepth -> GenDepth
forall a. Ord a => a -> a -> a
min (GenDepth -> GenDepth -> GenDepth)
-> GenDepth -> GenDepth -> GenDepth
forall a b. (a -> b) -> a -> b
$ Int -> GenDepth
GenDepth Int
15) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
String
-> ClosedTypeG
-> (ClosedTypeG -> ClosedTermG -> Assertion)
-> TestTree
forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
"type preservation - CK"
(TypeBuiltinG -> ClosedTypeG
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyUnitG)
((ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ())
-> ClosedTypeG -> ClosedTermG -> Assertion
forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_typePreservation)
, (GenDepth -> GenDepth) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (GenDepth -> GenDepth -> GenDepth
forall a. Ord a => a -> a -> a
min (GenDepth -> GenDepth -> GenDepth)
-> GenDepth -> GenDepth -> GenDepth
forall a b. (a -> b) -> a -> b
$ Int -> GenDepth
GenDepth Int
15) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
String
-> ClosedTypeG
-> (ClosedTypeG -> ClosedTermG -> Assertion)
-> TestTree
forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
"typed CK vs untyped CEK produce the same output"
(TypeBuiltinG -> ClosedTypeG
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyUnitG)
((ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ())
-> ClosedTypeG -> ClosedTermG -> Assertion
forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_agree_termEval)
]
handleError :: Type TyName DefaultUni ()
-> U.ErrorWithCause (U.EvaluationError structural operational) term
-> Either (U.ErrorWithCause (U.EvaluationError structural operational) term)
(Term TyName Name DefaultUni DefaultFun ())
handleError :: forall structural operational term.
Type TyName DefaultUni ()
-> ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term TyName Name DefaultUni DefaultFun ())
handleError Type TyName DefaultUni ()
ty ErrorWithCause (EvaluationError structural operational) term
e = case ErrorWithCause (EvaluationError structural operational) term
-> EvaluationError structural operational
forall err cause. ErrorWithCause err cause -> err
U._ewcError ErrorWithCause (EvaluationError structural operational) term
e of
U.StructuralEvaluationError structural
_ -> ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term TyName Name DefaultUni DefaultFun ())
forall a.
ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ErrorWithCause (EvaluationError structural operational) term
e
U.OperationalEvaluationError operational
_ -> Term TyName Name DefaultUni DefaultFun ()
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term TyName Name DefaultUni DefaultFun ())
forall a.
a
-> Either
(ErrorWithCause (EvaluationError structural operational) term) a
forall (m :: * -> *) a. Monad m => a -> m a
return (()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error () Type TyName DefaultUni ()
ty)
handleUError ::
U.ErrorWithCause (U.EvaluationError structural operational) term
-> Either (U.ErrorWithCause (U.EvaluationError structural operational) term)
(U.Term Name DefaultUni DefaultFun ())
handleUError :: forall structural operational term.
ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term Name DefaultUni DefaultFun ())
handleUError ErrorWithCause (EvaluationError structural operational) term
e = case ErrorWithCause (EvaluationError structural operational) term
-> EvaluationError structural operational
forall err cause. ErrorWithCause err cause -> err
U._ewcError ErrorWithCause (EvaluationError structural operational) term
e of
U.StructuralEvaluationError structural
_ -> ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term Name DefaultUni DefaultFun ())
forall a.
ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ErrorWithCause (EvaluationError structural operational) term
e
U.OperationalEvaluationError operational
_ -> Term Name DefaultUni DefaultFun ()
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term Name DefaultUni DefaultFun ())
forall a.
a
-> Either
(ErrorWithCause (EvaluationError structural operational) term) a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
U.Error ())
prop_typePreservation :: ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_typePreservation :: ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_typePreservation ClosedTypeG
tyG ClosedTermG
tmG = do
TypeCheckConfig DefaultUni DefaultFun
tcConfig <- (TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun)
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun))
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun)
forall a b. (a -> b) -> a -> b
$ ()
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(TypeCheckConfig DefaultUni DefaultFun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
getDefTypeCheckConfig ()
Type TyName DefaultUni ()
ty <- (GenError -> TestFail)
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Kind ()
-> ClosedTypeG
-> ExceptT GenError Quote (Type TyName DefaultUni ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) ClosedTypeG
tyG
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ KindCheckConfig
-> ()
-> Type TyName DefaultUni ()
-> Kind ()
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
forall err term (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err term uni fun ann m =>
KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
checkKind KindCheckConfig
defKindCheckConfig () Type TyName DefaultUni ()
ty (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
Term TyName Name DefaultUni DefaultFun ()
tm <- (GenError -> TestFail)
-> ExceptT
GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT
GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> ExceptT
GenError Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> m (Term TyName Name DefaultUni DefaultFun ())
convertClosedTerm Stream Text
tynames Stream Text
names ClosedTypeG
tyG ClosedTermG
tmG
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ TypeCheckConfig DefaultUni DefaultFun
-> ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Normalized (Type TyName DefaultUni ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkType TypeCheckConfig DefaultUni DefaultFun
tcConfig () Term TyName Name DefaultUni DefaultFun ()
tm (Type TyName DefaultUni () -> Normalized (Type TyName DefaultUni ())
forall a. a -> Normalized a
Normalized Type TyName DefaultUni ()
ty)
Term TyName Name DefaultUni DefaultFun ()
tmCK <- (CkEvaluationException DefaultUni DefaultFun -> TestFail)
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT CkEvaluationException DefaultUni DefaultFun -> TestFail
CkP (ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ()))
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
BuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni 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 DefaultUni DefaultFun)
forall term.
HasMeaningIn DefaultUni term =>
BuiltinsRuntime DefaultFun term
defaultBuiltinsRuntimeForTesting Term TyName Name DefaultUni DefaultFun ()
tm Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
-> (CkEvaluationException DefaultUni DefaultFun
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ()))
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
forall a.
Either (CkEvaluationException DefaultUni DefaultFun) a
-> (CkEvaluationException DefaultUni DefaultFun
-> Either (CkEvaluationException DefaultUni DefaultFun) a)
-> Either (CkEvaluationException DefaultUni DefaultFun) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` Type TyName DefaultUni ()
-> CkEvaluationException DefaultUni DefaultFun
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
forall structural operational term.
Type TyName DefaultUni ()
-> ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term TyName Name DefaultUni DefaultFun ())
handleError Type TyName DefaultUni ()
ty
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ TypeCheckConfig DefaultUni DefaultFun
-> ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Normalized (Type TyName DefaultUni ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkType TypeCheckConfig DefaultUni DefaultFun
tcConfig () Term TyName Name DefaultUni DefaultFun ()
tmCK (Type TyName DefaultUni () -> Normalized (Type TyName DefaultUni ())
forall a. a -> Normalized a
Normalized Type TyName DefaultUni ()
ty)
prop_agree_termEval :: ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_agree_termEval :: ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_agree_termEval ClosedTypeG
tyG ClosedTermG
tmG = do
TypeCheckConfig DefaultUni DefaultFun
tcConfig <- (TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun)
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun))
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun)
forall a b. (a -> b) -> a -> b
$ ()
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(TypeCheckConfig DefaultUni DefaultFun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
getDefTypeCheckConfig ()
Type TyName DefaultUni ()
ty <- (GenError -> TestFail)
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Kind ()
-> ClosedTypeG
-> ExceptT GenError Quote (Type TyName DefaultUni ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) ClosedTypeG
tyG
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ KindCheckConfig
-> ()
-> Type TyName DefaultUni ()
-> Kind ()
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
forall err term (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err term uni fun ann m =>
KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
checkKind KindCheckConfig
defKindCheckConfig () Type TyName DefaultUni ()
ty (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
Term TyName Name DefaultUni DefaultFun ()
tm <- (GenError -> TestFail)
-> ExceptT
GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT
GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> ExceptT
GenError Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> m (Term TyName Name DefaultUni DefaultFun ())
convertClosedTerm Stream Text
tynames Stream Text
names ClosedTypeG
tyG ClosedTermG
tmG
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ TypeCheckConfig DefaultUni DefaultFun
-> ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Normalized (Type TyName DefaultUni ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkType TypeCheckConfig DefaultUni DefaultFun
tcConfig () Term TyName Name DefaultUni DefaultFun ()
tm (Type TyName DefaultUni () -> Normalized (Type TyName DefaultUni ())
forall a. a -> Normalized a
Normalized Type TyName DefaultUni ()
ty)
Term TyName Name DefaultUni DefaultFun ()
tmCk <- (CkEvaluationException DefaultUni DefaultFun -> TestFail)
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT CkEvaluationException DefaultUni DefaultFun -> TestFail
CkP (ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ()))
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
(CkEvaluationException DefaultUni DefaultFun)
Quote
(Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
BuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni 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 DefaultUni DefaultFun)
forall term.
HasMeaningIn DefaultUni term =>
BuiltinsRuntime DefaultFun term
defaultBuiltinsRuntimeForTesting Term TyName Name DefaultUni DefaultFun ()
tm Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
-> (CkEvaluationException DefaultUni DefaultFun
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ()))
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
forall a.
Either (CkEvaluationException DefaultUni DefaultFun) a
-> (CkEvaluationException DefaultUni DefaultFun
-> Either (CkEvaluationException DefaultUni DefaultFun) a)
-> Either (CkEvaluationException DefaultUni DefaultFun) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` Type TyName DefaultUni ()
-> CkEvaluationException DefaultUni DefaultFun
-> Either
(CkEvaluationException DefaultUni DefaultFun)
(Term TyName Name DefaultUni DefaultFun ())
forall structural operational term.
Type TyName DefaultUni ()
-> ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term TyName Name DefaultUni DefaultFun ())
handleError Type TyName DefaultUni ()
ty
let tmUCk :: Term Name DefaultUni DefaultFun ()
tmUCk = Term TyName Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term TyName Name DefaultUni DefaultFun ()
tmCk
Term Name DefaultUni DefaultFun ()
tmUCek <- (CekEvaluationException Name DefaultUni DefaultFun -> TestFail)
-> ExceptT
(CekEvaluationException Name DefaultUni DefaultFun)
Quote
(Term Name DefaultUni DefaultFun ())
-> ExceptT TestFail Quote (Term Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT CekEvaluationException Name DefaultUni DefaultFun -> TestFail
UCekP (ExceptT
(CekEvaluationException Name DefaultUni DefaultFun)
Quote
(Term Name DefaultUni DefaultFun ())
-> ExceptT TestFail Quote (Term Name DefaultUni DefaultFun ()))
-> ExceptT
(CekEvaluationException Name DefaultUni DefaultFun)
Quote
(Term Name DefaultUni DefaultFun ())
-> ExceptT TestFail Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Either
(CekEvaluationException Name DefaultUni DefaultFun)
(Term Name DefaultUni DefaultFun ())
-> ExceptT
(CekEvaluationException Name DefaultUni DefaultFun)
Quote
(Term Name DefaultUni DefaultFun ())
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either
(CekEvaluationException Name DefaultUni DefaultFun)
(Term Name DefaultUni DefaultFun ())
-> ExceptT
(CekEvaluationException Name DefaultUni DefaultFun)
Quote
(Term Name DefaultUni DefaultFun ()))
-> Either
(CekEvaluationException Name DefaultUni DefaultFun)
(Term Name DefaultUni DefaultFun ())
-> ExceptT
(CekEvaluationException Name DefaultUni DefaultFun)
Quote
(Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
MachineParameters
CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Either
(CekEvaluationException Name DefaultUni DefaultFun)
(Term Name DefaultUni DefaultFun ())
forall (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either
(CekEvaluationException Name uni fun) (Term Name uni fun ())
U.evaluateCekNoEmit MachineParameters
CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
forall ann.
Typeable ann =>
MachineParameters
CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
defaultCekParametersForTesting (Term TyName Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term TyName Name DefaultUni DefaultFun ()
tm) Either
(CekEvaluationException Name DefaultUni DefaultFun)
(Term Name DefaultUni DefaultFun ())
-> (CekEvaluationException Name DefaultUni DefaultFun
-> Either
(CekEvaluationException Name DefaultUni DefaultFun)
(Term Name DefaultUni DefaultFun ()))
-> Either
(CekEvaluationException Name DefaultUni DefaultFun)
(Term Name DefaultUni DefaultFun ())
forall a.
Either (CekEvaluationException Name DefaultUni DefaultFun) a
-> (CekEvaluationException Name DefaultUni DefaultFun
-> Either (CekEvaluationException Name DefaultUni DefaultFun) a)
-> Either (CekEvaluationException Name DefaultUni DefaultFun) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` CekEvaluationException Name DefaultUni DefaultFun
-> Either
(CekEvaluationException Name DefaultUni DefaultFun)
(Term Name DefaultUni DefaultFun ())
forall structural operational term.
ErrorWithCause (EvaluationError structural operational) term
-> Either
(ErrorWithCause (EvaluationError structural operational) term)
(Term Name DefaultUni DefaultFun ())
handleUError
Bool -> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term Name DefaultUni DefaultFun ()
tmUCk Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun () -> Bool
forall a. Eq a => a -> a -> Bool
== Term Name DefaultUni DefaultFun ()
tmUCek) (ExceptT TestFail Quote () -> ExceptT TestFail Quote ())
-> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$
Ctrex -> ExceptT TestFail Quote ()
throwCtrex (ClosedTypeG
-> ClosedTermG
-> [(String, Term Name DefaultUni DefaultFun ())]
-> Ctrex
CtrexUntypedTermEvaluationMismatch ClosedTypeG
tyG ClosedTermG
tmG [(String
"untyped CK",Term Name DefaultUni DefaultFun ()
tmUCk),(String
"untyped CEK",Term Name DefaultUni DefaultFun ()
tmUCek)])
prop_normalizeConvertCommuteTypes :: Kind ()
-> ClosedTypeG
-> ExceptT TestFail Quote ()
prop_normalizeConvertCommuteTypes :: Kind () -> ClosedTypeG -> ExceptT TestFail Quote ()
prop_normalizeConvertCommuteTypes Kind ()
k ClosedTypeG
tyG = do
Type TyName DefaultUni ()
ty <- (GenError -> TestFail)
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Kind ()
-> ClosedTypeG
-> ExceptT GenError Quote (Type TyName DefaultUni ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames Kind ()
k ClosedTypeG
tyG
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ KindCheckConfig
-> ()
-> Type TyName DefaultUni ()
-> Kind ()
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
forall err term (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err term uni fun ann m =>
KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
checkKind KindCheckConfig
defKindCheckConfig () Type TyName DefaultUni ()
ty Kind ()
k
Type TyName DefaultUni ()
ty1 <- (TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Normalized (Type TyName DefaultUni ()) -> Type TyName DefaultUni ()
forall a. Normalized a -> a
unNormalized (Normalized (Type TyName DefaultUni ())
-> Type TyName DefaultUni ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(Normalized (Type TyName DefaultUni ()))
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName DefaultUni ()
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
(Normalized (Type TyName DefaultUni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType Type TyName DefaultUni ()
ty
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail)
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> TestFail
TypeError (ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ())
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ KindCheckConfig
-> ()
-> Type TyName DefaultUni ()
-> Kind ()
-> ExceptT
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
Quote
()
forall err term (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err term uni fun ann m =>
KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
checkKind KindCheckConfig
defKindCheckConfig () Type TyName DefaultUni ()
ty Kind ()
k
Type TyName DefaultUni ()
ty2 <- (GenError -> TestFail)
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Kind ()
-> ClosedTypeG
-> ExceptT GenError Quote (Type TyName DefaultUni ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames Kind ()
k (ClosedTypeG -> ClosedTypeG
forall n. TypeG n -> TypeG n
normalizeTypeG ClosedTypeG
tyG)
Bool -> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type TyName DefaultUni ()
ty1 Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
== Type TyName DefaultUni ()
ty2) (ExceptT TestFail Quote () -> ExceptT TestFail Quote ())
-> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$
Ctrex -> ExceptT TestFail Quote ()
throwCtrex (Kind ()
-> ClosedTypeG
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Ctrex
CtrexNormalizeConvertCommuteTypes Kind ()
k ClosedTypeG
tyG Type TyName DefaultUni ()
ty1 Type TyName DefaultUni ()
ty2)
prop_normalTypesCannotReduce :: Kind ()
-> Normalized ClosedTypeG
-> ExceptT TestFail Quote ()
prop_normalTypesCannotReduce :: Kind () -> Normalized ClosedTypeG -> ExceptT TestFail Quote ()
prop_normalTypesCannotReduce Kind ()
k (Normalized ClosedTypeG
tyG) =
Bool -> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe ClosedTypeG -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe ClosedTypeG -> Bool) -> Maybe ClosedTypeG -> Bool
forall a b. (a -> b) -> a -> b
$ ClosedTypeG -> Maybe ClosedTypeG
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG ClosedTypeG
tyG) (ExceptT TestFail Quote () -> ExceptT TestFail Quote ())
-> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$
Ctrex -> ExceptT TestFail Quote ()
throwCtrex (Kind () -> ClosedTypeG -> Ctrex
CtrexNormalTypesCannotReduce Kind ()
k ClosedTypeG
tyG)
data TestFail
= GenError GenError
| TypeError
(TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
())
| AgdaErrorP ()
| FVErrorP FreeVariableError
| CkP (CkEvaluationException DefaultUni DefaultFun)
| UCekP (U.CekEvaluationException Name DefaultUni DefaultFun)
| Ctrex Ctrex
data Ctrex
= CtrexNormalizeConvertCommuteTypes
(Kind ())
ClosedTypeG
(Type TyName DefaultUni ())
(Type TyName DefaultUni ())
| CtrexNormalTypesCannotReduce
(Kind ())
ClosedTypeG
| CtrexKindCheckFail
(Kind ())
ClosedTypeG
| CtrexKindPreservationFail
(Kind ())
ClosedTypeG
| CtrexKindMismatch
(Kind ())
ClosedTypeG
(Kind ())
(Kind ())
| CtrexTypeNormalizationFail
(Kind ())
ClosedTypeG
| CtrexTypeNormalizationMismatch
(Kind ())
ClosedTypeG
(Type TyName DefaultUni ())
(Type TyName DefaultUni ())
| CtrexTypeCheckFail
ClosedTypeG
ClosedTermG
| CtrexTypePreservationFail
ClosedTypeG
ClosedTermG
(Term TyName Name DefaultUni DefaultFun ())
(Term TyName Name DefaultUni DefaultFun ())
| CtrexTermEvaluationFail
String
ClosedTypeG
ClosedTermG
| CtrexTermEvaluationMismatch
ClosedTypeG
ClosedTermG
[(String,Term TyName Name DefaultUni DefaultFun ())]
| CtrexUntypedTermEvaluationMismatch
ClosedTypeG
ClosedTermG
[(String,U.Term Name DefaultUni DefaultFun ())]
instance Show TestFail where
show :: TestFail -> String
show (TypeError TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
e) = String
"type error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
-> String
forall a. Show a => a -> String
show TypeError
(Term TyName Name DefaultUni DefaultFun ())
DefaultUni
DefaultFun
()
e
show (GenError GenError
e) = String
"generator error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ GenError -> String
forall a. Show a => a -> String
show GenError
e
show (Ctrex Ctrex
e) = String
"counter example error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctrex -> String
forall a. Show a => a -> String
show Ctrex
e
show (AgdaErrorP ()
e) = String
"agda error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ () -> String
forall a. Show a => a -> String
show ()
e
show (FVErrorP FreeVariableError
e) = String
"free variable error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FreeVariableError -> String
forall a. Show a => a -> String
show FreeVariableError
e
show (CkP CkEvaluationException DefaultUni DefaultFun
e) = String
"CK error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CkEvaluationException DefaultUni DefaultFun -> String
forall a. Show a => a -> String
show CkEvaluationException DefaultUni DefaultFun
e
show (UCekP CekEvaluationException Name DefaultUni DefaultFun
e) = String
"UCEK error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CekEvaluationException Name DefaultUni DefaultFun -> String
forall a. Show a => a -> String
show CekEvaluationException Name DefaultUni DefaultFun
e
instance Show Ctrex where
show :: Ctrex -> String
show (CtrexNormalizeConvertCommuteTypes Kind ()
k ClosedTypeG
tyG Type TyName DefaultUni ()
ty1 Type TyName DefaultUni ()
ty2) =
String -> String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf
String
tpl
(ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
(Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
(Doc Any -> String
forall a. Show a => a -> String
show (Type TyName DefaultUni () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Type TyName DefaultUni () -> Doc ann
pretty Type TyName DefaultUni ()
ty1))
(Doc Any -> String
forall a. Show a => a -> String
show (Type TyName DefaultUni () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Type TyName DefaultUni () -> Doc ann
pretty Type TyName DefaultUni ()
ty2))
where
tpl :: String
tpl = [String] -> String
unlines
[ String
"Counterexample found: %s :: %s"
, String
"- convert then normalize gives %s"
, String
"- normalize then convert gives %s"
]
show (CtrexNormalTypesCannotReduce Kind ()
k ClosedTypeG
tyG) =
String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
where
tpl :: String
tpl = String
"Counterexample found: normal type %s of kind %s can reduce."
show (CtrexKindCheckFail Kind ()
k ClosedTypeG
tyG) =
String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
where
tpl :: String
tpl = String
"Counterexample found (kind check fail): %s :: %s"
show (CtrexKindPreservationFail Kind ()
k ClosedTypeG
tyG) =
String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
where
tpl :: String
tpl = String
"Counterexample found (kind preservation fail): %s :: %s"
show (CtrexKindMismatch Kind ()
k ClosedTypeG
tyG Kind ()
k' Kind ()
k'') =
String -> String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf
String
tpl
(Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
(ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
(Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k'))
(Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k''))
where
tpl :: String
tpl = [String] -> String
unlines
[ String
"Counterexample found: %s :: %s"
, String
"- inferer1 gives %s"
, String
"- inferer2 gives %s"
]
show (CtrexTypeNormalizationFail Kind ()
k ClosedTypeG
tyG) =
String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
where
tpl :: String
tpl = String
"Counterexample found (type normalisation fail): %s :: %s"
show (CtrexTypeNormalizationMismatch Kind ()
k ClosedTypeG
tyG Type TyName DefaultUni ()
ty1 Type TyName DefaultUni ()
ty2) =
String -> String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf
String
tpl
(ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
(Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
(Doc Any -> String
forall a. Show a => a -> String
show (Type TyName DefaultUni () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Type TyName DefaultUni () -> Doc ann
pretty Type TyName DefaultUni ()
ty1))
(Doc Any -> String
forall a. Show a => a -> String
show (Type TyName DefaultUni () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Type TyName DefaultUni () -> Doc ann
pretty Type TyName DefaultUni ()
ty2))
where
tpl :: String
tpl = [String] -> String
unlines
[ String
"Counterexample found: %s :: %s"
, String
"- normalizer1 gives %s"
, String
"- normalizer2 gives %s"
]
show (CtrexTypeCheckFail ClosedTypeG
tyG ClosedTermG
tmG) =
String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
where
tpl :: String
tpl = String
"Counterexample found (typecheck fail): %s :: %s"
show (CtrexTermEvaluationFail String
s ClosedTypeG
tyG ClosedTermG
tmG) =
String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
where
tpl :: String
tpl = String
"Counterexample found (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" term evaluation fail): %s :: %s"
show (CtrexTermEvaluationMismatch ClosedTypeG
tyG ClosedTermG
tmG [(String, Term TyName Name DefaultUni DefaultFun ())]
tms) =
String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, Term TyName Name DefaultUni DefaultFun ())] -> String
forall {a}. Pretty a => [(String, a)] -> String
results [(String, Term TyName Name DefaultUni DefaultFun ())]
tms
where
tpl :: String
tpl = String
"TypedTermEvaluationMismatch\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Counterexample found: %s :: %s\n"
results :: [(String, a)] -> String
results ((String
s,a
t):[(String, a)]
ts) = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" evaluation: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (a -> Doc Any
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, a)] -> String
results [(String, a)]
ts
results [] = String
""
show (CtrexUntypedTermEvaluationMismatch ClosedTypeG
tyG ClosedTermG
tmG [(String, Term Name DefaultUni DefaultFun ())]
tms) =
String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, Term Name DefaultUni DefaultFun ())] -> String
forall {a}. Pretty a => [(String, a)] -> String
results [(String, Term Name DefaultUni DefaultFun ())]
tms
where
tpl :: String
tpl = String
"UntypedTermEvaluationMismatch\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Counterexample found: %s :: %s\n"
results :: [(String, a)] -> String
results ((String
s,a
t):[(String, a)]
ts) = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" evaluation: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (a -> Doc Any
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, a)] -> String
results [(String, a)]
ts
results [] = String
""
show (CtrexTypePreservationFail ClosedTypeG
tyG ClosedTermG
tmG Term TyName Name DefaultUni DefaultFun ()
tm1 Term TyName Name DefaultUni DefaultFun ()
tm2) =
String -> String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Term TyName Name DefaultUni DefaultFun () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Term TyName Name DefaultUni DefaultFun () -> Doc ann
pretty Term TyName Name DefaultUni DefaultFun ()
tm1)) (Doc Any -> String
forall a. Show a => a -> String
show (Term TyName Name DefaultUni DefaultFun () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Term TyName Name DefaultUni DefaultFun () -> Doc ann
pretty Term TyName Name DefaultUni DefaultFun ()
tm2))
where
tpl :: String
tpl = [String] -> String
unlines
[ String
"Counterexample found: %s :: %s"
, String
"before evaluation: %s"
, String
"after evaluation: %s"
]
throwCtrex :: Ctrex -> ExceptT TestFail Quote ()
throwCtrex :: Ctrex -> ExceptT TestFail Quote ()
throwCtrex Ctrex
ctrex = TestFail -> ExceptT TestFail Quote ()
forall a. TestFail -> ExceptT TestFail Quote a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Ctrex -> TestFail
Ctrex Ctrex
ctrex)
tynames :: Stream.Stream Text.Text
tynames :: Stream Text
tynames = Text -> Stream Text
mkTextNameStream Text
"t"
names :: Stream.Stream Text.Text
names :: Stream Text
names = Text -> Stream Text
mkTextNameStream Text
"x"
packAssertion :: (Show e) => (t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion :: forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion t -> a -> ExceptT e Quote ()
f t
t a
a =
case Quote (Either e ()) -> Either e ()
forall a. Quote a -> a
runQuote (Quote (Either e ()) -> Either e ())
-> (ExceptT e Quote () -> Quote (Either e ()))
-> ExceptT e Quote ()
-> Either e ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT e Quote () -> Quote (Either e ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT e Quote () -> Either e ())
-> ExceptT e Quote () -> Either e ()
forall a b. (a -> b) -> a -> b
$ t -> a -> ExceptT e Quote ()
f t
t a
a of
Left e
e -> String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure (String -> Assertion) -> String -> Assertion
forall a b. (a -> b) -> a -> b
$ e -> String
forall a. Show a => a -> String
show e
e
Right ()
_ -> () -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
bigTest :: (Check t a, Enumerable a)
=> String -> t -> (t -> a -> Assertion) -> TestTree
bigTest :: forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
s t
t t -> a -> Assertion
f = (GenMode -> TestTree) -> TestTree
forall v. IsOption v => (v -> TestTree) -> TestTree
askOption ((GenMode -> TestTree) -> TestTree)
-> (GenMode -> TestTree) -> TestTree
forall a b. (a -> b) -> a -> b
$ \ GenMode
genMode -> (GenDepth -> TestTree) -> TestTree
forall v. IsOption v => (v -> TestTree) -> TestTree
askOption ((GenDepth -> TestTree) -> TestTree)
-> (GenDepth -> TestTree) -> TestTree
forall a b. (a -> b) -> a -> b
$ \ GenDepth
genDepth -> String -> IO String -> TestTree
testCaseInfo String
s (IO String -> TestTree) -> IO String -> TestTree
forall a b. (a -> b) -> a -> b
$ do
[a]
as <- Options -> Int -> (a -> Cool) -> IO [a]
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> IO [a]
search' (GenMode -> Options
unGenMode GenMode
genMode) (GenDepth -> Int
unGenDepth GenDepth
genDepth) (\a
a -> t -> a -> Cool
forall t a. Check t a => t -> a -> Cool
check t
t a
a)
[()]
_ <- (a -> Assertion) -> [a] -> IO [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (t -> a -> Assertion
f t
t) [a]
as
String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as)