{-# 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 as CV2
import Constrained.Base (shrinkWithSpec, simplifySpec)
import Constrained.GenT (GE (..), GenMode (..))
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) fn rule era =
  ( c (ExecEnvironment fn rule era)
  , c (ExecState fn rule era)
  , c (ExecSignal fn rule era)
  )

type ForAllExecSpecRep (c :: Type -> Constraint) fn rule era =
  ( c (SpecRep (ExecEnvironment fn rule era))
  , c (SpecRep (ExecState fn rule era))
  , c (SpecRep (ExecSignal fn rule era))
  )

class
  ( ForAllExecTypes (CV2.HasSpec fn) fn rule era
  , ForAllExecTypes ToExpr fn rule era
  , ForAllExecTypes NFData fn rule era
  , KnownSymbol rule
  , STS (EraRule rule era)
  , BaseM (EraRule rule era) ~ ShelleyBase
  , SpecTranslate (ExecContext fn rule era) (PredicateFailure (EraRule rule era))
  , Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era))
  , Inject (ExecState fn rule era) (State (EraRule rule era))
  , Inject (ExecSignal fn rule era) (Signal (EraRule rule era))
  ) =>
  ExecSpecRule fn (rule :: Symbol) era
  where
  type ExecContext fn rule era
  type ExecContext fn rule era = ()

  type ExecEnvironment fn rule era
  type ExecEnvironment fn rule era = Environment (EraRule rule era)

  type ExecState fn rule era
  type ExecState fn rule era = State (EraRule rule era)

  type ExecSignal fn rule era
  type ExecSignal fn rule era = Signal (EraRule rule era)

  environmentSpec ::
    HasCallStack =>
    ExecContext fn rule era ->
    CV2.Specification fn (ExecEnvironment fn rule era)

  stateSpec ::
    HasCallStack =>
    ExecContext fn rule era ->
    ExecEnvironment fn rule era ->
    CV2.Specification fn (ExecState fn rule era)

  signalSpec ::
    HasCallStack =>
    ExecContext fn rule era ->
    ExecEnvironment fn rule era ->
    ExecState fn rule era ->
    CV2.Specification fn (ExecSignal fn rule era)

  classOf :: ExecSignal fn rule era -> Maybe String
  classOf ExecSignal fn rule era
_ = forall a. Maybe a
Nothing

  genExecContext :: HasCallStack => Gen (ExecContext fn rule era)
  default genExecContext ::
    Arbitrary (ExecContext fn rule era) =>
    Gen (ExecContext fn rule era)
  genExecContext = forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary

  runAgdaRule ::
    HasCallStack =>
    SpecRep (ExecEnvironment fn rule era) ->
    SpecRep (ExecState fn rule era) ->
    SpecRep (ExecSignal fn rule era) ->
    Either OpaqueErrorString (SpecRep (ExecState fn rule era))

  translateInputs ::
    HasCallStack =>
    ExecEnvironment fn rule era ->
    ExecState fn rule era ->
    ExecSignal fn rule era ->
    ExecContext fn rule era ->
    ImpTestM
      era
      ( SpecRep (ExecEnvironment fn rule era)
      , SpecRep (ExecState fn rule era)
      , SpecRep (ExecSignal fn rule era)
      )
  default translateInputs ::
    ( ForAllExecTypes (SpecTranslate (ExecContext fn rule era)) fn rule era
    , ForAllExecSpecRep ToExpr fn rule era
    ) =>
    ExecEnvironment fn rule era ->
    ExecState fn rule era ->
    ExecSignal fn rule era ->
    ExecContext fn rule era ->
    ImpTestM
      era
      ( SpecRep (ExecEnvironment fn rule era)
      , SpecRep (ExecState fn rule era)
      , SpecRep (ExecSignal fn rule era)
      )
  translateInputs ExecEnvironment fn rule era
env ExecState fn rule era
st ExecSignal fn rule era
sig ExecContext fn rule era
ctx = do
    let
      expectRight' :: Either Text a -> f a
