{-# LANGUAGE QuantifiedConstraints #-}

module Plutarch.Extra.Applicative (
  -- * Type classes
  PApply (..),
  PApplicative (..),
  PAlt (..),
  PAlternative (..),

  -- * Functions
  (#<*>),
  (#*>),
  (#<*),
  (#<!>),
  preplicateA,
  preplicateA_,
  pwhen,
  punless,
  ppureIf,
) where

import Plutarch.Api.V1.Maybe (PMaybeData (PDJust, PDNothing))
import Plutarch.Extra.Boring (PBoring (pboring))
import Plutarch.Extra.Function (papply, pconst)
import Plutarch.Extra.Functor (PFunctor (PSubcategory))
import Plutarch.Extra.Maybe (pdnothing, pnothing)
import Plutarch.Extra.TermCont (pletC, pmatchC)
import Plutarch.List (puncons)

-- | @since 1.0.0
class (PFunctor f) => PApply (f :: (S -> Type) -> S -> Type) where
  pliftA2 ::
    forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
    (PSubcategory f a, PSubcategory f b, PSubcategory f c) =>
    Term s ((a :--> b :--> c) :--> f a :--> f b :--> f c)

-- | @since 1.0.0
instance PApply PMaybe where
  pliftA2 :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSubcategory PMaybe a, PSubcategory PMaybe b,
 PSubcategory PMaybe c) =>
Term
  s
  ((a :--> (b :--> c)) :--> (PMaybe a :--> (PMaybe b :--> PMaybe c)))
pliftA2 = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
f Term s (PMaybe a)
xs Term s (PMaybe b)
ys -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PMaybe a s
xs' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PMaybe a)
xs
      PMaybe b s
ys' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PMaybe 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 :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ case (PMaybe a s
xs', PMaybe b s
ys') of
        (PJust Term s a
x, PJust Term s b
y) -> forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y
        (PMaybe a s, PMaybe b s)
_ -> forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing

-- | @since 1.0.0
instance PApply PMaybeData where
  pliftA2 :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSubcategory PMaybeData a, PSubcategory PMaybeData b,
 PSubcategory PMaybeData c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PMaybeData a :--> (PMaybeData b :--> PMaybeData c)))
pliftA2 = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
f Term s (PMaybeData a)
xs Term s (PMaybeData b)
ys -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PMaybeData a s
xs' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PMaybeData a)
xs
      PMaybeData b s
ys' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PMaybeData b)
ys
      case (PMaybeData a s
xs', PMaybeData b s
ys') of
        (PDJust Term s (PDataRecord '[ "_0" ':= a])
x, PDJust Term s (PDataRecord '[ "_0" ':= b])
y) -> do
          Term s a
x' <- forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (b :: S -> Type) (p :: S -> Type) (s :: S)
       (a :: S -> Type) (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 :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= a])
x)
          Term s b
y' <- forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (b :: S -> Type) (p :: S -> Type) (s :: S)
       (a :: S -> Type) (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 :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[ "_0" ':= b])
y)
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PMaybeData a s
PDJust forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (a :--> (b :--> c))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x' forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y') forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil
        (PMaybeData a s, PMaybeData b s)
_ -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '[]) -> PMaybeData a s
PDNothing forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s (PDataRecord '[])
pdnil

-- | @since 1.0.0
instance PApply PList where
  pliftA2 :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSubcategory PList a, PSubcategory PList b,
 PSubcategory PList c) =>
Term
  s ((a :--> (b :--> c)) :--> (PList a :--> (PList b :--> PList c)))
pliftA2 = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic
    forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix
      #$ plam
    $ \self f xs ys -> unTermCont $ do
      t <- pmatchC (puncons # ys)
      case t of
        PNothing -> pure pnil
        PJust t' -> do
          PPair thead ttail <- pmatchC t'
          res <- pletC (pmap # plam (\x -> f # x # thead) # xs)
          pure $ pconcat # res # (self # f # xs # ttail)

-- | @since 1.0.0
instance PApply PBuiltinList where
  pliftA2 :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSubcategory PBuiltinList a, PSubcategory PBuiltinList b,
 PSubcategory PBuiltinList c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PBuiltinList a :--> (PBuiltinList b :--> PBuiltinList c)))
