{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module PlutusIR.Pass.Test where
import Control.Monad.Except
import Data.Typeable
import PlutusCore qualified as PLC
import PlutusCore.Builtin
import PlutusCore.Generators.QuickCheck (forAllDoc)
import PlutusCore.Pretty qualified as PLC
import PlutusIR.Core.Type
import PlutusIR.Error qualified as PIR
import PlutusIR.Generators.QuickCheck
import PlutusIR.Pass
import PlutusIR.TypeCheck
import PlutusIR.TypeCheck qualified as TC
import PlutusPrelude
import Test.QuickCheck
convertToEitherString :: Either (PIR.Error PLC.DefaultUni PLC.DefaultFun ()) ()
-> Either String ()
convertToEitherString :: Either (Error DefaultUni DefaultFun ()) () -> Either String ()
convertToEitherString = \case
Left Error DefaultUni DefaultFun ()
err -> String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ Error DefaultUni DefaultFun () -> String
forall a. Show a => a -> String
show Error DefaultUni DefaultFun ()
err
Right () -> () -> Either String ()
forall a b. b -> Either a b
Right ()
instance Arbitrary (BuiltinSemanticsVariant PLC.DefaultFun) where
arbitrary :: Gen (BuiltinSemanticsVariant DefaultFun)
arbitrary = [BuiltinSemanticsVariant DefaultFun]
-> Gen (BuiltinSemanticsVariant DefaultFun)
forall a. HasCallStack => [a] -> Gen a
elements [BuiltinSemanticsVariant DefaultFun]
forall a. (Enum a, Bounded a) => [a]
enumerate
numTestsForPassProp :: Int
numTestsForPassProp :: Int
numTestsForPassProp = Int
99
runTestPass
:: (PLC.ThrowableBuiltins uni fun
, PLC.Typecheckable uni fun
, PLC.Pretty a
, Typeable a
, Monoid a
, Monad m
)
=> (TC.PirTCConfig uni fun -> Pass m tyname name uni fun a)
-> Term tyname name uni fun a
-> m (Term tyname name uni fun a)
runTestPass :: forall (uni :: * -> *) fun a (m :: * -> *) tyname name.
(ThrowableBuiltins uni fun, Typecheckable uni fun, Pretty a,
Typeable a, Monoid a, Monad m) =>
(PirTCConfig uni fun -> Pass m tyname name uni fun a)
-> Term tyname name uni fun a -> m (Term tyname name uni fun a)
runTestPass PirTCConfig uni fun -> Pass m tyname name uni fun a
pass Term tyname name uni fun a
t = do
Either (Error uni fun a) (Term tyname name uni fun a)
res <- ExceptT (Error uni fun a) m (Term tyname name uni fun a)
-> m (Either (Error uni fun a) (Term tyname name uni fun a))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT (Error uni fun a) m (Term tyname name uni fun a)
-> m (Either (Error uni fun a) (Term tyname name uni fun a)))
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
-> m (Either (Error uni fun a) (Term tyname name uni fun a))
forall a b. (a -> b) -> a -> b
$ do
PirTCConfig uni fun
tcconfig <- a -> ExceptT (Error uni fun a) m (PirTCConfig uni fun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (PirTCConfig uni fun)
TC.getDefTypeCheckConfig a
forall a. Monoid a => a
mempty
(String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Monad m =>
(String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
runPass (\String
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Bool
True (PirTCConfig uni fun -> Pass m tyname name uni fun a
pass PirTCConfig uni fun
tcconfig) Term tyname name uni fun a
t
case Either (Error uni fun a) (Term tyname name uni fun a)
res of
Left Error uni fun a
e -> Error uni fun a -> m (Term tyname name uni fun a)
forall a e. Exception e => e -> a
throw Error uni fun a
e
Right Term tyname name uni fun a
v -> Term tyname name uni fun a -> m (Term tyname name uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
v
testPassProp ::
Monad m
=> (forall a . m a -> a)
-> (TC.PirTCConfig PLC.DefaultUni PLC.DefaultFun
-> Pass m TyName Name PLC.DefaultUni PLC.DefaultFun ())
-> Property
testPassProp :: forall (m :: * -> *).
Monad m =>
(forall a. m a -> a)
-> (PirTCConfig DefaultUni DefaultFun
-> Pass m TyName Name DefaultUni DefaultFun ())
-> Property
testPassProp forall a. m a -> a
exitMonad PirTCConfig DefaultUni DefaultFun
-> Pass m TyName Name DefaultUni DefaultFun ()
pass =
()
-> (Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ())
-> (ExceptT (Error DefaultUni DefaultFun ()) m ()
-> Either String ())
-> (PirTCConfig DefaultUni DefaultFun
-> Pass m TyName Name DefaultUni DefaultFun ())
-> Property
forall (m :: * -> *) tyname name a prop.
(Monad m, Testable prop) =>
a
-> (Term TyName Name DefaultUni DefaultFun ()
-> Term tyname name DefaultUni DefaultFun a)
-> (ExceptT (Error DefaultUni DefaultFun a) m () -> prop)
-> (PirTCConfig DefaultUni DefaultFun
-> Pass m tyname name DefaultUni DefaultFun a)
-> Property
testPassProp'
()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a. a -> a
id
ExceptT (Error DefaultUni DefaultFun ()) m () -> Either String ()
forall {a}.
ExceptT (Error DefaultUni DefaultFun a) m () -> Either String ()
after
PirTCConfig DefaultUni DefaultFun
-> Pass m TyName Name DefaultUni DefaultFun ()
pass
where
after :: ExceptT (Error DefaultUni DefaultFun a) m () -> Either String ()
after ExceptT (Error DefaultUni DefaultFun a) m ()
res = Either (Error DefaultUni DefaultFun ()) () -> Either String ()
convertToEitherString (Either (Error DefaultUni DefaultFun ()) () -> Either String ())
-> Either (Error DefaultUni DefaultFun ()) () -> Either String ()
forall a b. (a -> b) -> a -> b
$ (Error DefaultUni DefaultFun a -> Error DefaultUni DefaultFun ())
-> Either (Error DefaultUni DefaultFun a) ()
-> Either (Error DefaultUni DefaultFun ()) ()
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Error DefaultUni DefaultFun a -> Error DefaultUni DefaultFun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either (Error DefaultUni DefaultFun a) ()
-> Either (Error DefaultUni DefaultFun ()) ())
-> Either (Error DefaultUni DefaultFun a) ()
-> Either (Error DefaultUni DefaultFun ()) ()
forall a b. (a -> b) -> a -> b
$ m (Either (Error DefaultUni DefaultFun a) ())
-> Either (Error DefaultUni DefaultFun a) ()
forall a. m a -> a
exitMonad (m (Either (Error DefaultUni DefaultFun a) ())
-> Either (Error DefaultUni DefaultFun a) ())
-> m (Either (Error DefaultUni DefaultFun a) ())
-> Either (Error DefaultUni DefaultFun a) ()
forall a b. (a -> b) -> a -> b
$ ExceptT (Error DefaultUni DefaultFun a) m ()
-> m (Either (Error DefaultUni DefaultFun a) ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT (Error DefaultUni DefaultFun a) m ()
res
testPassProp' ::
forall m tyname name a prop
. (Monad m, Testable prop)
=> a
-> (Term TyName Name PLC.DefaultUni PLC.DefaultFun ()
-> Term tyname name PLC.DefaultUni PLC.DefaultFun a)
-> (ExceptT (PIR.Error PLC.DefaultUni PLC.DefaultFun a) m () -> prop)
-> (TC.PirTCConfig PLC.DefaultUni PLC.DefaultFun
-> Pass m tyname name PLC.DefaultUni PLC.DefaultFun a)
-> Property
testPassProp' :: forall (m :: * -> *) tyname name a prop.
(Monad m, Testable prop) =>
a
-> (Term TyName Name DefaultUni DefaultFun ()
-> Term tyname name DefaultUni DefaultFun a)
-> (ExceptT (Error DefaultUni DefaultFun a) m () -> prop)
-> (PirTCConfig DefaultUni DefaultFun
-> Pass m tyname name DefaultUni DefaultFun a)
-> Property
testPassProp' a
ann Term TyName Name DefaultUni DefaultFun ()
-> Term tyname name DefaultUni DefaultFun a
before ExceptT (Error DefaultUni DefaultFun a) m () -> prop
after PirTCConfig DefaultUni DefaultFun
-> Pass m tyname name DefaultUni DefaultFun a
pass =
String
-> Gen
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> ((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())])
-> ((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> prop)
-> Property
forall a p.
(PrettyReadable a, Testable p) =>
String -> Gen a -> (a -> [a]) -> (a -> p) -> Property
forAllDoc String
"ty,tm" Gen
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
genTypeAndTerm_ (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
shrinkClosedTypedTerm (((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> prop)
-> Property)
-> ((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> prop)
-> Property
forall a b. (a -> b) -> a -> b
$ \ (Type TyName DefaultUni ()
_ty, Term TyName Name DefaultUni DefaultFun ()
tm) ->
let
res :: ExceptT (PIR.Error PLC.DefaultUni PLC.DefaultFun a) m ()
res :: ExceptT (Error DefaultUni DefaultFun a) m ()
res = do
PirTCConfig DefaultUni DefaultFun
tcconfig <- a
-> ExceptT
(Error DefaultUni DefaultFun a)
m
(PirTCConfig DefaultUni DefaultFun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (PirTCConfig uni fun)
getDefTypeCheckConfig a
ann
let tm' :: Term tyname name DefaultUni DefaultFun a
tm' = Term TyName Name DefaultUni DefaultFun ()
-> Term tyname name DefaultUni DefaultFun a
before Term TyName Name DefaultUni DefaultFun ()
tm
Term tyname name DefaultUni DefaultFun a
_ <- (String -> m ())
-> Bool
-> Pass m tyname name DefaultUni DefaultFun a
-> Term tyname name DefaultUni DefaultFun a
-> ExceptT
(Error DefaultUni DefaultFun a)
m
(Term tyname name DefaultUni DefaultFun a)
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Monad m =>
(String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
runPass (\String
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Bool
True (PirTCConfig DefaultUni DefaultFun
-> Pass m tyname name DefaultUni DefaultFun a
pass PirTCConfig DefaultUni DefaultFun
tcconfig) Term tyname name DefaultUni DefaultFun a
tm'
() -> ExceptT (Error DefaultUni DefaultFun a) m ()
forall a. a -> ExceptT (Error DefaultUni DefaultFun a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
in ExceptT (Error DefaultUni DefaultFun a) m () -> prop
after ExceptT (Error DefaultUni DefaultFun a) m ()
res