{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Plutarch.Api.V1.AssocMap (
  PMap (PMap),
  KeyGuarantees (Unsorted, Sorted),

  -- * Creation
  pempty,
  psingleton,
  psingletonData,
  pinsert,
  pinsertData,
  pdelete,
  pfromAscList,
  passertSorted,
  pforgetSorted,

  -- * Lookups
  plookup,
  plookupData,
  pfindWithDefault,
  pfoldAt,
  pnull,

  -- * Folds
  pall,
  pany,

  -- * Filters and traversals
  pfilter,
  pmap,
  pmapData,
  pmapMaybe,
  pmapMaybeData,

  -- * Combining
  pdifference,
  punionWith,
  punionWithData,

  -- * Partial order operations
  pcheckBinRel,
) where

import PlutusLedgerApi.V1 qualified as Plutus
import PlutusTx.AssocMap qualified as PlutusMap
import PlutusTx.Monoid qualified as PlutusTx
import PlutusTx.Semigroup qualified as PlutusTx

import Plutarch.Builtin (
  pasMap,
  pdataImpl,
  pforgetData,
  pfromDataImpl,
  ppairDataBuiltin,
 )
import Plutarch.Internal (punsafeBuiltin)
import Plutarch.Internal.Witness (witness)
import Plutarch.Lift (
  PConstantDecl,
  PConstantRepr,
  PConstanted,
  PLifted,
  PUnsafeLiftDecl,
  pconstantFromRepr,
  pconstantToRepr,
 )
import Plutarch.List qualified as List
import Plutarch.Prelude hiding (pall, pany, pfilter, pmap, pnull, psingleton)
import Plutarch.Prelude qualified as PPrelude
import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
import Plutarch.Unsafe (punsafeCoerce, punsafeDowncast)
import PlutusCore qualified as PLC

import Data.Foldable (foldl')
import GHC.Exts (IsList (Item, fromList, toList))
import Prelude hiding (all, any, filter, lookup, null)

import Data.Proxy (Proxy (Proxy))
import Data.Traversable (for)

import Data.Bifunctor (bimap)

data KeyGuarantees = Sorted | Unsorted

type PBuiltinListOfPairs k v = PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))

newtype Flip f a b = Flip (f b a) deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
$cto :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
$cfrom :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
Generic)

type role PMap nominal nominal nominal nominal
newtype PMap (keysort :: KeyGuarantees) (k :: PType) (v :: PType) (s :: S) = PMap (Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))))
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S) x.
Rep (PMap keysort k v s) x -> PMap keysort k v s
forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S) x.
PMap keysort k v s -> Rep (PMap keysort k v s) x
$cto :: forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S) x.
Rep (PMap keysort k v s) x -> PMap keysort k v s
$cfrom :: forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S) x.
PMap keysort k v s -> Rep (PMap keysort k v s) x
Generic)
  deriving anyclass (forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S).
PMap keysort k v s -> Term s (PInner (PMap keysort k v))
forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S) (b :: PType).
Term s (PInner (PMap keysort k v))
-> (PMap keysort k v s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PMap keysort k v))
-> (PMap keysort k v s -> Term s b) -> Term s b
$cpmatch' :: forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S) (b :: PType).
Term s (PInner (PMap keysort k v))
-> (PMap keysort k v s -> Term s b) -> Term s b
pcon' :: forall (s :: S).
PMap keysort k v s -> Term s (PInner (PMap keysort k v))
$cpcon' :: forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S).
PMap keysort k v s -> Term s (PInner (PMap keysort k v))
PlutusType, forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S).
(PIsData k, PIsData v, PShow k, PShow v) =>
Bool -> Term s (PMap keysort k v) -> Term s PString
forall (t :: PType).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
pshow' :: forall (s :: S).
Bool -> Term s (PMap keysort k v) -> Term s PString
$cpshow' :: forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S).
(PIsData k, PIsData v, PShow k, PShow v) =>
Bool -> Term s (PMap keysort k v) -> Term s PString
PShow)
instance DerivePlutusType (PMap keysort k v) where type DPTStrat _ = PlutusTypeNewtype

instance PIsData (PMap keysort k v) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PMap keysort k v)) -> Term s (PMap keysort k v)
pfromDataImpl Term s (PAsData (PMap keysort k v))
x = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
pasMap forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData (PMap keysort k v))
x
  pdataImpl :: forall (s :: S). Term s (PMap keysort k v) -> Term s PData
pdataImpl Term s (PMap keysort k v)
x = forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MapData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap keysort k v)
x

