{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Transaction

module Ledger.Dijkstra.Specification.Script.ScriptPurpose (txs : TransactionStructure) where

open import Ledger.Prelude
open TransactionStructure txs
open import Ledger.Dijkstra.Specification.Certs govStructure


ScriptPurposeData : Tag → Type
ScriptPurposeData Spend         = TxIn
ScriptPurposeData Mint          = ScriptHash
ScriptPurposeData Cert          = DCert
ScriptPurposeData Reward        = RewardAddress
ScriptPurposeData Vote          = GovVoter
ScriptPurposeData Propose       = GovProposal
ScriptPurposeData Guard         = Credential

record ScriptPurpose : Type where
  constructor ⟦_,_⟧ˢᵖ
  field
    tag   : Tag
    data′ : ScriptPurposeData tag


mutual
  record TxInfo : Type where
    inductive
    field
      realizedInputs      : UTxO
      txOuts              : Ix ⇀ TxOut
      txFee               : Maybe Fees
      mint                : Value
      txCerts             : List DCert
      txWithdrawals       : Withdrawals
      txVldt              : Maybe Slot × Maybe Slot
      vkKey               : ℙ KeyHash     -- native/phase-1/timelock signers
      txGuards            : ℙ Credential  -- CIP-0112/0118 guards (required by tx body)
      txData              : ℙ Datum
      txId                : TxId
      txInfoSubTxs        : Maybe (List SubTxInfo)
      txDirectDeposits    : DirectDeposits
      txBalanceIntervals  : AccountBalanceIntervals

  SubTxInfo : Type
  SubTxInfo = TxInfo