{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Constrained.Preds.PParams (
  pParamsPreds,
  pParamsStage,
  extract,
  mainPParams,
  demoTest,
) where

import Cardano.Ledger.Alonzo.Scripts (ExUnits (..))
import qualified Cardano.Ledger.Alonzo.Scripts as Script (Prices (..))
import Cardano.Ledger.Api.Era
import Cardano.Ledger.BaseTypes (
  EpochInterval (..),
  NonNegativeInterval,
  boundRational,
 )
import Cardano.Ledger.Coin (Coin (..))
import Control.Monad (when)
import GHC.Num (Natural)
import Lens.Micro ((^.))
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes (OrdCond (..))
import Test.Cardano.Ledger.Constrained.Env (Access (..), V (..), emptyEnv)
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Rewrite (standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Solver
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.Fields
import Test.Cardano.Ledger.Generic.Functions (protocolVersion)
import Test.Cardano.Ledger.Generic.Proof
import Test.Cardano.Ledger.Generic.Updaters (defaultCostModels, newPParams)
import Test.Tasty (TestTree, defaultMain)
import Test.Tasty.QuickCheck

extract :: Era era => Term era t -> Term era s -> Pred era
extract :: forall era t s. Era era => Term era t -> Term era s -> Pred era
extract term :: Term era t
term@(Var (V String
_ Rep era t
_ (Yes Rep era s
r1 Lens' s t
lens))) Term era s
record =
  case Rep era s -> Rep era s -> Maybe (s :~: s)
forall i j. Rep era i -> Rep era j -> Maybe (i :~: j)
forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era s
r1 (Term era s -> Rep era s
forall era t. Era era => Term era t -> Rep era t
termRep Term era s
record) of
    Just s :~: s
Refl -> Term era t
term Term era t -> RootTarget era Void t -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String -> (s -> t) -> RootTarget era Void (s -> t)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"lookup" (\s
x -> s
x s -> Getting t s t -> t
forall s a. s -> Getting a s a -> a
^. Getting t s t
Lens' s t
lens) RootTarget era Void (s -> t) -> Term era s -> RootTarget era Void t
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era s
Term era s
record)
    Maybe (s :~: s)
Nothing -> String -> Pred era
forall a. HasCallStack => String -> a
error (String
"Term " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term era t -> String
forall a. Show a => a -> String
show Term era t
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with bad Access in extract2")
extract Term era t
term Term era s
_ = String -> Pred era
forall a. HasCallStack => String -> a
error (String
"Non Var term " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term era t -> String
forall a. Show a => a -> String
show Term era t
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in extract2")

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

nonNegativeInterval :: Rational -> NonNegativeInterval
nonNegativeInterval :: Rational -> NonNegativeInterval
nonNegativeInterval Rational
r = case (forall r. BoundedRational r => Rational -> Maybe r
boundRational @NonNegativeInterval Rational
r) of
  Just NonNegativeInterval
nn -> NonNegativeInterval
nn
  Maybe NonNegativeInterval
Nothing -> String -> NonNegativeInterval
forall a. HasCallStack => String -> a
error (String
"Can't make NonNegativeInterval from: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
r)

{- Preds we want to be True in pparams. This comment is meant as a statement of intent
   The actual code acheives this algorithmically, but we want this declaration of what should be true
  [ Sized (AtLeast 1) (maxBHSize proof)
  , Sized (AtLeast 1) (maxTxSize proof)
  , SumsTo (Right 1) (maxBBSize proof) LTE [One (maxBHSize proof), One (maxTxSize proof)]
  , Component
      (Right (pparams proof))
      [field pp (maxTxSize proof), field pp (maxBHSize proof), field pp (maxBBSize proof)]
  ]
-}

genPParams :: Reflect era => Proof era -> Natural -> Natural -> Natural -> Gen (PParamsF era)
genPParams :: forall era.
Reflect era =>
Proof era -> Natural -> Natural -> Natural -> Gen (PParamsF era)
genPParams Proof era
proof Natural
tx Natural
bb Natural
bh = do
  ExUnits
maxTxExUnits2 <-
    Natural -> Natural -> ExUnits
ExUnits
      (Natural -> Natural -> ExUnits)
-> Gen Natural -> Gen (Natural -> ExUnits)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Gen Int -> Gen Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
100 :: Int, Int
10000))
      Gen (Natural -> ExUnits) -> Gen Natural -> Gen ExUnits
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Gen Int -> Gen Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
100 :: Int, Int
10000))
  Natural
maxCollateralInputs <- [Natural] -> Gen Natural
forall a. HasCallStack => [a] -> Gen a
elements [Natural
3 .. Natural
5]
  Natural
collateralPercentage2 <- Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Gen Int -> Gen Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
chooseInt (Int
1, Int
200)
  Coin
minfeeA <- Integer -> Coin
Coin (Integer -> Coin) -> Gen Integer -> Gen Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
100)
  Coin
