{-# LANGUAGE QuantifiedConstraints #-}

module Plutarch.Extra.These (
  -- * Types
  PThese (..),
  PDThese (..),

  -- * Functions
  pthese,
  pdthese,
  toPDThese,
  fromPDThese,
) where

import Plutarch.Extra.Applicative (PApplicative (ppure), PApply (pliftA2))
import Plutarch.Extra.Bool (pcompare)
import Plutarch.Extra.Boring (pboring)
import Plutarch.Extra.Functor (
  PBifunctor (PSubcategoryLeft, PSubcategoryRight, pbimap, psecond),
  PFunctor (PSubcategory, pfmap),
  Plut,
 )
import Plutarch.Extra.TermCont (pletC, pmatchC)
import Plutarch.Extra.Traversable (PTraversable (ptraverse, ptraverse_))

{- | A data type which contains an @a@, a @b@, or both. This uses a
 Scott-encoded representation.

 @since 1.0.0
-}
data PThese (a :: S -> Type) (b :: S -> Type) (s :: S)
  = PThis (Term s a)
  | PThat (Term s b)
  | PThese (Term s a) (Term s b)
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (b :: PType) (s :: S) x.
Rep (PThese a b s) x -> PThese a b s
forall (a :: PType) (b :: PType) (s :: S) x.
PThese a b s -> Rep (PThese a b s) x
$cto :: forall (a :: PType) (b :: PType) (s :: S) x.
Rep (PThese a b s) x -> PThese a b s
$cfrom :: forall (a :: PType) (b :: PType) (s :: S) x.
PThese a b s -> Rep (PThese a b 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 (a :: PType) (b :: PType) (s :: S).
PThese a b s -> Term s (PInner (PThese a b))
forall (a :: PType) (b :: PType) (s :: S) (b :: PType).
Term s (PInner (PThese a b))
-> (PThese a b s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PThese a b))
-> (PThese a b s -> Term s b) -> Term s b
$cpmatch' :: forall (a :: PType) (b :: PType) (s :: S) (b :: PType).
Term s (PInner (PThese a b))
-> (PThese a b s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PThese a b s -> Term s (PInner (PThese a b))
$cpcon' :: forall (a :: PType) (b :: PType) (s :: S).
PThese a b s -> Term s (PInner (PThese a b))
PlutusType, forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
forall (a :: PType) (b :: PType) (s :: S).
(PEq a, PEq b) =>
Term s (PThese a b) -> Term s (PThese a b) -> Term s PBool
#== :: forall (s :: S).
Term s (PThese a b) -> Term s (PThese a b) -> Term s PBool
$c#== :: forall (a :: PType) (b :: PType) (s :: S).
(PEq a, PEq b) =>
Term s (PThese a b) -> Term s (PThese a b) -> Term s PBool
PEq)

instance DerivePlutusType (PThese a b) where type DPTStrat _ = PlutusTypeScott

-- | @since 1.0.0
instance (POrd a, POrd b) => PPartialOrd (PThese a b) where
  Term s (PThese a b)
t1 #<= :: forall (s :: S).
Term s (PThese a b) -> Term s (PThese a b) -> Term s PBool
#<= Term s (PThese a b)
t2 = forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PThese a b s
t1' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t1
    PThese a b s
t2' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t2
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case (PThese a b s
t1', PThese a b s
t2') of
      (PThis Term s a
ta, PThis Term s a
ta') -> Term s a
ta forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
ta'
      (PThis Term s a
_, PThese a b s
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue
      (PThat Term s b
_, PThis Term s a
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
      (PThat Term s b
tb, PThat Term s b
tb') -> Term s b
tb forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s b
tb'
      (PThat Term s b
_, PThese a b s
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue
      (PThese Term s a
_ Term s b
_, PThis Term s a
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
      (PThese Term s a
_ Term s b
_, PThat Term s b
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
      (PThese Term s a
ta Term s b
tb, PThese Term s a
ta' Term s b
tb') ->
        forall (a :: PType) (b :: PType) (s :: S).
POrd a =>
Term s a
-> Term s a -> Term s b -> Term s b -> Term s b -> Term s b
pcompare Term s a
ta Term s a
ta' (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue) (Term s b
tb forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s b
tb') (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse)
  Term s (PThese a b)
t1 #< :: forall (s :: S).
Term s (PThese a b) -> Term s (PThese a b) -> Term s PBool
#< Term s (PThese a b)
t2 = forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PThese a b s
t1' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t1
    PThese a b s
t2' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t2
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case (PThese a b s
t1', PThese a b s
t2') of
      (PThis Term s a
ta, PThis Term s a
ta') -> Term s a
ta forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s a
ta'
      (PThis Term s a
_, PThese a b s
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue
      (PThat Term s b
_, PThis Term s a
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
      (PThat Term s b
tb, PThat Term s b
tb') -> Term s b
tb forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s b
tb'
      (PThat Term s b
_, PThese a b s
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue
      (PThese Term s a
_ Term s b
_, PThis Term s a
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
      (PThese Term s a
_ Term s b
_, PThat Term s b
_) -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse
      (PThese Term s a
ta Term s b
tb, PThese Term s a
ta' Term s b
tb') ->
        forall (a :: PType) (b :: PType) (s :: S).
POrd a =>
Term s a
-> Term s a -> Term s b -> Term s b -> Term s b -> Term s b
pcompare Term s a
ta Term s a
ta' (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue) (Term s b
tb forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s b
tb') (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse)

-- | @since 1.0.0
deriving anyclass instance (PShow a, PShow b) => PShow (PThese a b)

-- | @since 3.1.0
instance PFunctor (PThese a) where
  type PSubcategory (PThese a) = Plut
  pfmap :: forall (a :: PType) (b :: PType) (s :: S).
(PSubcategory (PThese a) a, PSubcategory (PThese a) b) =>
Term s ((a :--> b) :--> (PThese a a :--> PThese a b))
pfmap = forall (f :: PType -> PType -> PType) (a :: PType) (b :: PType)
       (d :: PType) (s :: S).
(PBifunctor f, PSubcategoryLeft f a, PSubcategoryRight f b,
 PSubcategoryRight f d) =>
Term s ((b :--> d) :--> (f a b :--> f a d))
psecond

-- | @since 3.1.0
instance PBifunctor PThese where
  type PSubcategoryLeft PThese = Plut
  type PSubcategoryRight PThese = Plut
  pbimap :: forall (a :: PType) (b :: PType) (c :: PType) (d :: PType)
       (s :: S).
(PSubcategoryLeft PThese a, PSubcategoryLeft PThese c,
 PSubcategoryRight PThese b, PSubcategoryRight PThese d) =>
Term
  s ((a :--> c) :--> ((b :--> d) :--> (PThese a b :--> PThese c d)))
pbimap = 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 :--> c)
f Term s (b :--> d)
g Term s (PThese a b)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PThese a b s
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case PThese a b s
t' of
        PThis Term s a
ta -> 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) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis forall a b. (a -> b) -> a -> b
$ Term s (a :--> c)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
ta
        PThat Term s b
tb -> 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) (b :: PType) (s :: S). Term s b -> PThese a b s
PThat forall a b. (a -> b) -> a -> b
$ Term s (b :--> d)
g forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb
        PThese Term s a
ta Term s b
tb -> 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) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese (Term s (a :--> c)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
ta) forall a b. (a -> b) -> a -> b
$ Term s (b :--> d)
g forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb

-- | @since 1.0.0
instance (forall (s :: S). Semigroup (Term s a)) => PApply (PThese a) where
  pliftA2 :: forall (a :: PType) (b :: PType) (c :: PType) (s :: S).
(PSubcategory (PThese a) a, PSubcategory (PThese a) b,
 PSubcategory (PThese a) c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PThese a a :--> (PThese a b :--> PThese a c)))
pliftA2 = 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 :--> c))
f Term s (PThese a a)
xs Term s (PThese a b)
ys -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PThese a a s
xs' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a a)
xs
      PThese a b s
ys' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
ys
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ case (PThese a a s
xs', PThese a b s
ys') of
        (PThis Term s a
ta, PThis Term s a
ta') -> forall (a :: PType) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis (Term s a
ta forall a. Semigroup a => a -> a -> a
<> Term s a
ta')
        (PThis Term s a
ta, PThat Term s b
_) -> forall (a :: PType) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis Term s a
ta
        (PThis Term s a
ta, PThese Term s a
ta' Term s b
_) -> forall (a :: PType) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis (Term s a
ta forall a. Semigroup a => a -> a -> a
<> Term s a
ta')
        (PThat Term s a
_, PThis Term s a
ta') -> forall (a :: PType) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis Term s a
ta'
        (PThat Term s a
tb, PThat Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S). Term s b -> PThese a b s
PThat forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tb forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb'
        (PThat Term s a
tb, PThese Term s a
ta' Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese Term s a
ta' forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tb forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb'
        (PThese Term s a
ta Term s a
_, PThis Term s a
ta') -> forall (a :: PType) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis (Term s a
ta forall a. Semigroup a => a -> a -> a
<> Term s a
ta')
        (PThese Term s a
ta Term s a
tb, PThat Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese Term s a
ta forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tb forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb'
        (PThese Term s a
ta Term s a
tb, PThese Term s a
ta' Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese (Term s a
ta forall a. Semigroup a => a -> a -> a
<> Term s a
ta') forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tb forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb'

-- | @since 1.0.0
instance (forall (s :: S). Semigroup (Term s a)) => PApplicative (PThese a) where
  ppure :: forall (a :: PType) (s :: S).
PSubcategory (PThese a) a =>
Term s (a :--> PThese a a)
ppure = 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
$ 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) (b :: PType) (s :: S). Term s b -> PThese a b s
PThat

-- | @since 1.0.0
instance
  (forall (s' :: S). Semigroup (Term s' a), forall (s' :: S). Semigroup (Term s' b)) =>
  Semigroup (Term s (PThese a b))
  where
  Term s (PThese a b)
t <> :: Term s (PThese a b) -> Term s (PThese a b) -> Term s (PThese a b)
<> Term s (PThese a b)
t' = forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PThese a b s
tleft <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t
    PThese a b s
tright <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t'
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ case (PThese a b s
tleft, PThese a b s
tright) of
      (PThis Term s a
ta, PThis Term s a
ta') -> forall (a :: PType) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis (Term s a
ta forall a. Semigroup a => a -> a -> a
<> Term s a
ta')
      (PThis Term s a
ta, PThat Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese Term s a
ta Term s b
tb'
      (PThis Term s a
ta, PThese Term s a
ta' Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese (Term s a
ta forall a. Semigroup a => a -> a -> a
<> Term s a
ta') Term s b
tb'
      (PThat Term s b
tb, PThis Term s a
ta') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese Term s a
ta' Term s b
tb
      (PThat Term s b
tb, PThat Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S). Term s b -> PThese a b s
PThat (Term s b
tb forall a. Semigroup a => a -> a -> a
<> Term s b
tb')
      (PThat Term s b
tb, PThese Term s a
ta' Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese Term s a
ta' (Term s b
tb forall a. Semigroup a => a -> a -> a
<> Term s b
tb')
      (PThese Term s a
ta Term s b
tb, PThis Term s a
ta') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese (Term s a
ta forall a. Semigroup a => a -> a -> a
<> Term s a
ta') Term s b
tb
      (PThese Term s a
ta Term s b
tb, PThat Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese Term s a
ta (Term s b
tb forall a. Semigroup a => a -> a -> a
<> Term s b
tb')
      (PThese Term s a
ta Term s b
tb, PThese Term s a
ta' Term s b
tb') -> forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese (Term s a
ta forall a. Semigroup a => a -> a -> a
<> Term s a
ta') (Term s b
tb forall a. Semigroup a => a -> a -> a
<> Term s b
tb')

-- | @since 1.0.0
instance
  (forall (s' :: S). Monoid (Term s' a), forall (s' :: S). Monoid (Term s' b)) =>
  Monoid (Term s (PThese a b))
  where
  mempty :: Term s (PThese a b)
mempty = 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) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a
mempty

-- | @since 1.0.0
instance PTraversable (PThese a) where
  ptraverse :: forall (f :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PApplicative f, PSubcategory f a, PSubcategory f b,
 PSubcategory f (PThese a b), PSubcategory (PThese a) a,
 PSubcategory (PThese a) b) =>
Term s ((a :--> f b) :--> (PThese a a :--> f (PThese a b)))
ptraverse = 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 :--> f b)
f Term s (PThese a a)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PThese a a s
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a a)
t
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case PThese a a s
t' of
        PThis Term s a
ta -> forall (f :: PType -> PType) (a :: PType) (s :: S).
(PApplicative f, PSubcategory f a) =>
Term s (a :--> f a)
ppure forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (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) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis forall a b. (a -> b) -> a -> b
$ Term s a
ta)
        PThat Term s a
tb -> forall (f :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s ((a :--> b) :--> (f a :--> f b))
pfmap 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). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (b :: PType) (s :: S). Term s b -> PThese a b s
PThat) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> f b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tb)
        PThese Term s a
ta Term s a
tb -> forall (f :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s ((a :--> b) :--> (f a :--> f b))
pfmap 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). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese Term s a
ta) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> f b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tb)
  ptraverse_ :: forall (b :: PType) (f :: PType -> PType) (a :: PType) (s :: S).
(PApplicative f, PSubcategory f b, PBoring b,
 PSubcategory (PThese a) a) =>
Term s ((a :--> f b) :--> (PThese a a :--> f b))
ptraverse_ = 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 :--> f b)
f Term s (PThese a a)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PThese a a s
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a a)
t
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case PThese a a s
t' of
        PThis Term s a
_ -> forall (f :: PType -> PType) (a :: PType) (s :: S).
(PApplicative f, PSubcategory f a) =>
Term s (a :--> f a)
ppure forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S). PBoring a => Term s a
pboring
        PThat Term s a
tb -> Term s (a :--> f b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tb
        PThese Term s a
_ Term s a
tb -> Term s (a :--> f b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tb

{- | As 'PThese', but using a 'PlutusCore.Data.Data' encoding instead.

 @since 1.0.0
-}
data PDThese (a :: S -> Type) (b :: S -> Type) (s :: S)
  = PDThis (Term s (PDataRecord '["_0" ':= a]))
  | PDThat (Term s (PDataRecord '["_0" ':= b]))
  | PDThese (Term s (PDataRecord '["_0" ':= a, "_1" ':= b]))
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (b :: PType) (s :: S) x.
Rep (PDThese a b s) x -> PDThese a b s
forall (a :: PType) (b :: PType) (s :: S) x.
PDThese a b s -> Rep (PDThese a b s) x
$cto :: forall (a :: PType) (b :: PType) (s :: S) x.
Rep (PDThese a b s) x -> PDThese a b s
$cfrom :: forall (a :: PType) (b :: PType) (s :: S) x.
PDThese a b s -> Rep (PDThese a b 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 (a :: PType) (b :: PType) (s :: S).
PDThese a b s -> Term s (PInner (PDThese a b))
forall (a :: PType) (b :: PType) (s :: S) (b :: PType).
Term s (PInner (PDThese a b))
-> (PDThese a b s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PDThese a b))
-> (PDThese a b s -> Term s b) -> Term s b
$cpmatch' :: forall (a :: PType) (b :: PType) (s :: S) (b :: PType).
Term s (PInner (PDThese a b))
-> (PDThese a b s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PDThese a b s -> Term s (PInner (PDThese a b))
$cpcon' :: forall (a :: PType) (b :: PType) (s :: S).
PDThese a b s -> Term s (PInner (PDThese a b))
PlutusType, forall (a :: PType).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
forall (a :: PType) (b :: PType) (s :: S).
Term s (PAsData (PDThese a b)) -> Term s (PDThese a b)
forall (a :: PType) (b :: PType) (s :: S).
Term s (PDThese a b) -> Term s PData
pdataImpl :: forall (s :: S). Term s (PDThese a b) -> Term s PData
$cpdataImpl :: forall (a :: PType) (b :: PType) (s :: S).
Term s (PDThese a b) -> Term s PData
pfromDataImpl :: forall (s :: S).
Term s (PAsData (PDThese a b)) -> Term s (PDThese a b)
$cpfromDataImpl :: forall (a :: PType) (b :: PType) (s :: S).
Term s (PAsData (PDThese a b)) -> Term s (PDThese a b)
PIsData, forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
forall (a :: PType) (b :: PType) (s :: S).
Term s (PDThese a b) -> Term s (PDThese a b) -> Term s PBool
#== :: forall (s :: S).
Term s (PDThese a b) -> Term s (PDThese a b) -> Term s PBool
$c#== :: forall (a :: PType) (b :: PType) (s :: S).
Term s (PDThese a b) -> Term s (PDThese a b) -> Term s PBool
PEq)

-- | @since 1.0.0
instance DerivePlutusType (PDThese a b) where type DPTStrat _ = PlutusTypeData

-- | @since 1.0.0
deriving anyclass instance (POrd a, POrd b, PIsData a, PIsData b) => PPartialOrd (PDThese a b)

-- | @since 1.0.0
deriving anyclass instance (POrd a, POrd b, PIsData a, PIsData b) => POrd (PDThese a b)

-- | @since 1.0.0
instance (PIsData a) => PFunctor (PDThese a) where
  type PSubcategory (PDThese a) = PIsData
  pfmap :: forall (a :: PType) (b :: PType) (s :: S).
(PSubcategory (PDThese a) a, PSubcategory (PDThese a) b) =>
Term s ((a :--> b) :--> (PDThese a a :--> PDThese a b))
pfmap = forall (f :: PType -> PType -> PType) (a :: PType) (b :: PType)
       (d :: PType) (s :: S).
(PBifunctor f, PSubcategoryLeft f a, PSubcategoryRight f b,
 PSubcategoryRight f d) =>
Term s ((b :--> d) :--> (f a b :--> f a d))
psecond

-- | @since 1.0.0
instance PBifunctor PDThese where
  type PSubcategoryLeft PDThese = PIsData
  type PSubcategoryRight PDThese = PIsData
  pbimap :: forall (a :: PType) (b :: PType) (c :: PType) (d :: PType)
       (s :: S).
(PSubcategoryLeft PDThese a, PSubcategoryLeft PDThese c,
 PSubcategoryRight PDThese b, PSubcategoryRight PDThese d) =>
Term
  s
  ((a :--> c) :--> ((b :--> d) :--> (PDThese a b :--> PDThese c d)))
pbimap = 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 :--> c)
f Term s (b :--> d)
g Term s (PDThese a b)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PDThese a b s
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PDThese a b)
t
      case PDThese a b s
t' of
        PDThis Term s (PDataRecord '[ "_0" ':= a])
ta -> do
          Term s (PAsData a)
ta' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta)
          Term s (PAsData c)
ta'' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (a :--> c)
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)
ta'))
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PDThese a b s
PDThis forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData c)
ta'' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        PDThat Term s (PDataRecord '[ "_0" ':= b])
tb -> do
          Term s (PAsData b)
tb' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= b])
tb)
          Term s (PAsData d)
tb'' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (b :--> d)
g 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 b)
tb'))
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= b]) -> PDThese a b s
PDThat forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData d)
tb'' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab -> do
          Term s (PAsData a)
ta' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab)
          Term s (PAsData c)
ta'' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (a :--> c)
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)
ta'))
          Term s (PAsData b)
tb' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_1" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab)
          Term s (PAsData d)
tb'' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (b :--> d)
g 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 b)
tb'))
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b]) -> PDThese a b s
PDThese forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData c)
ta'' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData d)
tb'' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil)

-- | @since 1.0.0
instance
  (PIsData a, forall (s :: S). Semigroup (Term s (PAsData a))) =>
  PApply (PDThese a)
  where
  pliftA2 :: forall (a :: PType) (b :: PType) (c :: PType) (s :: S).
(PSubcategory (PDThese a) a, PSubcategory (PDThese a) b,
 PSubcategory (PDThese a) c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PDThese a a :--> (PDThese a b :--> PDThese a c)))