expectRight' (Right a
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
      expectRight' (Left Text
e) = forall (m :: * -> *) a. (HasCallStack, MonadIO m) => String -> m a
assertFailure (Text -> String
T.unpack Text
e)
    SpecRep (ExecEnvironment fn rule era)
agdaEnv <- forall {f :: * -> *} {a}. MonadIO f => Either Text a -> f a
expectRight' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext fn rule era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecEnvironment fn rule era
env
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"agdaEnv:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecEnvironment fn rule era)
agdaEnv
    SpecRep (ExecState fn rule era)
agdaSt <- forall {f :: * -> *} {a}. MonadIO f => Either Text a -> f a
expectRight' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext fn rule era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecState fn rule era
st
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"agdaSt:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecState fn rule era)
agdaSt
    SpecRep (ExecSignal fn rule era)
agdaSig <- forall {f :: * -> *} {a}. MonadIO f => Either Text a -> f a
expectRight' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext fn rule era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecSignal fn rule era
sig
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"agdaSig:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecSignal fn rule era)
agdaSig
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecRep (ExecEnvironment fn rule era)
agdaEnv, SpecRep (ExecState fn rule era)
agdaSt, SpecRep (ExecSignal fn rule era)
agdaSig)

  testConformance ::
    ( ShelleyEraImp era
    , SpecTranslate (ExecContext fn rule era) (State (EraRule rule era))
    , ForAllExecSpecRep NFData fn rule era
    , ForAllExecSpecRep ToExpr fn rule era
    , NFData (SpecRep (PredicateFailure (EraRule rule era)))
    , ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
    , Eq (SpecRep (PredicateFailure (EraRule rule era)))
    , Eq (SpecRep (ExecState fn rule era))
    , Inject
        (State (EraRule rule era))
        (ExecState fn rule era)
    , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
    , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
    , FixupSpecRep (SpecRep (ExecState fn rule era))
    , Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era))
    , Inject (ExecState fn rule era) (State (EraRule rule era))
    , Inject (ExecSignal fn rule era) (Signal (EraRule rule era))
    , EncCBOR (ExecContext fn rule era)
    , EncCBOR (Environment (EraRule rule era))
    , EncCBOR (State (EraRule rule era))
    , EncCBOR (Signal (EraRule rule era))
    , ToExpr (ExecContext fn rule era)
    , ToExpr (PredicateFailure (EraRule rule era))
    , NFData (PredicateFailure (EraRule rule era))
    , HasCallStack
    ) =>
    ExecContext fn rule era ->
    ExecEnvironment fn rule era ->
    ExecState fn rule era ->
    ExecSignal fn rule era ->
    Property
  testConformance = forall (fn :: [*] -> * -> *) era (rule :: Symbol).
(HasCallStack, ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (PredicateFailure (EraRule rule era)),
 Eq (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)),
 ToExpr (ExecContext fn rule era),
 ToExpr (PredicateFailure (EraRule rule era))) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> Property
defaultTestConformance @fn @era @rule

  extraInfo ::
    HasCallStack =>
    Globals ->
    ExecContext fn 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 fn rule era
_ Environment (EraRule rule era)
_ State (EraRule rule era)
_ Signal (EraRule rule era)
_ = 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 <- forall (m :: * -> *). MonadIO m => String -> m String
makeAbsolute forall a b. (a -> b) -> a -> b
$ String
path forall a. Semigroup a => a -> a -> a
<> String
"/" forall a. Semigroup a => a -> a -> a
<> String
name String -> String -> String
<.> String
"cbor"
  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 =
  forall doc. Pretty doc -> Edit EditExpr -> doc
ppEditExpr Pretty (Doc AnsiStyle)
conformancePretty (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 :: Doc AnsiStyle -> Doc AnsiStyle
ppDel = forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
delColor) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc AnsiStyle
"Impl: " forall a. Semigroup a => a -> a -> a
<>)
        , ppIns :: Doc AnsiStyle -> Doc AnsiStyle
