{-# LANGUAGE QuantifiedConstraints #-}

{- |
 Module: Plutarch.Extra.Map
 Copyright: (C) Liqwid Labs 2022
 License: Apache 2.0
 Maintainer: Koz Ross <[email protected]>
 Portability: GHC only
 Stability: Experimental

 Various helpers for 'PMap' use. This module is intended to be imported
 qualified.
-}
module Plutarch.Extra.Map (
  -- * Lookup
  ptryLookup,
  plookupGe,

  -- * Comparisons
  pkeysEqual,
  pkeysEqualUnsorted,

  -- * Modification
  pupdate,
  padjust,

  -- * Folds
  pfoldMapWithKey,
  pfoldlWithKey,

  -- * Elimination
  phandleMin,

  -- * Conversion
  punsortedMapFromFoldable,
  psortedMapFromFoldable,
  pkeys,

  -- * Key-value pair manipulation
  pkvPairKey,
  pkvPairValue,
  pkvPairLt,
) where

import Data.Foldable (foldl')
import Plutarch.Api.V1.AssocMap (
  KeyGuarantees (Sorted, Unsorted),
  PMap (PMap),
  pdelete,
  pempty,
  pinsert,
  plookup,
 )
import Plutarch.Builtin (ppairDataBuiltin)
import Plutarch.Extra.List (phandleList)
import Plutarch.Extra.Maybe (passertPJust)
import Plutarch.List qualified as PList

{- | Eliminates a sorted 'PMap', similarly to 'pelimList'. The function
 argument, if used, will be given the smallest key in the 'PMap', with its
 corresponding value, as well as the \'rest\' of the 'PMap'.

 @since 3.9.0
-}
phandleMin ::
  forall (r :: S -> Type) (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData k, PIsData v) =>
  Term s (PMap 'Sorted k v) ->
  Term s r ->
  (Term s k -> Term s v -> Term s (PMap 'Sorted k v) -> Term s r) ->
  Term s r
phandleMin :: forall (r :: S -> Type) (k :: S -> Type) (v :: S -> Type) (s :: S).
(PIsData k, PIsData v) =>
Term s (PMap 'Sorted k v)
-> Term s r
-> (Term s k -> Term s v -> Term s (PMap 'Sorted k v) -> Term s r)
-> Term s r
phandleMin Term s (PMap 'Sorted k v)
xs Term s r
whenNil Term s k -> Term s v -> Term s (PMap 'Sorted k v) -> Term s r
whenCons =
  forall (a :: S -> Type) (r :: S -> Type)
       (ell :: (S -> Type) -> S -> Type) (s :: S).
(PElemConstraint ell a, PListLike ell) =>
Term s (ell a)
-> Term s r -> (Term s a -> Term s (ell a) -> Term s r) -> Term s r
phandleList (forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s (PMap 'Sorted k v)
xs) Term s r
whenNil forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair (PAsData k) (PAsData v))
kv Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
kvs ->
    let k :: Term s k
k = forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv
        v :: Term s v
v = forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv
     in Term s k -> Term s v -> Term s (PMap 'Sorted k v) -> Term s r
whenCons Term s k
k Term s v
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: S -> Type) (v :: S -> Type)
       (s :: S).
Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> PMap keysort k v s
PMap forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
kvs

{- | As 'plookup', but also yields the portion of the 'PMap' whose keys are
 greater than the target if the search is successful.

 @since 3.9.0
-}
plookupGe ::
  forall (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData k, POrd k) =>
  Term s (k :--> PMap 'Sorted k v :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
plookupGe :: forall (k :: S -> Type) (v :: S -> Type) (s :: S).
(PIsData k, POrd k) =>
Term
  s
  (k
   :--> (PMap 'Sorted k v
         :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v))))
plookupGe = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s k
needle ->
    forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term
  s
  (PMap 'Sorted k v
   :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
self Term s (PMap 'Sorted k v)
xs ->
      forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (forall (s' :: S).
Term s' k
-> Term
     s'
     (PMap 'Sorted k v
      :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
-> Term s' (PBuiltinPair (PAsData k) (PAsData v))
-> Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> Term s' (PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
go Term s k
needle Term
  s
  (PMap 'Sorted k v
   :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
self) (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto forall a b. (a -> b) -> a -> b
$ Term s (PMap 'Sorted k v)
xs
  where
    go ::
      forall (s' :: S).
      Term s' k ->
      Term s' (PMap 'Sorted k v :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v))) ->
      Term s' (PBuiltinPair (PAsData k) (PAsData v)) ->
      Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))) ->
      Term s' (PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
    go :: forall (s' :: S).
Term s' k
-> Term
     s'
     (PMap 'Sorted k v
      :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
-> Term s' (PBuiltinPair (PAsData k) (PAsData v))
-> Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> Term s' (PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
go Term s' k
needle Term
  s'
  (PMap 'Sorted k v
   :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
self Term s' (PBuiltinPair (PAsData k) (PAsData v))
h Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
t =
      let current :: Term s' k
current = forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PBuiltinPair (PAsData k) (PAsData v))
h
       in forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s' k
needle forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s' k
current)
            (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair (forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PBuiltinPair (PAsData k) (PAsData v))
h) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: S -> Type) (v :: S -> Type)
       (s :: S).
Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> PMap keysort k v s
PMap forall a b. (a -> b) -> a -> b
$ Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
t)
            ( forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                (Term s' k
needle forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s' k
current)
                (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)
                (Term
  s'
  (PMap 'Sorted k v
   :--> PMaybe (PPair (PAsData v) (PMap 'Sorted k v)))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: S -> Type) (v :: S -> Type)
       (s :: S).
Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> PMap keysort k v s
PMap forall a b. (a -> b) -> a -> b
$ Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
t))
            )

{- | If a value exists at the specified key, apply the function argument to it;
 otherwise, do nothing.

 This is necessarily linear in the size of the map performance-wise, as we
 have to scan the entire map to find the key in the worst case.

 @since 3.4.0
-}
padjust ::
  forall (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData k, PEq k, PIsData v) =>
  Term s ((v :--> v) :--> k :--> PMap 'Unsorted k v :--> PMap 'Unsorted k v)
padjust :: forall (k :: S -> Type) (v :: S -> Type) (s :: S).
(PIsData k, PEq k, PIsData v) =>
Term
  s
  ((v :--> v)
   :--> (k :--> (PMap 'Unsorted k v :--> PMap 'Unsorted k v)))
padjust = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (v :--> v)
f Term s k
key Term s (PMap 'Unsorted k v)
kvs ->
    forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMap 'Unsorted k v)
kvs forall a b. (a -> b) -> a -> b
$ \(PMap Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
kvs') ->
      forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: S -> Type) (v :: S -> Type)
       (s :: S).
Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> PMap keysort k v s
PMap forall a b. (a -> b) -> a -> b
$ forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
PList.pmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s' :: S).
Term
  s'
  ((v :--> v)
   :--> (k
         :--> (PBuiltinPair (PAsData k) (PAsData v)
               :--> PBuiltinPair (PAsData k) (PAsData v))))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (v :--> v)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s k
key) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
kvs'
  where
    go ::
      forall (s' :: S).
      Term
        s'
        ( (v :--> v)
            :--> k
            :--> PBuiltinPair (PAsData k) (PAsData v)
            :--> PBuiltinPair (PAsData k) (PAsData v)
        )
    go :: forall (s' :: S).
Term
  s'
  ((v :--> v)
   :--> (k
         :--> (PBuiltinPair (PAsData k) (PAsData v)
               :--> PBuiltinPair (PAsData k) (PAsData v))))
go = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
      forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (v :--> v)
f Term s k
target Term s (PBuiltinPair (PAsData k) (PAsData v))
kv ->
        forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          ((forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv) forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s k
target)
          (forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (v :--> v)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData v =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> v)
pkvPairValue forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv))
          Term s (PBuiltinPair (PAsData k) (PAsData v))
kv

{- | As 'pkeysEqual', but requires only 'PEq' constraints for the keys, and
 works for 'Unsorted' 'PMap's. This requires a number of equality comparisons
 between keys proportional to the product of the lengths of both arguments:
 that is, this function is quadratic.

 @since 3.4.0
-}
pkeysEqualUnsorted ::
  forall (k :: S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PIsData k, PIsData a, PIsData b) =>
  Term s (PMap 'Unsorted k a :--> PMap 'Unsorted k b :--> PBool)
pkeysEqualUnsorted :: forall (k :: S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
(PIsData k, PIsData a, PIsData b) =>
Term s (PMap 'Unsorted k a :--> (PMap 'Unsorted k b :--> PBool))
pkeysEqualUnsorted = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PMap 'Unsorted k a)
kvs Term s (PMap 'Unsorted k b)
kvs' ->
    forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMap 'Unsorted k a)
kvs forall a b. (a -> b) -> a -> b
$ \(PMap Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell) ->
      forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMap 'Unsorted k b)
kvs' forall a b. (a -> b) -> a -> b
$ \(PMap Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell') ->
        forall (s' :: S).
Term
  s'
  (PMap 'Unsorted k a
   :--> (PMap 'Unsorted k b
         :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
               :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
                     :--> PBool))))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k a)
kvs forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k b)
kvs' forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell'
  where
    go ::
      forall (s' :: S).
      Term
        s'
        ( PMap 'Unsorted k a
            :--> PMap 'Unsorted k b
            :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
            :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
            :--> PBool
        )
    go :: forall (s' :: S).
Term
  s'
  (PMap 'Unsorted k a
   :--> (PMap 'Unsorted k b
         :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
               :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
                     :--> PBool))))
go = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
      forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term
  s
  (PMap 'Unsorted k a
   :--> (PMap 'Unsorted k b
         :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
               :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
                     :--> PBool))))
self Term s (PMap 'Unsorted k a)
kvs Term s (PMap 'Unsorted k b)
kvs' Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell' ->
        forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
PList.puncons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell) forall a b. (a -> b) -> a -> b
$ \case
          PMaybe
  (PPair
     (PBuiltinPair (PAsData k) (PAsData a))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))))
  s
PNothing -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
PList.puncons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell') forall a b. (a -> b) -> a -> b
$ \case
            -- We reached the end, so we match
            PMaybe
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
  s
PNothing -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue
            PJust Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
ht' -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
ht' forall a b. (a -> b) -> a -> b
$ \(PPair Term s (PBuiltinPair (PAsData k) (PAsData b))
h' Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
t') ->
              forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (k :: S -> Type) (v :: S -> Type) (s :: S)
       (any :: KeyGuarantees).
(PIsData k, PIsData v) =>
Term s (k :--> (PMap any k v :--> PMaybe v))
plookup forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData b))
h') forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k a)
kvs) forall a b. (a -> b) -> a -> b
$ \case
                -- We mismatch, so fail
                PMaybe a s
PNothing -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
                -- We match, so continue
                PJust Term s a
_ -> Term
  s
  (PMap 'Unsorted k a
   :--> (PMap 'Unsorted k b
         :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
               :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
                     :--> PBool))))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k a)
kvs forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k b)
kvs' forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
t'
          PJust Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData a))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))))