pliftA2 = 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 :--> c))
f Term s (PDThese a a)
xs Term s (PDThese a b)
ys -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PDThese a a s
xs' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PDThese a a)
xs
      PDThese a b s
ys' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PDThese a b)
ys
      case (PDThese a a s
xs', PDThese a b s
ys') of
        (PDThis Term s (PDataRecord '[ "_0" ':= a])
ta, PDThis Term s (PDataRecord '[ "_0" ':= a])
ta') -> do
          Term s (PAsData a)
taData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta)
          Term s (PAsData a)
taData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PDThese a b s
PDThis forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PAsData a)
taData forall a. Semigroup a => a -> a -> a
<> Term s (PAsData a)
taData') forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        (PDThis Term s (PDataRecord '[ "_0" ':= a])
ta, PDThat Term s (PDataRecord '[ "_0" ':= b])
_) -> do
          Term s (PAsData a)
taData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta)
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PDThese a b s
PDThis forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
taData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        (PDThis Term s (PDataRecord '[ "_0" ':= a])
ta, PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab') -> do
          Term s (PAsData a)
taData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta)
          Term s (PAsData a)
taData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PDThese a b s
PDThis forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PAsData a)
taData forall a. Semigroup a => a -> a -> a
<> Term s (PAsData a)
taData') forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        (PDThat Term s (PDataRecord '[ "_0" ':= a])
_, PDThis Term s (PDataRecord '[ "_0" ':= a])
ta') -> do
          Term s (PAsData a)