ppIns = forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
insColor) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc AnsiStyle
"Agda: " forall a. Semigroup a => a -> a -> a
<>)
        }

checkConformance ::
  forall rule era fn.
  ( Era era
  , ToExpr (SpecRep (ExecState fn rule era))
  , Eq (SpecRep (ExecState fn rule era))
  , EncCBOR (ExecContext fn rule era)
  , EncCBOR (Environment (EraRule rule era))
  , EncCBOR (State (EraRule rule era))
  , EncCBOR (Signal (EraRule rule era))
  , HasCallStack
  ) =>
  ExecContext fn rule era ->
  Environment (EraRule rule era) ->
  State (EraRule rule era) ->
  Signal (EraRule rule era) ->
  Either OpaqueErrorString (SpecRep (ExecState fn rule era)) ->
  Either OpaqueErrorString (SpecRep (ExecState fn rule era)) ->
  ImpTestM era ()
checkConformance :: forall (rule :: Symbol) era (fn :: [*] -> * -> *).
(Era era, ToExpr (SpecRep (ExecState fn rule era)),
 Eq (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> ImpTestM era ()
checkConformance ExecContext fn rule era
ctx Environment (EraRule rule era)
env State (EraRule rule era)
st Signal (EraRule rule era)
sig Either OpaqueErrorString (SpecRep (ExecState fn rule era))
implResTest Either OpaqueErrorString (SpecRep (ExecState fn rule era))
agdaResTest = do
  let
    failMsg :: Doc AnsiStyle
failMsg =
      forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Yellow) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. [Doc ann] -> Doc ann
vsep forall a b. (a -> b) -> a -> b
$
        [ Doc AnsiStyle
"===== DIFF ====="
        , forall a. ToExpr a => a -> a -> Doc AnsiStyle
diffConformance Either OpaqueErrorString (SpecRep (ExecState fn rule era))
implResTest Either OpaqueErrorString (SpecRep (ExecState fn rule era))
agdaResTest
        ]
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Either OpaqueErrorString (SpecRep (ExecState fn rule era))
implResTest forall a. Eq a => a -> a -> Bool
== Either OpaqueErrorString (SpecRep (ExecState fn rule era))
agdaResTest) forall a b. (a -> b) -> a -> b
$ do
    let envVarName :: String
envVarName = String
"CONFORMANCE_CBOR_DUMP_PATH"
    Maybe String
mbyCborDumpPath <- forall (m :: * -> *). MonadIO m => String -> m (Maybe String)
lookupEnv String
envVarName
    case Maybe String
mbyCborDumpPath of
      Just String
path -> do
        forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path ExecContext fn rule era
ctx String
"conformance_dump_ctx"
        forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path Environment (EraRule rule era)
env String
"conformance_dump_env"
        forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path State (EraRule rule era)
st String
"conformance_dump_st"
        forall era a.
(EncCBOR a, Era era) =>
String -> a -> String -> ImpTestM era ()
dumpCbor String
path Signal (EraRule rule era)
sig String
"conformance_dump_sig"
        forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"Dumped the CBOR files to " forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr String
path
      Maybe String
Nothing ->
        forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$
          Doc AnsiStyle
"Run the test again with "
            forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => String -> a
fromString String
envVarName
            forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
"=<path> to get a CBOR dump of the test data"
    forall (m :: * -> *). (HasCallStack, MonadIO m) => String -> m ()
expectationFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc AnsiStyle -> String
ansiDocToString forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
failMsg

defaultTestConformance ::
  forall fn era rule.
  ( HasCallStack
  , ShelleyEraImp era
  , ExecSpecRule fn rule era
  , ForAllExecSpecRep NFData fn rule era
  , ForAllExecSpecRep ToExpr fn rule era
  , NFData (PredicateFailure (EraRule rule era))
  , Eq (SpecRep (ExecState fn rule era))
  , Inject (State (EraRule rule era)) (ExecState fn rule era)
  , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
  , FixupSpecRep (SpecRep (ExecState fn rule era))
  , EncCBOR (ExecContext fn rule era)
  , EncCBOR (Environment (EraRule rule era))
  , EncCBOR (State (EraRule rule era))
  , EncCBOR (Signal (EraRule rule era))
  , ToExpr (ExecContext fn rule era)
  , ToExpr (PredicateFailure (EraRule rule era))
  ) =>
  ExecContext fn rule era ->
  ExecEnvironment fn rule era ->
  ExecState fn rule era ->
  ExecSignal fn rule era ->
  Property
