From 43cd0c450760f08038e7ae37a5b9f472edcefbf7 Mon Sep 17 00:00:00 2001
From: Jack Hodgkinson <30505104+jhodgdev@users.noreply.github.com>
Date: Fri, 4 Mar 2022 09:27:41 +0000
Subject: [PATCH] Added These data types

---
 agora.cabal                  |  2 +
 src/Agora/Treasury.hs        | 44 ++++-----------------
 src/Agora/Utils.hs           | 57 ---------------------------
 src/Agora/Utils/Value.hs     | 76 +++++++++++++++---------------------
 src/Plutarch/Api/V1/These.hs | 62 +++++++++++++++++++++++++++++
 src/Plutarch/These.hs        | 12 ++++++
 6 files changed, 114 insertions(+), 139 deletions(-)
 create mode 100644 src/Plutarch/Api/V1/These.hs
 create mode 100644 src/Plutarch/These.hs

diff --git a/agora.cabal b/agora.cabal
index 00e342c..3d8cdf0 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -125,6 +125,8 @@ library
   other-modules:
     Agora.Utils
     Agora.Utils.Value
+    Plutarch.Api.V1.These
+    Plutarch.These
 
   hs-source-dirs:  src
 
diff --git a/src/Agora/Treasury.hs b/src/Agora/Treasury.hs
index 61ae19d..d487f5a 100644
--- a/src/Agora/Treasury.hs
+++ b/src/Agora/Treasury.hs
@@ -1,5 +1,3 @@
-{-# OPTIONS_GHC -Wwarn #-}
-
 {- |
 Module: Agora.Treasury
 Maintainer: jack@mlabs.city
@@ -8,28 +6,16 @@ Description: Treasury scripts.
 Contains the datum, redeemer and validator for a template DAO
 treasury.
 -}
-module Agora.Treasury (treasuryV) where
+module Agora.Treasury (module Agora.Treasury) where
 
 import GHC.Generics qualified as GHC
 import Generics.SOP
-import Plutarch.Api.V1.Contexts (
-  PScriptContext,
-  PTuple,
-  PTxInfo (PTxInfo),
- )
-import Plutarch.Api.V1.Maybe (PMaybeData (PDJust))
-import Plutarch.Api.V1.Scripts (PDatum, PDatumHash)
-import Plutarch.Api.V1.Tx (
-  PTxInInfo,
-  PTxOut,
- )
-import Plutarch.Api.V1.Value (PCurrencySymbol, PValue)
-import Plutarch.Builtin (pforgetData)
+import Plutarch.Api.V1.Contexts (PScriptContext)
+import Plutarch.Api.V1.Value (PCurrencySymbol)
 import Plutarch.DataRepr (
   PDataFields,
   PIsDataReprInstances (PIsDataReprInstances),
  )
-import Plutarch.Monadic qualified as P
 
 {- | Validator ensuring that transactions consuming the treasury
      do so in a valid manner.
@@ -42,28 +28,13 @@ treasuryV ::
         :--> PAsData PScriptContext
         :--> PUnit
     )
-treasuryV = plam $ \d r ctx' -> P.do
+treasuryV = plam $ \_d r _ctx' -> P.do
   pmatch (pfromData r) $ \case
     -- Redeemer seeking to alter treasury parameters. Must ensure
     -- a valid GAT is burned in the transaction.
     PAlterTrParams _ ->
+      -- TODO: Implement.
       ptraceError "Altering treasury parameters is not currently supported."
-    -- Redeemer for all other treasury actions. Must ensure datum
-    -- is unchanged and no value has been removed from the
-    -- treasury.
-    PRedeemTreasury _ -> P.do
-      -- Amount of value treasury has before transaction.
-      let valueTrIn = undefined
-
-      -- Amount of value treasury has after transaction.
-      let valueTrOut = undefined
-
-      let vOutExceedsVIn = undefined
-
-      pif
-        (vOutExceedsVIn)
-        (pconstant ())
-        (ptraceError "Value has been illegally deducted from treasury.")
 
 {- | Plutarch level type representing datum of the treasury.
      Contains:
@@ -90,10 +61,9 @@ newtype PTreasuryDatum (s :: S)
      treasury.
 -}
 data PTreasuryRedeemer (s :: S)
-  = -- | TODO: will allow the burning of GATs to alter Treasury params.
+  = -- | Alters treasury parameters (subject to the burning of a
+    --   governance authority token).
     PAlterTrParams (Term s (PDataRecord '[]))
-  | -- | All other treasury actions. Value must not decrease.
-    PRedeemTreasury (Term s (PDataRecord '[]))
   deriving stock (GHC.Generic)
   deriving anyclass (Generic, PIsDataRepr)
   deriving
diff --git a/src/Agora/Utils.hs b/src/Agora/Utils.hs
index d70e9f1..124c57b 100644
--- a/src/Agora/Utils.hs
+++ b/src/Agora/Utils.hs
@@ -1,5 +1,3 @@
-{-# OPTIONS_GHC -Wwarn #-}
-
 {- |
 Module     : Agora.Utils
 Maintainer : emi@haskell.fyi
@@ -52,8 +50,6 @@ import Plutarch.Api.V1 (
   PTxOutRef,
   PValue (PValue),
  )
-import Plutarch.Api.V1.Tuple (ptupleFromBuiltin)
-import Plutarch.Bool (pand)
 import Plutarch.Builtin (ppairDataBuiltin)
 import Plutarch.Internal (punsafeCoerce)
 import Plutarch.Monadic qualified as P
@@ -259,59 +255,6 @@ pfindTxInByTxOutRef = phoistAcyclic $
           )
         #$ (pfield @"inputs" # txInfo)
 
--- -- | Determines if a value is a subset of another.
--- pisValueSubset :: Term s (PValue :--> PValue :--> PBool)
--- pisValueSubset = plam $ \v0 _v1 -> P.do
---   -- v0Map :: Term s (PMap PCurrencySymbol (PMap PTokenName PInteger))
---   PValue v0Map <- pmatch v0
-
---   -- v0BuiltinMap :: Term s (PBuiltinMap k v)
---   PMap v0BuiltinMap <- pmatch v0Map
-
---   -- ks0 :: Term s (PBuiltinList PCurrencySymbol)
---   let ks0 = pmap # pfstBuiltin # v0BuiltinMap
---   pconstant True
-
--- -- | Determines if a PTokenName/PInteger pmap is a subset of another.
--- pisTnISubset ::
---   Term
---     s
---     ( PMap PTokenName PInteger
---         :--> PMap PTokenName PInteger
---         :--> PBool
---     )
--- pisTnISubset = plam $ \m0 m1 -> P.do
---   -- m0BuiltinMap :: Term s (PBuiltinMap PTokenName PInteger)
---   PMap m0BuiltinMap <- pmatch m0
-
---   -- ks0 :: Term s (PBuiltinList PTokenName)
---   let ks0 = pmap # pfstBuiltin # m0BuiltinMap
---   pconstant True
-
--- pcompareKeys ::
---   Term
---     s
---     ( PBuiltinList k
---         :--> PMap k v
---         :--> PMap k v
---         :--> PBool
---     )
--- pcompareKeys = plam $ \ks m0' m1' -> P.do
---   PMap m0 <- m0'
---   PMap m1 <- m1'
---   bs <- pmatch $ pmap # f # ks
---   pconstant True
-
--- f :: Term s (k :--> PMap k v :--> PMap k v :--> PBool)
--- f = plam $ \k m0' m1' -> P.do
---   PMap m0 <- m0'
---   PMap m1 <- m1'
---   pmatch (plookup # k # m1) $ \case
---     PNothing -> pconstant False
---     PJust n1 -> P.do
---       PJust n0 <- pmatch $ plookup # k # m0
---       n0 #<= n1
-
 --------------------------------------------------------------------------------
 -- Functions which should (probably) not be upstreamed
 
diff --git a/src/Agora/Utils/Value.hs b/src/Agora/Utils/Value.hs
index b27d569..90efdaa 100644
--- a/src/Agora/Utils/Value.hs
+++ b/src/Agora/Utils/Value.hs
@@ -1,46 +1,15 @@
-{-# OPTIONS_GHC -Wwarn #-}
+{-# OPTIONS_GHC -Wno-unused-imports #-}
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
 
-module Agora.Utils.Value where
+module Agora.Utils.Value (pgeq, pleq, pgt, plt) 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.These (PTheseData (..))
+import Plutarch.Api.V1.Tuple (ptupleFromBuiltin)
 import Plutarch.Api.V1.Value (PCurrencySymbol, PTokenName, PValue)
-import Plutarch.DataRepr (PIsDataReprInstances (PIsDataReprInstances))
-import Plutarch.Lift (PLifted, PUnsafeLiftDecl)
+import Plutarch.Lift (PUnsafeLiftDecl)
+import Plutarch.List (pconvertLists)
 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
@@ -60,10 +29,9 @@ pmapAll ::
 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 getV = plam $ \bip -> P.do
         let tuple = pfromData $ ptupleFromBuiltin (pdata bip)
-        pfield @"_1" # tuple
+        pfromData $ pfield @"_1" # tuple
 
   let vs = pmap # getV # builtinMap
   pall # f # vs
@@ -77,10 +45,12 @@ pcheckPred ::
         :--> 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)
+pcheckPred = plam $ \_f _l _r -> P.do
+  undefined
+
+--  let inner :: Term s (PMap PTokenName (PTheseData PInteger PInteger) :--> PBool)
+--      inner = pmapAll # f
+--  pmapAll # inner # (punionVal # l # r)
 
 pcheckBinRel ::
   forall {s :: S}.
@@ -100,8 +70,24 @@ pcheckBinRel = plam $ \f l r -> P.do
           PDThese r -> f # (pfield @"_0" # r) # (pfield @"_1" # r)
   pcheckPred # unThese # l # r
 
+-- | Establishes if a value is less than or equal to another.
 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
+
+-- | Establishes if a value is strictly less than another.
+plt :: Term s (PValue :--> PValue :--> PBool)
+plt = plam $ \v0 v1 -> (pcheckBinRel # plt') # v0 # v1
+
+plt' :: Term s (PInteger :--> PInteger :--> PBool)
+plt' = plam $ \m n -> m #< n
+
+-- | Establishes if a value is greater than or equal to another.
+pgeq :: Term s (PValue :--> PValue :--> PBool)
+pgeq = plam $ \v0 v1 -> pnot #$ plt # v0 # v1
+
+-- | Establishes if a value is strictly greater than another.
+pgt :: Term s (PValue :--> PValue :--> PBool)
+pgt = plam $ \v0 v1 -> pnot #$ pleq # v0 # v1
diff --git a/src/Plutarch/Api/V1/These.hs b/src/Plutarch/Api/V1/These.hs
new file mode 100644
index 0000000..e1ae1ed
--- /dev/null
+++ b/src/Plutarch/Api/V1/These.hs
@@ -0,0 +1,62 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Plutarch.Api.V1.These (PTheseData (..)) where
+
+import GHC.Generics qualified as GHC
+import Generics.SOP
+import Plutarch.DataRepr (PIsDataReprInstances (PIsDataReprInstances))
+import Plutarch.Lift (
+  PConstantRepr,
+  PConstanted,
+  PLifted,
+  PUnsafeLiftDecl,
+  pconstantFromRepr,
+  pconstantToRepr,
+ )
+import Plutus.V1.Ledger.Api qualified as Plutus
+import PlutusTx.These qualified as PlutusThese
+
+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)
+
+{- TODO: Make PTheseData an instance of PConstant:
+         https://github.com/Plutonomicon/plutarch/pull/355
+-}
+
+instance
+  ( PLifted (PConstanted a) ~ a
+  , Plutus.ToData b
+  , Plutus.FromData b
+  , Plutus.ToData a
+  , Plutus.FromData a
+  , PConstant a
+  , PLifted (PConstanted b) ~ b
+  , Plutus.FromData b
+  , Plutus.ToData b
+  , PConstant b
+  ) =>
+  PConstant (PlutusThese.These a b)
+  where
+  type PConstantRepr (PlutusThese.These a b) = [(Plutus.Data, Plutus.Data)]
+  type PConstanted (PlutusThese.These a b) = PTheseData (PConstanted a) (PConstanted b)
+  pconstantToRepr _t = undefined
+  pconstantFromRepr _t = undefined
diff --git a/src/Plutarch/These.hs b/src/Plutarch/These.hs
new file mode 100644
index 0000000..f9b225a
--- /dev/null
+++ b/src/Plutarch/These.hs
@@ -0,0 +1,12 @@
+module Plutarch.These (PThese (..)) where
+
+import GHC.Generics qualified as GHC
+import Generics.SOP
+
+-- | Plutus These type with Scott-encoded representation.
+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)