minfeeB <- Integer -> Coin
Coin (Integer -> Coin) -> Gen Integer -> Gen Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
10)
  PParamsF era -> Gen (PParamsF era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( Proof era -> PParams era -> PParamsF era
forall era. Proof era -> PParams era -> PParamsF era
PParamsF Proof era
proof (PParams era -> PParamsF era) -> PParams era -> PParamsF era
forall a b. (a -> b) -> a -> b
$
        Proof era -> [PParamsField era] -> PParams era
forall era.
EraPParams era =>
Proof era -> [PParamsField era] -> PParams era
newPParams
          Proof era
proof
          [ Coin -> PParamsField era
forall era. Coin -> PParamsField era
MinfeeA Coin
minfeeA
          , Coin -> PParamsField era
forall era. Coin -> PParamsField era
MinfeeB Coin
minfeeB
          , Prices -> PParamsField era
forall era. Prices -> PParamsField era
Prices (NonNegativeInterval -> NonNegativeInterval -> Prices
Script.Prices (Rational -> NonNegativeInterval
nonNegativeInterval Rational
1.0) (Rational -> NonNegativeInterval
nonNegativeInterval Rational
1.0))
          , Proof era -> PParamsField era
forall era. Proof era -> PParamsField era
defaultCostModels Proof era
proof
          , Natural -> PParamsField era
forall era. Natural -> PParamsField era
MaxValSize Natural
1000
          , Word32 -> PParamsField era
forall era. Word32 -> PParamsField era
MaxTxSize (String -> Natural -> Word32
forall a b.
(HasCallStack, Integral a, Show a, Integral b, Bounded b,
 Show b) =>
String -> a -> b
fromIntegralBounded String
"TxSize" Natural
tx) -- In the Model these are Natural
          , Word32 -> PParamsField era
forall era. Word32 -> PParamsField era
MaxBBSize (String -> Natural -> Word32
forall a b.
(HasCallStack, Integral a, Show a, Integral b, Bounded b,
 Show b) =>
String -> a -> b
fromIntegralBounded String
"BlockBodySize" Natural
bb) -- But in the PParams, they are
          , Word16 -> PParamsField era
forall era. Word16 -> PParamsField era
MaxBHSize (String -> Natural -> Word16
forall a b.
(HasCallStack, Integral a, Show a, Integral b, Bounded b,
 Show b) =>
String -> a -> b
fromIntegralBounded String
"BlockHeaderSize" Natural
bh) -- Word32, Word32, and Word16
          , ExUnits -> PParamsField era
forall era. ExUnits -> PParamsField era
MaxTxExUnits ExUnits
maxTxExUnits2
          , Natural -> PParamsField era
forall era. Natural -> PParamsField era
MaxCollateralInputs Natural
maxCollateralInputs
          , Natural -> PParamsField era
forall era. Natural -> PParamsField era
CollateralPercentage Natural
collateralPercentage2
          , ProtVer -> PParamsField era
forall era. ProtVer -> PParamsField era
ProtocolVersion (ProtVer -> PParamsField era) -> ProtVer -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Proof era -> ProtVer
forall era. Proof era -> ProtVer
protocolVersion Proof era
proof
          , Coin -> PParamsField era
forall era. Coin -> PParamsField era
PoolDeposit (Coin -> PParamsField era) -> Coin -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
5
          , Coin -> PParamsField era
forall era. Coin -> PParamsField era
KeyDeposit (Coin -> PParamsField era) -> Coin -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
2
          , Coin -> PParamsField era
forall era. Coin -> PParamsField era
DRepDeposit (Coin -> PParamsField era) -> Coin -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
7
          , Coin -> PParamsField era
forall era. Coin -> PParamsField era
GovActionDeposit (Coin -> PParamsField era) -> Coin -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
13
          , EpochInterval -> PParamsField era
forall era. EpochInterval -> PParamsField era
DRepActivity (EpochInterval -> PParamsField era)
-> EpochInterval -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Word32 -> EpochInterval
EpochInterval Word32
8
          , EpochInterval -> PParamsField era
forall era. EpochInterval -> PParamsField era
EMax (EpochInterval -> PParamsField era)
-> EpochInterval -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Word32 -> EpochInterval
EpochInterval Word32
100
          ]
    )

pParamsPreds :: Reflect era => Proof era -> [Pred era]
pParamsPreds :: forall era. Reflect era => Proof era -> [Pred era]
pParamsPreds Proof era
p =
  [ Term era (PParamsF era)
-> RootTarget era Void (Gen (PParamsF era)) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom
      (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
      ( String
-> (Natural -> Natural -> Natural -> Gen (PParamsF era))
-> RootTarget
     era Void (Natural -> Natural -> Natural -> Gen (PParamsF era))
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"genPParams" (Proof era -> Natural -> Natural -> Natural -> Gen (PParamsF era)
forall era.
Reflect era =>
Proof era -> Natural -> Natural -> Natural -> Gen (PParamsF era)
genPParams Proof era
p)
          RootTarget
  era Void (Natural -> Natural -> Natural -> Gen (PParamsF era))
-> Term era Natural
-> Target era (Natural -> Natural -> Gen (PParamsF era))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
p)
          Target era (Natural -> Natural -> Gen (PParamsF era))
-> Term era Natural -> Target era (Natural -> Gen (PParamsF era))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof era
p)
          Target era (Natural -> Gen (PParamsF era))
-> Term era Natural -> RootTarget era Void (Gen (PParamsF era))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
p)
      )
  , Term era ProtVer -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era ProtVer
