{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}

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

import Cardano.Crypto.Hash.Class (Hash, HashAlgorithm, castHash, hashWith)
import Cardano.Ledger.Address (Addr (..))
import Cardano.Ledger.Alonzo.TxOut (AlonzoEraTxOut (..), AlonzoTxOut (..))
import Cardano.Ledger.Babbage.TxOut (BabbageEraTxOut (..), BabbageTxOut (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core (
  Era,
  EraScript (..),
  EraTxOut (..),
  Script,
  TxOut,
  addrTxOutL,
  coinTxOutL,
  hashScript,
  valueTxOutL,
 )
import Cardano.Ledger.Hashes (DataHash, ScriptHash (..))
import Cardano.Ledger.Mary.Value (
  AssetName (..),
  MaryValue (..),
  MultiAsset (..),
  PolicyID (..),
  multiAssetFromList,
 )
import Cardano.Ledger.Plutus.Data (Data (..), Datum (..), dataToBinaryData, hashData)
import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..))
import Control.Monad (when)
import Data.Default (Default (def))
import Data.Int (Int64)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..), maybeToStrictMaybe, strictMaybeToMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (IsString (..))
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes
import Test.Cardano.Ledger.Constrained.Combinators (genFromMap, itemFromSet)
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.Repl
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.Universes hiding (demo, demoTest, main)
import Test.Cardano.Ledger.Constrained.Rewrite (rewriteGen, standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Size
import Test.Cardano.Ledger.Constrained.Solver (toolChain, 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.Fields (TxBodyField (..), TxOutField (..))
import Test.Cardano.Ledger.Generic.PrettyCore (
  pcData,
  pcDataHash,
  pcScript,
  pcScriptHash,
  pcTxOut,
  ppList,
  ppMap,
 )
import Test.Cardano.Ledger.Generic.Proof
import Test.Cardano.Ledger.Generic.Updaters (newTxBody, newTxOut)
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain)

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

scriptFL :: Reflect era => Lens' (Script era) (ScriptF era)
scriptFL :: forall era. Reflect era => Lens' (Script era) (ScriptF era)
scriptFL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (forall era. Proof era -> Script era -> ScriptF era
ScriptF forall era. Reflect era => Proof era
reify) (\Script era
_ (ScriptF Proof era
_ Script era
u) -> Script era
u)

strictMaybeMaybeL :: Lens' (StrictMaybe a) (Maybe a)
strictMaybeMaybeL :: forall a. Lens' (StrictMaybe a) (Maybe a)
strictMaybeMaybeL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (forall a b. a -> b -> a
const forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe)

txoutRefScriptL :: (Reflect era, BabbageEraTxOut era) => Lens' (TxOutF era) (Maybe (ScriptF era))
txoutRefScriptL :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Lens' (TxOutF era) (Maybe (ScriptF era))
txoutRefScriptL = forall era. Lens' (TxOutF era) (TxOut era)
txOutFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
BabbageEraTxOut era =>
Lens' (TxOut era) (StrictMaybe (Script era))
referenceScriptTxOutL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (StrictMaybe a) (Maybe a)
strictMaybeMaybeL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Lens' a b -> Lens' (Maybe a) (Maybe b)
liftMaybeL forall era. Reflect era => Lens' (Script era) (ScriptF era)
scriptFL

liftMaybeL :: Lens' a b -> Lens' (Maybe a) (Maybe b)
liftMaybeL :: forall a b. Lens' a b -> Lens' (Maybe a) (Maybe b)
liftMaybeL Lens' a b
l = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens Maybe a -> Maybe b
getter Maybe a -> Maybe b -> Maybe a
setter
  where
    getter :: Maybe a -> Maybe b
getter (Just a
x) = forall a. a -> Maybe a
Just (a
x forall s a. s -> Getting a s a -> a
^. Lens' a b
l)
    getter Maybe a
Nothing = forall a. Maybe a
Nothing
    setter :: Maybe a -> Maybe b -> Maybe a
setter (Just a
a) (Just b
b) = forall a. a -> Maybe a
Just (a
a forall a b. a -> (a -> b) -> b
& Lens' a b
l forall s t a b. ASetter s t a b -> b -> s -> t
.~ b
b)
    setter (Just a
_a) Maybe b
Nothing = forall a. Maybe a
Nothing -- Type wise this Nothing could be (Just a), but that is wrong
    setter Maybe a
Nothing Maybe b
_ = forall a. Maybe a
Nothing

txoutScriptF :: (Reflect era, BabbageEraTxOut era) => Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF = forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field String
"txoutScript" (forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR forall era. Reflect era => Proof era
reify)) (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR forall era. Reflect era => Proof era
reify) forall era.
(Reflect era, BabbageEraTxOut era) =>
Lens' (TxOutF era) (Maybe (ScriptF era))
txoutRefScriptL