defaultTestConformance :: forall (fn :: [*] -> * -> *) era (rule :: Symbol).
(HasCallStack, ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (PredicateFailure (EraRule rule era)),
 Eq (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)),
 ToExpr (ExecContext fn rule era),
 ToExpr (PredicateFailure (EraRule rule era))) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> Property
defaultTestConformance ExecContext fn rule era
ctx ExecEnvironment fn rule era
env ExecState fn rule era
st ExecSignal fn rule era
sig = forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ do
  (Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecRep (ExecState fn rule era))
implResTest, Either OpaqueErrorString (SpecRep (ExecState fn rule era))
agdaResTest, Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
implRes) <- forall (rule :: Symbol) (fn :: [*] -> * -> *) era.
(ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 ToExpr (ExecContext fn rule era), HasCallStack,
 NFData (PredicateFailure (EraRule rule era))) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> ImpTestM
     era
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecRep (ExecState fn rule era)),
      Either OpaqueErrorString (SpecRep (ExecState fn rule era)),
      Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (State (EraRule rule era), [Event (EraRule rule era)]))
runConformance @rule @fn @era ExecContext fn rule era
ctx ExecEnvironment fn rule era
env ExecState fn rule era
st ExecSignal fn rule era
sig
  Globals
globals <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use forall era. Lens' (ImpTestState era) Globals
impGlobalsL
  let
    extra :: Doc AnsiStyle
extra =
      forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Globals
-> ExecContext fn 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 @fn @rule @era
        Globals
globals
        ExecContext fn rule era
ctx
        (forall t s. Inject t s => t -> s
inject ExecEnvironment fn rule era
env)
        (forall t s. Inject t s => t -> s
inject ExecState fn rule era
st)
        (forall t s. Inject t s => t -> s
inject ExecSignal fn rule era
sig)
        (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
implRes)
  forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc Doc AnsiStyle
extra
  forall (rule :: Symbol) era (fn :: [*] -> * -> *).
(Era era, ToExpr (SpecRep (ExecState fn rule era)),
 Eq (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> ImpTestM era ()
checkConformance @rule @_ @fn
    ExecContext fn rule era
ctx
    (forall t s. Inject t s => t -> s
inject ExecEnvironment fn rule era
env)
    (forall t s. Inject t s => t -> s
inject ExecState fn rule era
st)
    (forall t s. Inject t s => t -> s
inject ExecSignal fn rule era
sig)
    (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecRep (ExecState fn rule era))
implResTest)
    Either OpaqueErrorString (SpecRep (ExecState fn rule era))
agdaResTest

runConformance ::
  forall (rule :: Symbol) (fn :: [Type] -> Type -> Type) era.
  ( ExecSpecRule fn rule era
  , ForAllExecSpecRep NFData fn rule era
  , ForAllExecSpecRep ToExpr fn rule era
  , FixupSpecRep (SpecRep (ExecState fn rule era))
  , Inject (State (EraRule rule era)) (ExecState fn rule era)
  , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
  , ToExpr (ExecContext fn rule era)
  , HasCallStack
  , NFData (PredicateFailure (EraRule rule era))
  ) =>
  ExecContext fn rule era ->
  ExecEnvironment fn rule era ->
  ExecState fn rule era ->
  ExecSignal fn rule era ->
  ImpTestM
    era
    ( Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecRep (ExecState fn rule era))
    , Either OpaqueErrorString (SpecRep (ExecState fn rule era))
    , Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (State (EraRule rule era), [Event (EraRule rule era)])
    )