pliftA2 = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic
    forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix
      #$ plam
    $ \self f xs ys -> unTermCont $ do
      t <- pmatchC (puncons # ys)
      case t of
        PNothing -> pure pnil
        PJust t' -> do
          PPair thead ttail <- pmatchC t'
          res <- pletC (pmap # plam (\x -> f # x # thead) # xs)
          pure $ pconcat # res # (self # f # xs # ttail)

-- | @since 1.0.0
instance (forall (s :: S). Semigroup (Term s a)) => PApply (PPair a) where
  pliftA2 :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSubcategory (PPair a) a, PSubcategory (PPair a) b,
 PSubcategory (PPair a) c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PPair a a :--> (PPair a b :--> PPair a c)))
pliftA2 = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
f Term s (PPair a a)
xs Term s (PPair a b)
ys -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PPair Term s a
x1 Term s a
x2 <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PPair a a)
xs
      PPair Term s a
y1 Term s b
y2 <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PPair 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 :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair (Term s a
x1 forall a. Semigroup a => a -> a -> a
<> Term s a
y1) forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x2 forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y2

{- | Forwards the /first/ 'PLeft'.

 @since 1.0.0
-}
instance PApply (PEither e) where
  pliftA2 :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSubcategory (PEither e) a, PSubcategory (PEither e) b,
 PSubcategory (PEither e) c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PEither e a :--> (PEither e b :--> PEither e c)))
pliftA2 = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
f Term s (PEither e a)
xs Term s (PEither e b)
ys -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PEither e a s
xs' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PEither e a)
xs
      PEither e b s
ys' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PEither e 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 :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ case (PEither e a s
xs', PEither e b s
ys') of
        (PLeft Term s e
e, PEither e b s
_) -> forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> PEither a b s
PLeft Term s e
e
        (PEither e a s
_, PLeft Term s e
e) -> forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> PEither a b s
PLeft Term s e
e
        (PRight Term s a
x, PRight Term s b
y) -> forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s b -> PEither a b s
PRight forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y

-- | @since 1.0.0
class (PApply f) => PApplicative (f :: (S -> Type) -> S -> Type) where
  ppure ::
    forall (a :: S -> Type) (s :: S).
    (PSubcategory f a) =>
    Term s (a :--> f a)

-- | @since 1.0.0
instance PApplicative PMaybe where
  ppure :: forall (a :: S -> Type) (s :: S).
PSubcategory PMaybe a =>
Term s (a :--> PMaybe a)
ppure = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust

-- | @since 1.0.0
instance PApplicative PMaybeData where
  ppure :: forall (a :: S -> Type) (s :: S).
PSubcategory PMaybeData a =>
Term s (a :--> PMaybeData a)
ppure = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '[ "_0" ':= a]) -> PMaybeData a s
PDJust forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord '[])
pdnil

-- | @since 1.0.0
instance PApplicative PList where
  ppure :: forall (a :: S -> Type) (s :: S).
PSubcategory PList a =>
Term s (a :--> PList a)
ppure = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

-- | @since 1.0.0
instance PApplicative PBuiltinList where
  ppure :: forall (a :: S -> Type) (s :: S).
PSubcategory PBuiltinList a =>
Term s (a :--> PBuiltinList a)
ppure = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

-- | @since 1.0.0
instance (forall (s :: S). Monoid (Term s a)) => PApplicative (PPair a) where
  ppure :: forall (a :: S -> Type) (s :: S).
PSubcategory (PPair a) a =>
Term s (a :--> PPair a a)
ppure = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair forall a. Monoid a => a
mempty

-- | @since 1.0.0
instance PApplicative (PEither e) where
  ppure :: forall (a :: S -> Type) (s :: S).
PSubcategory (PEither e) a =>
Term s (a :--> PEither e a)
ppure = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s b -> PEither a b s
PRight

