{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  ConformanceResult (..),
  SpecTRC (..),
  generatesWithin,
  runConformance,
  checkConformance,
  testConformance,
  translateWithContext,
  ForAllExecSpecRep,
  ForAllExecTypes,
  diffConformance,
  runFromAgdaFunction,
) where

import Cardano.Ledger.BaseTypes (Globals, ShelleyBase)
import Cardano.Ledger.Binary (EncCBOR)
import Cardano.Ledger.Core (Era, EraRule, eraProtVerLow)
import Control.State.Transition.Extended (STS (..), TRC (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Functor (($>))
import Data.List.NonEmpty (NonEmpty)
import Data.String (fromString)
import Data.Text (Text)
import qualified Data.Text as T
import Data.TreeDiff.Pretty (ansiWlExpr)
import Data.Typeable (Proxy (..), Typeable, typeRep)
import GHC.Base (Constraint, Symbol, Type)
import GHC.Generics (Generic)
import GHC.TypeLits (KnownSymbol)
import Lens.Micro.Mtl (use)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
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 (
  SpecNormalize (..),
  SpecTranslate (..),
  runSpecTransM,
  unComputationResult,
 )
import Test.Cardano.Ledger.Imp.Common
import Test.Cardano.Ledger.Shelley.ImpTest (
  ImpTestM,
  ShelleyEraImp,
  impAnn,
  impGlobalsL,
  logDoc,
  tryRunImpRule,
 )
import UnliftIO (evaluateDeep)
import UnliftIO.Directory (makeAbsolute)
import UnliftIO.Environment (lookupEnv)

type ForAllExecTypes (c :: Type -> Constraint) rule era =
  ( c (Environment (EraRule rule era))
  , c (State (EraRule rule era))
  , c (Signal (EraRule rule era))
  )

type ForAllExecSpecRep (c :: Type -> Constraint) rule era =
  ( c (SpecEnvironment rule era)
  , c (SpecState rule era)
  , c (SpecSignal rule era)
  )

data SpecTRC rule era = SpecTRC
  { forall (rule :: Symbol) era.
SpecTRC rule era -> SpecEnvironment rule era
strcEnvironment :: SpecEnvironment rule era
  , forall (rule :: Symbol) era. SpecTRC rule era -> SpecState rule era
strcState :: SpecState rule era
  , forall (rule :: Symbol) era.
SpecTRC rule era -> SpecSignal rule era
strcSignal :: SpecSignal rule era
  }
  deriving ((forall x. SpecTRC rule era -> Rep (SpecTRC rule era) x)
-> (forall x. Rep (SpecTRC rule era) x -> SpecTRC rule era)
-> Generic (SpecTRC rule era)
forall x. Rep (SpecTRC rule era) x -> SpecTRC rule era
forall x. SpecTRC rule era -> Rep (SpecTRC rule era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (rule :: Symbol) era x.
Rep (SpecTRC rule era) x -> SpecTRC rule era
forall (rule :: Symbol) era x.
SpecTRC rule era -> Rep (SpecTRC rule era) x
$cfrom :: forall (rule :: Symbol) era x.
SpecTRC rule era -> Rep (SpecTRC rule era) x
from :: forall x. SpecTRC rule era -> Rep (SpecTRC rule era) x
$cto :: forall (rule :: Symbol) era x.
Rep (SpecTRC rule era) x -> SpecTRC rule era
to :: forall x. Rep (SpecTRC rule era) x -> SpecTRC rule era
Generic)

deriving instance ForAllExecSpecRep Eq rule era => Eq (SpecTRC rule era)

instance ForAllExecSpecRep NFData rule era => NFData (SpecTRC rule era)

instance ForAllExecSpecRep ToExpr rule era => ToExpr (SpecTRC rule era)

class
  ( ShelleyEraImp era
  , STS (EraRule rule era)
  , BaseM (EraRule rule era) ~ ShelleyBase
  , KnownSymbol rule
  , ForAllExecSpecRep NFData rule era
  , ForAllExecSpecRep ToExpr rule era
  , ForAllExecTypes NFData rule era
  , ForAllExecTypes ToExpr rule era
  , ForAllExecTypes EncCBOR rule era
  , EncCBOR (ExecContext rule era)
  , Eq (SpecState rule era)
  , SpecNormalize (SpecState rule era)
  , NFData (ExecContext rule era)
  , NFData (PredicateFailure (EraRule rule era))
  , NFData (SpecTRC rule era)
  , ToExpr (ExecContext rule era)
  , ToExpr (PredicateFailure (EraRule rule era))
  ) =>
  ExecSpecRule (rule :: Symbol) era
  where
  type ExecContext rule era
  type ExecContext rule era = ()

  type SpecEnvironment rule era
  type SpecEnvironment rule era = SpecRep (Environment (EraRule rule era))

  type SpecState rule era
  type SpecState rule era = SpecRep (State (EraRule rule era))

  type SpecSignal rule era
  type SpecSignal rule era = SpecRep (Signal (EraRule rule era))

  runAgdaRule ::
    HasCallStack =>
    SpecTRC rule era ->
    Either Text (SpecState rule era)

  translateInputs ::
    HasCallStack =>
    ExecContext rule era ->
    TRC (EraRule rule era) ->
    Either Text (SpecTRC rule era)
  default translateInputs ::
    ( SpecTranslate (ExecContext rule era) (Environment (EraRule rule era))
    , SpecTranslate (ExecContext rule era) (State (EraRule rule era))
    , SpecTranslate (ExecContext rule era) (Signal (EraRule rule era))
    , SpecRep (Environment (EraRule rule era)) ~ SpecEnvironment rule era
    , SpecRep (State (EraRule rule era)) ~ SpecState rule era
    , SpecRep (Signal (EraRule rule era)) ~ SpecSignal rule era
    ) =>
    ExecContext rule era ->
    TRC (EraRule rule era) ->
    Either Text (SpecTRC rule era)
  translateInputs ExecContext rule era
ctx (TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
st, Signal (EraRule rule era)
sig)) = do
    ExecContext rule era
-> SpecTransM (ExecContext rule era) (SpecTRC rule era)
-> Either Text (SpecTRC rule era)
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext rule era
ctx (SpecTransM (ExecContext rule era) (SpecTRC rule era)
 -> Either Text (SpecTRC rule era))
-> SpecTransM (ExecContext rule era) (SpecTRC rule era)
-> Either Text (SpecTRC rule era)
forall a b. (a -> b) -> a -> b
$
      SpecEnvironment rule era
-> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era
forall (rule :: Symbol) era.
SpecEnvironment rule era
-> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era
SpecTRC (SpecEnvironment rule era
 -> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era)
-> SpecTransM (ExecContext rule era) (SpecEnvironment rule era)
-> SpecTransM
     (ExecContext rule era)
     (SpecState rule era -> SpecSignal rule era -> SpecTRC rule era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Environment (EraRule rule era)
-> SpecTransM
     (ExecContext rule era) (SpecRep (Environment (EraRule rule era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Environment (EraRule rule era)
env SpecTransM
  (ExecContext rule era)
  (SpecState rule era -> SpecSignal rule era -> SpecTRC rule era)
-> SpecTransM (ExecContext rule era) (SpecState rule era)
-> SpecTransM
     (ExecContext rule era) (SpecSignal rule era -> SpecTRC rule era)
forall a b.
SpecTransM (ExecContext rule era) (a -> b)
-> SpecTransM (ExecContext rule era) a
-> SpecTransM (ExecContext rule era) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State (EraRule rule era)
-> SpecTransM
     (ExecContext rule era) (SpecRep (State (EraRule rule era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep State (EraRule rule era)
st SpecTransM
  (ExecContext rule era) (SpecSignal rule era -> SpecTRC rule era)
-> SpecTransM (ExecContext rule era) (SpecSignal rule era)
-> SpecTransM (ExecContext rule era) (SpecTRC rule era)
forall a b.
SpecTransM (ExecContext rule era) (a -> b)
-> SpecTransM (ExecContext rule era) a
-> SpecTransM (ExecContext rule era) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Signal (EraRule rule era)
-> SpecTransM
     (ExecContext rule era) (SpecRep (Signal (EraRule rule era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Signal (EraRule rule era)
sig

  translateOutput ::
    ExecContext rule era ->
    TRC (EraRule rule era) ->
    State (EraRule rule era) ->
    Either Text (SpecState rule era)
  default translateOutput ::
    ( SpecTranslate (ExecContext rule era) (State (EraRule rule era))
    , SpecRep (State (EraRule rule era)) ~ SpecState rule era
    ) =>
    ExecContext rule era ->
    TRC (EraRule rule era) ->
    State (EraRule rule era) ->
    Either Text (SpecState rule era)
  translateOutput ExecContext rule era
ctx TRC (EraRule rule era)
_ State (EraRule rule era)
st = ExecContext rule era
-> SpecTransM (ExecContext rule era) (SpecState rule era)
-> Either Text (SpecState rule era)
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext rule era
ctx (SpecTransM (ExecContext rule era) (SpecState rule era)
 -> Either Text (SpecState rule era))
-> SpecTransM (ExecContext rule era) (SpecState rule era)
-> Either Text (SpecState rule era)
forall a b. (a -> b) -> a -> b
$ State (EraRule rule era)
-> SpecTransM
     (ExecContext rule era) (SpecRep (State (EraRule rule era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep State (EraRule rule era)
st

  extraInfo ::
    HasCallStack =>
    Globals ->
    ExecContext rule era ->
    TRC (EraRule rule era) ->
    Either Text (State (EraRule rule era), [Event (EraRule rule era)]) ->
    Doc AnsiStyle
  extraInfo Globals
_ ExecContext rule era
_ TRC (EraRule rule era)
_ Either Text (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) =>
FilePath -> a -> FilePath -> ImpTestM era ()
dumpCbor FilePath
path a
x FilePath
name = do
  FilePath
fullPath <- FilePath -> ImpM (LedgerSpec era) FilePath
forall (m :: * -> *). MonadIO m => FilePath -> m FilePath
makeAbsolute (FilePath -> ImpM (LedgerSpec era) FilePath)
-> FilePath -> ImpM (LedgerSpec era) FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
path FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"/" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
name FilePath -> FilePath -> FilePath
<.> FilePath
"cbor"
  Version -> FilePath -> a -> ImpTestM era ()
forall a (m :: * -> *).
(EncCBOR a, MonadIO m) =>
Version -> FilePath -> a -> m ()
writeCBOR (forall era. Era era => Version
eraProtVerLow @era) FilePath
fullPath a
x

diffConformance :: ToExpr a => Either Text a -> Either Text a -> Doc AnsiStyle
diffConformance :: forall a.
ToExpr a =>
Either Text a -> Either Text a -> Doc AnsiStyle
diffConformance (Right a
implRes) (Right 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: " <>)
        }
diffConformance Either Text a
implRes Either Text a
agdaRes =
  let
    prettyRes :: Bool -> a -> Doc AnsiStyle
prettyRes Bool
True a
x = Doc AnsiStyle
"Success):\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
White) (Expr -> Doc AnsiStyle
ansiWlExpr (Expr -> Doc AnsiStyle) -> Expr -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ a -> Expr
forall a. ToExpr a => a -> Expr
toExpr a
x)
    prettyRes Bool
False a
x = Doc AnsiStyle
"Failure):\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Red) (Expr -> Doc AnsiStyle
ansiWlExpr (Expr -> Doc AnsiStyle) -> Expr -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ a -> Expr
forall a. ToExpr a => a -> Expr
toExpr a
x)
   in
    [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
vsep
      [ Doc AnsiStyle
"Impl ("
          Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
nest
            Int
2
            ( case Either Text a
implRes of
                Right a
x -> Bool -> a -> Doc AnsiStyle
forall {a}. ToExpr a => Bool -> a -> Doc AnsiStyle
prettyRes Bool
True a
x
                Left Text
x -> Bool -> Text -> Doc AnsiStyle
forall {a}. ToExpr a => Bool -> a -> Doc AnsiStyle
prettyRes Bool
False Text
x
            )
      , Doc AnsiStyle
"Agda ("
          Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
nest
            Int
2
            ( case Either Text a
agdaRes of
                Right a
x -> Bool -> a -> Doc AnsiStyle
forall {a}. ToExpr a => Bool -> a -> Doc AnsiStyle
prettyRes Bool
True a
x
                Left Text
x -> Doc AnsiStyle
"Failure):\n" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Red) (Text -> Doc AnsiStyle
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
x)
            )
      ]

checkConformance ::
  forall rule era.
  ( HasCallStack
  , Era era
  , EncCBOR (ExecContext rule era)
  , EncCBOR (Environment (EraRule rule era))
  , EncCBOR (State (EraRule rule era))
  , EncCBOR (Signal (EraRule rule era))
  , ToExpr (SpecState rule era)
  , Eq (SpecState rule era)
  , SpecNormalize (SpecState rule era)
  ) =>
  ExecContext rule era ->
  TRC (EraRule rule era) ->
  Either Text (SpecState rule era) ->
  Either Text (SpecState rule era) ->
  ImpTestM era ()
checkConformance :: forall (rule :: Symbol) era.
(HasCallStack, Era era, EncCBOR (ExecContext rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), ToExpr (SpecState rule era),
 Eq (SpecState rule era), SpecNormalize (SpecState rule era)) =>
ExecContext rule era
-> TRC (EraRule rule era)
-> Either Text (SpecState rule era)
-> Either Text (SpecState rule era)
-> ImpTestM era ()
checkConformance ExecContext rule era
ctx (TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
st, Signal (EraRule rule era)
sig)) Either Text (SpecState rule era)
implResTest Either Text (SpecState rule era)
agdaResTest = do
  let
    implResNorm :: Either Text (SpecState rule era)
implResNorm = SpecState rule era -> SpecState rule era
forall a. SpecNormalize a => a -> a
specNormalize (SpecState rule era -> SpecState rule era)
-> Either Text (SpecState rule era)
-> Either Text (SpecState rule era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Text (SpecState rule era)
implResTest
    agdaResNorm :: Either Text (SpecState rule era)
agdaResNorm = SpecState rule era -> SpecState rule era
forall a. SpecNormalize a => a -> a
specNormalize (SpecState rule era -> SpecState rule era)
-> Either Text (SpecState rule era)
-> Either Text (SpecState rule era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Text (SpecState rule era)
agdaResTest
  case (Either Text (SpecState rule era)
implResNorm, Either Text (SpecState rule era)
agdaResNorm) of
    (Right SpecState rule era
agda, Right SpecState rule era
impl)
      | SpecState rule era
agda SpecState rule era -> SpecState rule era -> Bool
forall a. Eq a => a -> a -> Bool
== SpecState rule era
impl -> () -> ImpTestM era ()
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    (Left Text
_, Left Text
_) -> () -> ImpTestM era ()
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    (Either Text (SpecState rule era)
agda, Either Text (SpecState rule era)
impl) -> do
      let
        envVarName :: FilePath
envVarName = FilePath
"CONFORMANCE_CBOR_DUMP_PATH"
        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 Text (SpecState rule era)
-> Either Text (SpecState rule era) -> Doc AnsiStyle
forall a.
ToExpr a =>
Either Text a -> Either Text a -> Doc AnsiStyle
diffConformance Either Text (SpecState rule era)
agda Either Text (SpecState rule era)
impl
            ]
      Maybe FilePath
mbyCborDumpPath <- FilePath -> ImpM (LedgerSpec era) (Maybe FilePath)
forall (m :: * -> *). MonadIO m => FilePath -> m (Maybe FilePath)
lookupEnv FilePath
envVarName
      case Maybe FilePath
mbyCborDumpPath of
        Just FilePath
path -> do
          FilePath -> ExecContext rule era -> FilePath -> ImpTestM era ()
forall era a.
(EncCBOR a, Era era) =>
FilePath -> a -> FilePath -> ImpTestM era ()
dumpCbor FilePath
path ExecContext rule era
ctx FilePath
"conformance_dump_ctx"
          FilePath
-> Environment (EraRule rule era) -> FilePath -> ImpTestM era ()
forall era a.
(EncCBOR a, Era era) =>
FilePath -> a -> FilePath -> ImpTestM era ()
dumpCbor FilePath
path Environment (EraRule rule era)
env FilePath
"conformance_dump_env"
          FilePath -> State (EraRule rule era) -> FilePath -> ImpTestM era ()
forall era a.
(EncCBOR a, Era era) =>
FilePath -> a -> FilePath -> ImpTestM era ()
dumpCbor FilePath
path State (EraRule rule era)
st FilePath
"conformance_dump_st"
          FilePath
-> Signal (EraRule rule era) -> FilePath -> ImpTestM era ()
forall era a.
(EncCBOR a, Era era) =>
FilePath -> a -> FilePath -> ImpTestM era ()
dumpCbor FilePath
path Signal (EraRule rule era)
sig FilePath
"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
<> FilePath -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr FilePath
path
        Maybe FilePath
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
<> FilePath -> Doc AnsiStyle
forall a. IsString a => FilePath -> a
fromString FilePath
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"
      FilePath -> ImpTestM era ()
forall (m :: * -> *). (HasCallStack, MonadIO m) => FilePath -> m ()
expectationFailure (FilePath -> ImpTestM era ())
-> (Doc AnsiStyle -> FilePath) -> Doc AnsiStyle -> ImpTestM era ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc AnsiStyle -> FilePath
ansiDocToString (Doc AnsiStyle -> ImpTestM era ())
-> Doc AnsiStyle -> ImpTestM era ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
failMsg

testConformance ::
  forall rule era.
  ( HasCallStack
  , ExecSpecRule rule era
  ) =>
  ExecContext rule era ->
  TRC (EraRule rule era) ->
  Property
testConformance :: forall (rule :: Symbol) era.
(HasCallStack, ExecSpecRule rule era) =>
ExecContext rule era -> TRC (EraRule rule era) -> Property
testConformance ExecContext rule era
ctx TRC (EraRule rule era)
trc = 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
  ConformanceResult Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecState rule era)
implResTest Either Text (SpecState 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 =>
ExecContext rule era
-> TRC (EraRule rule era)
-> ImpTestM era (ConformanceResult rule era)
runConformance @rule @era ExecContext rule era
ctx TRC (EraRule rule era)
trc
  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
  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
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Globals
-> ExecContext rule era
-> TRC (EraRule rule era)
-> Either
     Text (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @rule @era Globals
globals ExecContext rule era
ctx TRC (EraRule rule era)
trc ((NonEmpty (PredicateFailure (EraRule rule era)) -> Text)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Either
     Text (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 (FilePath -> Text
T.pack (FilePath -> Text)
-> (NonEmpty (PredicateFailure (EraRule rule era)) -> FilePath)
-> NonEmpty (PredicateFailure (EraRule rule era))
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (PredicateFailure (EraRule rule era)) -> FilePath
forall a. Show a => a -> FilePath
show) Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
implRes)
  forall (rule :: Symbol) era.
(HasCallStack, Era era, EncCBOR (ExecContext rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), ToExpr (SpecState rule era),
 Eq (SpecState rule era), SpecNormalize (SpecState rule era)) =>
ExecContext rule era
-> TRC (EraRule rule era)
-> Either Text (SpecState rule era)
-> Either Text (SpecState rule era)
-> ImpTestM era ()
checkConformance @rule @_ ExecContext rule era
ctx TRC (EraRule rule era)
trc ((NonEmpty (PredicateFailure (EraRule rule era)) -> Text)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (SpecState rule era)
-> Either Text (SpecState 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 (FilePath -> Text
T.pack (FilePath -> Text)
-> (NonEmpty (PredicateFailure (EraRule rule era)) -> FilePath)
-> NonEmpty (PredicateFailure (EraRule rule era))
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (PredicateFailure (EraRule rule era)) -> FilePath
forall a. Show a => a -> FilePath
show) Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecState rule era)
implResTest) Either Text (SpecState rule era)
agdaResTest

data ConformanceResult rule era = ConformanceResult
  { forall (rule :: Symbol) era.
ConformanceResult rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (SpecState rule era)
crTranslationResult ::
      Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era)
  , forall (rule :: Symbol) era.
ConformanceResult rule era -> Either Text (SpecState rule era)
crSpecificationResult ::
      Either
        Text
        (SpecState rule era)
  , forall (rule :: Symbol) era.
ConformanceResult rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
crImplementationResult ::
      Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (State (EraRule rule era), [Event (EraRule rule era)])
  }
  deriving ((forall x.
 ConformanceResult rule era -> Rep (ConformanceResult rule era) x)
-> (forall x.
    Rep (ConformanceResult rule era) x -> ConformanceResult rule era)
-> Generic (ConformanceResult rule era)
forall x.
Rep (ConformanceResult rule era) x -> ConformanceResult rule era
forall x.
ConformanceResult rule era -> Rep (ConformanceResult rule era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (rule :: Symbol) era x.
Rep (ConformanceResult rule era) x -> ConformanceResult rule era
forall (rule :: Symbol) era x.
ConformanceResult rule era -> Rep (ConformanceResult rule era) x
$cfrom :: forall (rule :: Symbol) era x.
ConformanceResult rule era -> Rep (ConformanceResult rule era) x
from :: forall x.
ConformanceResult rule era -> Rep (ConformanceResult rule era) x
$cto :: forall (rule :: Symbol) era x.
Rep (ConformanceResult rule era) x -> ConformanceResult rule era
to :: forall x.
Rep (ConformanceResult rule era) x -> ConformanceResult rule era
Generic)

deriving instance
  ( Show (SpecState rule era)
  , Show (PredicateFailure (EraRule rule era))
  , Show (State (EraRule rule era))
  , Show (Event (EraRule rule era))
  ) =>
  Show (ConformanceResult rule era)

instance
  ( ToExpr (SpecState rule era)
  , ToExpr (PredicateFailure (EraRule rule era))
  , ToExpr (State (EraRule rule era))
  , ToExpr (Event (EraRule rule era))
  ) =>
  ToExpr (ConformanceResult rule era)

runConformance ::
  forall (rule :: Symbol) era.
  ExecSpecRule rule era =>
  ExecContext rule era ->
  TRC (EraRule rule era) ->
  ImpTestM era (ConformanceResult rule era)
runConformance :: forall (rule :: Symbol) era.
ExecSpecRule rule era =>
ExecContext rule era
-> TRC (EraRule rule era)
-> ImpTestM era (ConformanceResult rule era)
runConformance ExecContext rule era
execContext trc :: TRC (EraRule rule era)
trc@(TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
st, Signal (EraRule rule era)
sig)) = do
  SpecTRC SpecEnvironment rule era
specEnv SpecState rule era
specSt SpecSignal rule era
specSig <-
    FilePath
-> ImpM (LedgerSpec era) (SpecTRC rule era)
-> ImpM (LedgerSpec era) (SpecTRC rule era)
forall a t. NFData a => FilePath -> ImpM t a -> ImpM t a
impAnn FilePath
"Translating the inputs" (ImpM (LedgerSpec era) (SpecTRC rule era)
 -> ImpM (LedgerSpec era) (SpecTRC rule era))
-> ImpM (LedgerSpec era) (SpecTRC rule era)
-> ImpM (LedgerSpec era) (SpecTRC rule era)
forall a b. (a -> b) -> a -> b
$
      Either Text (SpecTRC rule era)
-> ImpM (LedgerSpec era) (SpecTRC rule era)
forall a b (m :: * -> *).
(HasCallStack, ToExpr a, NFData b, MonadIO m) =>
Either a b -> m b
expectRightDeepExpr (Either Text (SpecTRC rule era)
 -> ImpM (LedgerSpec era) (SpecTRC rule era))
-> Either Text (SpecTRC rule era)
-> ImpM (LedgerSpec era) (SpecTRC rule era)
forall a b. (a -> b) -> a -> b
$
        forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> TRC (EraRule rule era) -> Either Text (SpecTRC rule era)
translateInputs @rule @era ExecContext rule era
execContext TRC (EraRule rule era)
trc
  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
<> Environment (EraRule rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr Environment (EraRule 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
<> State (EraRule rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr State (EraRule 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
<> Signal (EraRule rule era) -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr Signal (EraRule 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
<> SpecEnvironment rule era -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecEnvironment 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
<> SpecState rule era -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecState 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
<> SpecSignal rule era -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr SpecSignal rule era
specSig
  Either Text (SpecState rule era)
agdaResTest <-
    (Either Text (SpecState rule era)
 -> Either Text (SpecState rule era))
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
-> ImpM (LedgerSpec era) (Either Text (SpecState 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 ((SpecState rule era -> SpecState rule era)
-> Either Text (SpecState rule era)
-> Either Text (SpecState 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 SpecState rule era -> SpecState rule era
forall a. SpecNormalize a => a -> a
specNormalize) (ImpM (LedgerSpec era) (Either Text (SpecState rule era))
 -> ImpM (LedgerSpec era) (Either Text (SpecState rule era)))
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
forall a b. (a -> b) -> a -> b
$
      FilePath
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
forall a t. NFData a => FilePath -> ImpM t a -> ImpM t a
impAnn FilePath
"Deep evaluating Agda output" (ImpM (LedgerSpec era) (Either Text (SpecState rule era))
 -> ImpM (LedgerSpec era) (Either Text (SpecState rule era)))
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
forall a b. (a -> b) -> a -> b
$
        Either Text (SpecState rule era)
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep (Either Text (SpecState rule era)
 -> ImpM (LedgerSpec era) (Either Text (SpecState rule era)))
-> Either Text (SpecState rule era)
-> ImpM (LedgerSpec era) (Either Text (SpecState rule era))
forall a b. (a -> b) -> a -> b
$
          forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
SpecTRC rule era -> Either Text (SpecState rule era)
runAgdaRule @rule @era (SpecEnvironment rule era
-> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era
forall (rule :: Symbol) era.
SpecEnvironment rule era
-> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era
SpecTRC SpecEnvironment rule era
specEnv SpecState rule era
specSt SpecSignal 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 Environment (EraRule rule era)
env State (EraRule rule era)
st Signal (EraRule rule era)
sig
  Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecState rule era)
implResTest <-
    FilePath
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era))
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era))
forall a t. NFData a => FilePath -> ImpM t a -> ImpM t a
impAnn FilePath
"Translating implementation values to SpecRep" (ImpM
   (LedgerSpec era)
   (Either
      (NonEmpty (PredicateFailure (EraRule rule era)))
      (SpecState rule era))
 -> ImpM
      (LedgerSpec era)
      (Either
         (NonEmpty (PredicateFailure (EraRule rule era)))
         (SpecState rule era)))
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era))
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era))
forall a b. (a -> b) -> a -> b
$
      case Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
implRes of
        Right (State (EraRule rule era)
st', [Event (EraRule rule era)]
_) ->
          (SpecState rule era
 -> Either
      (NonEmpty (PredicateFailure (EraRule rule era)))
      (SpecState rule era))
-> ImpM (LedgerSpec era) (SpecState rule era)
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState 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 (SpecState rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (SpecState rule era)
forall a b. b -> Either a b
Right (SpecState rule era
 -> Either
      (NonEmpty (PredicateFailure (EraRule rule era)))
      (SpecState rule era))
-> (SpecState rule era -> SpecState rule era)
-> SpecState rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (SpecState rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecState rule era -> SpecState rule era
forall a. SpecNormalize a => a -> a
specNormalize) (ImpM (LedgerSpec era) (SpecState rule era)
 -> ImpM
      (LedgerSpec era)
      (Either
         (NonEmpty (PredicateFailure (EraRule rule era)))
         (SpecState rule era)))
-> (Either Text (SpecState rule era)
    -> ImpM (LedgerSpec era) (SpecState rule era))
-> Either Text (SpecState rule era)
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text (SpecState rule era)
-> ImpM (LedgerSpec era) (SpecState rule era)
forall a (m :: * -> *) b.
(HasCallStack, ToExpr a, MonadIO m) =>
Either a b -> m b
expectRightExpr (Either Text (SpecState rule era)
 -> ImpM
      (LedgerSpec era)
      (Either
         (NonEmpty (PredicateFailure (EraRule rule era)))
         (SpecState rule era)))
-> Either Text (SpecState rule era)
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era))
forall a b. (a -> b) -> a -> b
$
            forall (rule :: Symbol) era.
ExecSpecRule rule era =>
ExecContext rule era
-> TRC (EraRule rule era)
-> State (EraRule rule era)
-> Either Text (SpecState rule era)
translateOutput @rule @era ExecContext rule era
execContext TRC (EraRule rule era)
trc State (EraRule rule era)
st'
        Left NonEmpty (PredicateFailure (EraRule rule era))
err -> Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecState rule era)
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era))
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either
   (NonEmpty (PredicateFailure (EraRule rule era)))
   (SpecState rule era)
 -> ImpM
      (LedgerSpec era)
      (Either
         (NonEmpty (PredicateFailure (EraRule rule era)))
         (SpecState rule era)))
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (SpecState rule era)
-> ImpM
     (LedgerSpec era)
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecState rule era))
forall a b. (a -> b) -> a -> b
$ NonEmpty (PredicateFailure (EraRule rule era))
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (SpecState rule era)
forall a b. a -> Either a b
Left NonEmpty (PredicateFailure (EraRule rule era))
err
  ConformanceResult rule era
-> ImpTestM era (ConformanceResult rule era)
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConformanceResult rule era
 -> ImpTestM era (ConformanceResult rule era))
-> ConformanceResult rule era
-> ImpTestM era (ConformanceResult rule era)
forall a b. (a -> b) -> a -> b
$ Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecState rule era)
-> Either Text (SpecState rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ConformanceResult rule era
forall (rule :: Symbol) era.
Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecState rule era)
-> Either Text (SpecState rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ConformanceResult rule era
ConformanceResult Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (SpecState rule era)
implResTest Either Text (SpecState rule era)
agdaResTest Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
implRes

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 =
  FilePath -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
FilePath -> prop -> Spec
prop (FilePath
aName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" generates within " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show Int
timeout FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"μs")
    (Property -> Spec)
-> ((a -> Property) -> Property) -> (a -> Property) -> Spec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen a -> (a -> FilePath) -> (a -> Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> FilePath) -> (a -> prop) -> Property
forAllShow Gen a
gen a -> FilePath
forall a. ToExpr a => a -> FilePath
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 :: FilePath
aName = TypeRep -> FilePath
forall a. Show a => a -> FilePath
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)

-- | 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 (Either Text (SpecRep a))
translateWithContext :: forall ctx a era.
SpecTranslate ctx a =>
ctx -> a -> ImpTestM era (Either Text (SpecRep a))
translateWithContext ctx
ctx a
x = Either Text (SpecRep a)
-> ImpM (LedgerSpec era) (Either Text (SpecRep a))
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text (SpecRep a)
 -> ImpM (LedgerSpec era) (Either Text (SpecRep a)))
-> (SpecTransM ctx (SpecRep a) -> Either Text (SpecRep a))
-> SpecTransM ctx (SpecRep a)
-> ImpM (LedgerSpec era) (Either Text (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)
 -> ImpM (LedgerSpec era) (Either Text (SpecRep a)))
-> SpecTransM ctx (SpecRep a)
-> ImpM (LedgerSpec era) (Either Text (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

runFromAgdaFunction ::
  ( SpecEnvironment rule era ->
    SpecState rule era ->
    SpecSignal rule era ->
    Agda.ComputationResult Text (SpecState rule era)
  ) ->
  SpecTRC rule era ->
  Either Text (SpecState rule era)
runFromAgdaFunction :: forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction SpecEnvironment rule era
-> SpecState rule era
-> SpecSignal rule era
-> ComputationResult Text (SpecState rule era)
f (SpecTRC SpecEnvironment rule era
env SpecState rule era
st SpecSignal rule era
sig) = ComputationResult Text (SpecState rule era)
-> Either Text (SpecState rule era)
forall a. ComputationResult Text a -> Either Text a
unComputationResult (ComputationResult Text (SpecState rule era)
 -> Either Text (SpecState rule era))
-> ComputationResult Text (SpecState rule era)
-> Either Text (SpecState rule era)
forall a b. (a -> b) -> a -> b
$ SpecEnvironment rule era
-> SpecState rule era
-> SpecSignal rule era
-> ComputationResult Text (SpecState rule era)
f SpecEnvironment rule era
env SpecState rule era
st SpecSignal rule era
sig