{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Test.Cardano.Ledger.Constrained.Preds.NewEpochState where

import Cardano.Ledger.Core (Era)
import Cardano.Ledger.State (
  EraCertState (..),
  PoolDistr (..),
  SnapShot (..),
  Stake (..),
  calculatePoolDistr,
 )
import qualified Cardano.Ledger.UMap as UMap
import Control.Monad (when)
import Data.Default (Default (def))
import qualified Data.Map.Strict as Map
import qualified Data.VMap as VMap
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.CertState (dstateStage, pstateStage, vstateStage)
import Test.Cardano.Ledger.Constrained.Preds.LedgerState (ledgerStateStage)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.UTxO (utxoStage)
import Test.Cardano.Ledger.Constrained.Preds.Universes (universeStage)
import Test.Cardano.Ledger.Constrained.Rewrite (OrderInfo (..), standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Solver (toolChainSub)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.PrettyCore (pcEpochState, pcNewEpochState)
import Test.Cardano.Ledger.Generic.Proof
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain)

-- ===========================================================

epochstatePreds :: EraCertState era => Proof era -> [Pred era]
epochstatePreds :: forall era. EraCertState era => Proof era -> [Pred era]
epochstatePreds Proof era
_proof =
  [ Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instantStakeTerm Term era (Map (Credential 'Staking) Coin)
-> Term era (Map (Credential 'Staking) Coin) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
markStake
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
markDelegs
  , Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
markPools
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
setStake Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
setDelegs Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
setDelegs Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era Size
-> Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
2) Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
setPools
  , Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
setPools Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
goStake Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
goDelegs Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
goDelegs Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era Size
-> Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
2) Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
goPools
  , Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
goPools Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
snapShotFee
  , Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
markPoolDistr
      Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
-> RootTarget
     era Void (Map (KeyHash 'StakePool) IndividualPoolStake)
-> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( String
-> (Map (Credential 'Staking) Coin
    -> Map (Credential 'Staking) (KeyHash 'StakePool)
    -> Map (KeyHash 'StakePool) PoolParams
    -> Map (KeyHash 'StakePool) IndividualPoolStake)
-> RootTarget
     era
     Void
     (Map (Credential 'Staking) Coin
      -> Map (Credential 'Staking) (KeyHash 'StakePool)
      -> Map (KeyHash 'StakePool) PoolParams
      -> Map (KeyHash 'StakePool) IndividualPoolStake)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr
               String
"calculatePoolDistr"
               ( \Map (Credential 'Staking) Coin
stak Map (Credential 'Staking) (KeyHash 'StakePool)
del Map (KeyHash 'StakePool) PoolParams
pl ->
                   PoolDistr -> Map (KeyHash 'StakePool) IndividualPoolStake
unPoolDistr (PoolDistr -> Map (KeyHash 'StakePool) IndividualPoolStake)
-> PoolDistr -> Map (KeyHash 'StakePool) IndividualPoolStake
forall a b. (a -> b) -> a -> b
$
                     SnapShot -> PoolDistr
calculatePoolDistr
                       ( Stake
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (KeyHash 'StakePool) PoolParams
-> SnapShot
SnapShot
                           (VMap VB VP (Credential 'Staking) (CompactForm Coin) -> Stake
Stake (Map (Credential 'Staking) (CompactForm Coin)
-> VMap VB VP (Credential 'Staking) (CompactForm Coin)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap ((Coin -> CompactForm Coin)
-> Map (Credential 'Staking) Coin
-> Map (Credential 'Staking) (CompactForm Coin)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
Coin -> CompactForm Coin
UMap.compactCoinOrError Map (Credential 'Staking) Coin
stak)))
                           (Map (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap Map (Credential 'Staking) (KeyHash 'StakePool)
del)
                           (Map (KeyHash 'StakePool) PoolParams
-> VMap VB VB (KeyHash 'StakePool) PoolParams
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap Map (KeyHash 'StakePool) PoolParams
pl)
                       )
               )
               RootTarget
  era
  Void
  (Map (Credential 'Staking) Coin
   -> Map (Credential 'Staking) (KeyHash 'StakePool)
   -> Map (KeyHash 'StakePool) PoolParams
   -> Map (KeyHash 'StakePool) IndividualPoolStake)
-> Term era (Map (Credential 'Staking) Coin)
-> Target
     era
     (Map (Credential 'Staking) (KeyHash 'StakePool)
      -> Map (KeyHash 'StakePool) PoolParams
      -> Map (KeyHash 'StakePool) IndividualPoolStake)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
markStake
               Target
  era
  (Map (Credential 'Staking) (KeyHash 'StakePool)
   -> Map (KeyHash 'StakePool) PoolParams
   -> Map (KeyHash 'StakePool) IndividualPoolStake)
-> Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Target
     era
     (Map (KeyHash 'StakePool) PoolParams
      -> Map (KeyHash 'StakePool) IndividualPoolStake)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
markDelegs
               Target
  era
  (Map (KeyHash 'StakePool) PoolParams
   -> Map (KeyHash 'StakePool) IndividualPoolStake)
-> Term era (Map (KeyHash 'StakePool) PoolParams)
-> RootTarget
     era Void (Map (KeyHash 'StakePool) IndividualPoolStake)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
markPools
           )
  ]

newEpochStatePreds :: Era era => Proof era -> [Pred era]
newEpochStatePreds :: forall era. Era era => Proof era -> [Pred era]
newEpochStatePreds Proof era
_proof =
  [ Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
4) (Term era (Map (KeyHash 'StakePool) Natural)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Natural)
forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
prevBlocksMade) -- Both prevBlocksMade and prevBlocksMadeDom will have size 4
  , Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
4) (Term era (Map (KeyHash 'StakePool) Natural)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Natural)
forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
currBlocksMade)
  , Term era (Map (KeyHash 'StakePool) Natural)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Natural)
forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
prevBlocksMade Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era (Map (KeyHash 'StakePool) Natural)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Natural)
forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
currBlocksMade Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  ]

-- ========================

epochStateStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
epochStateStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
epochStateStage Proof era
proof = Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
epochstatePreds Proof era
proof)

demoES :: Reflect era => Proof era -> ReplMode -> IO ()
demoES :: forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoES Proof era
proof ReplMode
mode = do
  Env era
env <-
    Gen (Env era) -> IO (Env era)
forall a. Gen a -> IO a
generate
      ( Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
forall a. Default a => a
def Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
forall a. Default a => a
def Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
epochStateStage Proof era
proof
          Gen (Subst era) -> (Subst era -> Gen (Env era)) -> Gen (Env era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv)
      )
  EpochState era
epochstate <- Typed (EpochState era) -> IO (EpochState era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (EpochState era) -> IO (EpochState era))
-> Typed (EpochState era) -> IO (EpochState era)
forall a b. (a -> b) -> a -> b
$ Env era
-> RootTarget era (EpochState era) (EpochState era)
-> Typed (EpochState era)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env (Proof era -> RootTarget era (EpochState era) (EpochState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (EpochState era) (EpochState era)
epochStateT Proof era
proof)
  let env2 :: Env era
env2 = EpochState era
-> RootTarget era (EpochState era) (EpochState era)
-> Env era
-> Env era
forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget EpochState era
epochstate (Proof era -> RootTarget era (EpochState era) (EpochState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (EpochState era) (EpochState era)
epochStateT Proof era
proof) Env era
forall era. Env era
emptyEnv
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ PDoc -> IO ()
forall a. Show a => a -> IO ()
print (Proof era -> EpochState era -> PDoc
forall era. Reflect era => Proof era -> EpochState era -> PDoc
pcEpochState Proof era
proof EpochState era
epochstate)
  ReplMode -> Proof era -> Env era -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof era
proof Env era
env2 String
""

demoESTest :: TestTree
demoESTest :: TestTree
demoESTest = String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing EpochState Stage" (Proof ConwayEra -> ReplMode -> IO ()
forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoES Proof ConwayEra
Conway ReplMode
CI)

mainES :: IO ()
mainES :: IO ()
mainES = TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing EpochState Stage" (Proof ConwayEra -> ReplMode -> IO ()
forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoES Proof ConwayEra
Conway ReplMode
Interactive)

-- ====================================================

newEpochStateStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
newEpochStateStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
newEpochStateStage Proof era
proof = Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof (OrderInfo
standardOrderInfo {sumBeforeParts = False}) (Proof era -> [Pred era]
forall era. Era era => Proof era -> [Pred era]
newEpochStatePreds Proof era
proof)

demoNES :: Reflect era => Proof era -> ReplMode -> IO ()
demoNES :: forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoNES Proof era
proof ReplMode
mode = do
  Env era
env <-
    Gen (Env era) -> IO (Env era)
forall a. Gen a -> IO a
generate
      ( Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
forall a. Default a => a
def Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
epochStateStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
newEpochStateStage Proof era
proof
          Gen (Subst era) -> (Subst era -> Gen (Env era)) -> Gen (Env era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv)
      )
  NewEpochState era
newepochstate <- Typed (NewEpochState era) -> IO (NewEpochState era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (NewEpochState era) -> IO (NewEpochState era))
-> Typed (NewEpochState era) -> IO (NewEpochState era)
forall a b. (a -> b) -> a -> b
$ Env era
-> RootTarget era (NewEpochState era) (NewEpochState era)
-> Typed (NewEpochState era)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env (Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof era
proof)
  let env2 :: Env era
env2 = NewEpochState era
-> RootTarget era (NewEpochState era) (NewEpochState era)
-> Env era
-> Env era
forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget NewEpochState era
newepochstate (Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof era
proof) Env era
forall era. Env era
emptyEnv
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (PDoc -> String
forall a. Show a => a -> String
show (Proof era -> NewEpochState era -> PDoc
forall era. Reflect era => Proof era -> NewEpochState era -> PDoc
pcNewEpochState Proof era
proof NewEpochState era
newepochstate))
  ReplMode -> Proof era -> Env era -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof era
proof Env era
env2 String
""

demoNESTest :: TestTree
demoNESTest :: TestTree
demoNESTest = String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing NewEpochState Stage" (Proof ConwayEra -> ReplMode -> IO ()
forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoNES Proof ConwayEra
Conway ReplMode
CI)

mainNES :: IO ()
mainNES :: IO ()
mainNES = TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing NewEpochState Stage" (Proof ConwayEra -> ReplMode -> IO ()
forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoNES Proof ConwayEra
Conway ReplMode
Interactive)

-- ==========================