taData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PDThese a b s
PDThis forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
taData' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        (PDThat Term s (PDataRecord '[ "_0" ':= a])
tb, PDThat Term s (PDataRecord '[ "_0" ':= b])
tb') -> do
          Term s (PAsData a)
tbData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
tb)
          Term s (PAsData b)
tbData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= b])
tb')
          Term s c
res <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (Term s (a :--> (b :--> c))
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)
tbData 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 b)
tbData')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= b]) -> PDThese a b s
PDThat forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 c
res forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        (PDThat Term s (PDataRecord '[ "_0" ':= a])
tb, PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab') -> do
          Term s (PAsData a)
tbData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
tb)
          Term s (PAsData a)
taData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab')
          Term s (PAsData b)
tbData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_1" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab')
          Term s c
res <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (Term s (a :--> (b :--> c))
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)
tbData 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 b)
tbData')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b]) -> PDThese a b s
PDThese forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
taData' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 c
res forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil)
        (PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= a])
tab, PDThis Term s (PDataRecord '[ "_0" ':= a])
ta') -> do
          Term s (PAsData a)
taData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= a])
tab)
          Term s (PAsData a)
taData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PDThese a b s
PDThis forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PAsData a)
taData forall a. Semigroup a => a -> a -> a
<> Term s (PAsData a)
taData') forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        (PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= a])
tab, PDThat Term s (PDataRecord '[ "_0" ':= b])
tb') -> do
          Term s (PAsData a)
