{-# 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 = (Script era -> ScriptF era)
-> (Script era -> ScriptF era -> Script era)
-> Lens (Script era) (Script era) (ScriptF era) (ScriptF era)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (Proof era -> Script era -> ScriptF era
forall era. Proof era -> Script era -> ScriptF era
ScriptF Proof era
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 (f :: * -> *).
Functor f =>
(Maybe a -> f (Maybe a)) -> StrictMaybe a -> f (StrictMaybe a)
strictMaybeMaybeL = (StrictMaybe a -> Maybe a)
-> (StrictMaybe a -> Maybe a -> StrictMaybe a)
-> Lens (StrictMaybe a) (StrictMaybe a) (Maybe a) (Maybe a)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens StrictMaybe a -> Maybe a
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe ((Maybe a -> StrictMaybe a)
-> StrictMaybe a -> Maybe a -> StrictMaybe a
forall a b. a -> b -> a
const Maybe a -> StrictMaybe a
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 = (TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era)
forall era (f :: * -> *).
Functor f =>
(TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era)
txOutFL ((TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era))
-> ((Maybe (ScriptF era) -> f (Maybe (ScriptF era)))
    -> TxOut era -> f (TxOut era))
-> (Maybe (ScriptF era) -> f (Maybe (ScriptF era)))
-> TxOutF era
-> f (TxOutF era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictMaybe (Script era) -> f (StrictMaybe (Script era)))
-> TxOut era -> f (TxOut era)
forall era.
BabbageEraTxOut era =>
Lens' (TxOut era) (StrictMaybe (Script era))
Lens' (TxOut era) (StrictMaybe (Script era))
referenceScriptTxOutL ((StrictMaybe (Script era) -> f (StrictMaybe (Script era)))
 -> TxOut era -> f (TxOut era))
-> ((Maybe (ScriptF era) -> f (Maybe (ScriptF era)))
    -> StrictMaybe (Script era) -> f (StrictMaybe (Script era)))
-> (Maybe (ScriptF era) -> f (Maybe (ScriptF era)))
-> TxOut era
-> f (TxOut era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (Script era) -> f (Maybe (Script era)))
-> StrictMaybe (Script era) -> f (StrictMaybe (Script era))
forall a (f :: * -> *).
Functor f =>
(Maybe a -> f (Maybe a)) -> StrictMaybe a -> f (StrictMaybe a)
strictMaybeMaybeL ((Maybe (Script era) -> f (Maybe (Script era)))
 -> StrictMaybe (Script era) -> f (StrictMaybe (Script era)))
-> ((Maybe (ScriptF era) -> f (Maybe (ScriptF era)))
    -> Maybe (Script era) -> f (Maybe (Script era)))
-> (Maybe (ScriptF era) -> f (Maybe (ScriptF era)))
-> StrictMaybe (Script era)
-> f (StrictMaybe (Script era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (Script era) (ScriptF era)
-> Lens' (Maybe (Script era)) (Maybe (ScriptF era))
forall a b. Lens' a b -> Lens' (Maybe a) (Maybe b)
liftMaybeL (ScriptF era -> f (ScriptF era)) -> Script era -> f (Script era)
forall era. Reflect era => Lens' (Script era) (ScriptF 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 = (Maybe a -> Maybe b)
-> (Maybe a -> Maybe b -> Maybe a)
-> Lens (Maybe a) (Maybe a) (Maybe b) (Maybe b)
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) = b -> Maybe b
forall a. a -> Maybe a
Just (a
x a -> Getting b a b -> b
forall s a. s -> Getting a s a -> a
^. Getting b a b
Lens' a b
l)
    getter Maybe a
Nothing = Maybe b
forall a. Maybe a
Nothing
    setter :: Maybe a -> Maybe b -> Maybe a
setter (Just a
a) (Just b
b) = a -> Maybe a
forall a. a -> Maybe a
Just (a
a a -> (a -> a) -> a
forall a b. a -> (a -> b) -> b
& (b -> Identity b) -> a -> Identity a
Lens' a b
l ((b -> Identity b) -> a -> Identity a) -> b -> a -> a
forall s t a b. ASetter s t a b -> b -> s -> t
.~ b
b)
    setter (Just a
_a) Maybe b
Nothing = Maybe a
forall a. Maybe a
Nothing -- Type wise this Nothing could be (Just a), but that is wrong
    setter Maybe a
Nothing Maybe b
_ = Maybe a
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 = String
-> Rep era (Maybe (ScriptF era))
-> Rep era (TxOutF era)
-> Lens' (TxOutF era) (Maybe (ScriptF era))
-> Field era (TxOutF era) (Maybe (ScriptF era))
forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field String
"txoutScript" (Rep era (ScriptF era) -> Rep era (Maybe (ScriptF era))
forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR (Proof era -> Rep era (ScriptF era)
forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
forall era. Reflect era => Proof era
reify)) (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
forall era. Reflect era => Proof era
reify) (Maybe (ScriptF era) -> f (Maybe (ScriptF era)))
-> TxOutF era -> f (TxOutF era)
forall era.
(Reflect era, BabbageEraTxOut era) =>
Lens' (TxOutF era) (Maybe (ScriptF 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 = Field era (TxOutF era) (Maybe (ScriptF era))
-> Term era (Maybe (ScriptF era))
forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era (TxOutF era) (Maybe (ScriptF era))
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 = String
-> Rep era (Datum era)
-> Rep era (TxOutF era)
-> Lens' (TxOutF era) (Datum era)
-> Field era (TxOutF era) (Datum era)
forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field String
"txoutDatumF" Rep era (Datum era)
forall era. Era era => Rep era (Datum era)
DatumR (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
forall era. Reflect era => Proof era
reify) ((TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era)
forall era (f :: * -> *).
Functor f =>
(TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era)
txOutFL ((TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era))
-> ((Datum era -> f (Datum era)) -> TxOut era -> f (TxOut era))
-> (Datum era -> f (Datum era))
-> TxOutF era
-> f (TxOutF era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Datum era -> f (Datum era)) -> TxOut era -> f (TxOut era)
forall era. BabbageEraTxOut era => Lens' (TxOut era) (Datum 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 = Field era (TxOutF era) (Datum era) -> Term era (Datum era)
forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era (TxOutF era) (Datum era)
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 =
  String
-> Rep era (Maybe DataHash)
-> Rep era (TxOutF era)
-> Lens' (TxOutF era) (Maybe DataHash)
-> Field era (TxOutF era) (Maybe DataHash)
forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field
    String
"txoutDataHashF"
    (Rep era DataHash -> Rep era (Maybe DataHash)
forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR Rep era DataHash
forall era. Era era => Rep era DataHash
DataHashR)
    (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
forall era. Reflect era => Proof era
reify)
    ((TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era)
forall era (f :: * -> *).
Functor f =>
(TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era)
txOutFL ((TxOut era -> f (TxOut era)) -> TxOutF era -> f (TxOutF era))
-> ((Maybe DataHash -> f (Maybe DataHash))
    -> TxOut era -> f (TxOut era))
-> (Maybe DataHash -> f (Maybe DataHash))
-> TxOutF era
-> f (TxOutF era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictMaybe DataHash -> f (StrictMaybe DataHash))
-> TxOut era -> f (TxOut era)
forall era.
AlonzoEraTxOut era =>
Lens' (TxOut era) (StrictMaybe DataHash)
Lens' (TxOut era) (StrictMaybe DataHash)
dataHashTxOutL ((StrictMaybe DataHash -> f (StrictMaybe DataHash))
 -> TxOut era -> f (TxOut era))
-> ((Maybe DataHash -> f (Maybe DataHash))
    -> StrictMaybe DataHash -> f (StrictMaybe DataHash))
-> (Maybe DataHash -> f (Maybe DataHash))
-> TxOut era
-> f (TxOut era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe DataHash -> f (Maybe DataHash))
-> StrictMaybe DataHash -> f (StrictMaybe DataHash)
forall a (f :: * -> *).
Functor f =>
(Maybe a -> f (Maybe a)) -> StrictMaybe a -> f (StrictMaybe a)
strictMaybeMaybeL)

txoutDataHash :: (Reflect era, AlonzoEraTxOut era) => Term era (Maybe DataHash)
txoutDataHash :: forall era.
(Reflect era, AlonzoEraTxOut era) =>
Term era (Maybe DataHash)
txoutDataHash = Field era (TxOutF era) (Maybe DataHash)
-> Term era (Maybe DataHash)
forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era (TxOutF era) (Maybe DataHash)
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 :: Int
usDatumFreq :: UnivSize -> Int
usDatumFreq} Proof era
p Term era Coin
balanceCoin Term era [TxOutF era]
outputS =
  [ Term era Size
-> Term era [Datum era]
-> [(Int, Target era (Datum era), [Pred era])]
-> Pred era
forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
      (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
6 Int
6)
      Term era [Datum era]
datums
      [ (Int
1, Term era (Datum era) -> Target era (Datum era)
forall era t. Term era t -> RootTarget era Void t
Simple (Rep era (Datum era) -> Datum era -> Term era (Datum era)
forall era t. Rep era t -> t -> Term era t
Lit Rep era (Datum era)
forall era. Era era => Rep era (Datum era)
DatumR Datum era
forall era. Datum era
NoDatum), [])
      , (Int
1, String
-> (DataHash -> Datum era)
-> RootTarget era Void (DataHash -> Datum era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"DatumHash" DataHash -> Datum era
forall era. DataHash -> Datum era
DatumHash RootTarget era Void (DataHash -> Datum era)
-> Term era DataHash -> Target era (Datum era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era DataHash
hash, [Direct (Term era DataHash) -> Term era (Set DataHash) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era DataHash -> Direct (Term era DataHash)
forall a b. a -> Either a b
Left Term era DataHash
hash) (Term era (Map DataHash (Data era)) -> Term era (Set DataHash)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map DataHash (Data era))
forall era. Era era => Term era (Map DataHash (Data era))
dataUniv)])
      ,
        ( Int
usDatumFreq
        , String
-> (Data era -> Datum era)
-> RootTarget era Void (Data era -> Datum era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"Datum" (BinaryData era -> Datum era
forall era. BinaryData era -> Datum era
Datum (BinaryData era -> Datum era)
-> (Data era -> BinaryData era) -> Data era -> Datum era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Data era -> BinaryData era
forall era. Data era -> BinaryData era
dataToBinaryData)
            RootTarget era Void (Data era -> Datum era)
-> Term era (Data era) -> Target era (Datum era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Data era)
dat
        , [Direct (Term era DataHash) -> Term era (Set DataHash) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era DataHash -> Direct (Term era DataHash)
forall a b. a -> Either a b
Left (Term era (Data era) -> Term era DataHash
forall era. Era era => Term era (Data era) -> Term era DataHash
HashD Term era (Data era)
dat)) (Term era (Map DataHash (Data era)) -> Term era (Set DataHash)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map DataHash (Data era))
forall era. Era era => Term era (Map DataHash (Data era))
dataUniv)]
        )
      ]
  , Term era (Set (Datum era))
datumsSet Term era (Set (Datum era))
-> RootTarget era Void (Set (Datum era)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era [Datum era] -> RootTarget era Void (Set (Datum era))
forall x era. Ord x => Term era [x] -> Target era (Set x)
listToSetTarget Term era [Datum era]
datums
  , case Proof era -> TxOutWit era
forall era. Proof era -> TxOutWit era
whichTxOut Proof era
p of
      TxOutWit era
TxOutShelleyToMary ->
        Term era Size
-> Term era [TxOutF era]
-> Pat era (TxOutF era)
-> [Pred era]
-> Pred era
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
          (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( Rep era (TxOutF era)
-> [Arg era (TxOutF era)] -> Pat era (TxOutF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat
              Rep era (TxOutF era)
outR
              [ Field era (TxOutF era) Addr -> Arg era (TxOutF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (TxOutF era) Addr
forall era. Reflect era => Field era (TxOutF era) Addr
txoutAddressF
              , Field era (TxOutF era) (ValueF era)
-> [Pat era (ValueF era)] -> Arg era (TxOutF era)
forall era t s. Field era t s -> [Pat era s] -> Arg era t
ArgPs Field era (TxOutF era) (ValueF era)
forall era. Reflect era => Field era (TxOutF era) (ValueF era)
txoutAmountF [Rep era (ValueF era)
-> [Arg era (ValueF era)] -> Pat era (ValueF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [Field era (ValueF era) Coin -> Arg era (ValueF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (ValueF era) Coin
forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], Rep era (ValueF era)
-> [Arg era (ValueF era)] -> Pat era (ValueF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [Field era (ValueF era) MultiAsset -> Arg era (ValueF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (ValueF era) MultiAsset
forall era. Reflect era => Field era (ValueF era) MultiAsset
valueFMultiAssetF]]
              ]
          )
          [ Direct (Term era Addr) -> Term era (Set Addr) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era Addr -> Direct (Term era Addr)
forall a b. a -> Either a b
Left Term era Addr
forall era. Reflect era => Term era Addr
txoutAddress) Term era (Set Addr)
forall era. Era era => Term era (Set Addr)
addrUniv
          , Direct (Term era (ValueF era))
-> [AnyF era (ValueF era)] -> Pred era
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (Term era (ValueF era) -> Direct (Term era (ValueF era))
forall a b. b -> Either a b
Right Term era (ValueF era)
forall era. Reflect era => Term era (ValueF era)
txoutAmount) [Rep era (ValueF era) -> Term era Coin -> AnyF era (ValueF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) Term era Coin
forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin, Rep era (ValueF era)
-> Term era MultiAsset -> AnyF era (ValueF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) Term era MultiAsset
forall era. Reflect era => Term era MultiAsset
valueFMultiAsset]
          , -- , SumsTo (Left (Coin 1)) balanceCoin EQL [One valCoin]
            Coin -> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
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 [Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , Term era MultiAsset
-> RootTarget era Void (Gen MultiAsset) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era MultiAsset
forall era. Reflect era => Term era MultiAsset
valueFMultiAsset (String
-> (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
-> RootTarget
     era Void (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"multiAsset" (UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size) RootTarget
  era Void (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
-> Term era (Map ScriptHash (ScriptF era))
-> RootTarget era Void (Gen MultiAsset)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
      TxOutWit era
TxOutAlonzoToAlonzo ->
        Term era Size
-> Term era [TxOutF era]
-> Pat era (TxOutF era)
-> [Pred era]
-> Pred era
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
          (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( Rep era (TxOutF era)
-> [Arg era (TxOutF era)] -> Pat era (TxOutF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat -- analog to Haskell pattern (TxOut{txoutAddress, txoutAmount{valCoin}, txoutDataHash})
              (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)
              [ Field era (TxOutF era) Addr -> Arg era (TxOutF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (TxOutF era) Addr
forall era. Reflect era => Field era (TxOutF era) Addr
txoutAddressF
              , Field era (TxOutF era) (ValueF era)
-> [Pat era (ValueF era)] -> Arg era (TxOutF era)
forall era t s. Field era t s -> [Pat era s] -> Arg era t
ArgPs Field era (TxOutF era) (ValueF era)
forall era. Reflect era => Field era (TxOutF era) (ValueF era)
txoutAmountF [Rep era (ValueF era)
-> [Arg era (ValueF era)] -> Pat era (ValueF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat Rep era (ValueF era)
valueR [Field era (ValueF era) Coin -> Arg era (ValueF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (ValueF era) Coin
forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], Rep era (ValueF era)
-> [Arg era (ValueF era)] -> Pat era (ValueF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [Field era (ValueF era) MultiAsset -> Arg era (ValueF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (ValueF era) MultiAsset
forall era. Reflect era => Field era (ValueF era) MultiAsset
valueFMultiAssetF]]
              , Field era (TxOutF era) (Maybe DataHash) -> Arg era (TxOutF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (TxOutF era) (Maybe DataHash)
forall era.
(Reflect era, AlonzoEraTxOut era) =>
Field era (TxOutF era) (Maybe DataHash)
txoutDataHashF
              ]
          )
          [ Direct (Term era Addr) -> Term era (Set Addr) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era Addr -> Direct (Term era Addr)
forall a b. a -> Either a b
Left Term era Addr
forall era. Reflect era => Term era Addr
txoutAddress) Term era (Set Addr)
forall era. Era era => Term era (Set Addr)
addrUniv
          , Direct (Term era (ValueF era))
-> [AnyF era (ValueF era)] -> Pred era
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (Term era (ValueF era) -> Direct (Term era (ValueF era))
forall a b. b -> Either a b
Right Term era (ValueF era)
forall era. Reflect era => Term era (ValueF era)
txoutAmount) [Rep era (ValueF era) -> Term era Coin -> AnyF era (ValueF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) Term era Coin
forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , Term era (Maybe DataHash)
-> RootTarget era Void DataHash -> [Pred era] -> Pred era
forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe Term era (Maybe DataHash)
forall era.
(Reflect era, AlonzoEraTxOut era) =>
Term era (Maybe DataHash)
txoutDataHash (Term era DataHash -> RootTarget era Void DataHash
forall era t. Term era t -> RootTarget era Void t
Simple Term era DataHash
hash) [Direct (Term era DataHash) -> Term era (Set DataHash) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era DataHash -> Direct (Term era DataHash)
forall a b. a -> Either a b
Left Term era DataHash
hash) (Term era (Map DataHash (Data era)) -> Term era (Set DataHash)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map DataHash (Data era))
forall era. Era era => Term era (Map DataHash (Data era))
dataUniv)]
          , Coin -> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
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 [Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , Term era MultiAsset
-> RootTarget era Void (Gen MultiAsset) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era MultiAsset
forall era. Reflect era => Term era MultiAsset
valueFMultiAsset (String
-> (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
-> RootTarget
     era Void (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"multiAsset" (UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size) RootTarget
  era Void (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
-> Term era (Map ScriptHash (ScriptF era))
-> RootTarget era Void (Gen MultiAsset)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
      TxOutWit era
TxOutBabbageToConway ->
        Term era Size
-> Term era [TxOutF era]
-> Pat era (TxOutF era)
-> [Pred era]
-> Pred era
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
          (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( Rep era (TxOutF era)
-> [Arg era (TxOutF era)] -> Pat era (TxOutF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat
              (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)
              [ Field era (TxOutF era) Addr -> Arg era (TxOutF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (TxOutF era) Addr
forall era. Reflect era => Field era (TxOutF era) Addr
txoutAddressF
              , Rep era (TxOutF era)
-> Term era (ValueF era)
-> [Pat era (ValueF era)]
-> Arg era (TxOutF era)
forall era s t. Rep era s -> Term era t -> [Pat era t] -> Arg era s
argP Rep era (TxOutF era)
outR Term era (ValueF era)
forall era. Reflect era => Term era (ValueF era)
txoutAmount [Rep era (ValueF era)
-> [Arg era (ValueF era)] -> Pat era (ValueF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [Field era (ValueF era) Coin -> Arg era (ValueF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (ValueF era) Coin
forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], Rep era (ValueF era)
-> [Arg era (ValueF era)] -> Pat era (ValueF era)
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [Field era (ValueF era) MultiAsset -> Arg era (ValueF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (ValueF era) MultiAsset
forall era. Reflect era => Field era (ValueF era) MultiAsset
valueFMultiAssetF]]
              , Field era (TxOutF era) (Maybe (ScriptF era))
-> Arg era (TxOutF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (TxOutF era) (Maybe (ScriptF era))
forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF
              , Field era (TxOutF era) (Datum era) -> Arg era (TxOutF era)
forall era t s. Field era t s -> Arg era t
Arg Field era (TxOutF era) (Datum era)
forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Datum era)
txoutDatumF
              ]
          )
          [ Direct (Term era Addr) -> Term era (Set Addr) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era Addr -> Direct (Term era Addr)
forall a b. a -> Either a b
Left Term era Addr
forall era. Reflect era => Term era Addr
txoutAddress) Term era (Set Addr)
forall era. Era era => Term era (Set Addr)
addrUniv
          , Direct (Term era (ValueF era))
-> [AnyF era (ValueF era)] -> Pred era
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (Term era (ValueF era) -> Direct (Term era (ValueF era))
forall a b. b -> Either a b
Right Term era (ValueF era)
forall era. Reflect era => Term era (ValueF era)
txoutAmount) [Rep era (ValueF era) -> Term era Coin -> AnyF era (ValueF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) Term era Coin
forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , Term era (Maybe (ScriptF era))
-> RootTarget era Void (ScriptF era) -> [Pred era] -> Pred era
forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe Term era (Maybe (ScriptF era))
forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Maybe (ScriptF era))
txoutScript (Term era (ScriptF era) -> RootTarget era Void (ScriptF era)
forall era t. Term era t -> RootTarget era Void t
Simple Term era (ScriptF era)
script) [Direct (Term era ScriptHash)
-> Term era (Set ScriptHash) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era ScriptHash -> Direct (Term era ScriptHash)
forall a b. a -> Either a b
Left (Term era (ScriptF era) -> Term era ScriptHash
forall era.
Reflect era =>
Term era (ScriptF era) -> Term era ScriptHash
HashS Term era (ScriptF era)
script)) (Term era (Map ScriptHash (ScriptF era))
-> Term era (Set ScriptHash)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
spendscriptUniv Proof era
p))]
          , Direct (Term era (Datum era))
-> Term era (Set (Datum era)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (Datum era) -> Direct (Term era (Datum era))
forall a b. a -> Either a b
Left Term era (Datum era)
forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Datum era)
txoutDatum) Term era (Set (Datum era))
datumsSet
          , Coin -> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
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 [Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , Term era MultiAsset
-> RootTarget era Void (Gen MultiAsset) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era MultiAsset
forall era. Reflect era => Term era MultiAsset
valueFMultiAsset (String
-> (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
-> RootTarget
     era Void (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"multiAsset" (UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
forall era.
UnivSize -> Map ScriptHash (ScriptF era) -> Gen MultiAsset
multiAsset UnivSize
size) RootTarget
  era Void (Map ScriptHash (ScriptF era) -> Gen MultiAsset)
-> Term era (Map ScriptHash (ScriptF era))
-> RootTarget era Void (Gen MultiAsset)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
  ]
  where
    outR :: Rep era (TxOutF era)
outR = Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p
    valueR :: Rep era (ValueF era)
valueR = Proof era -> Rep era (ValueF era)
forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p
    script :: Term era (ScriptF era)
script = (String -> Rep era (ScriptF era) -> Term era (ScriptF era)
forall era t. Era era => String -> Rep era t -> Term era t
var String
"x" (Proof era -> Rep era (ScriptF era)
forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
p))
    datums :: Term era [Datum era]
datums = String -> Rep era [Datum era] -> Term era [Datum era]
forall era t. Era era => String -> Rep era t -> Term era t
var String
"datums" (Rep era (Datum era) -> Rep era [Datum era]
forall era a. Rep era a -> Rep era [a]
ListR Rep era (Datum era)
forall era. Era era => Rep era (Datum era)
DatumR)
    datumsSet :: Term era (Set (Datum era))
datumsSet = String -> Rep era (Set (Datum era)) -> Term era (Set (Datum era))
forall era t. Era era => String -> Rep era t -> Term era t
var String
"datumsSet" (Rep era (Datum era) -> Rep era (Set (Datum era))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era (Datum era)
forall era. Era era => Rep era (Datum era)
DatumR)
    hash :: Term era DataHash
hash = String -> Rep era DataHash -> Term era DataHash
forall era t. Era era => String -> Rep era t -> Term era t
var String
"hash" Rep era DataHash
forall era. Era era => Rep era DataHash
DataHashR
    dat :: Term era (Data era)
dat = String -> Rep era (Data era) -> Term era (Data era)
forall era t. Era era => String -> Rep era t -> Term era t
var String
"dat" Rep era (Data era)
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 <-
    Gen (Env ConwayEra) -> IO (Env ConwayEra)
forall a. Gen a -> IO a
generate
      ( Subst ConwayEra -> Gen (Subst ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst ConwayEra
forall era. Subst era
emptySubst
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
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 ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Env ConwayEra)) -> Gen (Env ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra
-> OrderInfo
-> [Pred ConwayEra]
-> Subst ConwayEra
-> Gen (Env ConwayEra)
forall era.
Era era =>
Proof era -> OrderInfo -> [Pred era] -> Subst era -> Gen (Env era)
toolChain Proof ConwayEra
proof OrderInfo
standardOrderInfo (UnivSize
-> Proof ConwayEra
-> Term ConwayEra Coin
-> Term ConwayEra [TxOutF ConwayEra]
-> [Pred ConwayEra]
forall era.
Reflect era =>
UnivSize
-> Proof era
-> Term era Coin
-> Term era [TxOutF era]
-> [Pred era]
txOutPreds UnivSize
forall a. Default a => a
def Proof ConwayEra
proof (Rep ConwayEra Coin -> Coin -> Term ConwayEra Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep ConwayEra Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
100)) (Proof ConwayEra -> Term ConwayEra [TxOutF ConwayEra]
forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof ConwayEra
proof))
      )
  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) (Env ConwayEra -> Term ConwayEra [TxOutF ConwayEra] -> IO ()
forall era a. Era era => Env era -> Term era a -> IO ()
displayTerm Env ConwayEra
env (Proof ConwayEra -> Term ConwayEra [TxOutF ConwayEra]
forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof ConwayEra
proof))
  ReplMode -> Proof ConwayEra -> Env ConwayEra -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ConwayEra
proof Env ConwayEra
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)

main :: IO ()
main :: IO ()
main = 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)