Use Value type

cardano-foundation · May 9, 2024 · 9e756dc · 9e756dc
1 parent 9b85d73
commit 9e756dc
Show file tree

Hide file tree

Showing 9 changed files with 34 additions and 57 deletions.
diff --git a/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure.agda b/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure.agda
@@ -78,7 +78,6 @@ open import Cardano.Wallet.Deposit.Read using
     ; TxIn
     ; TxOut
     ; Value
-    ; exceeds
     )
 open import Cardano.Write.Tx.Balance using
     ( ChangeAddressGen

diff --git a/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Read.agda b/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Read.agda
@@ -3,6 +3,15 @@ module Cardano.Wallet.Deposit.Read where
 
 open import Haskell.Prelude
 
+open import Cardano.Wallet.Deposit.Read.Value public
+
+{-# FOREIGN AGDA2HS
+-- Working around a limitation in agda2hs.
+import Cardano.Wallet.Deposit.Read.Value 
+    ( Value
+    )
+#-}
+
 import Haskell.Data.ByteString as BS
 import Haskell.Data.Map as Map
 
@@ -26,32 +35,6 @@ instance
 {-# COMPILE AGDA2HS Addr #-}
 {-# COMPILE AGDA2HS Address #-}
 
-{-----------------------------------------------------------------------------
-    Value
-------------------------------------------------------------------------------}
-data Value : Set where
-    MkValue : Integer → Value
-
-instance
-  iSemigroupValue : Semigroup Value
-  _<>_ {{iSemigroupValue}} (MkValue a) (MkValue b) = MkValue (a + b)
-
-  iMonoidValue : Monoid Value
-  iMonoidValue =
-    record {DefaultMonoid (λ where .DefaultMonoid.mempty → MkValue 0)}
-
-exceeds : Value → Value → Bool
-exceeds (MkValue a) (MkValue b) = a >= b
-
-minus : Value → Value → Value
-minus (MkValue a) (MkValue b) = MkValue (a - b)
-
-{-# COMPILE AGDA2HS Value #-}
-{-# COMPILE AGDA2HS iSemigroupValue #-}
-{-# COMPILE AGDA2HS iMonoidValue #-}
-{-# COMPILE AGDA2HS exceeds #-}
-{-# COMPILE AGDA2HS minus #-}
-
 {-----------------------------------------------------------------------------
     Transactions
 ------------------------------------------------------------------------------}

diff --git a/lib/customer-deposit-wallet-pure/agda/Cardano/Write/Tx/Balance.agda b/lib/customer-deposit-wallet-pure/agda/Cardano/Write/Tx/Balance.agda
@@ -24,8 +24,8 @@ open import Cardano.Wallet.Deposit.Read using
     ; TxIn
     ; TxOut
     ; Value
-    ; exceeds
-    ; minus
+    ; largerOrEqual
+    ; monus
     )
 open import Haskell.Data.List.Prop using ( _∈_ )
 open import Haskell.Data.Maybe using ( isJust )
@@ -76,9 +76,9 @@ coinSelectionGreedy
 coinSelectionGreedy v [] = (mempty , [])
 coinSelectionGreedy v ((txin , txout) ∷ xs) =
     let dv = (TxOut.value txout)
-    in  if exceeds v dv
-            then secondCons txin $ coinSelectionGreedy (minus v dv) xs
-            else (minus dv v , [])
+    in  if largerOrEqual v dv
+            then secondCons txin $ coinSelectionGreedy (monus v dv) xs
+            else (monus dv v , [])
 
 {-# COMPILE AGDA2HS secondCons #-}
 {-# COMPILE AGDA2HS coinSelectionGreedy #-}
@@ -102,7 +102,7 @@ balanceTransaction utxo newAddress c0 partialTx =
             ; value = changeValue
             }
     in
-    if exceeds target (UTxO.balance utxo)
+    if largerOrEqual target (UTxO.balance utxo)
         then Nothing
         else Just $ record
           { outputs = changeOutput ∷ PartialTx.outputs partialTx
@@ -134,7 +134,7 @@ lemma-balanceTransaction-addresses
   → map TxOut.address (TxBody.outputs tx)
     ≡ fst (new c0) ∷ map TxOut.address (PartialTx.outputs partialTx)
 lemma-balanceTransaction-addresses u partialTx new c0 tx balance
-  with exceeds (totalOut partialTx) (UTxO.balance u)
+  with largerOrEqual (totalOut partialTx) (UTxO.balance u)
 ...  | True = magic (unequal tx balance)
 ...  | False = begin
           map TxOut.address (TxBody.outputs tx)

diff --git a/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure.hs b/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure.hs
@@ -1,7 +1,8 @@
 module Cardano.Wallet.Deposit.Pure where
 
 import Cardano.Wallet.Address.BIP32_Ed25519 (XPub)
-import Cardano.Wallet.Deposit.Read (Address, Block(transactions), ChainPoint, Tx, TxBody, TxOut(TxOutC), Value, chainPointFromBlock)
+import Cardano.Wallet.Deposit.Read (Address, Block(transactions), ChainPoint, Tx, TxBody, TxOut(TxOutC), chainPointFromBlock)
+import Cardano.Wallet.Deposit.Read.Value (Value)
 import Cardano.Write.Tx.Balance (ChangeAddressGen, PartialTx(PartialTxC), balanceTransaction)
 import qualified Haskell.Data.Map as Map (Map, lookup)
 

diff --git a/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/UTxO/Tx.hs b/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/UTxO/Tx.hs
@@ -6,7 +6,8 @@ import Cardano.Wallet.Deposit.Pure.UTxO.UTxO (UTxO)
 import qualified Cardano.Wallet.Deposit.Pure.UTxO.UTxO as UTxO (filterByAddress, null, restrictedBy)
 import Cardano.Wallet.Deposit.Pure.UTxO.ValueTransfer (ValueTransfer, fromReceived, fromSpent)
 import Cardano.Wallet.Deposit.Read (Tx(txbody, txid), TxBody(inputs, outputs))
-import qualified Cardano.Wallet.Deposit.Read as Read (Addr, Address, TxIn, TxOut(address, value), Value)
+import qualified Cardano.Wallet.Deposit.Read as Read (Addr, Address, TxIn, TxOut(address, value))
+import qualified Cardano.Wallet.Deposit.Read.Value as Read (Value)
 import Data.Set (Set)
 import qualified Haskell.Data.ByteString (ByteString)
 import qualified Haskell.Data.Map as Map (Map, elems, fromList, fromListWith, map, unionWith)

diff --git a/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/UTxO/UTxO.hs b/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/UTxO/UTxO.hs
@@ -1,6 +1,7 @@
 module Cardano.Wallet.Deposit.Pure.UTxO.UTxO where
 
-import Cardano.Wallet.Deposit.Read (Address, TxIn, TxOut(address, value), Value)
+import Cardano.Wallet.Deposit.Read (Address, TxIn, TxOut(address, value))
+import Cardano.Wallet.Deposit.Read.Value (Value)
 import Data.Set (Set)
 import qualified Haskell.Data.Map as Map (Map, empty, filter, keysSet, member, null, restrictKeys, unionWith, withoutKeys)
 import qualified Haskell.Data.Set as Set (filter)

diff --git a/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/UTxO/ValueTransfer.hs b/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/UTxO/ValueTransfer.hs
@@ -1,6 +1,6 @@
 module Cardano.Wallet.Deposit.Pure.UTxO.ValueTransfer where
 
-import Cardano.Wallet.Deposit.Read (Value)
+import Cardano.Wallet.Deposit.Read.Value (Value)
 
 data ValueTransfer = ValueTransfer{spent :: Value,
                                    received :: Value}

diff --git a/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Read.hs b/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Read.hs
@@ -3,24 +3,15 @@ module Cardano.Wallet.Deposit.Read where
 import qualified Haskell.Data.ByteString as BS (ByteString)
 import Numeric.Natural (Natural)
 
+-- Working around a limitation in agda2hs.
+import Cardano.Wallet.Deposit.Read.Value
+    ( Value
+    )
+
 type Addr = BS.ByteString
 
 type Address = Addr
 
-data Value = MkValue Integer
-
-instance Semigroup Value where
-    MkValue a <> MkValue b = MkValue (a + b)
-
-instance Monoid Value where
-    mempty = MkValue 0
-
-exceeds :: Value -> Value -> Bool
-exceeds (MkValue a) (MkValue b) = a >= b
-
-minus :: Value -> Value -> Value
-minus (MkValue a) (MkValue b) = MkValue (a - b)
-
 type TxId = BS.ByteString
 
 type Ix = Int

diff --git a/lib/customer-deposit-wallet-pure/haskell/Cardano/Write/Tx/Balance.hs b/lib/customer-deposit-wallet-pure/haskell/Cardano/Write/Tx/Balance.hs
@@ -2,7 +2,8 @@ module Cardano.Write.Tx.Balance where
 
 import Cardano.Wallet.Deposit.Pure.UTxO.UTxO (UTxO)
 import qualified Cardano.Wallet.Deposit.Pure.UTxO.UTxO as UTxO (balance)
-import Cardano.Wallet.Deposit.Read (Address, TxBody(TxBodyC), TxIn, TxOut(TxOutC, value), Value, exceeds, minus)
+import Cardano.Wallet.Deposit.Read (Address, TxBody(TxBodyC), TxIn, TxOut(TxOutC, value))
+import Cardano.Wallet.Deposit.Read.Value (Value, largerOrEqual, monus)
 import qualified Haskell.Data.Map as Map (toAscList)
 
 data PartialTx = PartialTxC{outputs :: [TxOut]}
@@ -18,14 +19,14 @@ secondCons y (x, ys) = (x, y : ys)
 coinSelectionGreedy :: Value -> [(TxIn, TxOut)] -> (Value, [TxIn])
 coinSelectionGreedy v [] = (mempty, [])
 coinSelectionGreedy v ((txin, txout) : xs)
-  = if exceeds v (value txout) then
-      secondCons txin $ coinSelectionGreedy (minus v (value txout)) xs
-      else (minus (value txout) v, [])
+  = if largerOrEqual v (value txout) then
+      secondCons txin $ coinSelectionGreedy (monus v (value txout)) xs
+      else (monus (value txout) v, [])
 
 balanceTransaction ::
                    UTxO -> ChangeAddressGen c -> c -> PartialTx -> Maybe TxBody
 balanceTransaction utxo newAddress c0 partialTx
-  = if exceeds target (UTxO.balance utxo) then Nothing else
+  = if largerOrEqual target (UTxO.balance utxo) then Nothing else
       Just $
         TxBodyC (snd (coinSelectionGreedy target (Map.toAscList utxo)))
           (TxOutC (fst (newAddress c0))