{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}

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

import Cardano.Ledger.Core (EraRule)
import Constrained.API
import Control.Monad.Cont (ContT (..))
import Control.Monad.Trans (MonadTrans (..))
import Control.State.Transition.Extended (STS (..), TRC (..))
import Test.Cardano.Ledger.Conformance (ExecSpecRule (..), ForAllExecTypes, testConformance)
import Test.Cardano.Ledger.Constrained.Conway.MiniTrace (
  ConstrainedGeneratorBundle (..),
 )
import Test.Cardano.Ledger.Conway.ImpTest (ImpTestM, impAnn)
import Test.Cardano.Ledger.Imp.Common
import UnliftIO (MonadIO (..), evaluateDeep)

conformsToImpl ::
  forall rule era.
  ExecSpecRule rule era =>
  Gen (ExecContext rule era, TRC (EraRule rule era)) ->
  Property
conformsToImpl :: forall (rule :: Symbol) era.
ExecSpecRule rule era =>
Gen (ExecContext rule era, TRC (EraRule rule era)) -> Property
conformsToImpl Gen (ExecContext rule era, TRC (EraRule rule era))
genInputs = forall prop. Testable prop => prop -> Property
property @(ImpTestM era Property) (ImpTestM era Property -> Property)
-> (ContT Property (ImpM (LedgerSpec era)) Property
    -> ImpTestM era Property)
-> ContT Property (ImpM (LedgerSpec era)) Property
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ContT Property (ImpM (LedgerSpec era)) Property
-> (Property -> ImpTestM era Property) -> ImpTestM era Property
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
`runContT` Property -> ImpTestM era Property
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) (ContT Property (ImpM (LedgerSpec era)) Property -> Property)
-> ContT Property (ImpM (LedgerSpec era)) Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  let
    deepEvalAnn :: String -> String
deepEvalAnn String
s = String
"Deep evaluating " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
s
    deepEval :: a -> String -> t (ImpM t) ()
deepEval a
x String
s = do
      _ <- ImpM t a -> t (ImpM t) a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ImpM t a -> t (ImpM t) a) -> ImpM t a -> t (ImpM t) a
forall a b. (a -> b) -> a -> b
$ String -> ImpM t a -> ImpM t a
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn (String -> String
deepEvalAnn String
s) (IO a -> ImpM t a
forall a. IO a -> ImpM t a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (a -> IO a
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep a
x))
      pure ()
  (ctx, trc@(TRC (env, st, sig))) <- ImpM
  (LedgerSpec era) (ExecContext rule era, TRC (EraRule rule era))
-> ContT
     Property
     (ImpM (LedgerSpec era))
     (ExecContext rule era, TRC (EraRule rule era))
forall (m :: * -> *) a. Monad m => m a -> ContT Property m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ImpM
   (LedgerSpec era) (ExecContext rule era, TRC (EraRule rule era))
 -> ContT
      Property
      (ImpM (LedgerSpec era))
      (ExecContext rule era, TRC (EraRule rule era)))
-> ImpM
     (LedgerSpec era) (ExecContext rule era, TRC (EraRule rule era))
