module Plutarch.Extra.Star (
  -- * Type
  PStar (..),

  -- * Functions
  papplyStar,
) where

import Plutarch.Extra.Applicative (PApplicative (ppure), PApply (pliftA2))
import Plutarch.Extra.Bind (PBind ((#>>=)))
import Plutarch.Extra.Category (PCategory (pidentity), PSemigroupoid ((#>>>)))
import Plutarch.Extra.Functor (PFunctor (PSubcategory, pfmap), Plut)
import Plutarch.Extra.Profunctor (PProfunctor (PCoSubcategory, PContraSubcategory, pdimap))
import Plutarch.Extra.TermCont (pmatchC)

{- | The (profunctorial) view over a Kleisli arrow. Its name comes from category
 theory, as it is one of the ways we can lift a functor (in this case, @f@)
 into a profunctor.

 This essentially enables us to work with @a :--> f b@ using 'PSemigroupoid'
 and 'PCategory' operations as easily as we do @a :--> b@, provided that @f@
 is at least a 'PBind'. With the addition of a 'PApplicative' (for identities),
 we become a full 'PCategory'. Furthermore, we can also compose freely with
 ordinary Plutarch ':-->' at /both/ ends of a 'PStar', provided @f@ is at
 least 'PFunctor'.

 @since 3.0.1
-}
newtype PStar (f :: (S -> Type) -> S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S)
  = PStar (Term s (a :--> f b))
  deriving stock
    ( -- | @since 3.0.1
      forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S) x.
Rep (PStar f a b s) x -> PStar f a b s
forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S) x.
PStar f a b s -> Rep (PStar f a b s) x
$cto :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S) x.
Rep (PStar f a b s) x -> PStar f a b s
$cfrom :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S) x.
PStar f a b s -> Rep (PStar f a b s) x
Generic
    )
  deriving anyclass
    ( -- | @since 3.0.1
      forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
PStar f a b s -> Term s (PInner (PStar f a b))
forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PStar f a b))
-> (PStar f a b s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PStar f a b))
-> (PStar f a b s -> Term s b) -> Term s b
$cpmatch' :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PStar f a b))
-> (PStar f a b s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PStar f a b s -> Term s (PInner (PStar f a b))
$cpcon' :: forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
PStar f a b s -> Term s (PInner (PStar f a b))
PlutusType
    )

-- | @since 3.0.1
instance DerivePlutusType (PStar f a b) where
  type DPTStrat _ = PlutusTypeNewtype

{- | If @f@ is at least a 'PFunctor', we can pre-process and post-process work
 done in @PStar f@ using pure functions.

 @since 3.1.0
-}
instance (PFunctor f) => PProfunctor (PStar f) where
  type PContraSubcategory (PStar f) = Plut
  type PCoSubcategory (PStar f) = PSubcategory f
  pdimap :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type)
       (d :: S -> Type) (s :: S).
(PContraSubcategory (PStar f) a, PContraSubcategory (PStar f) b,
 PCoSubcategory (PStar f) c, PCoSubcategory (PStar f) d) =>
Term
  s
  ((a :--> b) :--> ((c :--> d) :--> (PStar f b c :--> PStar f a d)))
pdimap = 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)
into Term s (c :--> d)
outOf Term s (PStar f b c)
xs -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PStar Term s (b :--> f c)
g <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PStar f b c)
xs
      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 (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
Term s (a :--> f b) -> PStar f a b s
PStar forall a b. (a -> b) -> a -> b
$ forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (d :: S -> Type)
       (s :: S).
(PProfunctor p, PContraSubcategory p a, PContraSubcategory p b,
 PCoSubcategory p c, PCoSubcategory p d) =>
Term s ((a :--> b) :--> ((c :--> d) :--> (p b c :--> p a d)))
pdimap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
into 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) (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 (c :--> d)
outOf) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (b :--> f c)
g

{- | Strengthening @f@ to 'PBind' allows us to compose @PStar f@ computations
 like ordinary Plutarch functions.

 @since 3.0.1
-}
instance (PBind f) => PSemigroupoid (PStar f) where
  {-# INLINEABLE (#>>>) #-}
  Term s (PStar f a b)
t #>>> :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PContraSubcategory (PStar f) a, PContraSubcategory (PStar f) b,
 PCoSubcategory (PStar f) b, PCoSubcategory (PStar f) c) =>
Term s (PStar f a b)
-> Term s (PStar f b c) -> Term s (PStar f a c)
#>>> Term s (PStar f b c)
t' = forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PStar f a b)
t forall a b. (a -> b) -> a -> b
$ \case
    PStar Term s (a :--> f b)
ab -> 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 (PStar f b c)
t' forall a b. (a -> b) -> a -> b
$ \case
      PStar Term s (b :--> f c)
bc -> 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 (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
Term s (a :--> f b) -> PStar f a b s
PStar forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (a :--> f b)
ab 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)
       (b :: S -> Type) (s :: S).
(PBind f, PSubcategory f a, PSubcategory f b) =>
Term s (f a) -> Term s (a :--> f b) -> Term s (f b)
#>>= Term s (b :--> f c)
bc

