module Plutarch.Extra.Functor (
  -- * Type classes
  Plut,
  PFunctor (..),
  PBifunctor (..),

  -- * Functions
  (#<$),
  (#$>),
  (#<$>),
  (#<&>),
  pvoid,
) where

import Data.Kind (Constraint)
import Plutarch.Api.V1.AssocMap (KeyGuarantees, PMap (PMap))
import Plutarch.Api.V1.Maybe (PMaybeData (PDJust, PDNothing))
import Plutarch.Builtin (ppairDataBuiltin)
import Plutarch.Extra.Boring (PBoring (pboring))
import Plutarch.Extra.Function (pconst, pidentity)
import Plutarch.Extra.TermCont (pletC, pmatchC)
import Plutarch.Lift (PUnsafeLiftDecl)

{- | Describes the entire category of Plutarch types, with arrows being Plutarch
 functions. Since the typical name for the category of Haskell types is
 @Hask@, we follow this trend with naming, choosing 'Plut'.

 Use this for 'PSubcategory' if you want /any/ Plutarch type to be available.

 @since 3.1.0
-}
class Plut (a :: S -> Type)

-- | @since 3.1.0
instance Plut a

{- | Describes a Plutarch-level covariant endofunctor. However, unlike in
 Haskell, the endofunctor is defined over a subcategory of @Plut@, rather than
 all of it.

 Put another way, this is the Plutarch equivalent to 'Functor', but unlike in
 Haskell, instead of requiring full parametricity, we are allowed to constrain
 what we are parametric over.

 = Laws

 Formally, @f@ must be an endofunctor on a subcategory of @Plut@, as described
 by the 'PSubcategory' constraint. This means that the following must hold:

 * @'pfmap' '#' 'Plutarch.Extra.Category.pidentity'@ @=@
 @'Plutarch.Extra.Category.pidentity'@
 * @'pfmap' '#' (f 'Plutarch.Extra.Category.#>>>' g)@ @=@ @('pfmap' '#' f)
 'Plutarch.Extra.Category.#>>>' ('pfmap' '#' g)@

 If @'PSubcategory' f@ is 'Plut' (that is, @f@ is defined as an endofunctor on
 /all/ of @Plut@), the second law is a free theorem; however, in any other
 case, it may not be.

 @since 1.0.0
-}
class PFunctor (f :: (S -> Type) -> S -> Type) where
  {-# MINIMAL pfmap #-}

  -- | Describes the subcategory of @Plut@ that @f@ is an endofunctor on. Put
  -- another way, this describes what kind of types @f@ is \'parametric
  -- over\'.
  --
  -- Common choices for this are:
  --
  -- * 'Plut', which means \'parametric over anything of kind @'S' -> 'Type'@\'
  -- * 'PIsData', which means \'parametric over things which are
  -- @Data@-encodable\'
  -- * 'PUnsafeLiftDecl', which means \'parametric over things that have a
  -- Haskell-level equivalent\'
  type PSubcategory f :: (S -> Type) -> Constraint

  pfmap ::
    forall (a :: S -> Type) (b :: S -> Type) (s :: S).
    (PSubcategory f a, PSubcategory f b) =>
    Term s ((a :--> b) :--> f a :--> f b)

  -- | Replace all values to be computed with a fixed value. Defaults to
  -- @'pfmap' 'pconst'@, but could be more efficient for some 'PFunctor's.
  --
  -- @since 1.2.0
  {-# INLINEABLE pfconst #-}
  pfconst ::
    forall (a :: S -> Type) (b :: S -> Type) (s :: S).
    (PSubcategory f a, PSubcategory f b) =>
    Term s (a :--> f b :--> f a)
  pfconst = 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 Term s (f b)
ys -> forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s ((a :--> b) :--> (f a :--> f b))
pfmap 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 a
x) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f b)
ys

-- | @since 3.1.0
instance PFunctor PMaybe where
  type PSubcategory PMaybe = Plut
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory PMaybe a, PSubcategory PMaybe b) =>
Term s ((a :--> b) :--> (PMaybe a :--> PMaybe b))
pfmap = 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)
f Term s (PMaybe a)
t -> 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
t' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PMaybe a)
t
      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
t' of
        PMaybe a s
PNothing -> forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing
        PJust Term s a
t'' -> forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust forall a b. (a -> b) -> a -> b
$ Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
t''

-- | @since 1.0.0
instance PFunctor PMaybeData where
  type PSubcategory PMaybeData = PIsData
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory PMaybeData a, PSubcategory PMaybeData b) =>
Term s ((a :--> b) :--> (PMaybeData a :--> PMaybeData b))
pfmap = 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)
f Term s (PMaybeData a)
t -> 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
t' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PMaybeData a)
t
      case PMaybeData a s