-> ContT
     Property
     (ImpM (LedgerSpec era))
     (ExecContext rule era, TRC (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ Gen (ExecContext rule era, TRC (EraRule rule era))
-> ImpM
     (LedgerSpec era) (ExecContext rule era, TRC (EraRule rule era))
forall a. Gen a -> ImpM (LedgerSpec era) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen (ExecContext rule era, TRC (EraRule rule era))
genInputs
  deepEval ctx "context"
  deepEval env "environment"
  deepEval st "state"
  deepEval sig "signal"
  pure $ testConformance @rule @era ctx trc

genFromBundle_ ::
  ( HasSpec (Environment (EraRule rule era))
  , HasSpec (State (EraRule rule era))
  , HasSpec (Signal (EraRule rule era))
  , Arbitrary (ExecContext rule era)
  ) =>
  ConstrainedGeneratorBundle ctx rule era ->
  Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle_ :: forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era
-> Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle_ ConstrainedGeneratorBundle ctx rule era
x = ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
forall (rule :: Symbol) era ctx.
ForAllExecTypes HasSpec rule era =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle ConstrainedGeneratorBundle ctx rule era
x ((ctx
  -> Environment (EraRule rule era)
  -> State (EraRule rule era)
  -> Signal (EraRule rule era)
  -> Gen (ExecContext rule era))
 -> Gen (ExecContext rule era, TRC (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ \ctx
_ Environment (EraRule rule era)
_ State (EraRule rule era)
_ Signal (EraRule rule era)
_ -> Gen (ExecContext rule era)
forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary

genFromBundle ::
  ForAllExecTypes HasSpec rule era =>
  ConstrainedGeneratorBundle ctx rule era ->
  ( ctx ->
    Environment (EraRule rule era) ->
    State (EraRule rule era) ->
    Signal (EraRule rule era) ->
    Gen (ExecContext rule era)
  ) ->
  Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle :: forall (rule :: Symbol) era ctx.
ForAllExecTypes HasSpec rule era =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle ConstrainedGeneratorBundle {Gen ctx
ctx -> Specification (Environment (EraRule rule era))
ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbContextGen :: Gen ctx
cgbEnvironmentSpec :: ctx -> Specification (Environment (EraRule rule era))
cgbStateSpec :: ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbSignalSpec :: ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbSignalSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbStateSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbEnvironmentSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx -> Specification (Environment (EraRule rule era))
cgbContextGen :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era -> Gen ctx
..} ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Gen (ExecContext rule era)
genExecContext = do
  ctx <- Gen ctx
cgbContextGen
  env <- genFromSpec $ cgbEnvironmentSpec ctx
  st <- genFromSpec $ cgbStateSpec ctx env
  sig <- genFromSpec $ cgbSignalSpec ctx env st
  (,TRC (env, st, sig)) <$> genExecContext ctx env st sig

conformsToImplConstrained ::
  forall ctx rule era.
  ( ExecSpecRule rule era
  , ForAllExecTypes HasSpec rule era
  ) =>
  ConstrainedGeneratorBundle ctx rule era ->
  ( ctx ->
    Environment (EraRule rule era) ->
    State (EraRule rule era) ->
    Signal (EraRule rule era) ->
    Gen (ExecContext rule era)
  ) ->
  Property
conformsToImplConstrained :: forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle ctx rule era
bundle ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Gen (ExecContext rule era)
genExecContext =
  forall (rule :: Symbol) era.
ExecSpecRule rule era =>
Gen (ExecContext rule era, TRC (EraRule rule era)) -> Property
conformsToImpl @rule @era (Gen (ExecContext rule era, TRC (EraRule rule era)) -> Property)
-> Gen (ExecContext rule era, TRC (EraRule rule era)) -> Property
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
forall (rule :: Symbol) era ctx.
ForAllExecTypes HasSpec rule era =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle ConstrainedGeneratorBundle ctx rule era
bundle ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Gen (ExecContext rule era)
genExecContext

conformsToImplConstrained_ ::
  ( ExecSpecRule rule era
  , ForAllExecTypes HasSpec rule era
  , Arbitrary (ExecContext rule era)
  ) =>
  ConstrainedGeneratorBundle ctx rule era ->
  Property
conformsToImplConstrained_ :: forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle ctx rule era
bundle = ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle ctx rule era
bundle ((ctx
  -> Environment (EraRule rule era)
  -> State (EraRule rule era)
  -> Signal (EraRule rule era)
  -> Gen (ExecContext rule era))
 -> Property)
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
forall a b. (a -> b) -> a -> b
$ \ctx
_ Environment (EraRule rule era)
_ State (EraRule rule era)
_ Signal (EraRule rule era)
_ -> Gen (ExecContext rule era)
forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary