{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Constrained.Conway.Instances.TxBody where

import Cardano.Ledger.Address (RewardAccount (..))
import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.Allegra.TxBody (TxBody (..))
import Cardano.Ledger.Alonzo (AlonzoEra)
import Cardano.Ledger.Alonzo.TxBody (TxBody (..))
import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.Babbage.TxBody (TxBody (..))
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.Binary (Sized (..))
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Mary (MaryEra, TxBody (..))
import Cardano.Ledger.Mary.Value (MultiAsset (..))
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.PParams (Update (..))
import Cardano.Ledger.TxIn (TxIn (..))
import Constrained.API hiding (Sized)
import Constrained.Generic
import Data.Foldable (toList)
import Data.Map.Strict (Map)
import qualified Data.Sequence.Strict as SS (fromList)
import Data.Set (Set)
import Data.Typeable
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger

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

instance Typeable era => HasSimpleRep (Update era)

instance EraSpecPParams era => HasSpec (Update era)

-- =========================================
-- ShelleyTxBody

-- | This is an abstraction of the Pattern ShelleyTxBody, that uses [x] instead of (StrictSeq x)
--   and (Maybe x) instead of (StrictMaybe x). It transforms bewtween the two, in the toSimpleRep
--   and fromSimpleRep methods. This makes it much easier to write Specifications, because
--   the Constrained packaage knows about Lists and Maybe.
type ShelleyTxBodyTypes =
  '[ Set TxIn
   , [TxOut ShelleyEra]
   , [TxCert ShelleyEra]
   , Map RewardAccount Coin
   , Coin
   , SlotNo
   , Maybe (Update ShelleyEra)
   , Maybe TxAuxDataHash
   ]

instance HasSimpleRep (TxBody TopTx ShelleyEra) where
  type SimpleRep (TxBody TopTx ShelleyEra) = SOP '["ShelleyTxBody" ::: ShelleyTxBodyTypes]
  toSimpleRep :: TxBody TopTx ShelleyEra -> SimpleRep (TxBody TopTx ShelleyEra)
toSimpleRep (ShelleyTxBody Set TxIn
is StrictSeq (TxOut ShelleyEra)
os StrictSeq (TxCert ShelleyEra)
certs Withdrawals
w Coin
c SlotNo
s StrictMaybe (Update ShelleyEra)
up StrictMaybe TxAuxDataHash
aux) =
    forall (c :: Symbol) (constrs :: [*]).
Inject c constrs (SOP constrs) =>
FunTy (ConstrOf c constrs) (SOP constrs)
inject @"ShelleyTxBody" @'["ShelleyTxBody" ::: ShelleyTxBodyTypes]
      Set TxIn
is
      (StrictSeq (ShelleyTxOut ShelleyEra) -> [ShelleyTxOut ShelleyEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxOut ShelleyEra)
StrictSeq (ShelleyTxOut ShelleyEra)
os)
      (StrictSeq (ShelleyTxCert ShelleyEra) -> [ShelleyTxCert ShelleyEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxCert ShelleyEra)
StrictSeq (ShelleyTxCert ShelleyEra)
certs)
      (Withdrawals -> Map RewardAccount Coin
unWithdrawals Withdrawals
w)
      Coin
c
      SlotNo
s
      (StrictMaybe (Update ShelleyEra) -> Maybe (Update ShelleyEra)
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe (Update ShelleyEra)
up)
      (StrictMaybe TxAuxDataHash -> Maybe TxAuxDataHash
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe TxAuxDataHash
aux)

  fromSimpleRep :: SimpleRep (TxBody TopTx ShelleyEra) -> TxBody TopTx ShelleyEra
fromSimpleRep SimpleRep (TxBody TopTx ShelleyEra)
rep =
    forall (constrs :: [*]) r.
SOPLike constrs r =>
SOP constrs -> ALG constrs r
algebra @'["ShelleyTxBody" ::: ShelleyTxBodyTypes]
      SOP '["ShelleyTxBody" ::: ShelleyTxBodyTypes]