taData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= a])
tab)
          Term s (PAsData a)
tbData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_1" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= a])
tab)
          Term s (PAsData b)
tbData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= b])
tb')
          Term s c
res <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (Term s (a :--> (b :--> c))
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)
tbData 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 b)
tbData')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b]) -> PDThese a b s
PDThese forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
taData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 c
res forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil)
        (PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= a])
tab, PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab') -> do
          Term s (PAsData a)
taData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= a])
tab)
          Term s (PAsData a)
tbData <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_1" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= a])
tab)
          Term s (PAsData a)
taData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab')
          Term s (PAsData b)
tbData' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_1" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab')
          Term s c
res <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC (Term s (a :--> (b :--> c))
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)
tbData 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 b)
tbData')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b]) -> PDThese a b s
PDThese forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PAsData a)
taData forall a. Semigroup a => a -> a -> a
<> Term s (PAsData a)
taData') forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 c
res forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil)

-- | @since 1.0.0
instance
  (forall (s :: S). Semigroup (Term s (PAsData a)), PIsData a) =>
  PApplicative (PDThese a)
  where
  ppure :: forall (a :: PType) (s :: S).
PSubcategory (PDThese a) a =>
Term s (a :--> PDThese a a)
ppure = 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
x -> 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) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= b]) -> PDThese a b s
PDThat forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil

-- TODO: Semigroup, Monoid for Term s (PDThese a b)
-- TODO: PTraversable for PDThese a
-- TODO: PConstantDecl for PDThese, linking to plutus-tx

{- | Case analysis for 'PThese'.

 @since 1.0.0
-}
pthese ::
  forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
  Term s ((a :--> c) :--> (b :--> c) :--> (a :--> b :--> c) :--> PThese a b :--> c)
pthese :: forall (a :: PType) (b :: PType) (c :: PType) (s :: S).
Term
  s
  ((a :--> c)
   :--> ((b :--> c)
         :--> ((a :--> (b :--> c)) :--> (PThese a b :--> c))))
pthese = 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 :--> c)
f Term s (b :--> c)
g Term s (a :--> (b :--> c))
fg Term s (PThese a b)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PThese a b s
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case PThese a b s
t' of
      PThis Term s a
ta -> Term s (a :--> c)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
ta
      PThat Term s b
tb -> Term s (b :--> c)
g forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb
      PThese Term s a
ta Term s b
tb -> Term s (a :--> (b :--> c))
fg forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
ta forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb

{- | Case analysis for 'PDThese'.

 @since 1.0.0
-}
pdthese ::
  forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
  (PIsData a, PIsData b) =>
  Term s ((a :--> c) :--> (b :--> c) :--> (a :--> b :--> c) :--> PDThese a b :--> c)