instance PEq (PMap 'Sorted k v) where
  Term s (PMap 'Sorted k v)
x #== :: forall (s :: S).
Term s (PMap 'Sorted k v)
-> Term s (PMap 'Sorted k v) -> Term s PBool
#== Term s (PMap 'Sorted k v)
y = forall (s :: S).
Term s (PMap 'Sorted k v :--> (PMap 'Sorted k v :--> PBool))
peqViaData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
y
    where
      peqViaData :: Term s (PMap 'Sorted k v :--> PMap 'Sorted k v :--> PBool)
      peqViaData :: forall (s :: S).
Term s (PMap 'Sorted k v :--> (PMap 'Sorted k v :--> PBool))
peqViaData = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(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)
m0 Term s (PMap 'Sorted k v)
m1 -> forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PMap 'Sorted k v)
m0 forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PMap 'Sorted k v)
m1

instance
  ( PLiftData k
  , PLiftData v
  , Ord (PLifted k)
  ) =>
  PUnsafeLiftDecl (PMap 'Unsorted k v)
  where
  type PLifted (PMap 'Unsorted k v) = PlutusMap.Map (PLifted k) (PLifted v)

instance
  ( PConstantData k
  , PConstantData v
  , Ord k
  ) =>
  PConstantDecl (PlutusMap.Map k v)
  where
  type PConstantRepr (PlutusMap.Map k v) = [(Plutus.Data, Plutus.Data)]
  type PConstanted (PlutusMap.Map k v) = PMap 'Unsorted (PConstanted k) (PConstanted v)
  pconstantToRepr :: Map k v -> PConstantRepr (Map k v)
pconstantToRepr Map k v
m = forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall a. ToData a => a -> Data
Plutus.toData forall a. ToData a => a -> Data
Plutus.toData forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. Map k v -> [(k, v)]
PlutusMap.toList Map k v
m
  pconstantFromRepr :: PConstantRepr (Map k v) -> Maybe (Map k v)
pconstantFromRepr PConstantRepr (Map k v)
m = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k v. [(k, v)] -> Map k v
PlutusMap.fromList forall a b. (a -> b) -> a -> b
$
    forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for PConstantRepr (Map k v)
m forall a b. (a -> b) -> a -> b
$ \(Data
x, Data
y) -> do
      k
x' <- forall a. FromData a => Data -> Maybe a
Plutus.fromData Data
x
      v
y' <- forall a. FromData a => Data -> Maybe a
Plutus.fromData Data
y
      forall a. a -> Maybe a
Just (k
x', v
y')

instance
  ( PTryFrom PData (PAsData k)
  , PTryFrom PData (PAsData v)
  ) =>
  PTryFrom PData (PAsData (PMap 'Unsorted k v))
  where
  type PTryFromExcess PData (PAsData (PMap 'Unsorted k v)) = Flip Term (PMap 'Unsorted k v)
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData (PMap 'Unsorted k v)),
     Reduce (PTryFromExcess PData (PAsData (PMap 'Unsorted k v)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinList (PBuiltinPair PData PData))
opq' <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
pasMap forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
    Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
unwrapped <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
List.pmap forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S).
Term
  s
  (PBuiltinPair PData PData
   :--> PBuiltinPair (PAsData k) (PAsData v))
ptryFromPair forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair PData PData))
opq'
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (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)))
unwrapped)
    where
      ptryFromPair :: Term s (PBuiltinPair PData PData :--> PBuiltinPair (PAsData k) (PAsData v))
      ptryFromPair :: forall (s :: S).
Term
  s
  (PBuiltinPair PData PData
   :--> PBuiltinPair (PAsData k) (PAsData v))
ptryFromPair = forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PData PData)
p ->
        forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin
          # ptryFrom (pfstBuiltin # p) fst
          # ptryFrom (psndBuiltin # p) fst

instance
  ( POrd k
  , PIsData k
  , PIsData v
  , PTryFrom PData (PAsData k)
  , PTryFrom PData (PAsData v)
  ) =>
  PTryFrom PData (PAsData (PMap 'Sorted k v))
  where
  type PTryFromExcess PData (PAsData (PMap 'Sorted k v)) = Flip Term (PMap 'Sorted k v)
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData (PMap 'Sorted k v)),
     Reduce (PTryFromExcess PData (PAsData (PMap 'Sorted k v)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    (Term s (PAsData (PMap 'Unsorted k v))
opq', Term s (PMap 'Unsorted k v)
_) <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData (PMap 'Unsorted k v)) Term s PData
opq
    Term s (PMap 'Sorted k v)
unwrapped <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
papp forall (k :: PType) (v :: PType) (any :: KeyGuarantees) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term s (PMap any k v :--> PMap 'Sorted k v)
passertSorted forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PMap 'Unsorted k v))
opq'
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s (PMap 'Sorted k v)
unwrapped)

-- | Tests whether the map is empty.
pnull :: Term s (PMap any k v :--> PBool)
pnull :: forall (s :: S) (any :: KeyGuarantees) (k :: PType) (v :: PType).
Term s (PMap any k v :--> PBool)
pnull = forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s (PMap any k v)
m -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
List.pnull forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PMap any k v)
m)

-- | Look up the given key in a 'PMap'.
plookup :: (PIsData k, PIsData v) => Term s (k :--> PMap any k v :--> PMaybe v)
plookup :: forall (k :: PType) (v :: PType) (s :: S) (any :: KeyGuarantees).
(PIsData k, PIsData v) =>
Term s (k :--> (PMap any k v :--> PMaybe v))
plookup = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s k
key ->
    forall (s :: S) (k :: PType) (v :: PType) (x :: PType)
       (any :: KeyGuarantees).
Term
  s
  ((PBuiltinPair (PAsData k) (PAsData v) :--> PMaybe x)
   :--> (PAsData k :--> (PMap any k v :--> PMaybe x)))
plookupDataWith
      # phoistAcyclic (plam $ \pair -> pcon $ PJust $ pfromData $ psndBuiltin # pair)
      # pdata key

-- | Look up the given key data in a 'PMap'.
plookupData :: Term s (PAsData k :--> PMap any k v :--> PMaybe (PAsData v))
plookupData :: forall (s :: S) (k :: PType) (any :: KeyGuarantees) (v :: PType).
Term s (PAsData k :--> (PMap any k v :--> PMaybe (PAsData v)))
plookupData = forall (s :: S) (k :: PType) (v :: PType) (x :: PType)
       (any :: KeyGuarantees).
Term
  s
  ((PBuiltinPair (PAsData k) (PAsData v) :--> PMaybe x)
   :--> (PAsData k :--> (PMap any k v :--> PMaybe x)))
plookupDataWith forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (forall a (b :: PType) (s :: S) (c :: PType).
(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))
pair -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). Term s a -> PMaybe a s
PJust forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
pair)

-- | Look up the given key data in a 'PMap', applying the given function to the found key-value pair.
plookupDataWith ::
  Term
    s
    ( (PBuiltinPair (PAsData k) (PAsData v) :--> PMaybe x)
        :--> PAsData k
        :--> PMap any k v
        :--> PMaybe x
    )
plookupDataWith :: forall (s :: S) (k :: PType) (v :: PType) (x :: PType)
       (any :: KeyGuarantees).
Term
  s
  ((PBuiltinPair (PAsData k) (PAsData v) :--> PMaybe x)
   :--> (PAsData k :--> (PMap any k v :--> PMaybe x)))
plookupDataWith = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(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) :--> PMaybe x)
unwrap Term s (PAsData k)
key Term s (PMap any k v)
m ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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
      ( \Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)) :--> PMaybe x)
self Term s (PBuiltinPair (PAsData k) (PAsData v))
x Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs ->
          forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData k)
key)
            (Term s (PBuiltinPair (PAsData k) (PAsData v) :--> PMaybe x)
unwrap forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x)
            (Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)) :--> PMaybe x)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs)
      )
      (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (s :: S). PMaybe a s
PNothing)
      # pto m