SimpleRep (TxBody TopTx ShelleyEra)
rep
      ( \Set TxIn
is [ShelleyTxOut ShelleyEra]
os [ShelleyTxCert ShelleyEra]
certs Map RewardAccount Coin
w Coin
c SlotNo
s Maybe (Update ShelleyEra)
up Maybe TxAuxDataHash
aux ->
          Set TxIn
-> StrictSeq (TxOut ShelleyEra)
-> StrictSeq (TxCert ShelleyEra)
-> Withdrawals
-> Coin
-> SlotNo
-> StrictMaybe (Update ShelleyEra)
-> StrictMaybe TxAuxDataHash
-> TxBody TopTx ShelleyEra
ShelleyTxBody
            Set TxIn
is
            ([ShelleyTxOut ShelleyEra] -> StrictSeq (ShelleyTxOut ShelleyEra)
forall a. [a] -> StrictSeq a
SS.fromList [ShelleyTxOut ShelleyEra]
os)
            ([ShelleyTxCert ShelleyEra] -> StrictSeq (ShelleyTxCert ShelleyEra)
forall a. [a] -> StrictSeq a
SS.fromList [ShelleyTxCert ShelleyEra]
certs)
            (Map RewardAccount Coin -> Withdrawals
Withdrawals Map RewardAccount Coin
w)
            Coin
c
            SlotNo
s
            (Maybe (Update ShelleyEra) -> StrictMaybe (Update ShelleyEra)
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe (Update ShelleyEra)
up)
            (Maybe TxAuxDataHash -> StrictMaybe TxAuxDataHash
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe TxAuxDataHash
aux)
      )

instance HasSpec (TxBody TopTx ShelleyEra)

-- =======================================================
-- AllegraTxBody

-- | This is an abstraction of the Pattern AllegraTxBody, that uses [x] instead of (StrictSeq x)
--   and (Maybe x) instead of (StrictMaybe x). It transforms bewtween the two, in the toSimpleRep
--   and fromSimpleRep methods. This makes it much easier to write Specifications, because
--   the Constrained packaage knows about Lists and Maybe.
type AllegraTxBodyTypes =
  '[ Set TxIn
   , [TxOut AllegraEra]
   , [TxCert AllegraEra]
   , Map RewardAccount Coin
   , Coin
   , ValidityInterval
   , Maybe (Update AllegraEra)
   , Maybe TxAuxDataHash
   ]

instance HasSimpleRep (TxBody TopTx AllegraEra) where
  type SimpleRep (TxBody TopTx AllegraEra) = SOP '["AllegraTxBody" ::: AllegraTxBodyTypes]
  toSimpleRep :: TxBody TopTx AllegraEra -> SimpleRep (TxBody TopTx AllegraEra)
toSimpleRep (AllegraTxBody Set TxIn
is StrictSeq (TxOut AllegraEra)
os StrictSeq (TxCert AllegraEra)
certs Withdrawals
w Coin
c ValidityInterval
vi StrictMaybe (Update AllegraEra)
up StrictMaybe TxAuxDataHash
aux) =
    forall (c :: Symbol) (constrs :: [*]).
Inject c constrs (SOP constrs) =>
FunTy (ConstrOf c constrs) (SOP constrs)
inject @"AllegraTxBody" @'["AllegraTxBody" ::: AllegraTxBodyTypes]
      Set TxIn
is
      (StrictSeq (ShelleyTxOut AllegraEra) -> [ShelleyTxOut AllegraEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxOut AllegraEra)
StrictSeq (ShelleyTxOut AllegraEra)
os)
      (StrictSeq (ShelleyTxCert AllegraEra) -> [ShelleyTxCert AllegraEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxCert AllegraEra)
StrictSeq (ShelleyTxCert AllegraEra)
certs)
      (Withdrawals -> Map RewardAccount Coin
unWithdrawals Withdrawals
w)
      Coin
c
      ValidityInterval
vi
      (StrictMaybe (Update AllegraEra) -> Maybe (Update AllegraEra)
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe (Update AllegraEra)
up)
      (StrictMaybe TxAuxDataHash -> Maybe TxAuxDataHash
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe TxAuxDataHash
aux)

  fromSimpleRep :: SimpleRep (TxBody TopTx AllegraEra) -> TxBody TopTx AllegraEra
