Added Utils.Value

agora.cabal

@@ -122,7 +122,11 @@ library
     Agora.Treasury
     Agora.Voting
 
-  other-modules:   Agora.Utils
+  other-modules:   
+    Agora.Utils
+    Agora.Utils.Value
+    Plutarch.Extra.Map
+
   hs-source-dirs:  src
 
 library pprelude

src/Agora/Treasury.hs

@@ -30,7 +30,6 @@ import Plutarch.DataRepr (
   PIsDataReprInstances (PIsDataReprInstances),
  )
 import Plutarch.Monadic qualified as P
-import Agora.Utils (pisValueSubset)
 
 {- | Validator ensuring that transactions consuming the treasury
      do so in a valid manner.
@@ -59,7 +58,7 @@ treasuryV = plam $ \d r ctx' -> P.do
       -- Amount of value treasury has after transaction.
       let valueTrOut = undefined
 
-      let vOutExceedsVIn = pisValueSubset # valueTrIn # valueTrOut
+      let vOutExceedsVIn = undefined
 
       pif
         (vOutExceedsVIn)

src/Agora/Utils.hs

@@ -24,7 +24,6 @@ module Agora.Utils (
   pfindTxInByTxOutRef,
   psingletonValue,
   pfindMap,
-  pisValueSubset,
 
   -- * Functions which should (probably) not be upstreamed
   anyOutput,
@@ -260,58 +259,58 @@ pfindTxInByTxOutRef = phoistAcyclic $
           )
         #$ (pfield @"inputs" # txInfo)
 
--- | Determines if a value is a subset of another.
+-- -- | Determines if a value is a subset of another.
-pisValueSubset :: Term s (PValue :--> PValue :--> PBool)
+-- pisValueSubset :: Term s (PValue :--> PValue :--> PBool)
-pisValueSubset = plam $ \v0 _v1 -> P.do
+-- pisValueSubset = plam $ \v0 _v1 -> P.do
-  -- v0Map :: Term s (PMap PCurrencySymbol (PMap PTokenName PInteger))
+--   -- v0Map :: Term s (PMap PCurrencySymbol (PMap PTokenName PInteger))
-  PValue v0Map <- pmatch v0
+--   PValue v0Map <- pmatch v0
 
-  -- v0BuiltinMap :: Term s (PBuiltinMap k v)
+--   -- v0BuiltinMap :: Term s (PBuiltinMap k v)
-  PMap v0BuiltinMap <- pmatch v0Map
+--   PMap v0BuiltinMap <- pmatch v0Map
 
-  -- ks0 :: Term s (PBuiltinList PCurrencySymbol)
+--   -- ks0 :: Term s (PBuiltinList PCurrencySymbol)
-  let ks0 = pmap # pfstBuiltin # v0BuiltinMap
+--   let ks0 = pmap # pfstBuiltin # v0BuiltinMap
-  pconstant True
+--   pconstant True
 
--- | Determines if a PTokenName/PInteger pmap is a subset of another.
+-- -- | Determines if a PTokenName/PInteger pmap is a subset of another.
-pisTnISubset ::
+-- pisTnISubset ::
-  Term
+--   Term
-    s
+--     s
-    ( PMap PTokenName PInteger
+--     ( PMap PTokenName PInteger
-        :--> PMap PTokenName PInteger
+--         :--> PMap PTokenName PInteger
-        :--> PBool
+--         :--> PBool
-    )
+--     )
-pisTnISubset = plam $ \m0 m1 -> P.do
+-- pisTnISubset = plam $ \m0 m1 -> P.do
-  -- m0BuiltinMap :: Term s (PBuiltinMap PTokenName PInteger)
+--   -- m0BuiltinMap :: Term s (PBuiltinMap PTokenName PInteger)
-  PMap m0BuiltinMap <- pmatch m0
+--   PMap m0BuiltinMap <- pmatch m0
 
-  -- ks0 :: Term s (PBuiltinList PTokenName)
+--   -- ks0 :: Term s (PBuiltinList PTokenName)
-  let ks0 = pmap # pfstBuiltin # m0BuiltinMap
+--   let ks0 = pmap # pfstBuiltin # m0BuiltinMap
-  pconstant True
+--   pconstant True
 
-pcompareKeysForEq ::
+-- pcompareKeys ::
-  Term
+--   Term
-    s
+--     s
-    ( PBuiltinList k
+--     ( PBuiltinList k
-        :--> PMap k v
+--         :--> PMap k v
-        :--> PMap k v
+--         :--> PMap k v
-        :--> PBool
+--         :--> PBool
-    )
+--     )
-pcompareKeysForEq = plam $ \ks m0' m1' -> P.do
+-- pcompareKeys = plam $ \ks m0' m1' -> P.do
-  PMap m0 <- m0'
+--   PMap m0 <- m0'
-  PMap m1 <- m1'
+--   PMap m1 <- m1'
-  bs <- pmatch $ pmap # f # ks
+--   bs <- pmatch $ pmap # f # ks
-  pcon PTrue
+--   pconstant True
 
-f :: Term s (k :--> PMap k v :--> PMap k v)
+-- f :: Term s (k :--> PMap k v :--> PMap k v :--> PBool)
-f = plam $ \k m0' m1' -> P.do
+-- f = plam $ \k m0' m1' -> P.do
-  PMap m0 <- m0'
+--   PMap m0 <- m0'
-  PMap m1 <- m1'
+--   PMap m1 <- m1'
-  pmatch (plookup # k # m1) $ \case
+--   pmatch (plookup # k # m1) $ \case
-    PNothing -> pconstant False
+--     PNothing -> pconstant False
-    PJust n1 -> P.do
+--     PJust n1 -> P.do
-      PJust n0 <- pmatch $ plookup # k # m0
+--       PJust n0 <- pmatch $ plookup # k # m0
-      n0 #<= n1
+--       n0 #<= n1
 
 --------------------------------------------------------------------------------
 -- Functions which should (probably) not be upstreamed

src/Agora/Utils/Value.hs

@@ -0,0 +1,107 @@
+{-# OPTIONS_GHC -Wwarn #-}
+
+module Agora.Utils.Value where
+
+import GHC.Generics qualified as GHC
+import Generics.SOP
+import Plutarch.Api.V1.AssocMap (PMap (PMap))
+import Plutarch.Api.V1.Tuple (PTuple, ptupleFromBuiltin)
+import Plutarch.Api.V1.Value (PCurrencySymbol, PTokenName, PValue)
+import Plutarch.DataRepr (PIsDataReprInstances (PIsDataReprInstances))
+import Plutarch.Lift (PLifted, PUnsafeLiftDecl)
+import Plutarch.Monadic qualified as P
+import Plutus.V1.Ledger.Api qualified as Plutus
+import PlutusTx.These qualified as PlutusThese
+
+-- data PThese (a :: PType) (b :: PType) (s :: S)
+--   = PThis (Term s a)
+--   | PThat (Term s b)
+--   | PThese (Term s a) (Term s b)
+--   deriving stock (GHC.Generic)
+--   deriving anyclass (Generic, PlutusType)
+
+data PTheseData (a :: PType) (b :: PType) (s :: S)
+  = PDThis (Term s (PDataRecord '["_0" ':= a]))
+  | PDThat (Term s (PDataRecord '["_0" ':= b]))
+  | PDThese (Term s (PDataRecord '["_0" ':= a, "_1" ':= b]))
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic, PIsDataRepr)
+  deriving
+    (PlutusType, PIsData)
+    via PIsDataReprInstances (PTheseData a b)
+
+instance
+  ( Plutus.ToData (PLifted a)
+  , Plutus.ToData (PLifted b)
+  , Plutus.FromData (PLifted a)
+  , Plutus.FromData (PLifted b)
+  , PLift a
+  , PLift b
+  ) =>
+  PUnsafeLiftDecl (PTheseData a b)
+  where
+  type PLifted (PTheseData a b) = PlutusThese.These (PLifted a) (PLifted b)
+
+punionVal ::
+  Term
+    s
+    ( PValue
+        :--> PValue
+        :--> PMap
+              PCurrencySymbol
+              (PMap PTokenName (PTheseData PInteger PInteger))
+    )
+punionVal = undefined
+
+-- | Determines if a condition is true for all values in a map.
+pmapAll ::
+  (PUnsafeLiftDecl v, PIsData v) =>
+  Term s ((v :--> PBool) :--> PMap k v :--> PBool)
+pmapAll = plam $ \f m -> P.do
+  PMap builtinMap <- pmatch $ m
+
+  let getV :: PIsData v => Term s (PBuiltinPair (PAsData k) (PAsData v) :--> v)
+      getV = plam $ \bip -> P.do
+        let tuple = pfromData $ ptupleFromBuiltin (pdata bip)
+        pfield @"_1" # tuple
+
+  let vs = pmap # getV # builtinMap
+  pall # f # vs
+
+pcheckPred ::
+  forall {s :: S}.
+  Term
+    s
+    ( (PTheseData PInteger PInteger :--> PBool)
+        :--> PValue
+        :--> PValue
+        :--> PBool
+    )
+pcheckPred = plam $ \f l r -> P.do
+  let inner :: Term s (PMap PTokenName (PTheseData PInteger PInteger) :--> PBool)
+      inner = pmapAll # f
+  pmapAll # inner # (punionVal # l # r)
+
+pcheckBinRel ::
+  forall {s :: S}.
+  Term
+    s
+    ( (PInteger :--> PInteger :--> PBool)
+        :--> PValue
+        :--> PValue
+        :--> PBool
+    )
+pcheckBinRel = plam $ \f l r -> P.do
+  let unThese :: Term s (PTheseData PInteger PInteger :--> PBool)
+      unThese = plam $ \k' ->
+        pmatch k' $ \case
+          PDThis r -> f # (pfield @"_0" # r) # 0
+          PDThat r -> f # 0 # (pfield @"_0" # r)
+          PDThese r -> f # (pfield @"_0" # r) # (pfield @"_1" # r)
+  pcheckPred # unThese # l # r
+
+pleq :: Term s (PValue :--> PValue :--> PBool)
+pleq = plam $ \v0 v1 -> (pcheckBinRel # pleq') # v0 # v1
+
+pleq' :: Term s (PInteger :--> PInteger :--> PBool)
+pleq' = plam $ \m n -> m #<= n

src/Plutarch/Extra/Map.hs

@@ -0,0 +1,2 @@
+module Plutarch.Extra.Map () where
+