{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
ExecSpecRule (..),
conformsToImpl,
generatesWithin,
inputsGenerateWithin,
runConformance,
checkConformance,
defaultTestConformance,
translateWithContext,
ForAllExecSpecRep,
ForAllExecTypes,
diffConformance,
) where
import Cardano.Ledger.BaseTypes (Globals, Inject (..), ShelleyBase)
import Cardano.Ledger.Binary (EncCBOR)
import Cardano.Ledger.Core (Era, EraRule, eraProtVerLow)
import qualified Constrained.API as CV2 (HasSpec, Specification, genFromSpec, genFromSpecT)
import Constrained.GenT (GE (..), GenMode (..))
import qualified Constrained.GenT as CV1 (runGenT)
import Constrained.TheKnot (shrinkWithSpec, simplifySpec)
import Control.Monad.Cont (ContT (..))
import Control.Monad.Trans (MonadTrans (..))
import Control.State.Transition.Extended (STS (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (bimapM)
import Data.Functor (($>))
import Data.List.NonEmpty (NonEmpty)
import Data.String (fromString)
import qualified Data.Text as T
import Data.Typeable (Proxy (..), Typeable, typeRep)
import GHC.Base (Constraint, Symbol, Type)
import GHC.TypeLits (KnownSymbol)
import Lens.Micro.Mtl (use)
import Prettyprinter
import Prettyprinter.Render.Terminal
import System.FilePath ((<.>))
import Test.Cardano.Ledger.Api.DebugTools (writeCBOR)
import Test.Cardano.Ledger.Binary.TreeDiff (Pretty (..), ansiWlPretty, ediff, ppEditExpr)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (
FixupSpecRep (..),
OpaqueErrorString (..),
SpecTranslate (..),
runSpecTransM,
showOpaqueErrorString,
toTestRep,
)
import Test.Cardano.Ledger.Imp.Common
import Test.Cardano.Ledger.Shelley.ImpTest (
ImpTestM,
ShelleyEraImp,
impAnn,
impGlobalsL,
logDoc,
tryRunImpRule,
)
import UnliftIO (MonadIO (..), evaluateDeep)
import UnliftIO.Directory (makeAbsolute)
import UnliftIO.Environment (lookupEnv)
type ForAllExecTypes (c :: Type -> Constraint) rule era =
( c (ExecEnvironment rule era)
, c (ExecState rule era)
, c (ExecSignal rule era)
)
type ForAllExecSpecRep (c :: Type -> Constraint) rule era =
( c (SpecRep (ExecEnvironment rule era))
, c (SpecRep (ExecState rule era))
, c (SpecRep (ExecSignal rule era))
)
class
( ForAllExecTypes CV2.HasSpec rule era
, ForAllExecTypes ToExpr rule era
, ForAllExecTypes NFData rule era
, KnownSymbol rule
, STS (EraRule rule era)
, BaseM (EraRule rule era) ~ ShelleyBase
, SpecTranslate (ExecContext rule era) (PredicateFailure (EraRule rule era))
, Inject (ExecEnvironment rule era) (Environment (EraRule rule era))
, Inject (ExecState rule era) (State (EraRule rule era))
, Inject (ExecSignal rule era) (Signal (EraRule rule era))
) =>
ExecSpecRule (rule :: Symbol) era
where
type ExecContext rule era
type ExecContext rule era = ()
type ExecEnvironment rule era
type ExecEnvironment rule era = Environment (EraRule rule era)
type ExecState rule era
type ExecState rule era = State (EraRule rule era)
type ExecSignal rule era
type ExecSignal rule era = Signal (EraRule rule era)
environmentSpec ::
HasCallStack =>
ExecContext rule era ->
CV2.Specification (ExecEnvironment rule era)
stateSpec ::
HasCallStack =>
ExecContext rule era ->
ExecEnvironment rule era ->
CV2.Specification (ExecState rule era)
signalSpec ::
HasCallStack =>
ExecContext rule era ->
ExecEnvironment rule era ->
ExecState rule era ->
CV2.Specification (ExecSignal rule era)
classOf :: ExecSignal rule era -> Maybe String
classOf ExecSignal rule era
_ = Maybe String
forall a. Maybe a
Nothing
genExecContext :: HasCallStack => Gen (ExecContext rule era)
default genExecContext ::
Arbitrary (ExecContext rule era) =>
Gen (ExecContext rule era)
genExecContext = Gen (ExecContext rule era)
forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary
runAgdaRule ::
HasCallStack =>
SpecRep (ExecEnvironment rule era) ->
SpecRep (ExecState rule era) ->
SpecRep (ExecSignal rule era) ->
Either OpaqueErrorString (SpecRep (ExecState rule era))
translateInputs ::
HasCallStack =>
ExecEnvironment rule era ->
ExecState rule era ->
ExecSignal rule era ->
ExecContext rule era ->
ImpTestM
era
( SpecRep (ExecEnvironment rule era)
, SpecRep (ExecState rule era)
, SpecRep (ExecSignal rule era)
)
default translateInputs ::
( ForAllExecTypes (SpecTranslate (ExecContext rule era)) rule era
, ForAllExecSpecRep ToExpr rule era
) =>
ExecEnvironment rule era ->
ExecState rule era ->
ExecSignal rule era ->
ExecContext rule era ->
ImpTestM
era
( SpecRep (ExecEnvironment rule era)
, SpecRep (ExecState rule era)
, SpecRep (ExecSignal rule era)
)
translateInputs ExecEnvironment rule era
env ExecState rule era
st ExecSignal rule era
sig ExecContext rule era
ctx = do
let
expectRight' :: Either Text a -> f a
expectRight' (Right a
x) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
expectRight' (Left Text
e) = String -> f a
forall (m :: * -> *) a. (HasCallStack, MonadIO m) => String -> m a
assertFailure (Text -> String
T.unpack Text
e)
SpecRep (ExecEnvironment rule era)
agdaEnv <- Either Text (SpecRep (ExecEnvironment rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecEnvironment rule era))
forall {f :: * -> *} {a}. MonadIO f => Either Text a -> f a
expectRight' (Either Text (SpecRep (ExecEnvironment rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecEnvironment rule era)))
-> (SpecTransM
(ExecContext rule era) (SpecRep (ExecEnvironment rule era))
-> Either Text (SpecRep (ExecEnvironment rule era)))
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecEnvironment rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecEnvironment rule era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecContext rule era
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecEnvironment rule era))
-> Either Text (SpecRep (ExecEnvironment rule era))
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext rule era
ctx (SpecTransM
(ExecContext rule era) (SpecRep (ExecEnvironment rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecEnvironment rule era)))
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecEnvironment rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecEnvironment rule era))
forall a b. (a -> b) -> a -> b
$ ExecEnvironment rule era
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecEnvironment rule era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecEnvironment rule era
env
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"agdaEnv:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> SpecRep (ExecEnvironment rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecEnvironment rule era)
agdaEnv
SpecRep (ExecState rule era)
agdaSt <- Either Text (SpecRep (ExecState rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecState rule era))
forall {f :: * -> *} {a}. MonadIO f => Either Text a -> f a
expectRight' (Either Text (SpecRep (ExecState rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecState rule era)))
-> (SpecTransM
(ExecContext rule era) (SpecRep (ExecState rule era))
-> Either Text (SpecRep (ExecState rule era)))
-> SpecTransM (ExecContext rule era) (SpecRep (ExecState rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecState rule era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecContext rule era
-> SpecTransM (ExecContext rule era) (SpecRep (ExecState rule era))
-> Either Text (SpecRep (ExecState rule era))
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext rule era
ctx (SpecTransM (ExecContext rule era) (SpecRep (ExecState rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecState rule era)))
-> SpecTransM (ExecContext rule era) (SpecRep (ExecState rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecState rule era))
forall a b. (a -> b) -> a -> b
$ ExecState rule era
-> SpecTransM (ExecContext rule era) (SpecRep (ExecState rule era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecState rule era
st
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"agdaSt:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> SpecRep (ExecState rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecState rule era)
agdaSt
SpecRep (ExecSignal rule era)
agdaSig <- Either Text (SpecRep (ExecSignal rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecSignal rule era))
forall {f :: * -> *} {a}. MonadIO f => Either Text a -> f a
expectRight' (Either Text (SpecRep (ExecSignal rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecSignal rule era)))
-> (SpecTransM
(ExecContext rule era) (SpecRep (ExecSignal rule era))
-> Either Text (SpecRep (ExecSignal rule era)))
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecSignal rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecSignal rule era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecContext rule era
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecSignal rule era))
-> Either Text (SpecRep (ExecSignal rule era))
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext rule era
ctx (SpecTransM (ExecContext rule era) (SpecRep (ExecSignal rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecSignal rule era)))
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecSignal rule era))
-> ImpM (LedgerSpec era) (SpecRep (ExecSignal rule era))
forall a b. (a -> b) -> a -> b
$ ExecSignal rule era
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecSignal rule era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecSignal rule era
sig
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"agdaSig:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> SpecRep (ExecSignal rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecSignal rule era)
agdaSig
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era))
-> ImpTestM
era
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era))
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecRep (ExecEnvironment rule era)
agdaEnv, SpecRep (ExecState rule era)
agdaSt, SpecRep (ExecSignal rule era)
agdaSig)
testConformance ::
( ShelleyEraImp era
, SpecTranslate (ExecContext rule era) (State (EraRule rule era))
, ForAllExecSpecRep NFData rule era
, ForAllExecSpecRep ToExpr rule era
, NFData (SpecRep (PredicateFailure (EraRule rule era)))
, ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
, Eq (SpecRep (PredicateFailure (EraRule rule era)))
, Eq (SpecRep (ExecState rule era))
, Inject
(State (EraRule rule era))
(ExecState rule era)
, SpecTranslate (ExecContext rule era) (ExecState rule era)
, FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
, FixupSpecRep (SpecRep (ExecState rule era))
, Inject (ExecEnvironment rule era) (Environment (EraRule rule era))
, Inject (ExecState rule era) (State (EraRule rule era))
, Inject (ExecSignal rule era) (Signal (EraRule rule era))
, EncCBOR (ExecContext rule era)
, EncCBOR (Environment (EraRule rule era))
, EncCBOR (State (EraRule rule era))
, EncCBOR (Signal (EraRule rule era))
, ToExpr (ExecContext rule era)
, ToExpr (PredicateFailure (EraRule rule era))
, NFData (PredicateFailure (EraRule rule era))
, HasCallStack
) =>
ExecContext rule era ->
ExecEnvironment rule era ->
ExecState rule era ->
ExecSignal rule era ->
Property
testConformance = forall era (rule :: Symbol).
(HasCallStack, ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (PredicateFailure (EraRule rule era)),
Eq (SpecRep (ExecState rule era)),
Inject (State (EraRule rule era)) (ExecState rule era),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era),
ToExpr (PredicateFailure (EraRule rule era))) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> ExecSignal rule era
-> Property
defaultTestConformance @era @rule
::
HasCallStack =>
Globals ->
ExecContext rule era ->
Environment (EraRule rule era) ->
State (EraRule rule era) ->
Signal (EraRule rule era) ->
Either OpaqueErrorString (State (EraRule rule era), [Event (EraRule rule era)]) ->
Doc AnsiStyle
extraInfo Globals
_ ExecContext rule era
_ Environment (EraRule rule era)
_ State (EraRule rule era)
_ Signal (EraRule rule era)
_ = Either
OpaqueErrorString
(State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
forall a. Monoid a => a
mempty
dumpCbor ::
forall era a.
( EncCBOR a
, Era era
) =>
FilePath ->
a ->
String ->
ImpTestM era ()
dumpCbor :: forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path a
x String
name = do
String
fullPath <- String -> ImpM (LedgerSpec era) String
forall (m :: * -> *). MonadIO m => String -> m String
makeAbsolute (String -> ImpM (LedgerSpec era) String)
-> String -> ImpM (LedgerSpec era) String
forall a b. (a -> b) -> a -> b
$ String
path String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"/" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
name String -> String -> String
<.> String
"cbor"
Version -> String -> a -> ImpTestM era ()
forall a (m :: * -> *).
(EncCBOR a, MonadIO m) =>
Version -> String -> a -> m ()
writeCBOR (forall era. Era era => Version
eraProtVerLow @era) String
fullPath a
x
diffConformance :: ToExpr a => a -> a -> Doc AnsiStyle
diffConformance :: forall a. ToExpr a => a -> a -> Doc AnsiStyle
diffConformance a
implRes a
agdaRes =
Pretty (Doc AnsiStyle) -> Edit EditExpr -> Doc AnsiStyle
forall doc. Pretty doc -> Edit EditExpr -> doc
ppEditExpr Pretty (Doc AnsiStyle)
conformancePretty (a -> a -> Edit EditExpr
forall a. ToExpr a => a -> a -> Edit EditExpr
ediff a
implRes a
agdaRes)
where
delColor :: Color
delColor = Color
Red
insColor :: Color
insColor = Color
Magenta
conformancePretty :: Pretty (Doc AnsiStyle)
conformancePretty =
Pretty (Doc AnsiStyle)
ansiWlPretty
{ ppDel = annotate (color delColor) . parens . ("Impl: " <>)
, ppIns = annotate (color insColor) . parens . ("Agda: " <>)
}
checkConformance ::
forall rule era.
( Era era
, ToExpr (SpecRep (ExecState rule era))
, Eq (SpecRep (ExecState rule era))
, EncCBOR (ExecContext rule era)
, EncCBOR (Environment (EraRule rule era))
, EncCBOR (State (EraRule rule era))
, EncCBOR (Signal (EraRule rule era))
, HasCallStack
) =>
ExecContext rule era ->
Environment (EraRule rule era) ->
State (EraRule rule era) ->
Signal (EraRule rule era) ->
Either OpaqueErrorString (SpecRep (ExecState rule era)) ->
Either OpaqueErrorString (SpecRep (ExecState rule era)) ->
ImpTestM era ()
checkConformance :: forall (rule :: Symbol) era.
(Era era, ToExpr (SpecRep (ExecState rule era)),
Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> ImpTestM era ()
checkConformance ExecContext rule era
ctx Environment (EraRule rule era)
env State (EraRule rule era)
st Signal (EraRule rule era)
sig Either OpaqueErrorString (SpecRep (ExecState rule era))
implResTest Either OpaqueErrorString (SpecRep (ExecState rule era))
agdaResTest = do
let
failMsg :: Doc AnsiStyle
failMsg =
AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Yellow) (Doc AnsiStyle -> Doc AnsiStyle)
-> ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle]
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
vsep ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle] -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$
[ Doc AnsiStyle
"===== DIFF ====="
, Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Doc AnsiStyle
forall a. ToExpr a => a -> a -> Doc AnsiStyle
diffConformance Either OpaqueErrorString (SpecRep (ExecState rule era))
implResTest Either OpaqueErrorString (SpecRep (ExecState rule era))
agdaResTest
]
Bool -> ImpTestM era () -> ImpTestM era ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Either OpaqueErrorString (SpecRep (ExecState rule era))
implResTest Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era)) -> Bool
forall a. Eq a => a -> a -> Bool
== Either OpaqueErrorString (SpecRep (ExecState rule era))
agdaResTest) (ImpTestM era () -> ImpTestM era ())
-> ImpTestM era () -> ImpTestM era ()
forall a b. (a -> b) -> a -> b
$ do
let envVarName :: String
envVarName = String
"CONFORMANCE_CBOR_DUMP_PATH"
Maybe String
mbyCborDumpPath <- String -> ImpM (LedgerSpec era) (Maybe String)
forall (m :: * -> *). MonadIO m => String -> m (Maybe String)
lookupEnv String
envVarName
case Maybe String
mbyCborDumpPath of
Just String
path -> do
String -> ExecContext rule era -> String -> ImpTestM era ()
forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path ExecContext rule era
ctx String
"conformance_dump_ctx"
String
-> Environment (EraRule rule era) -> String -> ImpTestM era ()
forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path Environment (EraRule rule era)
env String
"conformance_dump_env"
String -> State (EraRule rule era) -> String -> ImpTestM era ()
forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path State (EraRule rule era)
st String
"conformance_dump_st"
String -> Signal (EraRule rule era) -> String -> ImpTestM era ()
forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path Signal (EraRule rule era)
sig String
"conformance_dump_sig"
Doc AnsiStyle -> ImpTestM era ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpTestM era ())
-> Doc AnsiStyle -> ImpTestM era ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"Dumped the CBOR files to " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> String -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr String
path
Maybe String
Nothing ->
Doc AnsiStyle -> ImpTestM era ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpTestM era ())
-> Doc AnsiStyle -> ImpTestM era ()
forall a b. (a -> b) -> a -> b
$
Doc AnsiStyle
"Run the test again with "
Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> String -> Doc AnsiStyle
forall a. IsString a => String -> a
fromString String
envVarName
Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
"=<path> to get a CBOR dump of the test data"
String -> ImpTestM era ()
forall (m :: * -> *). (HasCallStack, MonadIO m) => String -> m ()
expectationFailure (String -> ImpTestM era ())
-> (Doc AnsiStyle -> String) -> Doc AnsiStyle -> ImpTestM era ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc AnsiStyle -> String
ansiDocToString (Doc AnsiStyle -> ImpTestM era ())
-> Doc AnsiStyle -> ImpTestM era ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
failMsg
defaultTestConformance ::
forall era rule.
( HasCallStack
, ShelleyEraImp era
, ExecSpecRule rule era
, ForAllExecSpecRep NFData rule era
, ForAllExecSpecRep ToExpr rule era
, NFData (PredicateFailure (EraRule rule era))
, Eq (SpecRep (ExecState rule era))
, Inject (State (EraRule rule era)) (ExecState rule era)
, SpecTranslate (ExecContext rule era) (ExecState rule era)
, FixupSpecRep (SpecRep (ExecState rule era))
, EncCBOR (ExecContext rule era)
, EncCBOR (Environment (EraRule rule era))
, EncCBOR (State (EraRule rule era))
, EncCBOR (Signal (EraRule rule era))
, ToExpr (ExecContext rule era)
, ToExpr (PredicateFailure (EraRule rule era))
) =>
ExecContext rule era ->
ExecEnvironment rule era ->
ExecState rule era ->
ExecSignal rule era ->
Property
defaultTestConformance :: forall era (rule :: Symbol).
(HasCallStack, ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (PredicateFailure (EraRule rule era)),
Eq (SpecRep (ExecState rule era)),
Inject (State (EraRule rule era)) (ExecState rule era),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era),
ToExpr (PredicateFailure (EraRule rule era))) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> ExecSignal rule era
-> Property
defaultTestConformance ExecContext rule era
ctx ExecEnvironment rule era
env ExecState rule era
st ExecSignal rule era
sig = ImpM (LedgerSpec era) () -> Property
forall prop. Testable prop => prop -> Property
property (ImpM (LedgerSpec era) () -> Property)
-> ImpM (LedgerSpec era) () -> Property
forall a b. (a -> b) -> a -> b
$ do
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))
implResTest, Either OpaqueErrorString (SpecRep (ExecState rule era))
agdaResTest, Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
implRes) <- forall (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
FixupSpecRep (SpecRep (ExecState rule era)),
Inject (State (EraRule rule era)) (ExecState rule era),
SpecTranslate (ExecContext rule era) (ExecState rule era),
ToExpr (ExecContext rule era), HasCallStack,
NFData (PredicateFailure (EraRule rule era))) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> ExecSignal rule era
-> ImpTestM
era
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)),
Either OpaqueErrorString (SpecRep (ExecState rule era)),
Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)]))
runConformance @rule @era ExecContext rule era
ctx ExecEnvironment rule era
env ExecState rule era
st ExecSignal rule era
sig
Globals
globals <- Getting Globals (ImpTestState era) Globals
-> ImpM (LedgerSpec era) Globals
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting Globals (ImpTestState era) Globals
forall era (f :: * -> *).
Functor f =>
(Globals -> f Globals) -> ImpTestState era -> f (ImpTestState era)
impGlobalsL
let
extra :: Doc AnsiStyle
extra =
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Globals
-> ExecContext rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
OpaqueErrorString
(State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @rule @era
Globals
globals
ExecContext rule era
ctx
(ExecEnvironment rule era -> Environment (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecEnvironment rule era
env)
(ExecState rule era -> State (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecState rule era
st)
(ExecSignal rule era -> Signal (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecSignal rule era
sig)
((NonEmpty (PredicateFailure (EraRule rule era))
-> OpaqueErrorString)
-> Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
-> Either
OpaqueErrorString
(State (EraRule rule era), [Event (EraRule rule era)])
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 NonEmpty (PredicateFailure (EraRule rule era)) -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
implRes)
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc Doc AnsiStyle
extra
forall (rule :: Symbol) era.
(Era era, ToExpr (SpecRep (ExecState rule era)),
Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> ImpTestM era ()
checkConformance @rule @_
ExecContext rule era
ctx
(ExecEnvironment rule era -> Environment (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecEnvironment rule era
env)
(ExecState rule era -> State (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecState rule era
st)
(ExecSignal rule era -> Signal (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecSignal rule era
sig)
((NonEmpty (PredicateFailure (EraRule rule era))
-> OpaqueErrorString)
-> Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
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 NonEmpty (PredicateFailure (EraRule rule era)) -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))
implResTest)
Either OpaqueErrorString (SpecRep (ExecState rule era))
agdaResTest
runConformance ::
forall (rule :: Symbol) era.
( ExecSpecRule rule era
, ForAllExecSpecRep NFData rule era
, ForAllExecSpecRep ToExpr rule era
, FixupSpecRep (SpecRep (ExecState rule era))
, Inject (State (EraRule rule era)) (ExecState rule era)
, SpecTranslate (ExecContext rule era) (ExecState rule era)
, ToExpr (ExecContext rule era)
, HasCallStack
, NFData (PredicateFailure (EraRule rule era))
) =>
ExecContext rule era ->
ExecEnvironment rule era ->
ExecState rule era ->
ExecSignal rule era ->
ImpTestM
era
( Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))
, Either OpaqueErrorString (SpecRep (ExecState rule era))
, Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
)
runConformance :: forall (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
FixupSpecRep (SpecRep (ExecState rule era)),
Inject (State (EraRule rule era)) (ExecState rule era),
SpecTranslate (ExecContext rule era) (ExecState rule era),
ToExpr (ExecContext rule era), HasCallStack,
NFData (PredicateFailure (EraRule rule era))) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> ExecSignal rule era
-> ImpTestM
era
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)),
Either OpaqueErrorString (SpecRep (ExecState rule era)),
Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)]))
runConformance ExecContext rule era
execContext ExecEnvironment rule era
env ExecState rule era
st ExecSignal rule era
sig = do
(SpecRep (ExecEnvironment rule era)
specEnv, SpecRep (ExecState rule era)
specSt, SpecRep (ExecSignal rule era)
specSig) <-
String
-> ImpM
(LedgerSpec era)
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era))
-> ImpM
(LedgerSpec era)
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era))
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating the inputs" (ImpM
(LedgerSpec era)
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era))
-> ImpM
(LedgerSpec era)
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era)))
-> ImpM
(LedgerSpec era)
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era))
-> ImpM
(LedgerSpec era)
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era))
forall a b. (a -> b) -> a -> b
$
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecEnvironment rule era
-> ExecState rule era
-> ExecSignal rule era
-> ExecContext rule era
-> ImpTestM
era
(SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era),
SpecRep (ExecSignal rule era))
translateInputs @rule @era ExecEnvironment rule era
env ExecState rule era
st ExecSignal rule era
sig ExecContext rule era
execContext
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"ctx:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> ExecContext rule era -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecContext rule era
execContext
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implEnv:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> ExecEnvironment rule era -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecEnvironment rule era
env
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implSt:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> ExecState rule era -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecState rule era
st
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implSig:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> ExecSignal rule era -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecSignal rule era
sig
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specEnv:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> SpecRep (ExecEnvironment rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecEnvironment rule era)
specEnv
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specSt:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> SpecRep (ExecState rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecState rule era)
specSt
Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc (Doc AnsiStyle -> ImpM (LedgerSpec era) ())
-> Doc AnsiStyle -> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specSig:\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> SpecRep (ExecSignal rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecSignal rule era)
specSig
Either OpaqueErrorString (SpecRep (ExecState rule era))
agdaResTest <-
(Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
forall a b.
(a -> b) -> ImpM (LedgerSpec era) a -> ImpM (LedgerSpec era) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SpecRep (ExecState rule era) -> SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SpecRep (ExecState rule era) -> SpecRep (ExecState rule era)
forall a. FixupSpecRep a => a -> a
fixup) (ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era))))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
forall a b. (a -> b) -> a -> b
$
String
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Deep evaluating Agda output" (ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era))))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
forall a b. (a -> b) -> a -> b
$
Either OpaqueErrorString (SpecRep (ExecState rule era))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep (Either OpaqueErrorString (SpecRep (ExecState rule era))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era))))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> ImpM
(LedgerSpec era)
(Either OpaqueErrorString (SpecRep (ExecState rule era)))
forall a b. (a -> b) -> a -> b
$
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
SpecRep (ExecEnvironment rule era)
-> SpecRep (ExecState rule era)
-> SpecRep (ExecSignal rule era)
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
runAgdaRule @rule @era SpecRep (ExecEnvironment rule era)
specEnv SpecRep (ExecState rule era)
specSt SpecRep (ExecSignal rule era)
specSig
Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
implRes <- forall (rule :: Symbol) era.
(STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase) =>
Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> ImpTestM
era
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)]))
tryRunImpRule @rule @era (ExecEnvironment rule era -> Environment (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecEnvironment rule era
env) (ExecState rule era -> State (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecState rule era
st) (ExecSignal rule era -> Signal (EraRule rule era)
forall t s. Inject t s => t -> s
inject ExecSignal rule era
sig)
Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))
implResTest <-
String
-> ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating implementation values to SpecRep" (ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))))
-> ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
forall a b. (a -> b) -> a -> b
$
Either
Text
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
forall a (m :: * -> *) b.
(HasCallStack, ToExpr a, MonadIO m) =>
Either a b -> m b
expectRightExpr (Either
Text
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))))
-> Either
Text
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> ImpM
(LedgerSpec era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
forall a b. (a -> b) -> a -> b
$
ExecContext rule era
-> SpecTransM
(ExecContext rule era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> Either
Text
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext rule era
execContext (SpecTransM
(ExecContext rule era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> Either
Text
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))))
-> SpecTransM
(ExecContext rule era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
-> Either
Text
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
forall a b. (a -> b) -> a -> b
$
(NonEmpty (PredicateFailure (EraRule rule era))
-> SpecTransM
(ExecContext rule era)
(NonEmpty (PredicateFailure (EraRule rule era))))
-> ((State (EraRule rule era), [Event (EraRule rule era)])
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecState rule era)))
-> Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
-> SpecTransM
(ExecContext rule era)
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)))
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM NonEmpty (PredicateFailure (EraRule rule era))
-> SpecTransM
(ExecContext rule era)
(NonEmpty (PredicateFailure (EraRule rule era)))
forall a. a -> SpecTransM (ExecContext rule era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecState rule era
-> SpecTransM (ExecContext rule era) (SpecRep (ExecState rule era))
forall ctx a.
(SpecTranslate ctx a, FixupSpecRep (SpecRep a)) =>
a -> SpecTransM ctx (SpecRep a)
toTestRep (ExecState rule era
-> SpecTransM
(ExecContext rule era) (SpecRep (ExecState rule era)))
-> ((State (EraRule rule era), [Event (EraRule rule era)])
-> ExecState rule era)
-> (State (EraRule rule era), [Event (EraRule rule era)])
-> SpecTransM (ExecContext rule era) (SpecRep (ExecState rule era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s. Inject t s => t -> s
inject @_ @(ExecState rule era) (State (EraRule rule era) -> ExecState rule era)
-> ((State (EraRule rule era), [Event (EraRule rule era)])
-> State (EraRule rule era))
-> (State (EraRule rule era), [Event (EraRule rule era)])
-> ExecState rule era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State (EraRule rule era), [Event (EraRule rule era)])
-> State (EraRule rule era)
forall a b. (a, b) -> a
fst) Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
implRes
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)),
Either OpaqueErrorString (SpecRep (ExecState rule era)),
Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)]))
-> ImpTestM
era
(Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era)),
Either OpaqueErrorString (SpecRep (ExecState rule era)),
Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)]))
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(SpecRep (ExecState rule era))
implResTest, Either OpaqueErrorString (SpecRep (ExecState rule era))
agdaResTest, Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
implRes)
conformsToImpl ::
forall (rule :: Symbol) era.
( ShelleyEraImp era
, ExecSpecRule rule era
, ForAllExecSpecRep NFData rule era
, ForAllExecSpecRep ToExpr rule era
, NFData (SpecRep (PredicateFailure (EraRule rule era)))
, NFData (ExecContext rule era)
, ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
, ToExpr (ExecContext rule era)
, SpecTranslate (ExecContext rule era) (State (EraRule rule era))
, Eq (SpecRep (PredicateFailure (EraRule rule era)))
, Inject (State (EraRule rule era)) (ExecState rule era)
, Eq (SpecRep (ExecState rule era))
, SpecTranslate (ExecContext rule era) (ExecState rule era)
, FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
, FixupSpecRep (SpecRep (ExecState rule era))
, EncCBOR (ExecContext rule era)
, EncCBOR (Environment (EraRule rule era))
, EncCBOR (State (EraRule rule era))
, EncCBOR (Signal (EraRule rule era))
, HasCallStack
, NFData (PredicateFailure (EraRule rule era))
, ToExpr (PredicateFailure (EraRule rule era))
) =>
Property
conformsToImpl :: forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl = forall prop. Testable prop => prop -> Property
property @(ImpTestM era Property) (ImpTestM era Property -> Property)
-> (ContT Property (ImpM (LedgerSpec era)) Property
-> ImpTestM era Property)
-> ContT Property (ImpM (LedgerSpec era)) Property
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ContT Property (ImpM (LedgerSpec era)) Property
-> (Property -> ImpTestM era Property) -> ImpTestM era Property
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
`runContT` Property -> ImpTestM era Property
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) (ContT Property (ImpM (LedgerSpec era)) Property -> Property)
-> ContT Property (ImpM (LedgerSpec era)) Property -> Property
forall a b. (a -> b) -> a -> b
$ do
let
deepEvalAnn :: a -> a
deepEvalAnn a
s = a
"Deep evaluating " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
s
deepEval :: a -> String -> t (ImpM t) ()
deepEval a
x String
s = do
a
_ <- ImpM t a -> t (ImpM t) a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ImpM t a -> t (ImpM t) a) -> ImpM t a -> t (ImpM t) a
forall a b. (a -> b) -> a -> b
$ String -> ImpM t a -> ImpM t a
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn (String -> String
forall {a}. (Semigroup a, IsString a) => a -> a
deepEvalAnn String
s) (IO a -> ImpM t a
forall a. IO a -> ImpM t a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (a -> IO a
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep a
x))
() -> t (ImpM t) ()
forall a. a -> t (ImpM t) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
ExecContext rule era
ctx <- ((ExecContext rule era -> ImpTestM era Property)
-> ImpTestM era Property)
-> ContT Property (ImpM (LedgerSpec era)) (ExecContext rule era)
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((ExecContext rule era -> ImpTestM era Property)
-> ImpTestM era Property)
-> ContT Property (ImpM (LedgerSpec era)) (ExecContext rule era))
-> ((ExecContext rule era -> ImpTestM era Property)
-> ImpTestM era Property)
-> ContT Property (ImpM (LedgerSpec era)) (ExecContext rule era)
forall a b. (a -> b) -> a -> b
$ \ExecContext rule era -> ImpTestM era Property
c ->
Property -> ImpTestM era Property
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> ImpTestM era Property)
-> Property -> ImpTestM era Property
forall a b. (a -> b) -> a -> b
$ Gen (ExecContext rule era)
-> (ExecContext rule era -> String)
-> (ExecContext rule era -> ImpTestM era Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> String) -> (a -> prop) -> Property
forAllShow (forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Gen (ExecContext rule era)
genExecContext @rule @era) ExecContext rule era -> String
forall a. ToExpr a => a -> String
showExpr ExecContext rule era -> ImpTestM era Property
c
ExecContext rule era
-> String -> ContT Property (ImpM (LedgerSpec era)) ()
forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecContext rule era
ctx String
"context"
let
forAllSpec :: Specification a -> ContT Property m a
forAllSpec Specification a
spec = do
let
simplifiedSpec :: Specification a
simplifiedSpec = Specification a -> Specification a
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
spec
generator :: Gen (GE a)
generator = GenT GE a -> GenMode -> [NonEmpty String] -> Gen (GE a)
forall (m :: * -> *) a.
GenT m a -> GenMode -> [NonEmpty String] -> Gen (m a)
CV1.runGenT (Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
CV2.genFromSpecT Specification a
simplifiedSpec) GenMode
Loose []
shrinker :: GE a -> [GE a]
shrinker (Result a
x) = a -> GE a
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> GE a) -> [a] -> [GE a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
simplifiedSpec a
x
shrinker GE a
_ = []
GE a
res :: GE a <- ((GE a -> m Property) -> m Property) -> ContT Property m (GE a)
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((GE a -> m Property) -> m Property) -> ContT Property m (GE a))
-> ((GE a -> m Property) -> m Property) -> ContT Property m (GE a)
forall a b. (a -> b) -> a -> b
$ \GE a -> m Property
c ->
Property -> m Property
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> m Property) -> Property -> m Property
forall a b. (a -> b) -> a -> b
$ Gen (GE a) -> (GE a -> [GE a]) -> (GE a -> m Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind Gen (GE a)
generator GE a -> [GE a]
shrinker GE a -> m Property
c
case GE a
res of
Result a
x -> a -> ContT Property m a
forall a. a -> ContT Property m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
GE a
_ -> ((a -> m Property) -> m Property) -> ContT Property m a
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((a -> m Property) -> m Property) -> ContT Property m a)
-> (Property -> (a -> m Property) -> m Property)
-> Property
-> ContT Property m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Property -> (a -> m Property) -> m Property
forall a b. a -> b -> a
const (m Property -> (a -> m Property) -> m Property)
-> (Property -> m Property)
-> Property
-> (a -> m Property)
-> m Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Property -> m Property
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> ContT Property m a) -> Property -> ContT Property m a
forall a b. (a -> b) -> a -> b
$ Discard -> Property
forall prop. Testable prop => prop -> Property
property Discard
Discard
ExecEnvironment rule era
env <- Specification (ExecEnvironment rule era)
-> ContT
Property (ImpM (LedgerSpec era)) (ExecEnvironment rule era)
forall {a} {m :: * -> *}.
(HasSpec a, Applicative m, Testable (m Property)) =>
Specification a -> ContT Property m a
forAllSpec (Specification (ExecEnvironment rule era)
-> ContT
Property (ImpM (LedgerSpec era)) (ExecEnvironment rule era))
-> Specification (ExecEnvironment rule era)
-> ContT
Property (ImpM (LedgerSpec era)) (ExecEnvironment rule era)
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era -> Specification (ExecEnvironment rule era)
environmentSpec @rule @era ExecContext rule era
ctx
ExecEnvironment rule era
-> String -> ContT Property (ImpM (LedgerSpec era)) ()
forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecEnvironment rule era
env String
"environment"
ExecState rule era
st <- Specification (ExecState rule era)
-> ContT Property (ImpM (LedgerSpec era)) (ExecState rule era)
forall {a} {m :: * -> *}.
(HasSpec a, Applicative m, Testable (m Property)) =>
Specification a -> ContT Property m a
forAllSpec (Specification (ExecState rule era)
-> ContT Property (ImpM (LedgerSpec era)) (ExecState rule era))
-> Specification (ExecState rule era)
-> ContT Property (ImpM (LedgerSpec era)) (ExecState rule era)
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> ExecEnvironment rule era -> Specification (ExecState rule era)
stateSpec @rule @era ExecContext rule era
ctx ExecEnvironment rule era
env
ExecState rule era
-> String -> ContT Property (ImpM (LedgerSpec era)) ()
forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecState rule era
st String
"state"
ExecSignal rule era
sig <- Specification (ExecSignal rule era)
-> ContT Property (ImpM (LedgerSpec era)) (ExecSignal rule era)
forall {a} {m :: * -> *}.
(HasSpec a, Applicative m, Testable (m Property)) =>
Specification a -> ContT Property m a
forAllSpec (Specification (ExecSignal rule era)
-> ContT Property (ImpM (LedgerSpec era)) (ExecSignal rule era))
-> Specification (ExecSignal rule era)
-> ContT Property (ImpM (LedgerSpec era)) (ExecSignal rule era)
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> Specification (ExecSignal rule era)
signalSpec @rule @era ExecContext rule era
ctx ExecEnvironment rule era
env ExecState rule era
st
ExecSignal rule era
-> String -> ContT Property (ImpM (LedgerSpec era)) ()
forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecSignal rule era
sig String
"signal"
let classification :: Property -> Property
classification =
case forall (rule :: Symbol) era.
ExecSpecRule rule era =>
ExecSignal rule era -> Maybe String
classOf @rule @era ExecSignal rule era
sig of
Maybe String
Nothing -> Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
False String
"None"
Just String
c -> Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True String
c
Property -> ContT Property (ImpM (LedgerSpec era)) Property
forall a. a -> ContT Property (ImpM (LedgerSpec era)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> ContT Property (ImpM (LedgerSpec era)) Property)
-> (Property -> Property)
-> Property
-> ContT Property (ImpM (LedgerSpec era)) Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Property -> Property
classification (Property -> ContT Property (ImpM (LedgerSpec era)) Property)
-> Property -> ContT Property (ImpM (LedgerSpec era)) Property
forall a b. (a -> b) -> a -> b
$
forall (rule :: Symbol) era.
(ExecSpecRule rule era, ShelleyEraImp era,
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Eq (SpecRep (ExecState rule era)),
Inject (State (EraRule rule era)) (ExecState rule era),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
Inject (ExecEnvironment rule era) (Environment (EraRule rule era)),
Inject (ExecState rule era) (State (EraRule rule era)),
Inject (ExecSignal rule era) (Signal (EraRule rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era),
ToExpr (PredicateFailure (EraRule rule era)),
NFData (PredicateFailure (EraRule rule era)), HasCallStack) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> ExecSignal rule era
-> Property
testConformance @rule @era ExecContext rule era
ctx ExecEnvironment rule era
env ExecState rule era
st ExecSignal rule era
sig
generatesWithin ::
forall a.
( NFData a
, ToExpr a
, Typeable a
, HasCallStack
) =>
Gen a ->
Int ->
Spec
generatesWithin :: forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
generatesWithin Gen a
gen Int
timeout =
String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (String
aName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" generates within " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
timeout String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"μs")
(Property -> Spec)
-> ((a -> Property) -> Property) -> (a -> Property) -> Spec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen a -> (a -> String) -> (a -> Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> String) -> (a -> prop) -> Property
forAllShow Gen a
gen a -> String
forall a. ToExpr a => a -> String
showExpr
((a -> Property) -> Spec) -> (a -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ \a
x -> Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
timeout (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ IO () -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (a -> IO a
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep a
x IO a -> () -> IO ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ())
where
aName :: String
aName = TypeRep -> String
forall a. Show a => a -> String
show (Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a -> TypeRep) -> Proxy a -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
inputsGenerateWithin ::
forall (rule :: Symbol) era.
ExecSpecRule rule era =>
Int ->
Spec
inputsGenerateWithin :: forall (rule :: Symbol) era. ExecSpecRule rule era => Int -> Spec
inputsGenerateWithin Int
timeout =
String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (String
aName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" input generation time") (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
let
genEnv :: Gen (ExecEnvironment rule era)
genEnv = do
ExecContext rule era
ctx <- forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Gen (ExecContext rule era)
genExecContext @rule @era
Specification (ExecEnvironment rule era)
-> Gen (ExecEnvironment rule era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
CV2.genFromSpec (Specification (ExecEnvironment rule era)
-> Gen (ExecEnvironment rule era))
-> Specification (ExecEnvironment rule era)
-> Gen (ExecEnvironment rule era)
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era -> Specification (ExecEnvironment rule era)
environmentSpec @rule @era ExecContext rule era
ctx
genSt :: Gen (ExecState rule era)
genSt = do
ExecContext rule era
ctx <- forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Gen (ExecContext rule era)
genExecContext @rule @era
ExecEnvironment rule era
env <- Gen (ExecEnvironment rule era)
genEnv
Specification (ExecState rule era) -> Gen (ExecState rule era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
CV2.genFromSpec (Specification (ExecState rule era) -> Gen (ExecState rule era))
-> Specification (ExecState rule era) -> Gen (ExecState rule era)
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> ExecEnvironment rule era -> Specification (ExecState rule era)
stateSpec @rule @era ExecContext rule era
ctx ExecEnvironment rule era
env
genSig :: Gen (ExecSignal rule era)
genSig = do
ExecContext rule era
ctx <- forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Gen (ExecContext rule era)
genExecContext @rule @era
ExecEnvironment rule era
env <- Gen (ExecEnvironment rule era)
genEnv
ExecState rule era
st <- Gen (ExecState rule era)
genSt
Specification (ExecSignal rule era) -> Gen (ExecSignal rule era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
CV2.genFromSpec (Specification (ExecSignal rule era) -> Gen (ExecSignal rule era))
-> Specification (ExecSignal rule era) -> Gen (ExecSignal rule era)
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> Specification (ExecSignal rule era)
signalSpec @rule @era ExecContext rule era
ctx ExecEnvironment rule era
env ExecState rule era
st
Gen (ExecEnvironment rule era)
genEnv Gen (ExecEnvironment rule era) -> Int -> Spec
forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
`generatesWithin` Int
timeout
Gen (ExecState rule era)
genSt Gen (ExecState rule era) -> Int -> Spec
forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
`generatesWithin` Int
timeout
Gen (ExecSignal rule era)
genSig Gen (ExecSignal rule era) -> Int -> Spec
forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
`generatesWithin` Int
timeout
where
aName :: String
aName = TypeRep -> String
forall a. Show a => a -> String
show (Proxy rule -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy rule -> TypeRep) -> Proxy rule -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @rule)
translateWithContext :: SpecTranslate ctx a => ctx -> a -> ImpTestM era (SpecRep a)
translateWithContext :: forall ctx a era.
SpecTranslate ctx a =>
ctx -> a -> ImpTestM era (SpecRep a)
translateWithContext ctx
ctx a
x = do
let
expectRight' :: Either Text a -> f a
expectRight' (Right a
y) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
y
expectRight' (Left Text
e) = String -> f a
forall (m :: * -> *) a. (HasCallStack, MonadIO m) => String -> m a
assertFailure (Text -> String
T.unpack Text
e)
Either Text (SpecRep a) -> ImpTestM era (SpecRep a)
forall {f :: * -> *} {a}. MonadIO f => Either Text a -> f a
expectRight' (Either Text (SpecRep a) -> ImpTestM era (SpecRep a))
-> (SpecTransM ctx (SpecRep a) -> Either Text (SpecRep a))
-> SpecTransM ctx (SpecRep a)
-> ImpTestM era (SpecRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ctx -> SpecTransM ctx (SpecRep a) -> Either Text (SpecRep a)
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ctx
ctx (SpecTransM ctx (SpecRep a) -> ImpTestM era (SpecRep a))
-> SpecTransM ctx (SpecRep a) -> ImpTestM era (SpecRep a)
forall a b. (a -> b) -> a -> b
$ a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x