t' of
        PDNothing Term s (PDataRecord '[])
_ -> 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
        PDJust Term s (PDataRecord '[ "_0" ':= a])
t'' -> 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])
t'')
          Term s b
res <- forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s (a :--> b)
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 (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 b
res 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 3.1.0
instance PFunctor PList where
  type PSubcategory PList = Plut
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory PList a, PSubcategory PList b) =>
Term s ((a :--> b) :--> (PList a :--> PList b))
pfmap = 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)
f Term s (PList a)
t -> forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
t

-- | @since 1.0.0
instance PFunctor PBuiltinList where
  type PSubcategory PBuiltinList = PUnsafeLiftDecl
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory PBuiltinList a, PSubcategory PBuiltinList b) =>
Term s ((a :--> b) :--> (PBuiltinList a :--> PBuiltinList b))
pfmap = 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)
f Term s (PBuiltinList a)
t -> forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
t

-- | @since 1.0.0
instance forall (s :: KeyGuarantees) (k :: S -> Type). (PIsData k) => PFunctor (PMap s k) where
  type PSubcategory (PMap s k) = PIsData
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory (PMap s k) a, PSubcategory (PMap s k) b) =>
Term s ((a :--> b) :--> (PMap s k a :--> PMap s k b))
pfmap = forall (f :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (d :: S -> Type) (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 PFunctor (PPair a) where
  type PSubcategory (PPair a) = Plut
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory (PPair a) a, PSubcategory (PPair a) b) =>
Term s ((a :--> b) :--> (PPair a a :--> PPair a b))
pfmap = forall (f :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (d :: S -> Type) (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 PFunctor (PEither e) where
  type PSubcategory (PEither e) = Plut
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory (PEither e) a, PSubcategory (PEither e) b) =>
Term s ((a :--> b) :--> (PEither e a :--> PEither e b))
pfmap = forall (f :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (d :: S -> Type) (s :: S).
(PBifunctor f, PSubcategoryLeft f a, PSubcategoryRight f b,
 PSubcategoryRight f d) =>
Term s ((b :--> d) :--> (f a b :--> f a d))
psecond

{- | Infix, 'Term'-lifted version of 'pfconst'.

 @since 1.0.0
-}
(#<$) ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PFunctor f, PSubcategory f a, PSubcategory f b) =>
  Term s a ->
  Term s (f b) ->
  Term s (f a)
Term s a
x #<$ :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s a -> Term s (f b) -> Term s (f a)
#<$ Term s (f b)
f = forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s (a :--> (f b :--> f a))
pfconst 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 (f b)
f

infixl 4 #<$

{- | Flipped version of '#<$'.

 @since 1.0.0
-}
(#$>) ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PFunctor f, PSubcategory f a, PSubcategory f b) =>
  Term s (f a) ->
  Term s b ->
  Term s (f b)
#$> :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s (f a) -> Term s b -> Term s (f b)
(#$>) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s a -> Term s (f b) -> Term s (f a)
(#<$)

infixl 4 #$>

{- | Infix, 'Term'-level version of 'pfmap'.

 @since 1.0.0
-}
(#<$>) ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PFunctor f, PSubcategory f a, PSubcategory f b) =>
  Term s (a :--> b) ->
  Term s (f a) ->
  Term s (f b)
Term s (a :--> b)
f #<$> :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s (a :--> b) -> Term s (f a) -> Term s (f b)
#<$> Term s (f a)
t = forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s ((a :--> b) :--> (f a :--> f b))
pfmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
f 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

infixl 4 #<$>

{- | Flipped version of '#<$>'.

 @since 1.0.0
-}
(#<&>) ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PFunctor f, PSubcategory f a, PSubcategory f b) =>
  Term s (f a) ->
  Term s (a :--> b) ->
  Term s (f b)
#<&> :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s (f a) -> Term s (a :--> b) -> Term s (f b)
(#<&>) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s (a :--> b) -> Term s (f a) -> Term s (f b)
(#<$>)

infixl 1 #<&>

{- | Erases every location in the input.

 @since 1.2.0
-}
pvoid ::
  forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  (PFunctor f, PSubcategory f a, PSubcategory f b, PBoring b) =>
  Term s (f a) ->
  Term s (f b)
pvoid :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b, PBoring b) =>
Term s (f a) -> Term s (f b)
pvoid Term s (f a)
t = forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s (a :--> (f b :--> f a))
pfconst 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 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

{- | Similar to 'PFunctor', but is covariant in /two/ parameters instead of one.
 This means that types like 'PEither' don't need to be partially applied, as
 is the case with 'PFunctor'. Formally, this represents a Plutarch-level
 covariant bifunctor; just as with 'PFunctor' however, it is defined over a
 subcategory of 'Plut'.

 Similarly to 'PFunctor', this is the Plutarch equivalent of 'Bifunctor'.

 = Laws

 Formally, @f@ must be a bifunctor on a subcategory of @Plut@, as described by
 'PSubcategoryLeft' (for the first parameter) and 'PSubcategoryRight' (for the
 second). For 'pbimap', this means the following must hold:

 * @'pbimap' '#' 'Plutarch.Extra.Category.pidentity' '#'
 'Plutarch.Extra.Category.pidentity'@ @=@
 @'Plutarch.Extra.Category.pidentity'@
 * @'pbimap' '#' (f1 'Plutarch.Extra.Category.#>>>' f2) '#' (g1
 'Plutarch.Extra.Category.#>>>' g2)@ @=@ @('pbimap' '#' f1 '#' g1)
 'Plutarch.Extra.Category.#>>>' ('pbimap' '#' f2 '#' g2)@

 Furthermore, @'PSubcategoryLeft f' ~ 'PSubcategoryRight' f@ should hold; this
 may be required in the future. If both @'PSubcategoryLeft' f@ and
 @'PSubcategoryRight' f@ are 'Plut', the second law is a free theorem; however,
 this does not hold in general.

 If you define 'pfirst' and 'psecond', the following must also hold:

 * @'pfirst' '#' 'Plutarch.Extra.Category.pidentity'@ @=@ @'psecond' '#'
 'Plutarch.Extra.Category.pidentity'@ @=@
 @'Plutarch.Extra.Category.pidentity'@
 * @'pfirst' '#' f@ @=@ @'pbimap' '#' f '#'
 'Plutarch.Extra.Category.pidentity'@
 * @'psecond' '#' f@ @=@ @'pbimap' '#' 'Plutarch.Extra.Category.pidentity' '#'
 f@
 * @'pfirst' '#' (f 'Plutarch.Extra.Category.#>>>' g)@ @=@ @('pfirst' '#' f)
 'Plutarch.Extra.Category.#>>>' ('pfirst' '#' g)@
 * @'psecond' '#' (f 'Plutarch.Extra.Category.#>>>' g)@ @=@ @('psecond' '#' f)
 'Plutarch.Extra.Category.#>>>' ('psecond' '#' g)@

 If you define 'pfirst' and 'psecond' /instead/ of 'pbimap', the following
 must also hold:

 * @('pfirst' '#' f) 'Plutarch.Extra.Category.#>>>' ('psecond' '#' g)@ @=@
 @('psecond' '#' g) 'Plutarch.Extra.Category.#>>>' ('pfirst' '#' f)@ @=@
 @'pbimap' '#' f '#' g@

 = Note

 If @f a@ is also an instance of 'PFunctor', @'PSubcategoryRight' f ~
 'PSubcategory' (f a)@ should hold, and we should have @'pfmap' = 'psecond'@;
 once again, this is not currently enforced, but may be in the future.

 @since 1.0.0
-}
class PBifunctor (f :: (S -> Type) -> (S -> Type) -> S -> Type) where
  -- | Similar to 'PSubcategory', but for only the first parameter of @f@. See
  -- the documentation on 'PSubcategory' for common choices here.
  type PSubcategoryLeft f :: (S -> Type) -> Constraint

  -- | Similar to 'PSubcategory', but for only the second parameter of @f@.
  -- See the documentation on 'PSubcategory' for common choices here.
  type PSubcategoryRight f :: (S -> Type) -> Constraint

  {-# MINIMAL pbimap | pfirst, psecond #-}
  pbimap ::
    forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (d :: S -> Type) (s :: S).
    ( PSubcategoryLeft f a
    , PSubcategoryLeft f c
    , PSubcategoryRight f b
    , PSubcategoryRight f d
    ) =>
    Term s ((a :--> c) :--> (b :--> d) :--> f a b :--> f c d)
  pbimap = 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 :--> c)
f Term s (b :--> d)
g Term s (f a b)
t -> forall (f :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PBifunctor f, PSubcategoryLeft f a, PSubcategoryLeft f c,
 PSubcategoryRight f b) =>
Term s ((a :--> c) :--> (f a b :--> f c b))
pfirst forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> c)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (f :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (d :: S -> Type) (s :: S).
(PBifunctor f, PSubcategoryLeft f a, PSubcategoryRight f b,
 PSubcategoryRight f d) =>
Term s ((b :--> d) :--> (f a b :--> f a d))
psecond forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (b :--> d)
g 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)
t)
  pfirst ::
    forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
    ( PSubcategoryLeft f a
    , PSubcategoryLeft f c
    , PSubcategoryRight f b
    ) =>
    Term s ((a :--> c) :--> f a b :--> f c b)
  pfirst = 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 :--> c)
f Term s (f a b)
t -> forall (f :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (d :: S -> Type)
       (s :: S).
(PBifunctor f, PSubcategoryLeft f a, PSubcategoryLeft f c,
 PSubcategoryRight f b, PSubcategoryRight f d) =>
Term s ((a :--> c) :--> ((b :--> d) :--> (f a b :--> f c d)))
pbimap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> c)
f 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). Term s (a :--> a)
pidentity 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)
t
  psecond ::
    forall (a :: S -> Type) (b :: S -> Type) (d :: S -> Type) (s :: S).
    ( PSubcategoryLeft f a
    , PSubcategoryRight f b
    , PSubcategoryRight f d
    ) =>
    Term s ((b :--> d) :--> f a b :--> f a d)
  psecond = 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 (b :--> d)
g Term s (f a b)
t -> forall (f :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (d :: S -> Type)
       (s :: S).
(PBifunctor f, PSubcategoryLeft f a, PSubcategoryLeft f c,
 PSubcategoryRight f b, PSubcategoryRight f d) =>
Term s ((a :--> c) :--> ((b :--> d) :--> (f a b :--> f c d)))
pbimap 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). Term s (a :--> a)
pidentity forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (b :--> d)
g 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)
t

-- | @since 3.1.0
instance PBifunctor PPair where
  type PSubcategoryLeft PPair = Plut
  type PSubcategoryRight PPair = Plut
  pbimap :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type)
       (d :: S -> Type) (s :: S).
(PSubcategoryLeft PPair a, PSubcategoryLeft PPair c,
 PSubcategoryRight PPair b, PSubcategoryRight PPair d) =>
Term
  s ((a :--> c) :--> ((b :--> d) :--> (PPair a b :--> PPair c d)))
pbimap = 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 :--> c)
f Term s (b :--> d)
g Term s (PPair a b)
t -> 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
x Term s b
y <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PPair 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 :: 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 :--> 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 a b. (a -> b) -> a -> b
$ Term s (b :--> d)
g 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 3.1.0
instance PBifunctor PEither where
  type PSubcategoryLeft PEither = Plut
  type PSubcategoryRight PEither = Plut
  pbimap :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type)
       (d :: S -> Type) (s :: S).
(PSubcategoryLeft PEither a, PSubcategoryLeft PEither c,
 PSubcategoryRight PEither b, PSubcategoryRight PEither d) =>
Term
  s
  ((a :--> c) :--> ((b :--> d) :--> (PEither a b :--> PEither c d)))
pbimap = 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 :--> c)
f Term s (b :--> d)
g Term s (PEither a b)
t -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PEither a b s
t' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PEither 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 :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ case PEither a b s
t' of
        PLeft Term s a