-- | Look up the given key in a 'PMap', returning the default value if the key is absent.
pfindWithDefault :: (PIsData k, PIsData v) => Term s (v :--> k :--> PMap any k v :--> v)
pfindWithDefault :: forall (k :: PType) (v :: PType) (s :: S) (any :: KeyGuarantees).
(PIsData k, PIsData v) =>
Term s (v :--> (k :--> (PMap any k v :--> v)))
pfindWithDefault = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s v
def Term s k
key -> forall (s :: S) (k :: PType) (r :: PType) (v :: PType)
       (any :: KeyGuarantees).
Term
  s
  (PAsData k
   :--> (r :--> ((PAsData v :--> r) :--> (PMap any k v :--> r))))
foldAtData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s k
key forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s v
def forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData

{- | Look up the given key in a 'PMap'; return the default if the key is
 absent or apply the argument function to the value data if present.
-}
pfoldAt :: PIsData k => Term s (k :--> r :--> (PAsData v :--> r) :--> PMap any k v :--> r)
pfoldAt :: forall (k :: PType) (s :: S) (r :: PType) (v :: PType)
       (any :: KeyGuarantees).
PIsData k =>
Term
  s (k :--> (r :--> ((PAsData v :--> r) :--> (PMap any k v :--> r))))
pfoldAt = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
    \Term s k
key -> forall (s :: S) (k :: PType) (r :: PType) (v :: PType)
       (any :: KeyGuarantees).
Term
  s
  (PAsData k
   :--> (r :--> ((PAsData v :--> r) :--> (PMap any k v :--> r))))
foldAtData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s k
key

{- | Look up the given key data in a 'PMap'; return the default if the key is
 absent or apply the argument function to the value data if present.
-}
foldAtData :: Term s (PAsData k :--> r :--> (PAsData v :--> r) :--> PMap any k v :--> r)
foldAtData :: forall (s :: S) (k :: PType) (r :: PType) (v :: PType)
       (any :: KeyGuarantees).
Term
  s
  (PAsData k
   :--> (r :--> ((PAsData v :--> r) :--> (PMap any k v :--> r))))
foldAtData = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData k)
key Term s r
def Term s (PAsData v :--> r)
apply Term s (PMap any k v)
m ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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
      ( \Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)) :--> r)
self Term s (PBuiltinPair (PAsData k) (PAsData v))
x Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs ->
          forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData k)
key)
            (Term s (PAsData v :--> r)
apply forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x)
            (Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)) :--> r)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs)
      )
      (forall a b. a -> b -> a
const Term s r
def)
      # pto m

-- | Insert a new key/value pair into the map, overiding the previous if any.
pinsert :: (POrd k, PIsData k, PIsData v) => Term s (k :--> v :--> PMap 'Sorted k v :--> PMap 'Sorted k v)
pinsert :: forall (k :: PType) (v :: PType) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term s (k :--> (v :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
pinsert = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s k
key Term s v
val ->
    forall (k :: PType) (s :: S) (v :: PType) (g :: KeyGuarantees).
(POrd k, PIsData k) =>
Term
  s
  ((PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
    :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
   :--> (k :--> (PMap g k v :--> PMap g k v)))
rebuildAtKey forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s k
key forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s v
val) #) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s k
key

-- | Insert a new data-encoded key/value pair into the map, overiding the previous if any.
pinsertData ::
  (POrd k, PIsData k) =>
  Term s (PAsData k :--> PAsData v :--> PMap 'Sorted k v :--> PMap 'Sorted k v)
pinsertData :: forall (k :: PType) (s :: S) (v :: PType).
(POrd k, PIsData k) =>
Term
  s
  (PAsData k
   :--> (PAsData v :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
pinsertData = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData k)
key Term s (PAsData v)
val ->
    forall (k :: PType) (s :: S) (v :: PType) (g :: KeyGuarantees).
(POrd k, PIsData k) =>
Term
  s
  ((PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
    :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
   :--> (k :--> (PMap g k v :--> PMap g k v)))
rebuildAtKey forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData k)
key forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData v)
val) #) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData k)
key

-- | Delete a key from the map.
pdelete :: (POrd k, PIsData k) => Term s (k :--> PMap 'Sorted k v :--> PMap 'Sorted k v)
pdelete :: forall (k :: PType) (s :: S) (v :: PType).
(POrd k, PIsData k) =>
Term s (k :--> (PMap 'Sorted k v :--> PMap 'Sorted k v))
pdelete = forall (k :: PType) (s :: S) (v :: PType) (g :: KeyGuarantees).
(POrd k, PIsData k) =>
Term
  s
  ((PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
    :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
   :--> (k :--> (PMap g k v :--> PMap g k v)))
rebuildAtKey forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a. a -> a
id

-- | Rebuild the map at the given key.
rebuildAtKey ::
  (POrd k, PIsData k) =>
  Term
    s
    ( ( PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
          :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
      )
        :--> k
        :--> PMap g k v
        :--> PMap g k v
    )
rebuildAtKey :: forall (k :: PType) (s :: S) (v :: PType) (g :: KeyGuarantees).
(POrd k, PIsData k) =>
Term
  s
  ((PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
    :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
   :--> (k :--> (PMap g k v :--> PMap g k v)))
rebuildAtKey = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(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 v))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
handler Term s k
key Term s (PMap g k v)
m ->
    forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast forall a b. (a -> b) -> a -> b
$
      forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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
        ( \Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> ((PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
          :--> PInner (PMap g k v))
         :--> PInner (PMap g k v)))
self Term s (PBuiltinPair (PAsData k) (PAsData v))
x Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs ->
            forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x) forall a b. (a -> b) -> a -> b
$ \Term s k
k ->
              forall a (b :: PType) (s :: S) (c :: PType).
(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 v))
   :--> PInner (PMap g k v))