runConformance :: forall (rule :: Symbol) (fn :: [*] -> * -> *) era.
(ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 ToExpr (ExecContext fn rule era), HasCallStack,
 NFData (PredicateFailure (EraRule rule era))) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> ImpTestM
     era
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecRep (ExecState fn rule era)),
      Either OpaqueErrorString (SpecRep (ExecState fn rule era)),
      Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (State (EraRule rule era), [Event (EraRule rule era)]))
runConformance ExecContext fn rule era
execContext ExecEnvironment fn rule era
env ExecState fn rule era
st ExecSignal fn rule era
sig = do
  (SpecRep (ExecEnvironment fn rule era)
specEnv, SpecRep (ExecState fn rule era)
specSt, SpecRep (ExecSignal fn rule era)
specSig) <-
    forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating the inputs" forall a b. (a -> b) -> a -> b
$
      forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> ExecContext fn rule era
-> ImpTestM
     era
     (SpecRep (ExecEnvironment fn rule era),
      SpecRep (ExecState fn rule era), SpecRep (ExecSignal fn rule era))
translateInputs @fn @rule @era ExecEnvironment fn rule era
env ExecState fn rule era
st ExecSignal fn rule era
sig ExecContext fn rule era
execContext
  forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"ctx:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecContext fn rule era
execContext
  forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implEnv:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecEnvironment fn rule era
env
  forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implSt:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecState fn rule era
st
  forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"implSig:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr ExecSignal fn rule era
sig
  forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specEnv:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecEnvironment fn rule era)
specEnv
  forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specSt:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecState fn rule era)
specSt
  forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"specSig:\n" forall a. Semigroup a => a -> a -> a
<> forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecRep (ExecSignal fn rule era)
specSig
  Either OpaqueErrorString (SpecRep (ExecState fn rule era))
agdaResTest <-
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. FixupSpecRep a => a -> a
fixup) forall a b. (a -> b) -> a -> b
$
      forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Deep evaluating Agda output" forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep forall a b. (a -> b) -> a -> b
$
          forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
SpecRep (ExecEnvironment fn rule era)
-> SpecRep (ExecState fn rule era)
-> SpecRep (ExecSignal fn rule era)
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
runAgdaRule @fn @rule @era SpecRep (ExecEnvironment fn rule era)
specEnv SpecRep (ExecState fn rule era)
specSt SpecRep (ExecSignal fn 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 (forall t s. Inject t s => t -> s
inject ExecEnvironment fn rule era
env) (forall t s. Inject t s => t -> s
inject ExecState fn rule era
st) (forall t s. Inject t s => t -> s
inject ExecSignal fn rule era
sig)
  Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecRep (ExecState fn rule era))
implResTest <-
    forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating implementation values to SpecRep" forall a b. (a -> b) -> a -> b
$
      forall a (m :: * -> *) b.
(HasCallStack, ToExpr a, MonadIO m) =>
Either a b -> m b
expectRightExpr forall a b. (a -> b) -> a -> b
$
        forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext fn rule era
execContext forall a b. (a -> b) -> a -> b
$
          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 forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall ctx a.
(SpecTranslate ctx a, FixupSpecRep (SpecRep a)) =>
a -> SpecTransM ctx (SpecRep a)
toTestRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s. Inject t s => t -> s
inject @_ @(ExecState fn rule era) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
implRes
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecRep (ExecState fn rule era))
implResTest, Either OpaqueErrorString (SpecRep (ExecState fn rule era))
agdaResTest, Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
implRes)

conformsToImpl ::
  forall (rule :: Symbol) fn era.
  ( ShelleyEraImp era
  , ExecSpecRule fn rule era
  , ForAllExecSpecRep NFData fn rule era
  , ForAllExecSpecRep ToExpr fn rule era
  , NFData (SpecRep (PredicateFailure (EraRule rule era)))
  , NFData (ExecContext fn rule era)
  , ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
  , ToExpr (ExecContext fn rule era)
  , SpecTranslate (ExecContext fn rule era) (State (EraRule rule era))
  , Eq (SpecRep (PredicateFailure (EraRule rule era)))
  , Inject (State (EraRule rule era)) (ExecState fn rule era)
  , Eq (SpecRep (ExecState fn rule era))
  , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
  , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
  , FixupSpecRep (SpecRep (ExecState fn rule era))
  , EncCBOR (ExecContext fn 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) (fn :: [*] -> * -> *) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
`runContT` forall (f :: * -> *) a. Applicative f => a -> f a
pure) forall a b. (a -> b) -> a -> b
$ do
  let
    deepEvalAnn :: a -> a