-- | @since 1.0.0
(#<*>) ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PSubcategory f (a :--> b), PSubcategory f a, PSubcategory f b, PApply f) =>
  Term s (f (a :--> b)) ->
  Term s (f a) ->
  Term s (f b)
Term s (f (a :--> b))
fs #<*> :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PSubcategory f (a :--> b), PSubcategory f a, PSubcategory f b,
 PApply f) =>
Term s (f (a :--> b)) -> Term s (f a) -> Term s (f b)
#<*> Term s (f a)
xs = forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (c :: S -> Type) (s :: S).
(PApply f, PSubcategory f a, PSubcategory f b, PSubcategory f c) =>
Term s ((a :--> (b :--> c)) :--> (f a :--> (f b :--> f c)))
pliftA2 forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s ((a :--> b) :--> (a :--> b))
papply forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f (a :--> b))
fs forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
xs

infixl 4 #<*>

-- | @since 1.0.0
(#*>) ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PSubcategory f a, PSubcategory f b, PApply f) =>
  Term s (f a) ->
  Term s (f b) ->
  Term s (f b)
Term s (f a)
t #*> :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PSubcategory f a, PSubcategory f b, PApply f) =>
Term s (f a) -> Term s (f b) -> Term s (f b)
#*> Term s (f b)
t' = forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (c :: S -> Type) (s :: S).
(PApply f, PSubcategory f a, PSubcategory f b, PSubcategory f c) =>
Term s ((a :--> (b :--> c)) :--> (f a :--> (f b :--> f c)))
pliftA2 forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s a
_ Term s b
x -> Term s b
x) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
t forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f b)
t'

infixl 4 #*>

-- | @since 1.0.0
(#<*) ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PSubcategory f a, PSubcategory f b, PApply f) =>
  Term s (f a) ->
  Term s (f b) ->
  Term s (f a)
Term s (f a)
t #<* :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PSubcategory f a, PSubcategory f b, PApply f) =>
Term s (f a) -> Term s (f b) -> Term s (f a)
#<* Term s (f b)
t' = forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (c :: S -> Type) (s :: S).
(PApply f, PSubcategory f a, PSubcategory f b, PSubcategory f c) =>
Term s ((a :--> (b :--> c)) :--> (f a :--> (f b :--> f c)))
pliftA2 forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (a :--> (b :--> a))
pconst forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
t forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f b)
t'

infixl 4 #<*

{- | 'preplicateA' @n@ @comp@ repeats @comp@ @n@ times (0 if @n@ is negative),
 collects the results into a 'PListLike', and returns a single computation
 producing them all.

 = Notes

 The type of the 'PListLike' is left flexible: you can set it using
 @TypeApplications@. We put that type parameter first to make this easier.

 @since 1.2.0
-}
preplicateA ::
  forall
    (ell :: (S -> Type) -> S -> Type)
    (f :: (S -> Type) -> S -> Type)
    (a :: S -> Type)
    (s :: S).
  ( PApplicative f
  , PListLike ell
  , PElemConstraint ell a
  , PSubcategory f (ell a)
  , PSubcategory f a
  ) =>
  Term s (PInteger :--> f a :--> f (ell a))
preplicateA :: forall (ell :: (S -> Type) -> S -> Type)
       (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PApplicative f, PListLike ell, PElemConstraint ell a,
 PSubcategory f (ell a), PSubcategory f a) =>
Term s (PInteger :--> (f a :--> f (ell a)))
preplicateA = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (f a :--> f (ell a)))
self Term s PInteger
count Term s (f a)
comp ->
    forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s PInteger
0 forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
count) (forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PApplicative f, PSubcategory f a) =>
Term s (a :--> f a)
ppure forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil) (forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (c :: S -> Type) (s :: S).
(PApply f, PSubcategory f a, PSubcategory f b, PSubcategory f c) =>
Term s ((a :--> (b :--> c)) :--> (f a :--> (f b :--> f c)))
pliftA2 forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
comp forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PInteger :--> (f a :--> f (ell a)))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
count forall a. Num a => a -> a -> a
- Term s PInteger
1) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
comp))