prefix ->
                forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                  (Term s k
k forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s k
key)
                  (Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> ((PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
          :--> PInner (PMap g k v))
         :--> PInner (PMap g k v)))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(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 v)))
suffix -> Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> PInner (PMap g k v))
prefix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
suffix)
                  ( forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                      (Term s k
k forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s k
key)
                      (Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> PInner (PMap g k v))
prefix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
handler forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs)
                      (Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> PInner (PMap g k v))
prefix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
handler forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs)
                  )
        )
        (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
handler forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil))
        # pto m
        # plam id

-- | Construct an empty 'PMap'.
pempty :: Term s (PMap 'Sorted k v)
pempty :: forall (s :: S) (k :: PType) (v :: PType).
Term s (PMap 'Sorted k v)
pempty = forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

-- | Construct a singleton 'PMap' with the given key and value.
psingleton :: (PIsData k, PIsData v) => Term s (k :--> v :--> PMap 'Sorted k v)
psingleton :: forall (k :: PType) (v :: PType) (s :: S).
(PIsData k, PIsData v) =>
Term s (k :--> (v :--> PMap 'Sorted k v))
psingleton = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s k
key Term s v
value -> forall (s :: S) (k :: PType) (v :: PType).
Term s (PAsData k :--> (PAsData v :--> PMap 'Sorted k v))
psingletonData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s k
key forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s v
value

-- | Construct a singleton 'PMap' with the given data-encoded key and value.
psingletonData :: Term s (PAsData k :--> PAsData v :--> PMap 'Sorted k v)
psingletonData :: forall (s :: S) (k :: PType) (v :: PType).
Term s (PAsData k :--> (PAsData v :--> PMap 'Sorted k v))
psingletonData = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
    \Term s (PAsData k)
key Term s (PAsData v)
value -> forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData k)
key forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData v)
value) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)

-- | Construct a 'PMap' from a list of key-value pairs, sorted by ascending key data.
pfromAscList :: (POrd k, PIsData k, PIsData v) => Term s (PBuiltinListOfPairs k v :--> PMap 'Sorted k v)
pfromAscList :: forall (k :: PType) (v :: PType) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term s (PBuiltinListOfPairs k v :--> PMap 'Sorted k v)
pfromAscList = forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ (forall (k :: PType) (v :: PType) (any :: KeyGuarantees) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term s (PMap any k v :--> PMap 'Sorted k v)
passertSorted #) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S).
Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> PMap keysort k v s
PMap

-- | Assert the map is properly sorted.
passertSorted :: forall k v any s. (POrd k, PIsData k, PIsData v) => Term s (PMap any k v :--> PMap 'Sorted k v)
passertSorted :: forall (k :: PType) (v :: PType) (any :: KeyGuarantees) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term s (PMap any k v :--> PMap 'Sorted k v)
passertSorted =
  let ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy (PIsData v))
   in forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
        forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PMap any k v)
m ->
          forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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
            ( \Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> ((k :--> PBool) :--> PMap 'Sorted k v))
self Term s (PBuiltinPair (PAsData k) (PAsData v))
x Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs ->
                forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x) forall a b. (a -> b) -> a -> b
$ \Term s k
k ->
                  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (k :--> PBool)
badKey ->
                    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                      (Term s (k :--> PBool)
badKey forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s k
k)
                      (forall (s :: S) (a :: PType). Term s PString -> Term s a
ptraceError Term s PString
"unsorted map")
                      (Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> ((k :--> PBool) :--> PMap 'Sorted k v))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s k
k))
            )
            -- this is actually the empty map so we can
            -- safely assum that it is sorted
            (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PMap any k v)
m)
            # pto m
            # plam (const $ pcon PFalse)

-- | Forget the knowledge that keys were sorted.
pforgetSorted :: Term s (PMap 'Sorted k v) -> Term s (PMap g k v)
pforgetSorted :: forall (s :: S) (k :: PType) (v :: PType) (g :: KeyGuarantees).
Term s (PMap 'Sorted k v) -> Term s (PMap g k v)
pforgetSorted Term s (PMap 'Sorted k v)
v = forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PMap 'Sorted k v)
v)

{- | 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.
-}
punsortedMapFromFoldable ::
  forall (k :: PType) (v :: PType) (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 :: PType) (v :: PType) (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 :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (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 :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (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 :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
Term s a -> Term s (PBuiltinList a) -> PBuiltinList a s
PCons (forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s' k
key forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (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.
-}
psortedMapFromFoldable ::
  forall (k :: PType) (v :: PType) (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 :: PType) (v :: PType) (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 :: PType) (v :: PType).
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 :: PType) (v :: PType) (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 :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' k
key forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' v
val forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PMap 'Sorted k v)
acc

instance (PIsData k, PIsData v, POrd k) => IsList (Term s (PMap 'Unsorted k v)) where
  type Item (Term s (PMap 'Unsorted k v)) = (Term s k, Term s v)
  fromList :: [Item (Term s (PMap 'Unsorted k v))] -> Term s (PMap 'Unsorted k v)
fromList = forall (k :: PType) (v :: PType) (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
  toList :: Term s (PMap 'Unsorted k v) -> [Item (Term s (PMap 'Unsorted k v))]
toList = forall a. HasCallStack => [Char] -> a
error [Char]
"unimplemented"

instance (PIsData k, PIsData v, POrd k) => IsList (Term s (PMap 'Sorted k v)) where
  type Item (Term s (PMap 'Sorted k v)) = (Term s k, Term s v)
  fromList :: [Item (Term s (PMap 'Sorted k v))] -> Term s (PMap 'Sorted k v)
fromList = forall (k :: PType) (v :: PType) (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
  toList :: Term s (PMap 'Sorted k v) -> [Item (Term s (PMap 'Sorted k v))]
toList = forall a. HasCallStack => [Char] -> a
error [Char]
"unimplemented"

instance
  (POrd k, PIsData k, PIsData v, Semigroup (Term s v)) =>
  Semigroup (Term s (PMap 'Sorted k v))
  where
  Term s (PMap 'Sorted k v)
a <> :: Term s (PMap 'Sorted k v)
-> Term s (PMap 'Sorted k v) -> Term s (PMap 'Sorted k v)
<> Term s (PMap 'Sorted k v)
b = forall (k :: PType) (v :: PType) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term
  s
  ((v :--> (v :--> v))
   :--> (PMap 'Sorted k v
         :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
punionWith forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a. Semigroup a => a -> a -> a
(<>) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
b

instance
  (POrd k, PIsData k, PIsData v, Semigroup (Term s v)) =>
  Monoid (Term s (PMap 'Sorted k v))
  where
  mempty :: Term s (PMap 'Sorted k v)
mempty = forall (s :: S) (k :: PType) (v :: PType).
Term s (PMap 'Sorted k v)
pempty

instance
  (POrd k, PIsData k, PIsData v, PlutusTx.Semigroup (Term s v)) =>
  PlutusTx.Semigroup (Term s (PMap 'Sorted k v))
  where
  Term s (PMap 'Sorted k v)
a <> :: Term s (PMap 'Sorted k v)
-> Term s (PMap 'Sorted k v) -> Term s (PMap 'Sorted k v)
<> Term s (PMap 'Sorted k v)
b = forall (k :: PType) (v :: PType) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term
  s
  ((v :--> (v :--> v))
   :--> (PMap 'Sorted k v
         :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
punionWith forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a. Semigroup a => a -> a -> a
(PlutusTx.<>) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
b

instance
  (POrd k, PIsData k, PIsData v, PlutusTx.Semigroup (Term s v)) =>
  PlutusTx.Monoid (Term s (PMap 'Sorted k v))
  where
  mempty :: Term s (PMap 'Sorted k v)
mempty = forall (s :: S) (k :: PType) (v :: PType).
Term s (PMap 'Sorted k v)
pempty

instance
  (POrd k, PIsData k, PIsData v, PlutusTx.Group (Term s v)) =>
  PlutusTx.Group (Term s (PMap 'Sorted k v))
  where
  inv :: Term s (PMap 'Sorted k v) -> Term s (PMap 'Sorted k v)
inv Term s (PMap 'Sorted k v)
a = forall (a :: PType) (b :: PType) (s :: S) (g :: KeyGuarantees)
       (k :: PType).
(PIsData a, PIsData b) =>
Term s ((a :--> b) :--> (PMap g k a :--> PMap g k b))
pmap forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a. Group a => a -> a
PlutusTx.inv forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Sorted k v)
a

{- | Combine two 'PMap's applying the given function to any two values that
 share the same key.
-}
punionWith ::
  (POrd k, PIsData k, PIsData v) =>
  Term s ((v :--> v :--> v) :--> PMap 'Sorted k v :--> PMap 'Sorted k v :--> PMap 'Sorted k v)
punionWith :: forall (k :: PType) (v :: PType) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term
  s
  ((v :--> (v :--> v))
   :--> (PMap 'Sorted k v
         :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
punionWith = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(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 :--> v))
combine -> forall (k :: PType) (s :: S) (v :: PType).
(POrd k, PIsData k) =>
Term
  s
  ((PAsData v :--> (PAsData v :--> PAsData v))
   :--> (PMap 'Sorted k v
         :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
punionWithData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
      \Term s (PAsData v)
x Term s (PAsData v)
y -> forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (v :--> (v :--> v))
combine forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData v)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData v)
y)

data MapUnionCarrier k v s = MapUnionCarrier
  { forall (k :: PType) (v :: PType) (s :: S).
MapUnionCarrier k v s
-> Term
     s
     (PBuiltinListOfPairs k v
      :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v))
merge :: Term s (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)
  , forall (k :: PType) (v :: PType) (s :: S).
MapUnionCarrier k v s
-> Term
     s
     (PBuiltinPair (PAsData k) (PAsData v)
      :--> (PBuiltinListOfPairs k v
            :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)))
mergeInsert :: Term s (PBuiltinPair (PAsData k) (PAsData v) :--> PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)
  }
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (k :: PType) (v :: PType) (s :: S) x.
Rep (MapUnionCarrier k v s) x -> MapUnionCarrier k v s
forall (k :: PType) (v :: PType) (s :: S) x.
MapUnionCarrier k v s -> Rep (MapUnionCarrier k v s) x
$cto :: forall (k :: PType) (v :: PType) (s :: S) x.
Rep (MapUnionCarrier k v s) x -> MapUnionCarrier k v s
$cfrom :: forall (k :: PType) (v :: PType) (s :: S) x.
MapUnionCarrier k v s -> Rep (MapUnionCarrier k v s) x
Generic)
  deriving anyclass (forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (k :: PType) (v :: PType) (s :: S).
MapUnionCarrier k v s -> Term s (PInner (MapUnionCarrier k v))
forall (k :: PType) (v :: PType) (s :: S) (b :: PType).
Term s (PInner (MapUnionCarrier k v))
-> (MapUnionCarrier k v s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (MapUnionCarrier k v))
-> (MapUnionCarrier k v s -> Term s b) -> Term s b
$cpmatch' :: forall (k :: PType) (v :: PType) (s :: S) (b :: PType).
Term s (PInner (MapUnionCarrier k v))
-> (MapUnionCarrier k v s -> Term s b) -> Term s b
pcon' :: forall (s :: S).
MapUnionCarrier k v s -> Term s (PInner (MapUnionCarrier k v))
$cpcon' :: forall (k :: PType) (v :: PType) (s :: S).
MapUnionCarrier k v s -> Term s (PInner (MapUnionCarrier k v))
PlutusType)
instance DerivePlutusType (MapUnionCarrier k v) where type DPTStrat _ = PlutusTypeScott

mapUnionCarrier :: (POrd k, PIsData k) => Term s ((PAsData v :--> PAsData v :--> PAsData v) :--> MapUnionCarrier k v :--> MapUnionCarrier k v)
mapUnionCarrier :: forall (k :: PType) (s :: S) (v :: PType).
(POrd k, PIsData k) =>
Term
  s
  ((PAsData v :--> (PAsData v :--> PAsData v))
   :--> (MapUnionCarrier k v :--> MapUnionCarrier k v))
mapUnionCarrier = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam \Term s (PAsData v :--> (PAsData v :--> PAsData v))
combine Term s (MapUnionCarrier k v)
self ->
  let mergeInsert :: Term
  s
  (PBuiltinPair (PAsData k) (PAsData v)
   :--> (PBuiltinListOfPairs k v
         :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)))
mergeInsert = forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (MapUnionCarrier k v)
self \(MapUnionCarrier {Term
  s
  (PBuiltinPair (PAsData k) (PAsData v)
   :--> (PBuiltinListOfPairs k v
         :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)))
mergeInsert :: Term
  s
  (PBuiltinPair (PAsData k) (PAsData v)
   :--> (PBuiltinListOfPairs k v
         :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)))
$sel:mergeInsert:MapUnionCarrier :: forall (k :: PType) (v :: PType) (s :: S).
MapUnionCarrier k v s
-> Term
     s
     (PBuiltinPair (PAsData k) (PAsData v)
      :--> (PBuiltinListOfPairs k v
            :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)))
mergeInsert}) -> Term
  s
  (PBuiltinPair (PAsData k) (PAsData v)
   :--> (PBuiltinListOfPairs k v
         :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)))
mergeInsert
      merge :: Term
  s
  (PBuiltinListOfPairs k v
   :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v))
merge = forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (MapUnionCarrier k v)
self \(MapUnionCarrier {Term
  s
  (PBuiltinListOfPairs k v
   :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v))
merge :: Term
  s
  (PBuiltinListOfPairs k v
   :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v))
$sel:merge:MapUnionCarrier :: forall (k :: PType) (v :: PType) (s :: S).
MapUnionCarrier k v s
-> Term
     s
     (PBuiltinListOfPairs k v
      :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v))
merge}) -> Term
  s
  (PBuiltinListOfPairs k v
   :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v))
merge
   in forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$
        MapUnionCarrier
          { $sel:merge:MapUnionCarrier :: Term
  s
  (PBuiltinListOfPairs k v
   :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v))
merge = forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinListOfPairs k v)
xs Term s (PBuiltinListOfPairs k v)
ys -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinListOfPairs k v)
xs forall a b. (a -> b) -> a -> b
$ \case
              PBuiltinListOfPairs k v s
PNil -> Term s (PBuiltinListOfPairs k v)
ys
              PCons Term s (PBuiltinPair (PAsData k) (PAsData v))
x Term s (PBuiltinListOfPairs k v)
xs' -> Term
  s
  (PBuiltinPair (PAsData k) (PAsData v)
   :--> (PBuiltinListOfPairs k v
         :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)))
mergeInsert forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinListOfPairs k v)
xs' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinListOfPairs k v)
ys
          , $sel:mergeInsert:MapUnionCarrier :: Term
  s
  (PBuiltinPair (PAsData k) (PAsData v)
   :--> (PBuiltinListOfPairs k v
         :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v)))
mergeInsert = forall a (b :: PType) (s :: S) (c :: PType).
(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))
x Term s (PBuiltinListOfPairs k v)
xs Term s (PBuiltinListOfPairs k v)
ys ->
              forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinListOfPairs k v)
ys forall a b. (a -> b) -> a -> b
$ \case
                PBuiltinListOfPairs k v s
PNil -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinListOfPairs k v)
xs
                PCons Term s (PBuiltinPair (PAsData k) (PAsData v))
y1 Term s (PBuiltinListOfPairs k v)
ys' ->
                  forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PBuiltinPair (PAsData k) (PAsData v))
y1 forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair (PAsData k) (PAsData v))
y ->
                    forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x) forall a b. (a -> b) -> a -> b
$ \Term s (PAsData k)
xk ->
                      forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
y) forall a b. (a -> b) -> a -> b
$ \Term s (PAsData k)
yk ->
                        forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                          (Term s (PAsData k)
xk forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData k)
yk)
                          ( forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons
                              # (ppairDataBuiltin # xk #$ combine # (psndBuiltin # x) # (psndBuiltin # y))
                                #$ merge
                              # xs
                              # ys'
                          )
                          ( forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                              (forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData k)
xk forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData k)
yk)
                              ( forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons
                                  # x
                                  # (mergeInsert # y # ys' # xs)
                              )
                              ( forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons
                                  # y
                                  # (mergeInsert # x # xs # ys')
                              )
                          )
          }

mapUnion :: forall k v s. (POrd k, PIsData k) => Term s ((PAsData v :--> PAsData v :--> PAsData v) :--> MapUnionCarrier k v)
mapUnion :: forall (k :: PType) (v :: PType) (s :: S).
(POrd k, PIsData k) =>
Term
  s
  ((PAsData v :--> (PAsData v :--> PAsData v))
   :--> MapUnionCarrier k v)
mapUnion = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam \Term s (PAsData v :--> (PAsData v :--> PAsData v))
combine -> forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (k :: PType) (s :: S) (v :: PType).
(POrd k, PIsData k) =>
Term
  s
  ((PAsData v :--> (PAsData v :--> PAsData v))
   :--> (MapUnionCarrier k v :--> MapUnionCarrier k v))
mapUnionCarrier forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData v :--> (PAsData v :--> PAsData v))
combine :: Term _ (MapUnionCarrier k v :--> MapUnionCarrier k v))

{- | Combine two 'PMap's applying the given function to any two data-encoded
 values that share the same key.
-}
punionWithData ::
  (POrd k, PIsData k) =>
  Term
    s
    ( (PAsData v :--> PAsData v :--> PAsData v)
        :--> PMap 'Sorted k v
        :--> PMap 'Sorted k v
        :--> PMap 'Sorted k v
    )
punionWithData :: forall (k :: PType) (s :: S) (v :: PType).
(POrd k, PIsData k) =>
Term
  s
  ((PAsData v :--> (PAsData v :--> PAsData v))
   :--> (PMap 'Sorted k v
         :--> (PMap 'Sorted k v :--> PMap 'Sorted k v)))
punionWithData = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData v :--> (PAsData v :--> PAsData v))
combine Term s (PMap 'Sorted k v)
x Term s (PMap 'Sorted k v)
y ->
    forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (s :: S).
Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> PMap keysort k v s
PMap forall a b. (a -> b) -> a -> b
$ (forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (k :: PType) (v :: PType) (s :: S).
(POrd k, PIsData k) =>
Term
  s
  ((PAsData v :--> (PAsData v :--> PAsData v))
   :--> MapUnionCarrier k v)
mapUnion forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData v :--> (PAsData v :--> PAsData v))
combine) \(MapUnionCarrier {Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
         :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))))
merge :: Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
         :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))))
$sel:merge:MapUnionCarrier :: forall (k :: PType) (v :: PType) (s :: S).
MapUnionCarrier k v s
-> Term
     s
     (PBuiltinListOfPairs k v
      :--> (PBuiltinListOfPairs k v :--> PBuiltinListOfPairs k v))
merge}) -> Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
         :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))))
merge) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PMap 'Sorted k v)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PMap 'Sorted k v)
y

-- | Difference of two maps. Return elements of the first map not existing in the second map.
pdifference :: PIsData k => Term s (PMap g k a :--> PMap any k b :--> PMap g k a)
pdifference :: forall (k :: PType) (s :: S) (g :: KeyGuarantees) (a :: PType)
       (any :: KeyGuarantees) (b :: PType).
PIsData k =>
Term s (PMap g k a :--> (PMap any k b :--> PMap g k a))
pdifference = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PMap g k a)
left Term s (PMap any k b)
right ->
    forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (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 :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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
        ( \Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
self Term s (PBuiltinPair (PAsData k) (PAsData a))
x Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
xs ->
            forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
xs) forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
xs' ->
              forall (k :: PType) (s :: S) (r :: PType) (v :: PType)
       (any :: KeyGuarantees).
PIsData k =>
Term
  s (k :--> (r :--> ((PAsData v :--> r) :--> (PMap any k v :--> r))))
pfoldAt
                # pfromData (pfstBuiltin # x)
                # (pcons # x # xs')
                # plam (const xs')
                # right
        )
        (forall a b. a -> b -> a
const forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)
        # pto left

-- | Tests if all values in the map satisfy the given predicate.
pall :: PIsData v => Term s ((v :--> PBool) :--> PMap any k v :--> PBool)
pall :: forall (v :: PType) (s :: S) (any :: KeyGuarantees) (k :: PType).
PIsData v =>
Term s ((v :--> PBool) :--> (PMap any k v :--> PBool))
pall = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (v :--> PBool)
pred Term s (PMap any k v)
m ->
    forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
List.pall forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s (PBuiltinPair (PAsData k) (PAsData v))
pair -> Term s (v :--> PBool)
pred forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
pair) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PMap any k v)
m

-- | Tests if anu value in the map satisfies the given predicate.
pany :: PIsData v => Term s ((v :--> PBool) :--> PMap any k v :--> PBool)
pany :: forall (v :: PType) (s :: S) (any :: KeyGuarantees) (k :: PType).
PIsData v =>
Term s ((v :--> PBool) :--> (PMap any k v :--> PBool))
pany = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (v :--> PBool)
pred Term s (PMap any k v)
m ->
    forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
List.pany forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s (PBuiltinPair (PAsData k) (PAsData v))
pair -> Term s (v :--> PBool)
pred forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
pair) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PMap any k v)
m

