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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  ExecSpecTopLevelRule (..),
  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.Core.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.Base (
  SpecNormalize (..),
  SpecTransM,
  SpecTranslate (..),
  runSpecTransM,
  unComputationResult,
  withCtxSpecTransM,
 )
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 era (Environment (EraRule rule era))

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

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

  runAgdaRule ::
    HasCallStack =>
    SpecTRC rule era ->
    Either Text (SpecState rule era)
  runAgdaRule = ((SpecState rule era, Text) -> SpecState rule era)
-> Either Text (SpecState rule era, Text)
-> Either Text (SpecState rule era)
forall a b. (a -> b) -> Either Text a -> Either Text b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SpecState rule era, Text) -> SpecState rule era
forall a b. (a, b) -> a
fst (Either Text (SpecState rule era, Text)
 -> Either Text (SpecState rule era))
-> (SpecTRC rule era -> Either Text (SpecState rule era, Text))
-> SpecTRC rule era
-> Either Text (SpecState rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecTRC rule era -> Either Text (SpecState rule era, Text)
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
SpecTRC rule era -> Either Text (SpecState rule era, Text)
runAgdaRuleWithDebug

  runAgdaRuleWithDebug ::
    HasCallStack =>
    SpecTRC rule era ->
    Either Text (SpecState rule era, Text)
  runAgdaRuleWithDebug = (SpecState rule era -> (SpecState rule era, Text))
-> Either Text (SpecState rule era)
-> Either Text (SpecState rule era, Text)
forall a b. (a -> b) -> Either Text a -> Either Text b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Text
"") (Either Text (SpecState rule era)
 -> Either Text (SpecState rule era, Text))
-> (SpecTRC rule era -> Either Text (SpecState rule era))
-> SpecTRC rule era
-> Either Text (SpecState rule era, Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecTRC rule era -> Either Text (SpecState rule era)
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
SpecTRC rule era -> Either Text (SpecState rule era)
runAgdaRule

  translateInputs ::
    HasCallStack =>
    TRC (EraRule rule era) ->
    SpecTransM era (ExecContext rule era) (SpecTRC rule era)
  default translateInputs ::
    ( SpecTranslate era (Environment (EraRule rule era))
    , SpecTranslate era (State (EraRule rule era))
    , SpecTranslate era (Signal (EraRule rule era))
    , SpecContext era (Environment (EraRule rule era)) ~ ExecContext rule era
    , SpecContext era (State (EraRule rule era)) ~ ExecContext rule era
    , SpecContext era (Signal (EraRule rule era)) ~ ExecContext rule era
    , SpecRep era (Environment (EraRule rule era)) ~ SpecEnvironment rule era
    , SpecRep era (State (EraRule rule era)) ~ SpecState rule era
    , SpecRep era (Signal (EraRule rule era)) ~ SpecSignal rule era
    ) =>
    TRC (EraRule rule era) ->
    SpecTransM era (ExecContext rule era) (SpecTRC rule era)
  translateInputs (TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
st, Signal (EraRule rule era)
sig)) = do
    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 era (ExecContext rule era) (SpecEnvironment rule era)