forall era. Era era => Proof era -> Term era ProtVer
protVer Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , Term era Coin -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
minFeeA Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , Term era Coin -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
minFeeB Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , Term era Coin -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
keyDepAmt Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , Term era Coin -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
poolDepAmt Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , Term era EpochInterval -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era EpochInterval
forall era. Era era => Proof era -> Term era EpochInterval
maxEpoch Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , Term era Size -> Term era Natural -> 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
AtLeast Int
100) (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
p)
  , Term era Size -> Term era Natural -> 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
AtLeast Int
40000) (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
p)
  , Direct Natural
-> Term era Natural -> OrdCond -> [Sum era Natural] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Natural -> Direct Natural
forall a b. b -> Either a b
Right Natural
1) (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof era
p) OrdCond
LTE [Term era Natural -> Sum era Natural
forall era c. Term era c -> Sum era c
One (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
p), Term era Natural -> Sum era Natural
forall era c. Term era c -> Sum era c
One (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
p)]
  , (Proof era -> Term era ProtVer
forall era. Era era => Proof era -> Term era ProtVer
protVer Proof era
p) Term era ProtVer -> Term era ProtVer -> Pred era
forall n era. Count n => Term era n -> Term era n -> Pred era
`CanFollow` (Proof era -> Term era ProtVer
forall era. Era era => Proof era -> Term era ProtVer
prevProtVer Proof era
p)
  ]
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ ( case Proof era -> PParamsWit era
forall era. Proof era -> PParamsWit era
whichPParams Proof era
p of
           PParamsWit era
PParamsShelleyToMary -> []
           PParamsWit era
PParamsAlonzoToAlonzo ->
             [ Term era ExUnits -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era ExUnits
forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             , Term era Natural -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Natural
forall era. AlonzoEraPParams era => Proof era -> Term era Natural
collateralPercentage Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             ]
           PParamsWit era
PParamsBabbageToBabbage ->
             [ Term era ExUnits -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era ExUnits
forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             , Term era Natural -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Natural
forall era. AlonzoEraPParams era => Proof era -> Term era Natural
collateralPercentage Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             ]
           PParamsWit era
PParamsConwayToConway ->
             [ Term era ExUnits -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era ExUnits
forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             , Term era Natural -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Natural
forall era. AlonzoEraPParams era => Proof era -> Term era Natural
collateralPercentage Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             , Term era EpochInterval -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era EpochInterval
forall era.
ConwayEraPParams era =>
Proof era -> Term era EpochInterval
drepActivity Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             , Term era Coin -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Coin
forall era. ConwayEraPParams era => Proof era -> Term era Coin
drepDeposit Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             , Term era Coin -> Term era (PParamsF era) -> Pred era
forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (Proof era -> Term era Coin
forall era. ConwayEraPParams era => Proof era -> Term era Coin
proposalDeposit Proof era
p) (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
             ]
       )

pParamsStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
pParamsStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage 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. Reflect era => Proof era -> [Pred era]
pParamsPreds Proof era
proof)

demo :: ReplMode -> IO ()
demo :: ReplMode -> IO ()
demo ReplMode
mode = do
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
  Subst BabbageEra
subst <- Gen (Subst BabbageEra) -> IO (Subst BabbageEra)
forall a. Gen a -> IO a
generate (Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof BabbageEra
proof Subst BabbageEra
forall era. Subst era
emptySubst)
  Env BabbageEra
env <- Typed (Env BabbageEra) -> IO (Env BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Subst BabbageEra -> Env BabbageEra -> Typed (Env BabbageEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst BabbageEra
subst Env BabbageEra
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 String
"\n" IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStrLn (Subst BabbageEra -> String
forall a. Show a => a -> String
show Subst BabbageEra
subst)
  ReplMode -> Proof BabbageEra -> Env BabbageEra -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof BabbageEra
proof Env BabbageEra
env String
""

demoTest :: TestTree
demoTest :: TestTree
demoTest = String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing TxOut Stage" (ReplMode -> IO ()
demo ReplMode
CI)

mainPParams :: IO ()
mainPParams :: IO ()
mainPParams = 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 TxOut Stage" (ReplMode -> IO ()
demo ReplMode
Interactive)