fromSimpleRep SimpleRep (TxBody TopTx AllegraEra)
rep =
    forall (constrs :: [*]) r.
SOPLike constrs r =>
SOP constrs -> ALG constrs r
algebra @'["AllegraTxBody" ::: AllegraTxBodyTypes]
      SOP '["AllegraTxBody" ::: AllegraTxBodyTypes]
SimpleRep (TxBody TopTx AllegraEra)
rep
      ( \Set TxIn
is [ShelleyTxOut AllegraEra]
os [ShelleyTxCert AllegraEra]
certs Map RewardAccount Coin
w Coin
c ValidityInterval
vi Maybe (Update AllegraEra)
up Maybe TxAuxDataHash
aux ->
          Set TxIn
-> StrictSeq (TxOut AllegraEra)
-> StrictSeq (TxCert AllegraEra)
-> Withdrawals
-> Coin
-> ValidityInterval
-> StrictMaybe (Update AllegraEra)
-> StrictMaybe TxAuxDataHash
-> TxBody TopTx AllegraEra
(EraTxOut AllegraEra, EraTxCert AllegraEra) =>
Set TxIn
-> StrictSeq (TxOut AllegraEra)
-> StrictSeq (TxCert AllegraEra)
-> Withdrawals
-> Coin
-> ValidityInterval
-> StrictMaybe (Update AllegraEra)
-> StrictMaybe TxAuxDataHash
-> TxBody TopTx AllegraEra
AllegraTxBody
            Set TxIn
is
            ([ShelleyTxOut AllegraEra] -> StrictSeq (ShelleyTxOut AllegraEra)
forall a. [a] -> StrictSeq a
SS.fromList [ShelleyTxOut AllegraEra]
os)
            ([ShelleyTxCert AllegraEra] -> StrictSeq (ShelleyTxCert AllegraEra)
forall a. [a] -> StrictSeq a
SS.fromList [ShelleyTxCert AllegraEra]
certs)
            (Map RewardAccount Coin -> Withdrawals
Withdrawals Map RewardAccount Coin
w)
            Coin
c
            ValidityInterval
vi
            (Maybe (Update AllegraEra) -> StrictMaybe (Update AllegraEra)
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe (Update AllegraEra)
up)
            (Maybe TxAuxDataHash -> StrictMaybe TxAuxDataHash
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe TxAuxDataHash
aux)
      )

instance HasSpec (TxBody TopTx AllegraEra)

-- =========================================================================
-- MaryTxBody

-- | This is an abstraction of the Pattern MaryTxBody, that uses [x] instead of (StrictSeq x)
--   and (Maybe x) instead of (StrictMaybe x). It transforms between the abstractions and the
--   real types in the toSimpleRep and fromSimpleRep methods. This makes it much easier to
--   write Specifications, because the Constrained packaage knows about Lists and Maybe.
type MaryTxBodyTypes =
  '[ Set TxIn
   , [TxOut MaryEra]
   , [TxCert MaryEra]
   , Map RewardAccount Coin
   , Coin
   , ValidityInterval
   , Maybe (Update MaryEra)
   , Maybe TxAuxDataHash
   , MultiAsset
   ]

instance HasSimpleRep (TxBody TopTx MaryEra) where
  type SimpleRep (TxBody TopTx MaryEra) = SOP '["MaryTxBody" ::: MaryTxBodyTypes]
  toSimpleRep :: TxBody TopTx MaryEra -> SimpleRep (TxBody TopTx MaryEra)
toSimpleRep (MaryTxBody Set TxIn
is StrictSeq (TxOut MaryEra)
os StrictSeq (TxCert MaryEra)
certs Withdrawals
w Coin
c ValidityInterval
vi StrictMaybe (Update MaryEra)
up StrictMaybe TxAuxDataHash
aux MultiAsset
ma) =
    forall (c :: Symbol) (constrs :: [*]).
Inject c constrs (SOP constrs) =>
FunTy (ConstrOf c constrs) (SOP constrs)
inject @"MaryTxBody" @'["MaryTxBody" ::: MaryTxBodyTypes]
      Set TxIn