ht -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData a))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))))
ht forall a b. (a -> b) -> a -> b
$ \(PPair Term s (PBuiltinPair (PAsData k) (PAsData a))
h Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
t) ->
            forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
PList.puncons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell') forall a b. (a -> b) -> a -> b
$ \case
              PMaybe
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
  s
PNothing -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (k :: S -> Type) (v :: S -> Type) (s :: S)
       (any :: KeyGuarantees).
(PIsData k, PIsData v) =>
Term s (k :--> (PMap any k v :--> PMaybe v))
plookup forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData a))
h) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k b)
kvs') forall a b. (a -> b) -> a -> b
$ \case
                -- We mismatch, so fail
                PMaybe b s
PNothing -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
                -- We match, so continue
                PJust Term s b
_ -> Term
  s
  (PMap 'Unsorted k a
   :--> (PMap 'Unsorted k b
         :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
               :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
                     :--> PBool))))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k a)
kvs forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k b)
kvs' forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
t forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell'
              -- To save some effort, we try both matches in one shot
              PJust Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
ht' -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
ht' forall a b. (a -> b) -> a -> b
$ \(PPair Term s (PBuiltinPair (PAsData k) (PAsData b))
h' Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
t') ->
                forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (k :: S -> Type) (v :: S -> Type) (s :: S)
       (any :: KeyGuarantees).
(PIsData k, PIsData v) =>
Term s (k :--> (PMap any k v :--> PMaybe v))
plookup forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData a))
h) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k b)
kvs') forall a b. (a -> b) -> a -> b
$ \case
                  -- We mismatch, so fail
                  PMaybe b s