deepEvalAnn a
s = a
"Deep evaluating " forall a. Semigroup a => a -> a -> a
<> a
s
    deepEval :: a -> String -> t (ImpM t) ()
deepEval a
x String
s = do
      a
_ <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn (forall {a}. (Semigroup a, IsString a) => a -> a
deepEvalAnn String
s) (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep a
x))
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  ExecContext fn rule era
ctx <- forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT forall a b. (a -> b) -> a -> b
$ \ExecContext fn rule era -> ImpTestM era Property
c ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop a.
Testable prop =>
Gen a -> (a -> String) -> (a -> prop) -> Property
forAllShow (forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Gen (ExecContext fn rule era)
genExecContext @fn @rule @era) forall a. ToExpr a => a -> String
showExpr ExecContext fn rule era -> ImpTestM era Property
c
  forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecContext fn rule era
ctx String
"context"
  let
    forAllSpec :: Specification fn a -> ContT Property m a
forAllSpec Specification fn a
spec = do
      let
        simplifiedSpec :: Specification fn a
simplifiedSpec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec Specification fn a
spec
        generator :: Gen (GE a)
generator = forall (m :: * -> *) a. GenT m a -> GenMode -> Gen (m a)
CV2.runGenT (forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
CV2.genFromSpecT Specification fn a
simplifiedSpec) GenMode
Loose
        shrinker :: GE a -> [GE a]