is
      (StrictSeq (ShelleyTxOut MaryEra) -> [ShelleyTxOut MaryEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxOut MaryEra)
StrictSeq (ShelleyTxOut MaryEra)
os)
      (StrictSeq (ShelleyTxCert MaryEra) -> [ShelleyTxCert MaryEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxCert MaryEra)
StrictSeq (ShelleyTxCert MaryEra)
certs)
      (Withdrawals -> Map RewardAccount Coin
unWithdrawals Withdrawals
w)
      Coin
c
      ValidityInterval
vi
      (StrictMaybe (Update MaryEra) -> Maybe (Update MaryEra)
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe (Update MaryEra)
up)
      (StrictMaybe TxAuxDataHash -> Maybe TxAuxDataHash
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe TxAuxDataHash
aux)
      MultiAsset
ma

  fromSimpleRep :: SimpleRep (TxBody TopTx MaryEra) -> TxBody TopTx MaryEra
fromSimpleRep SimpleRep (TxBody TopTx MaryEra)
rep =
    forall (constrs :: [*]) r.
SOPLike constrs r =>
SOP constrs -> ALG constrs r
algebra @'["MaryTxBody" ::: MaryTxBodyTypes]
      SOP '["MaryTxBody" ::: MaryTxBodyTypes]
SimpleRep (TxBody TopTx MaryEra)
rep
      ( \Set TxIn
is [ShelleyTxOut MaryEra]
os [ShelleyTxCert MaryEra]
certs Map RewardAccount Coin
w Coin
c ValidityInterval
vi Maybe (Update MaryEra)
up Maybe TxAuxDataHash
aux MultiAsset
ma ->
          Set TxIn
-> StrictSeq (TxOut MaryEra)
-> StrictSeq (TxCert MaryEra)
-> Withdrawals
-> Coin
-> ValidityInterval
-> StrictMaybe (Update MaryEra)
-> StrictMaybe TxAuxDataHash
-> MultiAsset
-> TxBody TopTx MaryEra
(EraTxOut MaryEra, EraTxCert MaryEra) =>
Set TxIn
-> StrictSeq (TxOut MaryEra)
-> StrictSeq (TxCert MaryEra)
-> Withdrawals
-> Coin
-> ValidityInterval
-> StrictMaybe (Update MaryEra)
-> StrictMaybe TxAuxDataHash
-> MultiAsset
-> TxBody TopTx MaryEra
MaryTxBody
            Set TxIn
is
            ([ShelleyTxOut MaryEra] -> StrictSeq (ShelleyTxOut MaryEra)
forall a. [a] -> StrictSeq a
SS.fromList [ShelleyTxOut MaryEra]
os)
            ([ShelleyTxCert MaryEra] -> StrictSeq (ShelleyTxCert MaryEra)
forall a. [a] -> StrictSeq a
SS.fromList [ShelleyTxCert MaryEra]
certs)
            (Map RewardAccount Coin -> Withdrawals
Withdrawals Map RewardAccount Coin
w)
            Coin
c
            ValidityInterval
vi
            (Maybe (Update MaryEra) -> StrictMaybe (Update MaryEra)
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe (Update MaryEra)
up)
            (Maybe TxAuxDataHash -> StrictMaybe TxAuxDataHash
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe TxAuxDataHash
aux)
            MultiAsset
ma
      )

instance HasSpec (TxBody TopTx MaryEra)

-- =================================================================================
-- AlonzoTxBody

-- | This is an abstraction of the Pattern AlonzoTxBody, that uses [x] instead of (StrictSeq x)
--   and (Maybe x) instead of (StrictMaybe x). It transforms between the abstractions and the
--   real types in the toSimpleRep and fromSimpleRep methods. This makes it much easier to
--   write Specifications, because the Constrained packaage knows about Lists and Maybe.
type AlonzoTxBodyTypes =
  '[ Set TxIn
   , Set TxIn
   , [TxOut AlonzoEra]
   , [TxCert AlonzoEra]
   , Map RewardAccount Coin
   , Coin
   , ValidityInterval
   , Maybe (Update AlonzoEra)
   , Set (KeyHash Guard)
   , MultiAsset
   , Maybe ScriptIntegrityHash
   , Maybe TxAuxDataHash
   , Maybe Network
   ]