PNothing -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
                  -- Try the other direction
                  PJust Term s b
_ -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (k :: S -> Type) (v :: S -> Type) (s :: S)
       (any :: KeyGuarantees).
(PIsData k, PIsData v) =>
Term s (k :--> (PMap any k v :--> PMaybe v))
plookup forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData b))
h') forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k a)
kvs) forall a b. (a -> b) -> a -> b
$ \case
                    -- We mismatch, so fail
                    PMaybe a s
PNothing -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
                    -- Both succeeded, so continue on tails
                    PJust Term s a
_ -> Term
  s
  (PMap 'Unsorted k a
   :--> (PMap 'Unsorted k b
         :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
               :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
                     :--> PBool))))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k a)
kvs forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted k b)
kvs' forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
t forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
t'

{- | Gives 'PTrue' if both argument 'PMap's contain mappings for exactly the
 same set of keys. Requires a number of equality comparisons between keys
 proportional to the length of the shorter argument.

 @since 1.1.0
-}
pkeysEqual ::
  forall (k :: S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PIsData k, PEq k) =>
  Term s (PMap 'Sorted k a :--> PMap 'Sorted k b :--> PBool)
pkeysEqual :: forall (k :: S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
(PIsData k, PEq k) =>
Term s (PMap 'Sorted k a :--> (PMap 'Sorted k b :--> PBool))
pkeysEqual = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PMap 'Sorted k a)
kvs Term s (PMap 'Sorted k b)
kvs' ->
    forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMap 'Sorted k a)
kvs forall a b. (a -> b) -> a -> b
$ \(PMap Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell) ->
      forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMap 'Sorted k b)
kvs' forall a b. (a -> b) -> a -> b
$ \(PMap Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell') ->
        forall (s' :: S).
Term
  s'
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
         :--> PBool))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell'
  where
    go ::
      forall (s' :: S).
      Term
        s'
        ( PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
            :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
            :--> PBool
        )
    go :: forall (s' :: S).
Term
  s'
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
         :--> PBool))
go = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
      forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
         :--> PBool))
self Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell' ->
        forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
PList.puncons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
ell) forall a b. (a -> b) -> a -> b
$ \case
          PMaybe
  (PPair
     (PBuiltinPair (PAsData k) (PAsData a))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))))
  s
PNothing -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
PList.puncons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell') forall a b. (a -> b) -> a -> b
$ \case
            PMaybe
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
  s
PNothing -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue -- no mismatches found
            PJust Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
_ -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse -- one argument too long
          PJust Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData a))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))))
kv -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
PList.puncons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
ell') forall a b. (a -> b) -> a -> b
$ \case
            PMaybe
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
  s
PNothing -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse -- one argument too long
            PJust Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
kv' -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData a))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))))
kv forall a b. (a -> b) -> a -> b
$ \(PPair Term s (PBuiltinPair (PAsData k) (PAsData a))
h Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
t) ->
              forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PPair
     (PBuiltinPair (PAsData k) (PAsData b))
     (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))))
kv' forall a b. (a -> b) -> a -> b
$ \(PPair Term s (PBuiltinPair (PAsData k) (PAsData b))
h' Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
t') ->
                forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                  ((forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData a))
h) forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData b))
h'))
                  (Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b))
         :--> PBool))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
t forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
t') -- continue
                  (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse) -- key mismatch

{- | Get the key of a key-value pair.

 @since 1.1.0
-}
pkvPairKey ::
  forall (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData k) =>
  Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey :: forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair (PAsData k) (PAsData v))
kv -> forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv)

