{-# 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 (..),
  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.Base (
  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)
  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 =>
    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) =>
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 (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
  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 (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
  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 ::
  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