-- | Filters the map so it contains only the values that satisfy the given predicate.
pfilter :: PIsData v => Term s ((v :--> PBool) :--> PMap g k v :--> PMap g k v)
pfilter :: forall (v :: PType) (s :: S) (g :: KeyGuarantees) (k :: PType).
PIsData v =>
Term s ((v :--> PBool) :--> (PMap g k v :--> PMap g k v))
pfilter = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (v :--> PBool)
pred ->
    forall (a :: PType) (b :: PType) (s :: S) (g :: KeyGuarantees)
       (k :: PType).
(PIsData a, PIsData b) =>
Term s ((a :--> PMaybe b) :--> (PMap g k a :--> PMap g k b))
pmapMaybe forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(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 -> forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s (v :--> PBool)
pred forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s v
v) (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). Term s a -> PMaybe a s
PJust Term s v
v) (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (s :: S). PMaybe a s
PNothing)

-- | Maps and filters the map, much like 'Data.List.mapMaybe'.
pmapMaybe ::
  (PIsData a, PIsData b) =>
  Term s ((a :--> PMaybe b) :--> PMap g k a :--> PMap g k b)
pmapMaybe :: forall (a :: PType) (b :: PType) (s :: S) (g :: KeyGuarantees)
       (k :: PType).
(PIsData a, PIsData b) =>
Term s ((a :--> PMaybe b) :--> (PMap g k a :--> PMap g k b))
pmapMaybe = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PMaybe b)
f -> forall (s :: S) (a :: PType) (b :: PType) (g :: KeyGuarantees)
       (k :: PType).