instance HasSimpleRep (TxBody TopTx AlonzoEra) where
  type SimpleRep (TxBody TopTx AlonzoEra) = SOP '["AlonzoTxBody" ::: AlonzoTxBodyTypes]
  toSimpleRep :: TxBody TopTx AlonzoEra -> SimpleRep (TxBody TopTx AlonzoEra)
toSimpleRep (AlonzoTxBody Set TxIn
inputs Set TxIn
colinputs StrictSeq (TxOut AlonzoEra)
os StrictSeq (TxCert AlonzoEra)
certs Withdrawals
w Coin
c ValidityInterval
vi StrictMaybe (Update AlonzoEra)
up Set (KeyHash Guard)
kh MultiAsset
ma StrictMaybe ScriptIntegrityHash
ihash StrictMaybe TxAuxDataHash
aux StrictMaybe Network
nw) =
    forall (c :: Symbol) (constrs :: [*]).
Inject c constrs (SOP constrs) =>
FunTy (ConstrOf c constrs) (SOP constrs)
inject @"AlonzoTxBody" @'["AlonzoTxBody" ::: AlonzoTxBodyTypes]
      Set TxIn
inputs
      Set TxIn
colinputs
      (StrictSeq (AlonzoTxOut AlonzoEra) -> [AlonzoTxOut AlonzoEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxOut AlonzoEra)
StrictSeq (AlonzoTxOut AlonzoEra)
os)
      (StrictSeq (ShelleyTxCert AlonzoEra) -> [ShelleyTxCert AlonzoEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxCert AlonzoEra)
StrictSeq (ShelleyTxCert AlonzoEra)
certs)
      (Withdrawals -> Map RewardAccount Coin
unWithdrawals Withdrawals
w)
      Coin
c
      ValidityInterval
vi
      (StrictMaybe (Update AlonzoEra) -> Maybe (Update AlonzoEra)
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe (Update AlonzoEra)
up)
      Set (KeyHash Guard)
kh
      MultiAsset
ma
      (StrictMaybe ScriptIntegrityHash -> Maybe ScriptIntegrityHash
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe ScriptIntegrityHash
ihash)
      (StrictMaybe TxAuxDataHash -> Maybe TxAuxDataHash
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe TxAuxDataHash
aux)
      (StrictMaybe Network -> Maybe Network
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe Network
nw)

  fromSimpleRep :: SimpleRep (TxBody TopTx AlonzoEra) -> TxBody TopTx AlonzoEra
fromSimpleRep SimpleRep (TxBody TopTx AlonzoEra)
rep =
    forall (constrs :: [*]) r.
SOPLike constrs r =>
SOP constrs -> ALG constrs r
algebra @'["AlonzoTxBody" ::: AlonzoTxBodyTypes]
      SOP '["AlonzoTxBody" ::: AlonzoTxBodyTypes]
SimpleRep (TxBody TopTx AlonzoEra)
rep
      ( \Set TxIn
inputs Set TxIn
colinputs [AlonzoTxOut AlonzoEra]
os [ShelleyTxCert AlonzoEra]
certs Map RewardAccount Coin
w Coin
c ValidityInterval
vi Maybe (Update AlonzoEra)
up Set (KeyHash Guard)
kh MultiAsset
ma Maybe ScriptIntegrityHash
ihash Maybe TxAuxDataHash
aux Maybe Network
nw ->
          Set TxIn
-> Set TxIn
-> StrictSeq (TxOut AlonzoEra)
-> StrictSeq (TxCert AlonzoEra)
-> Withdrawals
-> Coin
-> ValidityInterval
-> StrictMaybe (Update AlonzoEra)
-> Set (KeyHash Guard)
-> MultiAsset
-> StrictMaybe ScriptIntegrityHash
-> StrictMaybe TxAuxDataHash
-> StrictMaybe Network
-> TxBody TopTx AlonzoEra
AlonzoTxBody
            Set TxIn
inputs
            Set TxIn
colinputs
            ([AlonzoTxOut AlonzoEra] -> StrictSeq (AlonzoTxOut AlonzoEra)
forall a. [a] -> StrictSeq a
SS.fromList [AlonzoTxOut AlonzoEra]
os)
            ([ShelleyTxCert AlonzoEra] -> StrictSeq (ShelleyTxCert AlonzoEra)
forall a. [a] -> StrictSeq a
SS.fromList [ShelleyTxCert AlonzoEra]
certs)
            (Map RewardAccount Coin -> Withdrawals
Withdrawals Map RewardAccount Coin
w)
            Coin
c
            ValidityInterval
vi
            (Maybe (Update AlonzoEra) -> StrictMaybe (Update AlonzoEra)
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe (Update AlonzoEra)
up)
            Set (KeyHash Guard)
kh
            MultiAsset
ma
            (Maybe ScriptIntegrityHash -> StrictMaybe ScriptIntegrityHash
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe ScriptIntegrityHash
ihash)
            (Maybe TxAuxDataHash -> StrictMaybe TxAuxDataHash
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe TxAuxDataHash
aux)
            (Maybe Network -> StrictMaybe Network
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe Network
nw)
      )