x -> forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> PEither a b s
PLeft forall a b. (a -> b) -> a -> b
$ Term s (a :--> 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
        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 (b :--> d)
g 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
instance forall (keys :: KeyGuarantees). PBifunctor (PMap keys) where
  type PSubcategoryLeft (PMap keys) = PIsData
  type PSubcategoryRight (PMap keys) = PIsData
  pbimap ::
    forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (d :: S -> Type) (s :: S).
    (PIsData a, PIsData b, PIsData c, PIsData d) =>
    Term s ((a :--> b) :--> (c :--> d) :--> PMap keys a c :--> PMap keys b d)
  pbimap :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type)
       (d :: S -> Type) (s :: S).
(PIsData a, PIsData b, PIsData c, PIsData d) =>
Term
  s
  ((a :--> b)
   :--> ((c :--> d) :--> (PMap keys a c :--> PMap keys b d)))
pbimap = 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)
f Term s (c :--> d)
g Term s (PMap keys a c)
t -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PMap Term s (PBuiltinList (PBuiltinPair (PAsData a) (PAsData c)))
t' <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PMap keys a c)
t
      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 (keysort :: KeyGuarantees) (k :: S -> Type) (v :: S -> Type)
       (s :: S).
Term s (PBuiltinList (PBuiltinPair (PAsData k) (PAsData v)))
-> PMap keysort k v s
PMap forall a b. (a -> b) -> a -> b
$ forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s ((a :--> b) :--> (f a :--> f b))
pfmap 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'
  ((a :--> b)
   :--> ((c :--> d)
         :--> (PBuiltinPair (PAsData a) (PAsData c)
               :--> PBuiltinPair (PAsData b) (PAsData d))))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (c :--> d)
g) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair (PAsData a) (PAsData c)))
t'
    where
      go ::
        forall (s' :: S).
        Term
          s'
          ( (a :--> b)
              :--> (c :--> d)
              :--> PBuiltinPair (PAsData a) (PAsData c)
              :--> PBuiltinPair (PAsData b) (PAsData d)
          )
      go :: forall (s' :: S).
Term
  s'
  ((a :--> b)
   :--> ((c :--> d)
         :--> (PBuiltinPair (PAsData a) (PAsData c)
               :--> PBuiltinPair (PAsData b) (PAsData d))))
go = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
        forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
f Term s (c :--> d)
g Term s (PBuiltinPair (PAsData a) (PAsData c))
p -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
          Term s a
k <- 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 (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData a) (PAsData c))
p)
          Term s c
v <- 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 (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData a) (PAsData c))
p)
          Term s b
k' <- forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
k)
          Term s d
v' <- forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s (c :--> d)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s c
v)
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s b
k' 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 d
v'