{- | Get the value of a key-value pair.

 @since 3.4.0
-}
pkvPairValue ::
  forall (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData v) =>
  Term s (PBuiltinPair (PAsData k) (PAsData v) :--> v)
pkvPairValue :: forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData v =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> v)
pkvPairValue = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair (PAsData k) (PAsData v))
kv -> forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv)

{- | Compare two key-value pairs by their keys. Gives 'PTrue' if the key of the
 first argument pair is less than the key of the second argument pair.

 @since 3.4.0
-}
pkvPairLt ::
  forall (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData k, PPartialOrd k) =>
  Term
    s
    ( PBuiltinPair (PAsData k) (PAsData v)
        :--> PBuiltinPair (PAsData k) (PAsData v)
        :--> PBool
    )
pkvPairLt :: forall (k :: S -> Type) (v :: S -> Type) (s :: S).
(PIsData k, PPartialOrd k) =>
Term
  s
  (PBuiltinPair (PAsData k) (PAsData v)
   :--> (PBuiltinPair (PAsData k) (PAsData v) :--> PBool))
pkvPairLt = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair (PAsData k) (PAsData v))
kv Term s (PBuiltinPair (PAsData k) (PAsData v))
kv' ->
    (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv) forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv')

{- | As 'plookup', but errors when the key is missing.

 @since 3.4.0
-}
ptryLookup ::
  forall (k :: S -> Type) (v :: S -> Type) (keys :: KeyGuarantees) (s :: S).
  (PIsData k, PIsData v) =>
  Term s (k :--> PMap keys k v :--> v)
ptryLookup :: forall (k :: S -> Type) (v :: S -> Type) (keys :: KeyGuarantees)
       (s :: S).
(PIsData k, PIsData v) =>
Term s (k :--> (PMap keys k v :--> v))
ptryLookup = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s k
k Term s (PMap keys k v)
kvs ->
    forall (a :: S -> Type) (s :: S).
Term s (PString :--> (PMaybe a :--> a))
passertPJust
      # "plookupPartial: No value found for key."
      # (plookup # k # kvs)

{- | Given a 'Foldable' of key-value pairs, construct an unsorted 'PMap'.
 Performs linearly with respect to its argument.

 = Note

 If there are duplicate keys in the input, the /last/ key will \'win\' in a
 lookup.

 @since 3.4.0
-}
punsortedMapFromFoldable ::
  forall (k :: S -> Type) (v :: S -> Type) (f :: Type -> Type) (s :: S).
  (Foldable f, PIsData k, PIsData v) =>
  f (Term s k, Term s v) ->
  Term s (PMap 'Unsorted k v)
punsortedMapFromFoldable :: forall (k :: S -> Type) (v :: S -> Type) (f :: Type -> Type)
       (s :: S).
(Foldable f, PIsData k, PIsData v) =>
f (Term s k, Term s v) -> Term s (PMap 'Unsorted k v)
punsortedMapFromFoldable = forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: S -> Type) (v :: S -> Type)
       (s :: S).
Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> PMap keysort k v s
PMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall (s' :: S).
Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> (Term s' k, Term s' v)
-> Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
go (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: S -> Type) (s :: S). PBuiltinList a s
PNil)
  where
    go ::
      forall (s' :: S).
      Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))) ->
      (Term s' k, Term s' v) ->
      Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
    go :: forall (s' :: S).
Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> (Term s' k, Term s' v)
-> Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
go Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
acc (Term s' k
key, Term s' v
val) =
      forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S).
Term s a -> Term s (PBuiltinList a) -> PBuiltinList a s
PCons (forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s' k
key forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s' v
val) forall a b. (a -> b) -> a -> b
$ Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
acc