shrinker (Result [NonEmpty String]
_ a
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn a
simplifiedSpec a
x
        shrinker GE a
_ = []
      GE a
res :: GE a <- forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT forall a b. (a -> b) -> a -> b
$ \GE a -> m Property
c ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 [NonEmpty String]
_ a
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
        GE a
_ -> forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Discard
Discard
  ExecEnvironment fn rule era
env <- forall {fn :: [*] -> * -> *} {a} {m :: * -> *}.
(HasSpec fn a, Applicative m, Testable (m Property)) =>
Specification fn a -> ContT Property m a
forAllSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> Specification fn (ExecEnvironment fn rule era)
environmentSpec @fn @rule @era ExecContext fn rule era
ctx
  forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecEnvironment fn rule era
env String
"environment"
  ExecState fn rule era
st <- forall {fn :: [*] -> * -> *} {a} {m :: * -> *}.
(HasSpec fn a, Applicative m, Testable (m Property)) =>
Specification fn a -> ContT Property m a
forAllSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> Specification fn (ExecState fn rule era)
stateSpec @fn @rule @era ExecContext fn rule era
ctx ExecEnvironment fn rule era
env
  forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecState fn rule era
st String
"state"
  ExecSignal fn rule era
sig <- forall {fn :: [*] -> * -> *} {a} {m :: * -> *}.
(HasSpec fn a, Applicative m, Testable (m Property)) =>
Specification fn a -> ContT Property m a
forAllSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> Specification fn (ExecSignal fn rule era)
signalSpec @fn @rule @era ExecContext fn rule era
ctx ExecEnvironment fn rule era
env ExecState fn rule era
st
  forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecSignal fn rule era
sig String
"signal"
  let classification :: Property -> Property
classification =
        case forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
ExecSpecRule fn rule era =>
ExecSignal fn rule era -> Maybe String
classOf @fn @rule @era ExecSignal fn rule era
sig of
          Maybe String
Nothing -> forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
False String
"None"
          Just String
c -> forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True String
c
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Property -> Property
classification forall a b. (a -> b) -> a -> b
$
    forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, ShelleyEraImp era,
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Eq (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 Inject
   (ExecEnvironment fn rule era) (Environment (EraRule rule era)),
 Inject (ExecState fn rule era) (State (EraRule rule era)),
 Inject (ExecSignal fn rule era) (Signal (EraRule rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)),
 ToExpr (ExecContext fn rule era),
 ToExpr (PredicateFailure (EraRule rule era)),
 NFData (PredicateFailure (EraRule rule era)), HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> Property
testConformance @fn @rule @era ExecContext fn rule era
ctx ExecEnvironment fn rule era
env ExecState fn rule era
st ExecSignal fn 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 =
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (String
aName forall a. Semigroup a => a -> a -> a
<> String
" generates within " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Int
timeout forall a. Semigroup a => a -> a -> a
<> String
"μs")
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop a.
Testable prop =>
Gen a -> (a -> String) -> (a -> prop) -> Property
forAllShow Gen a
gen forall a. ToExpr a => a -> String
showExpr
    forall a b. (a -> b) -> a -> b
$ \a
x -> forall prop. Testable prop => Int -> prop -> Property
within Int
timeout forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => IO prop -> Property
ioProperty (forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep a
x forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ())
  where
    aName :: String
aName = forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @a)

inputsGenerateWithin ::
  forall (fn :: [Type] -> Type -> Type) (rule :: Symbol) era.
  ExecSpecRule fn rule era =>
  Int ->
  Spec
inputsGenerateWithin :: forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
ExecSpecRule fn rule era =>
Int -> Spec
inputsGenerateWithin Int
timeout =
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe (String
aName forall a. Semigroup a => a -> a -> a
<> String
" input generation time") forall a b. (a -> b) -> a -> b
$ do
    let
      genEnv :: Gen (ExecEnvironment fn rule era)
genEnv = do
        ExecContext fn rule era
ctx <- forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Gen (ExecContext fn rule era)
genExecContext @fn @rule @era
        forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
CV2.genFromSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> Specification fn (ExecEnvironment fn rule era)
environmentSpec @fn @rule @era ExecContext fn rule era
ctx
      genSt :: Gen (ExecState fn rule era)
genSt = do
        ExecContext fn rule era
ctx <- forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Gen (ExecContext fn rule era)
genExecContext @fn @rule @era
        ExecEnvironment fn rule era
env <- Gen (ExecEnvironment fn rule era)
genEnv
        forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
CV2.genFromSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> Specification fn (ExecState fn rule era)
stateSpec @fn @rule @era ExecContext fn rule era
ctx ExecEnvironment fn rule era
env
      genSig :: Gen (ExecSignal fn rule era)
genSig = do
        ExecContext fn rule era
ctx <- forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Gen (ExecContext fn rule era)
genExecContext @fn @rule @era
        ExecEnvironment fn rule era
env <- Gen (ExecEnvironment fn rule era)
genEnv
        ExecState fn rule era
st <- Gen (ExecState fn rule era)
genSt
        forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
CV2.genFromSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> Specification fn (ExecSignal fn rule era)
signalSpec @fn @rule @era ExecContext fn rule era
ctx ExecEnvironment fn rule era
env ExecState fn rule era
st
    Gen (ExecEnvironment fn rule era)
genEnv forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
`generatesWithin` Int
timeout
    Gen (ExecState fn rule era)
genSt forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
`generatesWithin` Int
timeout
    Gen (ExecSignal fn rule era)
genSig forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
`generatesWithin` Int
timeout
  where
    aName :: String
aName = forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @rule)

-- | Translate a Haskell type 'a' whose translation context is 'ctx' into its Agda type, in the ImpTest monad.
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) = forall (f :: * -> *) a. Applicative f => a -> f a
pure a
y
    expectRight' (Left Text
e) = forall (m :: * -> *) a. (HasCallStack, MonadIO m) => String -> m a
assertFailure (Text -> String
T.unpack Text
e)
  forall {f :: * -> *} {a}. MonadIO f => Either Text a -> f a
expectRight' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ctx
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x