txoutScript :: (Reflect era, BabbageEraTxOut era) => Term era (Maybe (ScriptF era))
txoutScript :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Maybe (ScriptF era))
txoutScript = forall era rec field. Field era rec field -> Term era field
fieldToTerm forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF

txoutDatumF :: (Reflect era, BabbageEraTxOut era) => Field era (TxOutF era) (Datum era)
txoutDatumF :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Datum era)
txoutDatumF = forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field String
"txoutDatumF" forall era. Era era => Rep era (Datum era)
DatumR (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR forall era. Reflect era => Proof era
reify) (forall era. Lens' (TxOutF era) (TxOut era)
txOutFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. BabbageEraTxOut era => Lens' (TxOut era) (Datum era)
datumTxOutL)

txoutDatum :: (Reflect era, BabbageEraTxOut era) => Term era (Datum era)
txoutDatum :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Datum era)
txoutDatum = forall era rec field. Field era rec field -> Term era field
fieldToTerm forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Datum era)
txoutDatumF

txoutDataHashF ::
  (Reflect era, AlonzoEraTxOut era) => Field era (TxOutF era) (Maybe DataHash)
txoutDataHashF :: forall era.
(Reflect era, AlonzoEraTxOut era) =>
Field era (TxOutF era) (Maybe DataHash)
txoutDataHashF =
  forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field
    String
"txoutDataHashF"
    (forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR forall era. Era era => Rep era DataHash
DataHashR)
    (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR forall era. Reflect era => Proof era
reify)
    (forall era. Lens' (TxOutF era) (TxOut era)
txOutFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AlonzoEraTxOut era =>
Lens' (TxOut era) (StrictMaybe DataHash)
dataHashTxOutL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (StrictMaybe a) (Maybe a)
strictMaybeMaybeL)

txoutDataHash :: (Reflect era, AlonzoEraTxOut era) => Term era (Maybe DataHash)
txoutDataHash :: forall era.
(Reflect era, AlonzoEraTxOut era) =>
Term era (Maybe DataHash)
txoutDataHash = forall era rec field. Field era rec field -> Term era field
fieldToTerm forall era.
(Reflect era, AlonzoEraTxOut era) =>
Field era (TxOutF era) (Maybe DataHash)
txoutDataHashF

isBootstrapAddr :: Addr -> Bool
isBootstrapAddr :: Addr -> Bool
isBootstrapAddr (AddrBootstrap BootstrapAddress
_) = Bool
True
isBootstrapAddr (Addr Network
_ PaymentCredential
_ StakeReference
_) = Bool
False

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

txOutPreds ::
  Reflect era => UnivSize -> Proof era -> Term era Coin -> Term era [TxOutF era] -> [Pred era]
txOutPreds :: forall era.
Reflect era =>
UnivSize
-> Proof era
-> Term era Coin
-> Term era [TxOutF era]
-> [Pred era]
txOutPreds size :: UnivSize
size@UnivSize {Int
usDatumFreq :: UnivSize -> Int
usDatumFreq :: Int
usDatumFreq} Proof era
p Term era Coin
balanceCoin Term era [TxOutF era]
outputS =
  [ forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
      (forall era. Era era => Int -> Int -> Term era Size
Range Int
6 Int
6)
      Term era [Datum era]
datums
      [ (Int
1, forall era t. Term era t -> RootTarget era Void t
Simple (forall era t. Rep era t -> t -> Term era t
Lit forall era. Era era => Rep era (Datum era)
DatumR forall era. Datum era
NoDatum), [])
      , (Int
1, forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"DatumHash" forall era. DataHash -> Datum era
DatumHash forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era DataHash
hash, [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era DataHash
hash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map DataHash (Data era))
dataUniv)])
      ,
        ( Int
usDatumFreq
        , forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"Datum" (forall era. BinaryData era -> Datum era
Datum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Era era => Data era -> BinaryData era
dataToBinaryData)
            forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Data era)