{- | Given a 'Foldable' of (not necessarily sorted) key-value pairs, construct a
 'PMap' which is guaranteed sorted. Performs a linear number of ordered
 insertions with respect to the length of its argument.

 = Note

 If there are duplicate keys, only the /last/ key-value pair will remain in
 the result.

 @since 3.4.0
-}
psortedMapFromFoldable ::
  forall (k :: S -> Type) (v :: S -> Type) (f :: Type -> Type) (s :: S).
  (Foldable f, POrd k, PIsData k, PIsData v) =>
  f (Term s k, Term s v) ->
  Term s (PMap 'Sorted k v)
psortedMapFromFoldable :: forall (k :: S -> Type) (v :: S -> Type) (f :: Type -> Type)
       (s :: S).
(Foldable f, POrd k, PIsData k, PIsData v) =>
f (Term s k, Term s v) -> Term s (PMap 'Sorted k v)
psortedMapFromFoldable = forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall (s' :: S).
Term s' (PMap 'Sorted k v)
-> (Term s' k, Term s' v) -> Term s' (PMap 'Sorted k v)
go forall (s :: S) (k :: S -> Type) (v :: S -> Type).
Term s (PMap 'Sorted k v)
pempty
  where
    go ::
      forall (s' :: S).
      Term s' (PMap 'Sorted k v) ->
      (Term s' k, Term s' v) ->
      Term s' (PMap 'Sorted k v)
    go :: forall (s' :: S).
Term s' (PMap 'Sorted k v)
-> (Term s' k, Term s' v) -> Term s' (PMap 'Sorted k v)
go Term s' (PMap 'Sorted k v)
acc (Term s' k
key, Term s' v
val) = forall (k :: S -> Type) (v :: S -> Type) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term s (k :--> (v :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
pinsert forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' k
key forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' v
val forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PMap 'Sorted k v)
acc

{- | Get a list-like structure full of the keys of the argument 'PMap'. If the
 'PMap' is 'Sorted', the keys will maintain that order, and will be unique;
 otherwise, the order is unspecified, and duplicates may exist.

 = Note

 You will need to specify what manner of list-like structure you want; we have
 arranged the type signature to make specifying this easy with
 @TypeApplications@.

 @since 3.4.0
-}
pkeys ::
  forall
    (ell :: (S -> Type) -> S -> Type)
    (k :: S -> Type)
    (v :: S -> Type)
    (keys :: KeyGuarantees)
    (s :: S).
  (PListLike ell, PElemConstraint ell (PAsData k)) =>
  Term s (PMap keys k v :--> ell (PAsData k))
pkeys :: forall (ell :: (S -> Type) -> S -> Type) (k :: S -> Type)
       (v :: S -> Type) (keys :: KeyGuarantees) (s :: S).
(PListLike ell, PElemConstraint ell (PAsData k)) =>
Term s (PMap keys k v :--> ell (PAsData k))
pkeys = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PMap keys k v)
kvs -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMap keys k v)
kvs forall a b. (a -> b) -> a -> b
$ \(PMap Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
kvs') ->
    forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList forall (s' :: S).
Term
  s'
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> ell (PAsData k))
-> Term s' (PBuiltinPair (PAsData k) (PAsData v))
-> Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> Term s' (ell (PAsData k))
go (forall a b. a -> b -> a
const forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
kvs'
  where
    go ::
      forall (s' :: S).
      Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)) :--> ell (PAsData k)) ->
      Term s' (PBuiltinPair (PAsData k) (PAsData v)) ->
      Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))) ->
      Term s' (ell (PAsData k))
    go :: forall (s' :: S).
Term
  s'
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> ell (PAsData k))
-> Term s' (PBuiltinPair (PAsData k) (PAsData v))
-> Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> Term s' (ell (PAsData k))
go Term
  s'
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> ell (PAsData k))
self Term s' (PBuiltinPair (PAsData k) (PAsData v))
kv Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
acc = forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PBuiltinPair (PAsData k) (PAsData v))
kv) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term
  s'
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> ell (PAsData k))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
acc)

{- | Given an \'updater\' and a key, if the key exists in the 'PMap', apply the
 \'updater\' to it, otherwise do nothing. If the \'updater\' produces
 'PNothing', the value is deleted; otherwise, it is modified to the result.

 Performance will be equivalent to a lookup followed by an insert (or delete),
 as well as the cost of calling the \'updater\'.

 @since 3.4.0
-}
pupdate ::
  forall (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData k, PIsData v, POrd k) =>
  Term s ((v :--> PMaybe v) :--> k :--> PMap 'Sorted k v :--> PMap 'Sorted k v)