pdthese :: forall (a :: PType) (b :: PType) (c :: PType) (s :: S).
(PIsData a, PIsData b) =>
Term
  s
  ((a :--> c)
   :--> ((b :--> c)
         :--> ((a :--> (b :--> c)) :--> (PDThese a b :--> c))))
pdthese = 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 :--> c)
f Term s (b :--> c)
g Term s (a :--> (b :--> c))
fg Term s (PDThese a b)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PDThese a b s
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PDThese a b)
t
    case PDThese a b s
t' of
      PDThis Term s (PDataRecord '[ "_0" ':= a])
ta -> do
        Term s a
ta' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC 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 (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Term s (a :--> c)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
ta'
      PDThat Term s (PDataRecord '[ "_0" ':= b])
tb -> do
        Term s b
tb' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC 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 (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= b])
tb
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Term s (b :--> c)
g forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb'
      PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab -> do
        Term s a
ta' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC 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 (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab
        Term s b
tb' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC 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 (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_1" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
fg forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
ta' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
tb'

{- | Convert a 'PThese' into a 'PDThese', assuming 'PData' instances for both
 \'sides\'.

 @since 1.0.0
-}
toPDThese ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PIsData a, PIsData b) =>
  Term s (PThese a b :--> PDThese a b)
toPDThese :: forall (a :: PType) (b :: PType) (s :: S).
(PIsData a, PIsData b) =>
Term s (PThese a b :--> PDThese a b)
toPDThese = 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 (PThese a b)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PThese a b s
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PThese a b)
t
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case PThese a b s
t' of
      PThis Term s a
