{-# 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
_ = forall a. Maybe a
Nothing

  genExecContext :: HasCallStack => Gen (ExecContext rule era)
  default genExecContext ::
    Arbitrary (ExecContext rule era) =>
    Gen (ExecContext rule era)
  genExecContext = 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) = 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 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 rule era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecEnvironment 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 rule era)
agdaEnv
    SpecRep (ExecState 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 rule era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecState 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 rule era)
agdaSt
    SpecRep (ExecSignal 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 rule era
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecSignal 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 rule era)
agdaSig
    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

  extraInfo ::
    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)
_ = 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.
  ( 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 =
      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 rule era))
implResTest Either OpaqueErrorString (SpecRep (ExecState rule era))
agdaResTest
        ]
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Either OpaqueErrorString (SpecRep (ExecState rule era))
implResTest forall a. Eq a => a -> a -> Bool
== Either OpaqueErrorString (SpecRep (ExecState 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 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 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 = forall prop. Testable prop => prop -> Property
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 <- 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 (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
        (forall t s. Inject t s => t -> s
inject ExecEnvironment rule era
env)
        (forall t s. Inject t s => t -> s
inject ExecState rule era
st)
        (forall t s. Inject t s => t -> s
inject ExecSignal 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.
(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
    (forall t s. Inject t s => t -> s
inject ExecEnvironment rule era
env)
    (forall t s. Inject t s => t -> s
inject ExecState rule era
st)
    (forall t s. Inject t s => t -> s
inject ExecSignal 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 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) <-
    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 (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
  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 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 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 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 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 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 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 rule era)
specSig
  Either OpaqueErrorString (SpecRep (ExecState 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 (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 (forall t s. Inject t s => t -> s
inject ExecEnvironment rule era
env) (forall t s. Inject t s => t -> s
inject ExecState rule era
st) (forall t s. Inject t s => t -> s
inject ExecSignal rule era
sig)
  Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecRep (ExecState 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 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 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 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) 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 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 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 (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Gen (ExecContext rule era)
genExecContext @rule @era) forall a. ToExpr a => a -> String
showExpr ExecContext 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 rule era
ctx String
"context"
  let
    forAllSpec :: Specification a -> ContT Property m a
forAllSpec Specification a
spec = do
      let
        simplifiedSpec :: Specification a
simplifiedSpec = forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
spec
        generator :: Gen (GE a)
generator = forall (m :: * -> *) a.
GenT m a -> GenMode -> [NonEmpty String] -> Gen (m a)
CV1.runGenT (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) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification 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 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 rule era
env <- forall {a} {m :: * -> *}.
(HasSpec a, Applicative m, Testable (m Property)) =>
Specification a -> ContT Property m a
forAllSpec 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
  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 <- forall {a} {m :: * -> *}.
(HasSpec a, Applicative m, Testable (m Property)) =>
Specification a -> ContT Property m a
forAllSpec 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
  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 <- forall {a} {m :: * -> *}.
(HasSpec a, Applicative m, Testable (m Property)) =>
Specification a -> ContT Property m a
forAllSpec 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
  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 -> 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 (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 =
  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 (rule :: Symbol) era.
  ExecSpecRule rule era =>
  Int ->
  Spec
inputsGenerateWithin :: forall (rule :: Symbol) era. ExecSpecRule 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 rule era)
genEnv = do
        ExecContext rule era
ctx <- forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Gen (ExecContext rule era)
genExecContext @rule @era
        forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
CV2.genFromSpec 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
        forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
CV2.genFromSpec 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
        forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
CV2.genFromSpec 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 forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
`generatesWithin` Int
timeout
    Gen (ExecState rule era)
genSt forall a.
(NFData a, ToExpr a, Typeable a, HasCallStack) =>
Gen a -> Int -> Spec
`generatesWithin` Int
timeout
    Gen (ExecSignal 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