{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Test.Cardano.Ledger.Conformance.Imp.Core where

import Cardano.Ledger.BaseTypes (Globals)
import Cardano.Ledger.Core (EraRule)
import Control.State.Transition
import Data.Bifunctor (Bifunctor (..))
import Data.Data (Proxy (..))
import Data.List.NonEmpty
import Data.Text qualified as T
import GHC.TypeLits (symbolVal)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  ExecSpecTopLevelRule (..),
  SpecTRC (..),
  diffConformance,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecNormalize (..),
  runSpecTransM,
 )
import Test.Cardano.Ledger.Conway.ImpTest
import Test.Cardano.Ledger.Imp.Common hiding (Args)
import UnliftIO (evaluateDeep)

conformanceHook ::
  forall rule era t.
  ( ExecSpecRule rule era
  , ToExpr (Event (EraRule rule era))
  ) =>
  Globals ->
  TRC (EraRule rule era) ->
  ExecContext rule era ->
  Either
    (NonEmpty (PredicateFailure (EraRule rule era)))
    (State (EraRule rule era), [Event (EraRule rule era)]) ->
  ImpM t ()
conformanceHook :: forall (rule :: Symbol) era t.
(ExecSpecRule rule era, ToExpr (Event (EraRule rule era))) =>
Globals
-> TRC (EraRule rule era)
-> ExecContext rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpM t ()
conformanceHook Globals
globals trc :: TRC (EraRule rule era)
trc@(TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
state, Signal (EraRule rule era)
signal)) ExecContext rule era
ctx Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
impRuleResult =
  String -> ImpM t () -> ImpM t ()
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn (String
"Conformance hook (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Proxy rule -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @rule) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")") (ImpM t () -> ImpM t ()) -> ImpM t () -> ImpM t ()
forall a b. (a -> b) -> a -> b
$ do
    -- translate inputs
    specTRC@(SpecTRC specEnv specState specSignal) <-
      String -> ImpM t (SpecTRC rule era) -> ImpM t (SpecTRC rule era)
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Translating inputs" (ImpM t (SpecTRC rule era) -> ImpM t (SpecTRC rule era))
-> (Either Text (SpecTRC rule era) -> ImpM t (SpecTRC rule era))
-> Either Text (SpecTRC rule era)
-> ImpM t (SpecTRC rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text (SpecTRC rule era) -> ImpM t (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 t (SpecTRC rule era))
-> Either Text (SpecTRC rule era) -> ImpM t (SpecTRC rule era)
forall a b. (a -> b) -> a -> b
$ ExecContext rule era
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
-> Either Text (SpecTRC rule era)
forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM ExecContext rule era
ctx (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
    -- get agda response
    agdaResponse' <-
      fmap (second $ first specNormalize) . evaluateDeep $ runAgdaRuleWithDebug @rule @era specTRC
    -- translate imp response
    let
      agdaResponse = ((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)
agdaResponse'
      agdaDebug = (Text -> Text)
-> ((SpecState rule era, Text) -> Text)
-> Either Text (SpecState rule era, Text)
-> Text
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Text -> Text -> Text
forall a b. a -> b -> a
const Text
"") (SpecState rule era, Text) -> Text
forall a b. (a, b) -> b
snd Either Text (SpecState rule era, Text)
agdaResponse'
      impRuleResult' = (NonEmpty (PredicateFailure (EraRule rule era)) -> Text)
-> ((State (EraRule rule era), [Event (EraRule rule era)])
    -> State (EraRule rule era))
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Either Text (State (EraRule rule era))
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (String -> Text
T.pack (String -> Text)
-> (NonEmpty (PredicateFailure (EraRule rule era)) -> String)
-> NonEmpty (PredicateFailure (EraRule rule era))
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (PredicateFailure (EraRule rule era)) -> String
forall a. Show a => a -> String
show) (State (EraRule rule era), [Event (EraRule rule era)])
-> State (EraRule rule era)
forall a b. (a, b) -> a
fst Either
  (NonEmpty (PredicateFailure (EraRule rule era)))
  (State (EraRule rule era), [Event (EraRule rule era)])
impRuleResult
      impResponse = (Text -> Text)
-> Either Text (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 (String -> Text
T.pack (String -> Text) -> (Text -> String) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
forall a. Show a => a -> String
show) (Either Text (SpecState rule era)
 -> Either Text (SpecState rule era))
-> (State (EraRule rule era) -> Either Text (SpecState rule era))
-> State (EraRule rule era)
-> Either Text (SpecState rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM @era ExecContext rule era
ctx (SpecTransM era (ExecContext rule era) (SpecState rule era)
 -> Either Text (SpecState rule era))
-> (State (EraRule rule era)
    -> SpecTransM era (ExecContext rule era) (SpecState rule era))
-> State (EraRule rule era)
-> Either Text (SpecState rule era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) -> Either Text (SpecState rule era))
-> Either Text (State (EraRule rule era))
-> Either Text (SpecState rule era)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Either Text (State (EraRule rule era))
impRuleResult'

    logString "implEnv"
    logToExpr env
    logString "implState"
    logToExpr state
    logString "implSignal"
    logToExpr signal
    logString "implStateOut"
    logToExpr impRuleResult
    logString "specEnv"
    logToExpr specEnv
    logString "specState"
    logToExpr specState
    logString "specSignal"
    logToExpr specSignal
    logString "specDebug"
    logToExpr agdaDebug
    logString "Extra info:"
    logDoc $
      extraInfo @rule @era
        globals
        ctx
        (TRC (env, state, signal))
        (first (T.pack . show) impRuleResult)
    logString "diffConformance:"
    logDoc $ diffConformance impResponse agdaResponse
    case (impResponse, agdaResponse) of
      (Right SpecState rule era
impRes, Right SpecState rule era
agdaRes)
        | SpecState rule era
impRes SpecState rule era -> SpecState rule era -> Bool
forall a. Eq a => a -> a -> Bool
== SpecState rule era
agdaRes -> () -> ImpM t ()
forall a. a -> ImpM t a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      (Left Text
_, Left Text
_) -> () -> ImpM t ()
forall a. a -> ImpM t a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      (Either Text (SpecState rule era),
 Either Text (SpecState rule era))
_ -> String -> ImpM t ()
forall (m :: * -> *) a. (HasCallStack, MonadIO m) => String -> m a
assertFailure String
"Conformance failure"

submitTxConformanceHook ::
  forall era t.
  (HasCallStack, ExecSpecTopLevelRule "LEDGER" era) =>
  Globals ->
  TRC (EraRule "LEDGER" era) ->
  Either
    (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
    (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
  ImpM t ()
submitTxConformanceHook :: forall era t.
(HasCallStack, ExecSpecTopLevelRule "LEDGER" era) =>
Globals
-> TRC (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ImpM t ()
submitTxConformanceHook Globals
globals TRC (EraRule "LEDGER" era)
trc =
  Globals
-> TRC (EraRule "LEDGER" era)
-> ExecContext "LEDGER" era
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)])
-> ImpM t ()
forall (rule :: Symbol) era t.
(ExecSpecRule rule era, ToExpr (Event (EraRule rule era))) =>
Globals
-> TRC (EraRule rule era)
-> ExecContext rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpM t ()
conformanceHook Globals
globals TRC (EraRule "LEDGER" era)
trc (Globals -> TRC (EraRule "LEDGER" era) -> ExecContext "LEDGER" era
forall (rule :: Symbol) era.
ExecSpecTopLevelRule rule era =>
Globals -> TRC (EraRule rule era) -> ExecContext rule era
mkRuleExecContext Globals
globals TRC (EraRule "LEDGER" era)
trc)

epochBoundaryConformanceHook ::
  forall era t.
  ( ExecSpecTopLevelRule "NEWEPOCH" era
  , ToExpr (Event (EraRule "NEWEPOCH" era))
  ) =>
  Globals ->
  TRC (EraRule "NEWEPOCH" era) ->
  State (EraRule "NEWEPOCH" era) ->
  ImpM t ()
epochBoundaryConformanceHook :: forall era t.
(ExecSpecTopLevelRule "NEWEPOCH" era,
 ToExpr (Event (EraRule "NEWEPOCH" era))) =>
Globals
-> TRC (EraRule "NEWEPOCH" era)
-> State (EraRule "NEWEPOCH" era)
-> ImpM t ()
epochBoundaryConformanceHook Globals
globals TRC (EraRule "NEWEPOCH" era)
trc State (EraRule "NEWEPOCH" era)
res =
  forall (rule :: Symbol) era t.
(ExecSpecRule rule era, ToExpr (Event (EraRule rule era))) =>
Globals
-> TRC (EraRule rule era)
-> ExecContext rule era
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
-> ImpM t ()
conformanceHook @"NEWEPOCH" @era Globals
globals TRC (EraRule "NEWEPOCH" era)
trc (Globals
-> TRC (EraRule "NEWEPOCH" era) -> ExecContext "NEWEPOCH" era
forall (rule :: Symbol) era.
ExecSpecTopLevelRule rule era =>
Globals -> TRC (EraRule rule era) -> ExecContext rule era
mkRuleExecContext Globals
globals TRC (EraRule "NEWEPOCH" era)
trc) (Either
   (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" era)))
   (State (EraRule "NEWEPOCH" era), [Event (EraRule "NEWEPOCH" era)])
 -> ImpM t ())
-> Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" era)))
     (State (EraRule "NEWEPOCH" era), [Event (EraRule "NEWEPOCH" era)])
-> ImpM t ()
forall a b. (a -> b) -> a -> b
$ (NewEpochState era, [Event (EraRule "NEWEPOCH" era)])
-> Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" era)))
     (NewEpochState era, [Event (EraRule "NEWEPOCH" era)])
forall a b. b -> Either a b
Right (NewEpochState era
State (EraRule "NEWEPOCH" era)
res, [])