dat
        , [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left (forall era. Era era => Term era (Data era) -> Term era DataHash
HashD Term era (Data era)
dat)) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map DataHash (Data era))
dataUniv)]
        )
      ]
  , Term era (Set (Datum era))
datumsSet forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall x era. Ord x => Term era [x] -> Target era (Set x)
listToSetTarget Term era [Datum era]
datums
  , case forall era. Proof era -> TxOutWit era
whichTxOut Proof era
p of
      TxOutWit era
TxOutShelleyToMary ->
        forall era fs t.
(Era era, FromList fs t, Eq t) =>
Term era Size -> Term era fs -> Pat era t -> [Pred era] -> Pred era
ForEach
          (forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat
              Rep era (TxOutF era)
outR
              [ forall era t s. Field era t s -> Arg era t
Arg forall era. Reflect era => Field era (TxOutF era) Addr
txoutAddressF
              , forall era t s. Field era t s -> [Pat era s] -> Arg era t
ArgPs forall era. Reflect era => Field era (TxOutF era) (ValueF era)
txoutAmountF [forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t s. Field era t s -> Arg era t
Arg forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t s. Field era t s -> Arg era t
Arg forall era. Reflect era => Field era (ValueF era) MultiAsset
valueFMultiAssetF]]
              ]
          )
          [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Reflect era => Term era Addr
txoutAddress) forall era. Era era => Term era (Set Addr)
addrUniv
          , forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (forall a b. b -> Either a b
Right forall era. Reflect era => Term era (ValueF era)
txoutAmount) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin, forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) forall era. Reflect era => Term era MultiAsset
valueFMultiAsset]
          , -- , SumsTo (Left (Coin 1)) balanceCoin EQL [One valCoin]
            forall era c.
(Era era, Adds c) =>
c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumSplit (Integer -> Coin
Coin Integer
1) Term era Coin
balanceCoin OrdCond
EQL [forall era c. Term era c -> Sum era c
One forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Reflect era => Term era MultiAsset
valueFMultiAsset (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"multiAsset" (forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
      TxOutWit era
TxOutAlonzoToAlonzo ->
        forall era fs t.
(Era era, FromList fs t, Eq t) =>
Term era Size -> Term era fs -> Pat era t -> [Pred era] -> Pred era
ForEach
          (forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat -- analog to Haskell pattern (TxOut{txoutAddress, txoutAmount{valCoin}, txoutDataHash})
              (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)
              [ forall era t s. Field era t s -> Arg era t
Arg forall era. Reflect era => Field era (TxOutF era) Addr
txoutAddressF
              , forall era t s. Field era t s -> [Pat era s] -> Arg era t
ArgPs forall era. Reflect era => Field era (TxOutF era) (ValueF era)
txoutAmountF [forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat Rep era (ValueF era)
valueR [forall era t s. Field era t s -> Arg era t
Arg forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t s. Field era t s -> Arg era t
Arg forall era. Reflect era => Field era (ValueF era) MultiAsset
valueFMultiAssetF]]
              , forall era t s. Field era t s -> Arg era t
Arg forall era.
(Reflect era, AlonzoEraTxOut era) =>
Field era (TxOutF era) (Maybe DataHash)
txoutDataHashF
              ]
          )
          [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Reflect era => Term era Addr
txoutAddress) forall era. Era era => Term era (Set Addr)
addrUniv
          , forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (forall a b. b -> Either a b
Right forall era. Reflect era => Term era (ValueF era)
txoutAmount) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe forall era.
(Reflect era, AlonzoEraTxOut era) =>
Term era (Maybe DataHash)
txoutDataHash (forall era t. Term era t -> RootTarget era Void t
Simple Term era DataHash
hash) [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era DataHash
hash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map DataHash (Data era))
dataUniv)]
          , forall era c.
(Era era, Adds c) =>
c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumSplit (Integer -> Coin
Coin Integer
2) Term era Coin
balanceCoin OrdCond
EQL [forall era c. Term era c -> Sum era c
One forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Reflect era => Term era MultiAsset
valueFMultiAsset (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"multiAsset" (forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
      TxOutWit era
TxOutBabbageToConway ->
        forall era fs t.
(Era era, FromList fs t, Eq t) =>
Term era Size -> Term era fs -> Pat era t -> [Pred era] -> Pred era
ForEach
          (forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat
              (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)
              [ forall era t s. Field era t s -> Arg era t
Arg forall era. Reflect era => Field era (TxOutF era) Addr
txoutAddressF
              , forall era s t. Rep era s -> Term era t -> [Pat era t] -> Arg era s
argP Rep era (TxOutF era)
outR forall era. Reflect era => Term era (ValueF era)
txoutAmount [forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t s. Field era t s -> Arg era t
Arg forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t s. Field era t s -> Arg era t
Arg forall era. Reflect era => Field era (ValueF era) MultiAsset
valueFMultiAssetF]]
              , forall era t s. Field era t s -> Arg era t
Arg forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF
              , forall era t s. Field era t s -> Arg era t
Arg forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Datum era)
txoutDatumF
              ]
          )
          [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Reflect era => Term era Addr
txoutAddress) forall era. Era era => Term era (Set Addr)
addrUniv
          , forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (forall a b. b -> Either a b
Right forall era. Reflect era => Term era (ValueF era)
txoutAmount) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Maybe (ScriptF era))
txoutScript (forall era t. Term era t -> RootTarget era Void t
Simple Term era (ScriptF era)
script) [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left (forall era.
Reflect era =>
Term era (ScriptF era) -> Term era ScriptHash
HashS Term era (ScriptF era)
script)) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
spendscriptUniv Proof era
p))]
          , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Datum era)
