Add ResolvedTx and resolveInputs

cardano-foundation · Apr 25, 2024 · ce2e0ba · ce2e0ba
1 parent f56a4d7
commit ce2e0ba
Show file tree

Hide file tree

Showing 3 changed files with 31 additions and 0 deletions.
diff --git a/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/UTxO/Tx.agda b/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/UTxO/Tx.agda
@@ -77,3 +77,26 @@ applyTx isOurs tx u0 =
 {-# COMPILE AGDA2HS IsOurs #-}
 {-# COMPILE AGDA2HS applyTx #-}
 
+{-----------------------------------------------------------------------------
+    Resolve Inputs
+------------------------------------------------------------------------------}
+-- | A transaction whose inputs have been partially resolved.
+record ResolvedTx : Set where
+  field
+    resolvedTx : Read.Tx
+    resolvedInputs : UTxO
+
+open ResolvedTx public
+
+resolveInputs : UTxO → Read.Tx → ResolvedTx
+resolveInputs utxo tx =
+  record
+    { resolvedTx = tx
+    ; resolvedInputs =
+        UTxO.restrictedBy
+            utxo
+            (Set.fromList (TxBody.inputs (Tx.txbody tx)))
+    }
+
+{-# COMPILE AGDA2HS ResolvedTx #-}
+{-# COMPILE AGDA2HS resolveInputs #-}
diff --git a/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/UTxO/UTxO.agda b/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/UTxO/UTxO.agda
@@ -9,6 +9,7 @@ module Cardano.Wallet.Deposit.Pure.UTxO.UTxO
       ; balance
       ; union
       ; excluding
+      ; restrictedBy
       ; excludingS
       ; filterByAddress
     -}
@@ -55,6 +56,9 @@ union = Map.unionWith (λ x y → x)
 excluding : UTxO → Set.ℙ TxIn → UTxO
 excluding = Map.withoutKeys
 
+restrictedBy : UTxO → Set.ℙ TxIn → UTxO
+restrictedBy = Map.restrictKeys
+
 -- | Exclude the inputs of a 'UTxO' from a 'Set' of inputs.
 excludingS : Set.ℙ TxIn → UTxO → Set.ℙ TxIn
 excludingS s utxo = Set.filter (not ∘ (λ txin → Map.member txin utxo)) s
@@ -69,6 +73,7 @@ filterByAddress p = Map.filter (p ∘ TxOut.address)
 {-# COMPILE AGDA2HS balance #-}
 {-# COMPILE AGDA2HS union #-}
 {-# COMPILE AGDA2HS excluding #-}
+{-# COMPILE AGDA2HS restrictedBy #-}
 {-# COMPILE AGDA2HS excludingS #-}
 {-# COMPILE AGDA2HS filterByAddress #-}
 

diff --git a/lib/customer-deposit-wallet-pure/agda/Haskell/Data/Map.agda b/lib/customer-deposit-wallet-pure/agda/Haskell/Data/Map.agda
@@ -153,6 +153,9 @@ module
   withoutKeys : Map k a → Set.ℙ k → Map k a
   withoutKeys m s = filterWithKey (λ k _ → not (Set.member k s)) m
 
+  restrictKeys : Map k a → Set.ℙ k → Map k a
+  restrictKeys m s = filterWithKey (λ k _ → Set.member k s) m
+
   filter : (a → Bool) → Map k a → Map k a
   filter p = filterWithKey (λ _ x → p x)