ta -> 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) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PDThese a b s
PDThis forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 a
ta forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
      PThat Term s b
tb -> 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) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= b]) -> PDThese a b s
PDThat forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 b
tb forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
      PThese Term s a
ta Term s b
tb -> 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) (b :: PType) (s :: S).
Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b]) -> PDThese a b s
PDThese forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 a
ta forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons 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 b
tb forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil)

{- | Convert a 'PDThese' into a 'PThese'.

 @since 1.0.0
-}
fromPDThese ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PIsData a, PIsData b) =>
  Term s (PDThese a b :--> PThese a b)
fromPDThese :: forall (a :: PType) (b :: PType) (s :: S).
(PIsData a, PIsData b) =>
Term s (PDThese a b :--> PThese a b)
fromPDThese = 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 (PDThese a b)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PDThese a b s
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PDThese a b)
t
    case PDThese a b s
t' of
      PDThis Term s (PDataRecord '[ "_0" ':= a])
ta -> do
        Term s a
ta' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC 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 (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
ta
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S). Term s a -> PThese a b s
PThis forall a b. (a -> b) -> a -> b
$ Term s a
ta'
      PDThat Term s (PDataRecord '[ "_0" ':= b])
tb -> do
        Term s b
tb' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC 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 (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= b])
tb
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S). Term s b -> PThese a b s
PThat forall a b. (a -> b) -> a -> b
$ Term s b
tb'
      PDThese Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab -> do
        Term s a
ta' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC 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 (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab
        Term s b
tb' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont s (Term s a)
pletC 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 (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_1" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a, "_1" ':= b])
tab
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PThese a b s
PThese Term s a
ta' forall a b. (a -> b) -> a -> b
$ Term s b
tb'