Term
  s
  ((PAsData a :--> PMaybe (PAsData b))
   :--> (PMap g k a :--> PMap g k b))
pmapMaybeData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
v -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (a :--> PMaybe b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
v) forall a b. (a -> b) -> a -> b
$ \case
    PMaybe b s
PNothing -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (s :: S). PMaybe a s
PNothing
    PJust Term s b
v' -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). Term s a -> PMaybe a s
PJust (forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s b
v')

pmapMaybeData ::
  Term s ((PAsData a :--> PMaybe (PAsData b)) :--> PMap g k a :--> PMap g k b)
pmapMaybeData :: forall (s :: S) (a :: PType) (b :: PType) (g :: KeyGuarantees)
       (k :: PType).
Term
  s
  ((PAsData a :--> PMaybe (PAsData b))
   :--> (PMap g k a :--> PMap g k b))
pmapMaybeData = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a :--> PMaybe (PAsData b))
f Term s (PMap g k a)
m ->
    forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (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 :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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
        ( \Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
self Term s (PBuiltinPair (PAsData k) (PAsData a))
x Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
xs ->
            forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
xs) forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
xs' ->
              forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PAsData a :--> PMaybe (PAsData b))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData a))
x) forall a b. (a -> b) -> a -> b
$ \case
                PMaybe (PAsData b) s
