module Plutarch.Extra.Comonad (
  PExtend (..),
  PComonad (..),
) where

import Plutarch.Extra.Functor (PFunctor (PSubcategory))
import Plutarch.Extra.TermCont (pletC, pmatchC)
import Plutarch.List (puncons)

-- | @since 1.0.0
class (PFunctor w) => PExtend (w :: (S -> Type) -> S -> Type) where
  pextend ::
    forall (a :: S -> Type) (b :: S -> Type) (s :: S).
    (PSubcategory w a, PSubcategory w b) =>
    Term s ((w a :--> b) :--> w a :--> w b)

{- | Applies the given function over every proper suffix of a 'PList', from
 longest to shortest, and returns their results in a 'PList'.

 @since 1.0.0
-}
instance PExtend PList where
  pextend ::
    forall (a :: S -> Type) (b :: S -> Type) (s :: S).
    Term s ((PList a :--> b) :--> PList a :--> PList b)
  pextend :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s ((PList a :--> b) :--> (PList a :--> PList b))
pextend = 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 :--> b)
f Term s (PList 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
      PMaybe (PPair a (PList a)) s
t <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
puncons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
xs)
      case PMaybe (PPair a (PList a)) s
t of
        PMaybe (PPair a (PList a)) s
PNothing -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
        PJust Term s (PPair a (PList a))
t' -> do
          PPair Term s a
_ Term s (PList a)
ttail <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PPair a (PList a))
t'
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (s' :: S).
Term s' ((PList a :--> b) :--> (PList a :--> PList b))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList 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)
ttail
    where
      go ::
        forall (s' :: S).
        Term s' ((PList a :--> b) :--> PList a :--> PList b)
      go :: forall (s' :: S).
Term s' ((PList a :--> b) :--> (PList a :--> PList b))
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 (PList a :--> b)
f Term s (PList 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
          Term s b
res <- forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s (PList 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)
xs)
          PMaybe (PPair a (PList a)) s
t <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
puncons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
xs)
          case PMaybe (PPair a (PList a)) s
t of
            PMaybe (PPair a (PList a)) s
PNothing -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> 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 b
res 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
            PJust Term s (PPair a (PList a))
t' -> do
              PPair Term s a
_ Term s (PList a)
ttail <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PPair a (PList a))
t'
              forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> 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 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' ((PList a :--> b) :--> (PList a :--> PList b))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList 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)
ttail)

-- | @since 1.0.0
instance PExtend (PPair a) where
  pextend :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory (PPair a) a, PSubcategory (PPair a) b) =>
Term s ((PPair a a :--> b) :--> (PPair a a :--> PPair a b))
pextend = 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 (PPair a a :--> b)
f Term s (PPair a a)
p -> 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 a
_ <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PPair a a)
p
      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
x forall a b. (a -> b) -> a -> b
$ Term s (PPair a 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 (PPair a a)
p

-- | @since 1.0.0
class (PExtend w) => PComonad (w :: (S -> Type) -> S -> Type) where
  pextract ::
    forall (a :: S -> Type) (s :: S).
    (PSubcategory w a) =>
    Term s (w a :--> a)

-- | @since 1.0.0
instance PComonad (PPair a) where
  pextract :: forall (a :: S -> Type) (s :: S).
PSubcategory (PPair a) a =>
Term s (PPair a a :--> a)
pextract = 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 (PPair a a)
p -> 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
_ Term s a
t <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PPair a a)
p
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Term s a
t