pupdate :: forall (k :: S -> Type) (v :: S -> Type) (s :: S).
(PIsData k, PIsData v, POrd k) =>
Term
  s
  ((v :--> PMaybe v)
   :--> (k :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
pupdate = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (v :--> PMaybe v)
updater Term s k
key Term s (PMap 'Sorted k v)
kvs -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (k :: S -> Type) (v :: S -> Type) (s :: S)
       (any :: KeyGuarantees).
(PIsData k, PIsData v) =>
Term s (k :--> (PMap any k v :--> PMaybe v))
plookup forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s k
key forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
kvs) forall a b. (a -> b) -> a -> b
$ \case
    PMaybe v s
PNothing -> Term s (PMap 'Sorted k v)
kvs
    PJust Term s v
val -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (v :--> PMaybe v)
updater forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s v
val) forall a b. (a -> b) -> a -> b
$ \case
      PMaybe v s
PNothing -> forall (k :: S -> Type) (s :: S) (v :: S -> Type).
(POrd k, PIsData k) =>
Term s (k :--> (PMap 'Sorted k v :--> PMap 'Sorted k v))
pdelete forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s k
key forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
kvs
      PJust Term s v
newVal -> forall (k :: S -> Type) (v :: S -> Type) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term s (k :--> (v :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
pinsert forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s k
key forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s v
newVal forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
kvs

{- | Left-associative fold of a 'PMap' with keys. Keys and values will be
 presented in key order.

 @since 3.4.0
-}
pfoldlWithKey ::
  forall (a :: S -> Type) (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData k, PIsData v) =>
  Term s ((a :--> k :--> v :--> a) :--> a :--> PMap 'Sorted k v :--> a)
pfoldlWithKey :: forall (a :: S -> Type) (k :: S -> Type) (v :: S -> Type) (s :: S).
(PIsData k, PIsData v) =>
Term
  s
  ((a :--> (k :--> (v :--> a)))
   :--> (a :--> (PMap 'Sorted k v :--> a)))
pfoldlWithKey = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (k :--> (v :--> a)))
f Term s a
x Term s (PMap 'Sorted k v)
kvs -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMap 'Sorted k v)
kvs forall a b. (a -> b) -> a -> b
$ \case
    PMap Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
kvs' ->
      forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (b :: S -> Type).
PIsListLike list a =>
Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
pfoldl forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s a
acc Term s (PBuiltinPair (PAsData k) (PAsData v))
kv -> Term s (a :--> (k :--> (v :--> a)))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
acc forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData k =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> k)
pkvPairKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (k :: S -> Type) (v :: S -> Type) (s :: S).
PIsData v =>
Term s (PBuiltinPair (PAsData k) (PAsData v) :--> v)
pkvPairValue forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
kv)) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
kvs'

{- | Project all key-value pairs into a 'Monoid', then combine. Keys and values
 will be presented in key order.

 @since 3.4.0
-}
pfoldMapWithKey ::
  forall (m :: S -> Type) (k :: S -> Type) (v :: S -> Type) (s :: S).
  (PIsData k, PIsData v, forall (s' :: S). Monoid (Term s' m)) =>
  Term s ((k :--> v :--> m) :--> PMap 'Sorted k v :--> m)
pfoldMapWithKey :: forall (m :: S -> Type) (k :: S -> Type) (v :: S -> Type) (s :: S).
(PIsData k, PIsData v, forall (s' :: S). Monoid (Term s' m)) =>
Term s ((k :--> (v :--> m)) :--> (PMap 'Sorted k v :--> m))
pfoldMapWithKey = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (k :--> (v :--> m))
f Term s (PMap 'Sorted k v)
kvs ->
    forall (a :: S -> Type) (k :: S -> Type) (v :: S -> Type) (s :: S).
(PIsData k, PIsData v) =>
Term
  s
  ((a :--> (k :--> (v :--> a)))
   :--> (a :--> (PMap 'Sorted k v :--> a)))
pfoldlWithKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s m
acc Term s k
k Term s v
v -> Term s m
acc forall a. Semigroup a => a -> a -> a
<> (Term s (k :--> (v :--> m))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s k
k forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s v
v)) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a. Monoid a => a
mempty forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
kvs