PNothing -> Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
xs'
                PJust Term s (PAsData b)
v -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData a))
x) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData b)
v) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
xs'
        )
        (forall a b. a -> b -> a
const forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)
        # pto m

-- | Applies a function to every value in the map, much like 'Data.List.map'.
pmap ::
  (PIsData a, PIsData b) =>
  Term s ((a :--> b) :--> PMap g k a :--> PMap g k b)
pmap :: forall (a :: PType) (b :: PType) (s :: S) (g :: KeyGuarantees)
       (k :: PType).
(PIsData a, PIsData b) =>
Term s ((a :--> b) :--> (PMap g k a :--> PMap g k b))
pmap = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
    \Term s (a :--> b)
f -> forall (s :: S) (a :: PType) (b :: PType) (g :: KeyGuarantees)
       (k :: PType).
Term
  s ((PAsData a :--> PAsData b) :--> (PMap g k a :--> PMap g k b))
pmapData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
v -> forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (a :--> b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
v)

pmapData ::
  Term s ((PAsData a :--> PAsData b) :--> PMap g k a :--> PMap g k b)
pmapData :: forall (s :: S) (a :: PType) (b :: PType) (g :: KeyGuarantees)
       (k :: PType).
Term
  s ((PAsData a :--> PAsData b) :--> (PMap g k a :--> PMap g k b))