{- | As 'preplicateA', but ignores the results.

 @since 1.2.0
-}
preplicateA_ ::
  forall
    (f :: (S -> Type) -> S -> Type)
    (b :: S -> Type)
    (s :: S).
  (PApplicative f, PBoring b, PSubcategory f b) =>
  Term s (PInteger :--> f b :--> f b)
preplicateA_ :: forall (f :: (S -> Type) -> S -> Type) (b :: S -> Type) (s :: S).
(PApplicative f, PBoring b, PSubcategory f b) =>
Term s (PInteger :--> (f b :--> f b))
preplicateA_ = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (f b :--> f b))
self Term s PInteger
count Term s (f b)
comp ->
    forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s PInteger
0 forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
count) (forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PApplicative f, PSubcategory f a) =>
Term s (a :--> f a)
ppure forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S). PBoring a => Term s a
pboring) (Term s (f b)
comp forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PSubcategory f a, PSubcategory f b, PApply f) =>
Term s (f a) -> Term s (f b) -> Term s (f b)
#*> (Term s (PInteger :--> (f b :--> f b))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
count forall a. Num a => a -> a -> a
- Term s PInteger
1) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f b)
comp))

{- | 'pwhen' @b@ @comp@ executes @comp@ if @b@ is 'PTrue', and does nothing
 otherwise.

 @since 1.2.0
-}
pwhen ::
  forall
    (f :: (S -> Type) -> S -> Type)
    (b :: S -> Type)
    (s :: S).
  (PApplicative f, PBoring b, PSubcategory f b) =>
  Term s (PBool :--> f b :--> f b)
pwhen :: forall (f :: (S -> Type) -> S -> Type) (b :: S -> Type) (s :: S).
(PApplicative f, PBoring b, PSubcategory f b) =>
Term s (PBool :--> (f b :--> f b))
pwhen = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PBool
b Term s (f b)
comp -> forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif Term s PBool
b Term s (f b)
comp (forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PApplicative f, PSubcategory f a) =>
Term s (a :--> f a)
ppure forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S). PBoring a => Term s a
pboring)

{- | 'punless' @b@ @comp@ executes @comp@ if @b@ is 'PFalse', and does nothing
 otherwise.

 @since 1.2.0
-}
punless ::
  forall
    (f :: (S -> Type) -> S -> Type)
    (b :: S -> Type)
    (s :: S).
  (PApplicative f, PBoring b, PSubcategory f b) =>
  Term s (PBool :--> f b :--> f b)
punless :: forall (f :: (S -> Type) -> S -> Type) (b :: S -> Type) (s :: S).
(PApplicative f, PBoring b, PSubcategory f b) =>
Term s (PBool :--> (f b :--> f b))
punless = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PBool
b Term s (f b)
comp -> forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif Term s PBool
b (forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PApplicative f, PSubcategory f a) =>
Term s (a :--> f a)
ppure forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S). PBoring a => Term s a
pboring) Term s (f b)
comp

{- | Laws:

    > (a #<!> b) #<!> c = a #<!> (b #<!> c)
    > f #<$> (a #<!> b) = (f #<$> a) #<!> (f #<$> b)

    @since 3.14.1
-}
class (PFunctor f) => PAlt f where
  palt ::
    forall (a :: PType) (s :: S).
    (PSubcategory f a) =>
    Term s (f a :--> f a :--> f a)

infixl 3 #<!>

-- | @since 3.14.1
(#<!>) ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
  (PSubcategory f a, PAlt f) =>
  Term s (f a) ->
  Term s (f a) ->
  Term s (f a)
Term s (f a)
a #<!> :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PSubcategory f a, PAlt f) =>
Term s (f a) -> Term s (f a) -> Term s (f a)
#<!> Term s (f a)
b = forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PAlt f, PSubcategory f a) =>
Term s (f a :--> (f a :--> f a))
palt forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
a forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
b

-- | @since 3.14.1
instance PAlt PMaybe where
  palt :: forall (a :: S -> Type) (s :: S).
PSubcategory PMaybe a =>
Term s (PMaybe a :--> (PMaybe a :--> PMaybe a))
palt = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PMaybe a)
a Term s (PMaybe a)
b -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybe a)
a forall a b. (a -> b) -> a -> b
$ \case
      PMaybe a s