instance HasSpec (TxBody TopTx AlonzoEra)

-- =================================================================================
-- BabbageTxBody

-- | This is an abstraction of the Pattern BabbageTxBody, that uses [x] instead of (StrictSeq x)
--   and (Maybe x) instead of (StrictMaybe x). It transforms between the abstractions and the
--   real types in the toSimpleRep and fromSimpleRep methods. This makes it much easier to
--   write Specifications, because the Constrained packaage knows about Lists and Maybe.
type BabbageTxBodyTypes =
  '[ Set TxIn
   , Set TxIn
   , Set TxIn
   , [Sized (TxOut BabbageEra)]
   , Maybe (Sized (TxOut BabbageEra))
   , Maybe Coin
   , [TxCert BabbageEra]
   , Map RewardAccount Coin -- Withdrawals without the newtype
   , Coin
   , ValidityInterval
   , Maybe (Update BabbageEra)
   , Set (KeyHash Guard)
   , MultiAsset
   , Maybe ScriptIntegrityHash
   , Maybe TxAuxDataHash
   , Maybe Network
   ]

instance HasSimpleRep (TxBody TopTx BabbageEra) where
  type SimpleRep (TxBody TopTx BabbageEra) = SOP '["BabbageTxBody" ::: BabbageTxBodyTypes]
  toSimpleRep :: TxBody TopTx BabbageEra -> SimpleRep (TxBody TopTx BabbageEra)
toSimpleRep (BabbageTxBody Set TxIn
inputs Set TxIn
colinputs Set TxIn
refinputs StrictSeq (Sized (TxOut BabbageEra))
os StrictMaybe (Sized (TxOut BabbageEra))
colOut StrictMaybe Coin
coin StrictSeq (TxCert BabbageEra)
certs Withdrawals
w Coin
c ValidityInterval
vi StrictMaybe (Update BabbageEra)
up Set (KeyHash Guard)
kh MultiAsset
ma StrictMaybe ScriptIntegrityHash
ihash StrictMaybe TxAuxDataHash
aux StrictMaybe Network
nw) =
    forall (c :: Symbol) (constrs :: [*]).
Inject c constrs (SOP constrs) =>
FunTy (ConstrOf c constrs) (SOP constrs)
inject @"BabbageTxBody" @'["BabbageTxBody" ::: BabbageTxBodyTypes]
      Set TxIn
inputs
      Set TxIn
colinputs
      Set TxIn
refinputs
      (StrictSeq (Sized (BabbageTxOut BabbageEra))
-> [Sized (BabbageTxOut BabbageEra)]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (Sized (TxOut BabbageEra))
StrictSeq (Sized (BabbageTxOut BabbageEra))
os)
      (StrictMaybe (Sized (BabbageTxOut BabbageEra))
-> Maybe (Sized (BabbageTxOut BabbageEra))
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe (Sized (TxOut BabbageEra))
StrictMaybe (Sized (BabbageTxOut BabbageEra))
colOut)
      (StrictMaybe Coin -> Maybe Coin
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe Coin
coin)
      (StrictSeq (ShelleyTxCert BabbageEra) -> [ShelleyTxCert BabbageEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxCert BabbageEra)
StrictSeq (ShelleyTxCert BabbageEra)
certs)
      (Withdrawals -> Map RewardAccount Coin
unWithdrawals Withdrawals
w)
      Coin