{- | Strengthening @f@ by adding 'PApplicative' gives us an identity, which
 makes us a full category, on par with @Plut@ as evidenced by ':-->'.
,
 @since 3.0.1
-}
instance
  (PApplicative f, PBind f) =>
  PCategory (PStar f)
  where
  pidentity :: forall (a :: S -> Type) (s :: S).
(PContraSubcategory (PStar f) a, PCoSubcategory (PStar f) a) =>
Term s (PStar f a a)
pidentity = 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 (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
Term s (a :--> f b) -> PStar f a b s
PStar forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (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

{- | This essentially makes @PStar f a b@ equivalent to the Haskell @ReaderT a f
 b@: that is, a read-only environment of type @a@ producing a result of type
 @b@ in an effect @f@. If @f@ is /only/ a 'PFunctor', we can only lift, but
 not compose.

 @since 3.0.1
-}
instance (PFunctor f) => PFunctor (PStar f a) where
  type PSubcategory (PStar f a) = PSubcategory f
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory (PStar f a) a, PSubcategory (PStar f a) b) =>
Term s ((a :--> b) :--> (PStar f a a :--> PStar f a 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 (PStar f a a)
xs -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PStar Term s (a :--> f a)
g <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PStar f a a)
xs
      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 (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
Term s (a :--> f b) -> PStar f a b s
PStar forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (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 (a :--> f a)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x)

{- | Strengthening to 'PApply' for @f@ allows us to combine together
 computations in @PStar f a@ using the same \'view\' as in the 'PFunctor'
 instance.

 @since 3.0.1
-}
instance (PApply f) => PApply (PStar f a) where
  pliftA2 :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSubcategory (PStar f a) a, PSubcategory (PStar f a) b,
 PSubcategory (PStar f a) c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PStar f a a :--> (PStar f a b :--> PStar f 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 (PStar f a a)
xs Term s (PStar f 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
      PStar Term s (a :--> f a)
g <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PStar f a a)
xs
      PStar Term s (a :--> f b)
h <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PStar f 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 (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
Term s (a :--> f b) -> PStar f a b s
PStar forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (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
# 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 :--> f a)
g 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 (a :--> f b)
h forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x)

{- | Strengthening to 'PApplicative' for @f@ allows arbitrary lifts into @PStar
 f a@, using the same \'view\' as in the 'PFunctor' instance.

 @since 3.0.1
-}
instance (PApplicative f) => PApplicative (PStar f a) where
  ppure :: forall (a :: S -> Type) (s :: S).
PSubcategory (PStar f a) a =>
Term s (a :--> PStar f 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
$ \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 (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
Term s (a :--> f b) -> PStar f a b s
PStar forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
_ -> 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

{- | Strengthening to 'PBind' for @f@ allows dynamic control flow on the basis
 of the result of a @PStar f a@, using the same \'view\' as the 'PFunctor'
 instance.

 @since 3.0.1
-}
instance (PBind f) => PBind (PStar f a) where
  {-# INLINEABLE (#>>=) #-}
  Term s (PStar f a a)
xs #>>= :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory (PStar f a) a, PSubcategory (PStar f a) b) =>
Term s (PStar f a a)
-> Term s (a :--> PStar f a b) -> Term s (PStar f a b)
#>>= Term s (a :--> PStar f a b)
f = 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 (PStar f a a)
xs forall a b. (a -> b) -> a -> b
$ \case
    PStar Term s (a :--> f a)
g -> 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 (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
Term s (a :--> f b) -> PStar f a b s
PStar forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (a :--> f a)
g 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)
       (b :: S -> Type) (s :: S).
(PBind f, PSubcategory f a, PSubcategory f b) =>
Term s (f a) -> Term s (a :--> f b) -> Term s (f b)
#>>= (Term s (a :--> PStar f a b)
f forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSemigroupoid p, PContraSubcategory p a, PContraSubcategory p b,
 PCoSubcategory p b, PCoSubcategory p c) =>
Term s (p a b) -> Term s (p b c) -> Term s (p a c)
#>>> (forall (a :: S -> Type) (b :: S -> Type)
       (f :: (S -> Type) -> S -> Type) (s :: S).
Term s (a :--> (PStar f a b :--> f b))
papplyStar forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x))

{- | \'Run\' the 'PStar' as the function it secretly is. Useful for cases where
 you want to build up a large computation using 'PStar' instances, then
 execute.

 @since 3.0.1
-}
papplyStar ::
  forall (a :: S -> Type) (b :: S -> Type) (f :: (S -> Type) -> S -> Type) (s :: S).
  Term s (a :--> PStar f a b :--> f b)
papplyStar :: forall (a :: S -> Type) (b :: S -> Type)
       (f :: (S -> Type) -> S -> Type) (s :: S).
Term s (a :--> (PStar f a b :--> f b))
papplyStar = 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 (PStar f a b)
f -> 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 (PStar f a b)
f forall a b. (a -> b) -> a -> b
$ \case
    PStar Term s (a :--> f b)
f' -> Term s (a :--> f 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