-> SpecTransM
     era
     (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
     era
     (SpecContext era (Environment (EraRule rule era)))
     (SpecRep era (Environment (EraRule rule era)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Environment (EraRule rule era)
env SpecTransM
  era
  (ExecContext rule era)
  (SpecState rule era -> SpecSignal rule era -> SpecTRC rule era)
-> SpecTransM era (ExecContext rule era) (SpecState rule era)
-> SpecTransM
     era
     (ExecContext rule era)
     (SpecSignal rule era -> SpecTRC rule era)
forall a b.
SpecTransM era (ExecContext rule era) (a -> b)
-> SpecTransM era (ExecContext rule era) a
-> SpecTransM era (ExecContext rule era) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State (EraRule rule era)
-> SpecTransM
     era
     (SpecContext era (State (EraRule rule era)))
     (SpecRep era (State (EraRule rule era)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep State (EraRule rule era)
st SpecTransM
  era
  (ExecContext rule era)
  (SpecSignal rule era -> SpecTRC rule era)
-> SpecTransM era (ExecContext rule era) (SpecSignal rule era)
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
forall a b.
SpecTransM era (ExecContext rule era) (a -> b)
-> SpecTransM era (ExecContext rule era) a
-> SpecTransM era (ExecContext rule era) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Signal (EraRule rule era)
-> SpecTransM
     era
     (SpecContext era (Signal (EraRule rule era)))
     (SpecRep era (Signal (EraRule rule era)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Signal (EraRule rule era)
sig

  translateOutput ::
    TRC (EraRule rule era) ->
    State (EraRule rule era) ->
    SpecTransM era (ExecContext rule era) (SpecState rule era)
  default translateOutput ::
    ( SpecTranslate era (State (EraRule rule era))
    , SpecContext era (State (EraRule rule era)) ~ ()
    , SpecRep era (State (EraRule rule era)) ~ SpecState rule era
    ) =>
    TRC (EraRule rule era) ->
    State (EraRule rule era) ->
    SpecTransM era (ExecContext rule era) (SpecState rule era)
  translateOutput TRC (EraRule rule era)
_ = ()
-> SpecTransM era () (SpecState rule era)
-> SpecTransM era (ExecContext rule era) (SpecState rule era)
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM () (SpecTransM era () (SpecState rule era)
 -> SpecTransM era (ExecContext rule era) (SpecState rule era))
-> (State (EraRule rule era)
    -> SpecTransM era () (SpecState rule era))
-> State (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecState rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (EraRule rule era) -> SpecTransM era () (SpecState rule era)
State (EraRule rule era)
-> SpecTransM
     era
     (SpecContext era (State (EraRule rule era)))
     (SpecRep era (State (EraRule rule era)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

  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

class ExecSpecRule rule era => ExecSpecTopLevelRule rule era where
  mkRuleExecContext :: Globals -> TRC (EraRule rule era) -> ExecContext rule era
  default mkRuleExecContext ::
    ExecContext rule era ~ () =>
    Globals -> TRC (EraRule rule era) -> ExecContext rule era
  mkRuleExecContext Globals
_ TRC (EraRule rule era)
_ = ()

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
  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"
  writeCBOR (eraProtVerLow @era) fullPath 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 :: String
envVarName = String
"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
            ]
      mbyCborDumpPath <- String -> ImpM (LedgerSpec era) (Maybe String)
forall (m :: * -> *). MonadIO m => String -> m (Maybe String)
lookupEnv String
envVarName
      case 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"
      expectationFailure . ansiDocToString $ 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 implResTest agdaResTest 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 <- use impGlobalsL
  logDoc $ extraInfo @rule @era globals ctx trc (first (T.pack . show) implRes)
  checkConformance @rule @_ ctx trc (first (T.pack . show) implResTest) 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 specEnv specSt specSig <-
    String
-> ImpM (LedgerSpec era) (SpecTRC rule era)
-> ImpM (LedgerSpec era) (SpecTRC rule era)
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"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 era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM @era ExecContext rule era
execContext (SpecTransM era (ExecContext rule era) (SpecTRC rule era)
 -> Either Text (SpecTRC rule era))
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
-> Either Text (SpecTRC rule era)
forall a b. (a -> b) -> a -> b
$
          TRC (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
TRC (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
translateInputs TRC (EraRule rule era)
trc
  logDoc $ "ctx:\n" <> ansiExpr execContext
  logDoc $ "implEnv:\n" <> ansiExpr env
  logDoc $ "implSt:\n" <> ansiExpr st
  logDoc $ "implSig:\n" <> ansiExpr sig
  logDoc $ "specEnv:\n" <> ansiExpr specEnv
  logDoc $ "specSt:\n" <> ansiExpr specSt
  logDoc $ "specSig:\n" <> ansiExpr specSig
  agdaResTest <-
    fmap (second specNormalize) $
      impAnn "Deep evaluating Agda output" $
        evaluateDeep $
          runAgdaRule @rule @era (SpecTRC specEnv specSt specSig)
  implRes <- tryRunImpRule @rule @era env st sig
  implResTest <-
    impAnn "Translating implementation values to SpecRep" $
      case 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 era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM @era ExecContext rule era
execContext (SpecTransM era (ExecContext rule era) (SpecState rule era)
 -> Either Text (SpecState rule era))
-> SpecTransM era (ExecContext rule era) (SpecState rule era)
-> Either Text (SpecState rule era)
forall a b. (a -> b) -> a -> b
$
              TRC (EraRule rule era)
-> State (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecState rule era)
forall (rule :: Symbol) era.
ExecSpecRule rule era =>
TRC (EraRule rule era)
-> State (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecState rule era)
translateOutput 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
  pure $ ConformanceResult implResTest agdaResTest 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 =
  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)

-- | Translate a Haskell type 'a' whose translation context is 'ctx' into its Agda type, in the ImpTest monad.
translateWithContext ::
  forall era a.
  SpecTranslate era a => SpecContext era a -> a -> ImpTestM era (Either Text (SpecRep era a))
translateWithContext :: forall era a.
SpecTranslate era a =>
SpecContext era a
-> a -> ImpTestM era (Either Text (SpecRep era a))
translateWithContext SpecContext era a
ctx a
x = Either Text (SpecRep era a)
-> ImpM (LedgerSpec era) (Either Text (SpecRep era a))
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text (SpecRep era a)
 -> ImpM (LedgerSpec era) (Either Text (SpecRep era a)))
-> (SpecTransM era (SpecContext era a) (SpecRep era a)
    -> Either Text (SpecRep era a))
-> SpecTransM era (SpecContext era a) (SpecRep era a)
-> ImpM (LedgerSpec era) (Either Text (SpecRep era a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecContext era a
-> SpecTransM era (SpecContext era a) (SpecRep era a)
-> Either Text (SpecRep era a)
forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM SpecContext era a
ctx (SpecTransM era (SpecContext era a) (SpecRep era a)
 -> ImpM (LedgerSpec era) (Either Text (SpecRep era a)))
-> SpecTransM era (SpecContext era a) (SpecRep era a)
-> ImpM (LedgerSpec era) (Either Text (SpecRep era a))
forall a b. (a -> b) -> a -> b
$ forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep @era 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