c
      ValidityInterval
vi
      (StrictMaybe (Update BabbageEra) -> Maybe (Update BabbageEra)
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe (Update BabbageEra)
up)
      Set (KeyHash Guard)
kh
      MultiAsset
ma
      (StrictMaybe ScriptIntegrityHash -> Maybe ScriptIntegrityHash
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe ScriptIntegrityHash
ihash)
      (StrictMaybe TxAuxDataHash -> Maybe TxAuxDataHash
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe TxAuxDataHash
aux)
      (StrictMaybe Network -> Maybe Network
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe StrictMaybe Network
nw)

  fromSimpleRep :: SimpleRep (TxBody TopTx BabbageEra) -> TxBody TopTx BabbageEra
fromSimpleRep SimpleRep (TxBody TopTx BabbageEra)
rep =
    forall (constrs :: [*]) r.
SOPLike constrs r =>
SOP constrs -> ALG constrs r
algebra @'["BabbageTxBody" ::: BabbageTxBodyTypes]
      SOP '["BabbageTxBody" ::: BabbageTxBodyTypes]
SimpleRep (TxBody TopTx BabbageEra)
rep
      ( \Set TxIn
inputs Set TxIn
colinputs Set TxIn
refinputs [Sized (BabbageTxOut BabbageEra)]
os Maybe (Sized (BabbageTxOut BabbageEra))
colret Maybe Coin
totalcol [ShelleyTxCert BabbageEra]
certs Map RewardAccount Coin
w Coin
fee ValidityInterval
vi Maybe (Update BabbageEra)
up Set (KeyHash Guard)
kh MultiAsset
ma Maybe ScriptIntegrityHash
ihash Maybe TxAuxDataHash
aux Maybe Network
nw ->
          Set TxIn
-> Set TxIn
-> Set TxIn
-> StrictSeq (Sized (TxOut BabbageEra))
-> StrictMaybe (Sized (TxOut BabbageEra))
-> StrictMaybe Coin
-> StrictSeq (TxCert BabbageEra)
-> Withdrawals
-> Coin
-> ValidityInterval
-> StrictMaybe (Update BabbageEra)
-> Set (KeyHash Guard)
-> MultiAsset
-> StrictMaybe ScriptIntegrityHash
-> StrictMaybe TxAuxDataHash
-> StrictMaybe Network
-> TxBody TopTx BabbageEra
BabbageTxBody
            Set TxIn
inputs
            Set TxIn
colinputs
            Set TxIn
refinputs
            ([Sized (BabbageTxOut BabbageEra)]
-> StrictSeq (Sized (BabbageTxOut BabbageEra))
forall a. [a] -> StrictSeq a
SS.fromList [Sized (BabbageTxOut BabbageEra)]
os)
            (Maybe (Sized (BabbageTxOut BabbageEra))
-> StrictMaybe (Sized (BabbageTxOut BabbageEra))
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe (Sized (BabbageTxOut BabbageEra))
colret)
            (Maybe Coin -> StrictMaybe Coin
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe Coin
totalcol)
            ([ShelleyTxCert BabbageEra] -> StrictSeq (ShelleyTxCert BabbageEra)
forall a. [a] -> StrictSeq a
SS.fromList [ShelleyTxCert BabbageEra]
certs)
            (Map RewardAccount Coin -> Withdrawals
Withdrawals Map RewardAccount Coin
w)
            Coin
fee
            ValidityInterval
vi
            (Maybe (Update BabbageEra) -> StrictMaybe (Update BabbageEra)
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe (Update BabbageEra)
up)
            Set (KeyHash Guard)
kh
            MultiAsset
ma
            (Maybe ScriptIntegrityHash -> StrictMaybe ScriptIntegrityHash
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe ScriptIntegrityHash
ihash)
            (Maybe TxAuxDataHash -> StrictMaybe TxAuxDataHash
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe TxAuxDataHash
aux)
            (Maybe Network -> StrictMaybe Network
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe Network
nw)
      )

instance HasSpec (TxBody TopTx BabbageEra)