pmapData = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a :--> PAsData b)
f Term s (PMap g k a)
m ->
    forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (keysort :: KeyGuarantees) (k :: PType) (v :: PType)
       (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 :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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
        ( \Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a))
   :--> PBuiltinList (PBuiltinPair (PAsData k) (PAsData b)))
self Term s (PBuiltinPair (PAsData k) (PAsData a))
x Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData a)))
xs ->
            forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons
              # (ppairDataBuiltin # (pfstBuiltin # x) # (f #$ psndBuiltin # x))
              # (self # xs)
        )
        (forall a b. a -> b -> a
const forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)
        # pto m

{- | Given a comparison function and a "zero" value, check whether a binary relation holds over
2 sorted 'PMap's.

This is primarily intended to be used with 'PValue'.
-}
pcheckBinRel ::
  forall k v s.
  (POrd k, PIsData k, PIsData v) =>
  Term
    s
    ( (v :--> v :--> PBool)
        :--> v
        :--> PMap 'Sorted k v
        :--> PMap 'Sorted k v
        :--> PBool
    )
pcheckBinRel :: forall (k :: PType) (v :: PType) (s :: S).
(POrd k, PIsData k, PIsData v) =>
Term
  s
  ((v :--> (v :--> PBool))
   :--> (v
         :--> (PMap 'Sorted k v :--> (PMap 'Sorted k v :--> PBool))))
pcheckBinRel = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(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 :--> PBool))
f Term s v
z Term s (PMap 'Sorted k v)
m1 Term s (PMap 'Sorted k v)
m2 ->
    let inner :: Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
         :--> PBool))
inner = forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(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 v))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
         :--> PBool))
self Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
l1 Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
l2 ->
          forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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
            ( \Term s (PBuiltinPair (PAsData k) (PAsData v))
x Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs ->
                forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x) forall a b. (a -> b) -> a -> b
$ \Term s v
v1 ->
                  forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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
                    ( \Term s (PBuiltinPair (PAsData k) (PAsData v))
y Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
ys -> forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
                        Term s v
v2 <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
y
                        Term s k
k1 <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
x
                        Term s k
k2 <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
y
                        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
                          forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                            (Term s k
k1 forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s k
k2)
                            ( Term s (v :--> (v :--> PBool))
f
                                # v1
                                # v2 #&& self
                                # xs
                                # ys
                            )
                          forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                            (Term s k
k1 forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s k
k2)
                            (Term s (v :--> (v :--> PBool))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s v
v1 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s v
z forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
         :--> PBool))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
l2)
                          forall a b. (a -> b) -> a -> b
$ Term s (v :--> (v :--> PBool))
f
                            # z
                            # v2 #&& self
                            # l1
                            # ys
                    )
                    ( Term s (v :--> (v :--> PBool))
f
                        # v1
                        # z
                          #&& PPrelude.pall
                        # plam (\p -> f # pfromData (psndBuiltin # p) # z)
                        # xs
                    )
                    Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
l2
            )
            (forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
PPrelude.pall forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s (PBuiltinPair (PAsData k) (PAsData v))
p -> Term s (v :--> (v :--> PBool))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s v
z forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData k) (PAsData v))
p) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
l2)
            Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
l1
     in Term
  s
  (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
   :--> (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v))
         :--> PBool))
inner forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PMap 'Sorted k v)
m1 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PMap 'Sorted k v)
m2