{-# 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 Constrained.API (GE (..))
import qualified Constrained.API as CV2 (
  HasSpec,
  Specification,
  genFromSpec,
  genFromSpecT,
  looseGen,
  shrinkWithSpec,
 )
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

  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)
_ = 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
        generator :: Gen (GE a)
generator = GenT GE a -> Gen (GE a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
CV2.looseGen (Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
CV2.genFromSpecT Specification a
spec)
        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]
CV2.shrinkWithSpec Specification a
spec 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)

-- | 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) = 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