txoutDatum) Term era (Set (Datum era))
datumsSet
          , forall era c.
(Era era, Adds c) =>
c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumSplit (Integer -> Coin
Coin Integer
2) Term era Coin
balanceCoin OrdCond
EQL [forall era c. Term era c -> Sum era c
One forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Reflect era => Term era MultiAsset
valueFMultiAsset (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"multiAsset" (forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
  ]
  where
    outR :: Rep era (TxOutF era)
outR = forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p
    valueR :: Rep era (ValueF era)
valueR = forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p
    script :: Term era (ScriptF era)
script = (forall era t. Era era => String -> Rep era t -> Term era t
var String
"x" (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
p))
    datums :: Term era [Datum era]
datums = forall era t. Era era => String -> Rep era t -> Term era t
var String
"datums" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era (Datum era)
DatumR)
    datumsSet :: Term era (Set (Datum era))
datumsSet = forall era t. Era era => String -> Rep era t -> Term era t
var String
"datumsSet" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (Datum era)
DatumR)
    hash :: Term era DataHash
hash = forall era t. Era era => String -> Rep era t -> Term era t
var String
"hash" forall era. Era era => Rep era DataHash
DataHashR
    dat :: Term era (Data era)
dat = forall era t. Era era => String -> Rep era t -> Term era t
var String
"dat" forall era. Era era => Rep era (Data era)
DataR

demo :: ReplMode -> IO ()
demo :: ReplMode -> IO ()
demo ReplMode
mode = do
  let proof :: Proof ConwayEra
proof = Proof ConwayEra
Conway
  Env ConwayEra
env <-
    forall a. Gen a -> IO a
generate
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Era era =>
Proof era -> OrderInfo -> [Pred era] -> Subst era -> Gen (Env era)
toolChain Proof ConwayEra
proof OrderInfo
standardOrderInfo (forall era.
Reflect era =>
UnivSize
-> Proof era
-> Term era Coin
-> Term era [TxOutF era]
-> [Pred era]
txOutPreds forall a. Default a => a
def Proof ConwayEra
proof (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
100)) (forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof ConwayEra
proof))
      )
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (forall era a. Era era => Env era -> Term era a -> IO ()
displayTerm Env ConwayEra
env (forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof ConwayEra
proof))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ConwayEra
proof Env ConwayEra
env String
""

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

main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall a. String -> IO a -> TestTree
testIO String
"Testing TxOut Stage" (ReplMode -> IO ()
demo ReplMode
Interactive)