Lib

{-# OPTIONS --safe #-}

module Test.Examples.DEx.OffChain.Lib where

open import Data.List using (filter)

open import Ledger.Prelude
open import Ledger.Conway.Specification.Transaction using (TransactionStructure)

open import Test.Examples.DEx.Datum
open import Test.Examples.DEx.Validator
open import Test.Prelude DExData
open import Test.SymbolicData DExData
open import Test.LedgerImplementation SData SData

open TransactionStructure SVTransactionStructure

defaultTxBody : TxBody
defaultTxBody = record
                  { txIns = ∅
                  ; refInputs = ∅
                  ; collateralInputs = ∅
                  ; txOuts =  ∅
                  ; txFee = 
                  ; mint = 
                  ; txVldt = nothing , nothing
                  ; txCerts = []
                  ; txWithdrawals = ∅
                  ; txGovVotes = []
                  ; txGovProposals = []
                  ; txDonation = 
                  ; txADhash = nothing
                  ; txNetworkId = just 
                  ; currentTreasury = nothing
                  ; txId = 
                  ; reqSignerHashes = ∅
                  ; scriptIntegrityHash = nothing
                  }

matchScriptAddress : (scriptHash : ℕ) → Credential → Set
matchScriptAddress sh (KeyHashObj x) = ⊥
matchScriptAddress sh (ScriptObj y) = True (sh ≟ y)

matchScriptAddress? : (sh : ℕ) → (c : Credential) → Dec (matchScriptAddress sh c)
matchScriptAddress? sh (KeyHashObj x) = no (λ x₁ → x₁)
matchScriptAddress? sh (ScriptObj y) = T? ⌊ (sh ≟ y) ⌋

getScriptUTxO : (scriptHash : ℕ) → UTxO → Maybe (TxIn × TxOut)
getScriptUTxO sh (utxo , prf) = head $ filter (λ { (_ , addr , _) → matchScriptAddress? sh (payCred addr)}) (setToList utxo)

matchWalletHash : (keyHash : ℕ) → Credential → Set
matchWalletHash kh (KeyHashObj x) = True (kh ≟ x)
matchWalletHash kh (ScriptObj y) = ⊥

matchWalletHash? : (sh : ℕ) → (c : Credential) → Dec (matchWalletHash sh c)
matchWalletHash? kh (KeyHashObj x) = T? ⌊ (kh ≟ x) ⌋
matchWalletHash? kh (ScriptObj y) = no (λ x₁ → x₁)

getWalletUTxO : (scriptHash : ℕ) → UTxO → List (TxIn × TxOut)
getWalletUTxO sh (utxo , prf) = filter (λ { (_ , addr , _) → matchWalletHash? sh (payCred addr)}) (setToList utxo)

{-
succeedTxOut' : TxOut
succeedTxOut' = inj₁ (record { net = 0 ;
                           pay = ScriptObj 777 ;
                           stake = just (ScriptObj 777) })
                           , {!!} , just (inj₁ (inj₁ (inj₁ (Always [])))) , nothing
-- 700000000000 -}

getLabel : TxOut → Maybe Label
getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₁ x))) , snd) = just x
getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₂ y))) , snd) = nothing
getLabel (fst , fst₁ , just (inj₁ (inj₂ y)) , snd) = nothing
getLabel (fst , fst₁ , just (inj₂ y) , snd) = nothing
getLabel (fst , fst₁ , nothing , snd) = nothing



-- Assumes a list of filtered waller txins and subtracts a default fee from the head of the list
makeFeeTxOut : List (TxIn × TxOut) → List (ℕ × TxOut)
makeFeeTxOut [] = []
makeFeeTxOut ((txin , (fst , txValue , snd)) ∷ utxos) = (proj₂ txin , fst , txValue - feeValue , snd) ∷ []
--10000000000

makeFeeUnPaymentTxOut : List (TxIn × TxOut) → Value → List (ℕ × TxOut)
makeFeeUnPaymentTxOut [] v = []
makeFeeUnPaymentTxOut ((txin , (fst , txValue , snd)) ∷ utxos) v = (proj₂ txin , fst , _+_ {{addValue}} (txValue - feeValue) v , snd) ∷ []
-- 10000000000

makeFeePaymentTxOut : List (TxIn × TxOut) → Value → List (ℕ × TxOut)
makeFeePaymentTxOut [] v = []
makeFeePaymentTxOut ((txin , (fst , txValue , snd)) ∷ utxos) v = (proj₂ txin , fst , (txValue - feeValue ) - v , snd) ∷ []
--10000000000

makeFeeSwapTxOut : List (TxIn × TxOut) → Value → Value → List (ℕ × TxOut)
makeFeeSwapTxOut [] v1 v2 = []
makeFeeSwapTxOut ((txin , (fst , txValue , snd)) ∷ utxos) refund new = (proj₂ txin , fst , _+_ {{addValue}} ((txValue - feeValue ) - new) refund , snd) ∷ []

-- return id of 0 if no txins
getTxId : List (TxIn × TxOut) → ℕ
getTxId xs = maybe (λ x → proj₁ (proj₁ x))  (head xs)

{-
getVal : Label -> ℕ -> Value
getVal (Always l) w with lookup' w l
...| nothing = emptyValue
...| just v = v
-}