PNothing -> Term s (PMaybe a)
b
      PMaybe a s
_ -> Term s (PMaybe a)
a

-- | @since 3.14.1
instance PAlt (PEither a) where
  palt :: forall (a :: S -> Type) (s :: S).
PSubcategory (PEither a) a =>
Term s (PEither a a :--> (PEither a a :--> PEither a a))
palt = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PEither a a)
a Term s (PEither a a)
b -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PEither a a)
a forall a b. (a -> b) -> a -> b
$ \case
      PLeft Term s a
_ -> Term s (PEither a a)
b
      PEither a a s
_ -> Term s (PEither a a)
a

-- | @since 3.14.1
instance PAlt PMaybeData where
  palt :: forall (a :: S -> Type) (s :: S).
PSubcategory PMaybeData a =>
Term s (PMaybeData a :--> (PMaybeData a :--> PMaybeData a))
palt = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PMaybeData a)
a Term s (PMaybeData a)
b -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybeData a)
a forall a b. (a -> b) -> a -> b
$ \case
      PDNothing Term s (PDataRecord '[])
_ -> Term s (PMaybeData a)
b
      PMaybeData a s
_ -> Term s (PMaybeData a)
a

-- | @since 3.14.1
instance PAlt PList where
  palt :: forall (a :: S -> Type) (s :: S).
PSubcategory PList a =>
Term s (PList a :--> (PList a :--> PList a))
palt = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PList a)
a Term s (PList a)
b ->
      forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
a) Term s (PList a)
b Term s (PList a)
a

-- | @since 3.14.1
instance PAlt PBuiltinList where
  palt :: forall (a :: S -> Type) (s :: S).
PSubcategory PBuiltinList a =>
Term s (PBuiltinList a :--> (PBuiltinList a :--> PBuiltinList a))
palt = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList a)
a Term s (PBuiltinList a)
b ->
      forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
a) Term s (PBuiltinList a)
b Term s (PBuiltinList a)
a

{- | Laws:

    > pempty #<!> x = x
    > x #<!> pempty = x
    > (a #<!> b) #<*> c = (a #<*> c) #<!> (b #<*> c)

    @since 3.14.1
-}
class (PApplicative f, PAlt f) => PAlternative f where
  pempty ::
    forall (a :: PType) (s :: S).
    (PSubcategory f a) =>
    Term s (f a)

-- | @since 3.14.1
instance PAlternative PMaybe where
  pempty :: forall (a :: S -> Type) (s :: S).
PSubcategory PMaybe a =>
Term s (PMaybe a)
pempty = forall (a :: S -> Type) (s :: S). Term s (PMaybe a)
pnothing

-- | @since 3.14.1
instance PAlternative PMaybeData where
  pempty :: forall (a :: S -> Type) (s :: S).
PSubcategory PMaybeData a =>
Term s (PMaybeData a)
pempty = forall (a :: S -> Type) (s :: S). Term s (PMaybeData a)
pdnothing

-- | @since 3.14.1
instance PAlternative PList where
  pempty :: forall (a :: S -> Type) (s :: S).
PSubcategory PList a =>
Term s (PList a)
pempty = forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

-- | @since 3.14.1
instance PAlternative PBuiltinList where
  pempty :: forall (a :: S -> Type) (s :: S).
PSubcategory PBuiltinList a =>
Term s (PBuiltinList a)
pempty = forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

{- | Return a pure value if a condition is True, otherwise empty.

     @since 3.14.1
-}
ppureIf ::
  forall
    (f :: PType -> PType)
    (a :: PType)
    (s :: S).
  (PAlternative f, PSubcategory f a) =>
  Term s (PBool :--> a :--> f a)
ppureIf :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PAlternative f, PSubcategory f a) =>
Term s (PBool :--> (a :--> f a))
ppureIf = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PBool
cond Term s a
x ->
    forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      Term s PBool
cond
      (forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PApplicative f, PSubcategory f a) =>
Term s (a :--> f a)
ppure forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x)
      forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PAlternative f, PSubcategory f a) =>
Term s (f a)
pempty