From fbbb9c984248305d58c6a50a3ee4519823072fc0 Mon Sep 17 00:00:00 2001 From: Hongrui Fang Date: Mon, 3 Oct 2022 21:25:26 +0800 Subject: [PATCH] place a lock on the stake while cosigning --- agora/Agora/Proposal.hs | 21 ++-- agora/Agora/Proposal/Scripts.hs | 56 ++++------ agora/Agora/Stake.hs | 192 ++++++++++++++++---------------- agora/Agora/Stake/Redeemers.hs | 112 +++++++++++-------- agora/Agora/Utils.hs | 86 ++++++++++++++ 5 files changed, 283 insertions(+), 184 deletions(-) diff --git a/agora/Agora/Proposal.hs b/agora/Agora/Proposal.hs index 663f3d1..7827035 100644 --- a/agora/Agora/Proposal.hs +++ b/agora/Agora/Proposal.hs @@ -235,6 +235,8 @@ data ProposalThresholds = ProposalThresholds -- ^ How much GT required to to move into 'Locked'. , vote :: Tagged GTTag Integer -- ^ How much GT required to vote on a outcome. + , cosign :: Tagged GTTag Integer + -- ^ How much GT required to cosign a proposal. } deriving stock ( -- | @since 0.1.0 @@ -366,20 +368,18 @@ data ProposalDatum = ProposalDatum {- | Haskell-level redeemer for Proposal scripts. - @since 0.1.0 + @since 1.0.0 -} data ProposalRedeemer = -- | Cast one or more votes towards a particular 'ResultTag'. Vote ResultTag - | -- | Add one or more public keys to the cosignature list. - -- Must be signed by those cosigning. + | -- | Add a credential to the cosignature list. + -- Must be authorized by the stake owner. -- -- This is particularly used in the 'Draft' 'ProposalStatus', - -- where matching 'Agora.Stake.Stake's can be called to advance the proposal, - -- provided enough GT is shared among them. - -- - -- This list should be sorted in ascending order. - Cosign [Credential] + -- where matching 'Agora.Stake.Stake's can be witnessed to advance the + -- proposal, provided enough GT is shared among them. + Cosign | -- | Allow unlocking one or more stakes with votes towards particular 'ResultTag'. Unlock | -- | Advance the proposal, performing the required checks for whether that is legal. @@ -564,6 +564,7 @@ newtype PProposalThresholds (s :: S) = PProposalThresholds , "create" ':= PDiscrete GTTag , "toVoting" ':= PDiscrete GTTag , "vote" ':= PDiscrete GTTag + , "cosign" ':= PDiscrete GTTag ] ) } @@ -748,7 +749,7 @@ deriving via (DerivePConstantViaDataList ProposalDatum PProposalDatum) instance -} data PProposalRedeemer (s :: S) = PVote (Term s (PDataRecord '["resultTag" ':= PResultTag])) - | PCosign (Term s (PDataRecord '["newCosigners" ':= PBuiltinList (PAsData PCredential)])) + | PCosign (Term s (PDataRecord '[])) | PUnlock (Term s (PDataRecord '[])) | PAdvanceProposal (Term s (PDataRecord '[])) deriving stock @@ -964,6 +965,8 @@ pisProposalThresholdsValid = phoistAcyclic $ 0 #<= pfromData thresholdsF.toVoting , ptraceIfFalse "Vote threshold is less than or equal to 0" $ 0 #<= pfromData thresholdsF.vote + , ptraceIfFalse "Cosign threshold is less than or equal to 0" $ + 0 #<= pfromData thresholdsF.cosign ] {- | Retract votes given the option and the amount of votes. diff --git a/agora/Agora/Proposal/Scripts.hs b/agora/Agora/Proposal/Scripts.hs index 9d7f5ec..4d9549a 100644 --- a/agora/Agora/Proposal/Scripts.hs +++ b/agora/Agora/Proposal/Scripts.hs @@ -10,7 +10,6 @@ module Agora.Proposal.Scripts ( proposalPolicy, ) where -import Agora.Credential (authorizationContext, pauthorizedBy) import Agora.Proposal ( PProposalDatum (PProposalDatum), PProposalRedeemer (PAdvanceProposal, PCosign, PUnlock, PVote), @@ -31,12 +30,13 @@ import Agora.Scripts (AgoraScripts, governorSTSymbol, proposalSTSymbol, stakeSTA import Agora.Stake ( PStakeDatum, pextractVoteOption, - pgetStakeRole, + pgetStakeRoles, pisIrrelevant, - pisPureCreator, pisVoter, ) import Agora.Utils ( + pfromSingleton, + pinsertUniqueBy, plistEqualsBy, pmapMaybe, ) @@ -64,7 +64,7 @@ import Plutarch.Extra.Maybe ( pmaybe, pnothing, ) -import Plutarch.Extra.Ord (pallUnique, pfromOrdBy, psort, ptryMergeBy) +import Plutarch.Extra.Ord (pfromOrdBy, psort) import Plutarch.Extra.Record (mkRecordConstr, (.&), (.=)) import Plutarch.Extra.ScriptContext ( pfindTxInByTxOutRef, @@ -226,8 +226,6 @@ proposalValidator as maximumCosigners = currentTime <- pletC $ currentProposalTime # txInfoF.validRange - authorizedBy <- pletC $ pauthorizedBy # authorizationContext txInfoF - ---------------------------------------------------------------------------- PSpending ((pfield @"_0" #) -> propsalInputRef) <- @@ -406,38 +404,30 @@ proposalValidator as maximumCosigners = pure $ popaque $ pmatch proposalRedeemer $ \case - PCosign r -> witnessStakes $ \sctxF -> do + PCosign _ -> spendStakes $ \sctxF -> do pguardC "Should be in draft state" $ currentStatus #== pconstant Draft - newSigs <- pletC $ pfield @"newCosigners" # r + stakeF <- + pletFieldsC @'["owner", "stakedAmount"] $ + ptrace "Exactly one stake input" $ + pfromSingleton # sctxF.inputStakes - pguardC "Signed by all new cosigners" $ - pall # plam ((authorizedBy #) . pfromData) # newSigs + let newCosigner = stakeF.owner - -- Assuming that new signatures encoded in the redeemer and exsiting - -- cosigners are sorted in ascending order, the new list of - -- signatures will be ordered. updatedSigs <- pletC $ - ptryMergeBy # (pfromOrdBy # plam pfromData) - # newSigs - # proposalInputDatumF.cosigners + ptrace "Update signature set" $ + pinsertUniqueBy + # (pfromOrdBy # plam pfromData) + # newCosigner + # proposalInputDatumF.cosigners pguardC "Less cosigners than maximum limit" $ plength # updatedSigs #< pconstant maximumCosigners - -- assuming sigs are sorted - PJust cosUnique <- pmatchC $ pallUnique #$ pmap # plam pfromData # updatedSigs - pguardC "Cosigners are unique" cosUnique - - pguardC "All new cosigners are witnessed by their Stake datums" $ - -- Also, this ensures that the cosigners field in the output - -- propopsal datum is ordered. - plistEqualsBy - # plam (\x (pfromData -> y) -> x #== y) - # sctxF.orderedOwners - # newSigs + pguardC "Meet minimum GT requirement" $ + pfromData thresholdsF.cosign #<= stakeF.stakedAmount let expectedDatum = mkRecordConstr @@ -469,7 +459,7 @@ proposalValidator as maximumCosigners = pguardC "Same stake shouldn't vote on the same proposal twice" $ pnot #$ pisVoter - #$ pgetStakeRole + #$ pgetStakeRoles # proposalInputDatumF.proposalId # stakeF.lockedBy @@ -542,17 +532,17 @@ proposalValidator as maximumCosigners = @'["stakedAmount", "lockedBy"] stake - stakeRole <- + stakeRoles <- pletC $ - pgetStakeRole + pgetStakeRoles # proposalInputDatumF.proposalId # stakeF.lockedBy pguardC "Stake input should be relevant" $ - pnot #$ pisIrrelevant # stakeRole + pnot #$ pisIrrelevant # stakeRoles let canRetractVotes = - pnot #$ pisPureCreator # stakeRole + pisVoter # stakeRoles voteCount = pextract @@ -561,7 +551,7 @@ proposalValidator as maximumCosigners = newVotes = pretractVotes - # (pextractVoteOption # stakeRole) + # (pextractVoteOption # stakeRoles) # voteCount # votes diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs index b5b3aab..f8296f2 100644 --- a/agora/Agora/Stake.hs +++ b/agora/Agora/Stake.hs @@ -34,10 +34,10 @@ module Agora.Stake ( pstakeLocked, pnumCreatedProposals, pextractVoteOption, - pgetStakeRole, + pgetStakeRoles, pisVoter, pisCreator, - pisPureCreator, + pisCosigner, pisIrrelevant, runStakeRedeemerHandler, ) where @@ -51,6 +51,7 @@ import Agora.Proposal ( ResultTag, ) import Agora.SafeMoney (GTTag) +import Agora.Utils (pmapMaybe, ppureIf) import Data.Tagged (Tagged) import Generics.SOP qualified as SOP import Plutarch.Api.V1 (PCredential) @@ -68,6 +69,8 @@ import Plutarch.Extra.IsData ( PlutusTypeDataList, ProductIsData (ProductIsData), ) +import "liqwid-plutarch-extra" Plutarch.Extra.List (pfindJust) +import Plutarch.Extra.Maybe (passertPJust, pjust, pnothing) import Plutarch.Extra.Sum (PSum (PSum)) import Plutarch.Extra.Traversable (pfoldMap) import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (PLifted)) @@ -128,6 +131,7 @@ data ProposalLock -- ^ The identifier of the proposal. ResultTag -- ^ The option which was voted on. This allows votes to be retracted. + | Cosigned ProposalId deriving stock ( -- | @since 0.1.0 Show @@ -139,6 +143,7 @@ PlutusTx.makeIsDataIndexed ''ProposalLock [ ('Created, 0) , ('Voted, 1) + , ('Cosigned, 2) ] {- | Haskell-level redeemer for Stake scripts. @@ -292,8 +297,6 @@ data PStakeRedeemer (s :: S) ) deriving anyclass ( -- | @since 0.1.0 - SOP.Generic - , -- | @since 0.1.0 PlutusType , -- | @since 0.1.0 PIsData @@ -337,6 +340,14 @@ data PProposalLock (s :: S) ] ) ) + | PCosigned + ( Term + s + ( PDataRecord + '[ "cosigned" ':= PProposalId + ] + ) + ) deriving stock ( -- | @since 0.1.0 Generic @@ -403,7 +414,7 @@ pnumCreatedProposals = {- | The role of a stake for a particular proposal. Scott-encoded. - @since 0.2.0 + @since 1.0.0 -} data PStakeRole (s :: S) = -- | The stake was used to vote on the proposal. @@ -412,26 +423,24 @@ data PStakeRole (s :: S) -- ^ The option which was voted for. | -- | The stake was used to create the proposal. PCreator - | -- | The stake was used to both create and vote on the proposal. - PBoth - (Term s PResultTag) - -- ^ The option which was voted for. - | -- | The stake has nothing to do with the given proposal. - PIrrelevant + | -- | The stake was used to cosign the propsoal. + PCosigner deriving stock - ( -- | @since 0.2.0 + ( -- | @since 1.0.0 Generic ) deriving anyclass - ( -- | @since 0.2.0 + ( -- | @since 1.0.0 PlutusType - , -- | @since 0.2.0 - PEq ) +-- | @since 1.0.0 instance DerivePlutusType PStakeRole where type DPTStrat _ = PlutusTypeScott +-- | @since 1.0.0 +type PStakeRoles = PList PStakeRole + -------------------------------------------------------------------------------- {- | Who authorizes the transaction? @@ -603,114 +612,103 @@ data StakeRedeemerImpl = StakeRedeemerImpl {- | Retutn true if the stake was used to voted on the proposal. - @since 0.2.0 + @since 1.0.0 -} -pisVoter :: forall (s :: S). Term s (PStakeRole :--> PBool) -pisVoter = phoistAcyclic $ - plam $ \sr -> pmatch sr $ \case - PVoter _ -> pconstant True - PBoth _ -> pconstant True - _ -> pconstant False +pisVoter :: forall (s :: S). Term s (PStakeRoles :--> PBool) +pisVoter = + phoistAcyclic $ + pany + #$ plam + ( \r -> pmatch r $ \case + PVoter _ -> pconstant True + _ -> pconstant False + ) {- | Retutn true if the stake was used to create the proposal. - @since 0.2.0 + @since 1.0.0 -} -pisCreator :: forall (s :: S). Term s (PStakeRole :--> PBool) -pisCreator = phoistAcyclic $ - plam $ \sr -> pmatch sr $ \case - PCreator -> pconstant True - PBoth _ -> pconstant True - _ -> pconstant False +pisCreator :: forall (s :: S). Term s (PStakeRoles :--> PBool) +pisCreator = + phoistAcyclic $ + pany + #$ plam + ( \r -> pmatch r $ \case + PCreator -> pconstant True + _ -> pconstant False + ) -{- | Retutn true if the stake was used to create the proposal, but not vote on - the proposal. +{- | Retutn true if the stake was used to cosign the proposal. - @since 0.2.0 + @since 1.0.0 -} -pisPureCreator :: forall (s :: S). Term s (PStakeRole :--> PBool) -pisPureCreator = phoistAcyclic $ - plam $ \sr -> pmatch sr $ \case - PCreator -> pconstant True - _ -> pconstant False +pisCosigner :: forall (s :: S). Term s (PStakeRoles :--> PBool) +pisCosigner = + phoistAcyclic $ + pany + #$ plam + ( \r -> pmatch r $ \case + PCosigner -> pconstant True + _ -> pconstant False + ) {- | Return true if the stake isn't related to the proposal. - @since 0.2.0 + @since 1.0.0 -} -pisIrrelevant :: forall (s :: S). Term s (PStakeRole :--> PBool) -pisIrrelevant = phoistAcyclic $ - plam $ \sr -> pmatch sr $ \case - PIrrelevant -> pconstant True - _ -> pconstant False +pisIrrelevant :: forall (s :: S). Term s (PStakeRoles :--> PBool) +pisIrrelevant = pnull {- | Get the role of a stake for the proposal specified by the poroposal id, given the 'StakeDatum.lockedBy' field of the stake. - Note that the list of locks is cosidered valid only if it contains at most - two locks from the given proposal: one voter lock and one creator lock. - - @since 0.2.0 + @since 1.0.0 -} -pgetStakeRole :: +pgetStakeRoles :: forall (s :: S). Term s ( PProposalId :--> PBuiltinList (PAsData PProposalLock) - :--> PStakeRole + :--> PStakeRoles ) -pgetStakeRole = phoistAcyclic $ - plam $ \pid locks -> - pfoldl +pgetStakeRoles = phoistAcyclic $ + plam $ \pid -> + pmapMaybe # plam - ( \role (pfromData -> lock) -> - let thisRole = pmatch lock $ \case - PCreated ((pfield @"created" #) -> pid') -> - pif - (pid' #== pid) - (pcon PCreator) - (pcon PIrrelevant) - PVoted lock' -> pletAll lock' $ \lockF -> - pif - (lockF.votedOn #== pid) - (pcon $ PVoter lockF.votedFor) - (pcon PIrrelevant) - in pcombineStakeRole # thisRole # role + ( flip + pmatch + ( \case + PCreated ((pfield @"created" #) -> pid') -> + ppureIf + # (pid' #== pid) + # pcon PCreator + PVoted r -> pletAll r $ \rF -> + ppureIf + # (rF.votedOn #== pid) + # pcon (PVoter rF.votedFor) + PCosigned ((pfield @"cosigned" #) -> pid') -> + ppureIf + # (pid' #== pid) + # pcon PCosigner + ) + . pfromData ) - # pcon PIrrelevant - # locks - where - pcombineStakeRole :: - forall (s :: S). - Term - s - ( PStakeRole - :--> PStakeRole - :--> PStakeRole - ) - pcombineStakeRole = phoistAcyclic $ - plam $ \x y -> - let cannotCombine = ptraceError "duplicate roles" - in pmatch x $ \case - PVoter r -> pmatch y $ \case - PCreator -> pcon $ PBoth r - PIrrelevant -> x - _ -> cannotCombine - PCreator -> pmatch y $ \case - PVoter r -> pcon $ PBoth r - PIrrelevant -> x - _ -> cannotCombine - PBoth _ -> cannotCombine - PIrrelevant -> y {- | Get the outcome that was voted for. - @since 0.2.0 + @since 1.0.0 -} -pextractVoteOption :: forall (s :: S). Term s (PStakeRole :--> PResultTag) -pextractVoteOption = phoistAcyclic $ - plam $ \sr -> pmatch sr $ \case - PVoter r -> r - PBoth r -> r - _ -> ptraceError "not voter" +pextractVoteOption :: forall (s :: S). Term s (PStakeRoles :--> PResultTag) +pextractVoteOption = + phoistAcyclic $ + plam $ + (passertPJust # "not voter" #) + . ( pfindJust + # plam + ( flip pmatch $ \case + PVoter r -> pjust # r + _ -> pnothing + ) + # + ) diff --git a/agora/Agora/Stake/Redeemers.hs b/agora/Agora/Stake/Redeemers.hs index 01216ec..0e43a96 100644 --- a/agora/Agora/Stake/Redeemers.hs +++ b/agora/Agora/Stake/Redeemers.hs @@ -16,7 +16,7 @@ module Agora.Stake.Redeemers ( import Agora.Proposal ( PProposalId, - PProposalRedeemer (PUnlock, PVote), + PProposalRedeemer (PCosign, PUnlock, PVote), ProposalStatus (Finished), ) import Agora.Stake ( @@ -25,7 +25,7 @@ import Agora.Stake ( PNoProposal, PSpendProposal ), - PProposalLock (PCreated, PVoted), + PProposalLock (PCosigned, PCreated, PVoted), PSigContext (owner, signedBy), PSignedBy ( PSignedByDelegate, @@ -187,35 +187,47 @@ paddNewLock = phoistAcyclic $ @since 1.0.0 -} ppermitVote :: forall (s :: S). Term s PStakeRedeemerHandler -ppermitVote = phoistAcyclic $ - pvoteHelper #$ phoistAcyclic $ - plam $ \ctx -> unTermCont $ do - ctxF <- pmatchC ctx +ppermitVote = pvoteHelper #$ phoistAcyclic $ + plam $ \ctx -> unTermCont $ do + ctxF <- pmatchC ctx - let withOnlyOneStakeInput = - plam $ \lock -> unTermCont $ do - pguardC "Only one stake input allowed" $ - pisSingleton # ctxF.stakeInputDatums + withOnlyOneStakeInput <- pletC $ + plam $ \lock -> unTermCont $ do + pguardC "Only one stake input allowed" $ + pisSingleton # ctxF.stakeInputDatums - pure lock + pure lock - pure $ - paddNewLock #$ pmatch ctxF.proposalContext $ \case - PSpendProposal pid _ r -> pmatch r $ \case - PVote ((pfromData . (pfield @"resultTag" #)) -> voteFor) -> - mkRecordConstr - PVoted - ( #votedOn .= pdata pid - .& #votedFor .= pdata voteFor - ) - _ -> ptraceError "Expected Vote" - PNewProposal pid -> + pure $ + paddNewLock #$ pmatch ctxF.proposalContext $ \case + PSpendProposal pid _ r -> pmatch r $ \case + PVote ((pfromData . (pfield @"resultTag" #)) -> voteFor) -> + mkRecordConstr + PVoted + ( #votedOn .= pdata pid + .& #votedFor .= pdata voteFor + ) + PCosign _ -> withOnlyOneStakeInput #$ mkRecordConstr - PCreated - ( #created .= pdata pid + PCosigned + ( #cosigned .= pdata pid ) - _ -> ptraceError "Expected proposal" + _ -> ptraceError "Expected Vote" + PNewProposal pid -> + withOnlyOneStakeInput + #$ mkRecordConstr + PCreated + ( #created .= pdata pid + ) + _ -> ptraceError "Expected proposal" + +data PRemoveLocksMode (s :: S) = PRemoveVoterLockOnly | PRemoveAllLocks + deriving stock (Generic) + deriving anyclass (PlutusType, PEq) + +instance DerivePlutusType PRemoveLocksMode where + type DPTStrat _ = PlutusTypeScott {- | Remove stake locks with the proposal id given the list of existing locks. The first parameter controls whether to revmove creator locks or not. @@ -225,36 +237,46 @@ premoveLocks :: Term s ( PProposalId - :--> PBool + :--> PRemoveLocksMode :--> PBuiltinList (PAsData PProposalLock) :--> PBuiltinList (PAsData PProposalLock) ) premoveLocks = phoistAcyclic $ - plam $ \pid rc -> - pfilter - # plam - ( \(pfromData -> l) -> pnot #$ pmatch l $ \case - PCreated ((pfield @"created" #) -> pid') -> rc #&& pid' #== pid - PVoted ((pfield @"votedOn" #) -> pid') -> pid' #== pid - ) + plam $ \pid rl -> unTermCont $ do + shouldRemoveOtherLocks <- pletC $ + plam $ \pid' -> + pid' #== pid #&& rl #== pcon PRemoveAllLocks + + pure $ + pfilter + # plam + ( \(pfromData -> l) -> pnot #$ pmatch l $ \case + PCosigned ((pfield @"cosigned" #) -> pid') -> + shouldRemoveOtherLocks # pid' + PCreated ((pfield @"created" #) -> pid') -> + shouldRemoveOtherLocks # pid' + PVoted ((pfield @"votedOn" #) -> pid') -> pid' #== pid + ) {- | Default implementation of 'Agora.Stake.RetractVotes'. @since 1.0.0 -} pretractVote :: forall (s :: S). Term s PStakeRedeemerHandler -pretractVote = phoistAcyclic $ - pvoteHelper #$ phoistAcyclic $ - plam $ - flip pmatch $ \ctxF -> - pmatch ctxF.proposalContext $ \case - PSpendProposal pid s r -> pmatch r $ \case - PUnlock _ -> - let allowRemovingCreatorLock = - s #== pconstant Finished - in premoveLocks # pid # allowRemovingCreatorLock - _ -> ptraceError "Expected unlock" - _ -> ptraceError "Expected spending proposal" +pretractVote = pvoteHelper #$ phoistAcyclic $ + plam $ + flip pmatch $ \ctxF -> + pmatch ctxF.proposalContext $ \case + PSpendProposal pid s r -> pmatch r $ \case + PUnlock _ -> + let mode = + pif + (s #== pconstant Finished) + (pcon PRemoveAllLocks) + (pcon PRemoveVoterLockOnly) + in premoveLocks # pid # mode + _ -> ptraceError "Expected unlock" + _ -> ptraceError "Expected spending proposal" -- | Validation logic shared by 'pdelegateTo' and 'pclearDelegate'. pdelegateHelper :: diff --git a/agora/Agora/Utils.hs b/agora/Agora/Utils.hs index 61fc2e6..ecf1c2d 100644 --- a/agora/Agora/Utils.hs +++ b/agora/Agora/Utils.hs @@ -27,11 +27,19 @@ module Agora.Utils ( pisSingleton, pfromSingleton, pmapMaybe, + PAlternative (..), + ppureIf, + pltBy, + pinsertUniqueBy, ) where import Plutarch.Api.V1 (PPOSIXTime, PTokenName, PValidatorHash) import Plutarch.Api.V2 (PScriptHash) +import Plutarch.Extra.Applicative (PApplicative (ppure)) import Plutarch.Extra.Category (PCategory (pidentity)) +import Plutarch.Extra.Functor (PFunctor (PSubcategory)) +import Plutarch.Extra.Maybe (pnothing) +import Plutarch.Extra.Ord (PComparator, POrdering (PLT), pcompareBy, pequateBy) import Plutarch.Extra.Time (PCurrentTime (PCurrentTime)) import Plutarch.Unsafe (punsafeCoerce) import PlutusLedgerApi.V2 ( @@ -284,3 +292,81 @@ pmapMaybe = phoistAcyclic $ # (self # t) ) (const pnil) + +-- -- | @since 1.0.0 + +-- -- | @since 1.0.0 +-- ppureIf' + +infixl 3 #<|> + +-- | @since 1.0.0 +class (PApplicative f) => PAlternative (f :: PType -> PType) where + (#<|>) :: + forall (a :: PType) (s :: S). + (PSubcategory f a) => + Term s (f a :--> f a :--> f a) + pempty :: + forall (a :: PType) (s :: S). + (PSubcategory f a) => + Term s (f a) + +-- | @since 1.0.0 +instance PAlternative PMaybe where + (#<|>) = phoistAcyclic $ + plam $ \a b -> pmatch a $ \case + PNothing -> b + PJust _ -> a + pempty = pnothing + +-- | @since 1.0.0 +ppureIf :: + forall + (f :: PType -> PType) + (a :: PType) + (s :: S). + (PAlternative f, PSubcategory f a) => + Term s (PBool :--> a :--> f a) +ppureIf = phoistAcyclic $ + plam $ \cond x -> + pif + cond + (ppure # x) + pempty + +pltBy :: + forall (a :: PType) (s :: S). + Term + s + ( PComparator a + :--> a + :--> a + :--> PBool + ) +pltBy = phoistAcyclic $ + plam $ \c x y -> + pcompareBy # c # x # y #== pcon PLT + +-- | @since 1.0.0 +pinsertUniqueBy :: + forall (list :: PType -> PType) (a :: PType) (s :: S). + (PIsListLike list a) => + Term s (PComparator a :--> a :--> list a :--> list a) +pinsertUniqueBy = phoistAcyclic $ + plam $ \c x -> + let lt = pltBy # c + eq = pequateBy # c + in precList + ( \self h t -> + let ensureUniqueness = + pif + (eq # x # h) + (ptraceError "inserted value already exists") + next = + pif + (lt # x # h) + (pcons # x #$ pcons # h # t) + (pcons # h #$ self # t) + in ensureUniqueness next + ) + (const $ psingleton # x)