{-# LANGUAGE QuantifiedConstraints #-}

module Plutarch.Extra.Sum (
  PSum (..),
) where

import Plutarch.Extra.Applicative (PApplicative (ppure), PApply (pliftA2))
import Plutarch.Extra.Boring (PBoring (pboring))
import Plutarch.Extra.Comonad (PComonad (pextract), PExtend (pextend))
import Plutarch.Extra.Functor (PFunctor (PSubcategory, pfmap), Plut)
import Plutarch.Extra.TermCont (pmatchC)
import Plutarch.Num (PNum)

{- | A \'numerical\' value which is monoidal over its addition.

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

-- | @since 1.4.0
instance DerivePlutusType (PSum a) where
  type DPTStrat _ = PlutusTypeNewtype

-- | @since 1.0.0
deriving anyclass instance (PIsData a) => (PIsData (PSum a))

-- | @since 1.0.0
deriving anyclass instance (PEq a) => PEq (PSum a)

-- | @since 1.4.0
deriving anyclass instance (POrd a) => PPartialOrd (PSum a)

-- | @since 1.0.0
deriving anyclass instance (POrd a) => POrd (PSum a)

-- | @since 1.0.0
deriving anyclass instance (PIntegral a) => PIntegral (PSum a)

-- | @since 1.0.0
deriving anyclass instance (PNum a) => PNum (PSum a)

-- | @since 1.0.0
instance
  (forall (s' :: S). Num (Term s' a)) =>
  Semigroup (Term s (PSum a))
  where
  Term s (PSum a)
t <> :: Term s (PSum a) -> Term s (PSum a) -> Term s (PSum a)
<> Term s (PSum a)
t' = forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PSum Term s a
x <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PSum a)
t
    PSum Term s a
y <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PSum 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 :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). Term s a -> PSum a s
PSum forall a b. (a -> b) -> a -> b
$ Term s a
x forall a. Num a => a -> a -> a
+ Term s a
y

-- | @since 1.0.0
instance
  (forall (s' :: S). Num (Term s' a)) =>
  Monoid (Term s (PSum a))
  where
  mempty :: Term s (PSum a)
mempty = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). Term s a -> PSum a s
PSum forall a b. (a -> b) -> a -> b
$ Term s a
0

-- | @since 1.0.0
deriving anyclass instance (PShow a) => PShow (PSum a)

-- | @since 3.1.0
instance PFunctor PSum where
  type PSubcategory PSum = Plut
  pfmap :: forall (a :: PType) (b :: PType) (s :: S).
(PSubcategory PSum a, PSubcategory PSum b) =>
Term s ((a :--> b) :--> (PSum a :--> PSum b))
pfmap = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
f Term s (PSum a)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PSum Term s a
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PSum 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 :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). Term s a -> PSum a s
PSum forall a b. (a -> b) -> a -> b
$ Term s (a :--> b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
t'

-- | @since 1.0.0
instance PExtend PSum where
  pextend :: forall (a :: PType) (b :: PType) (s :: S).
(PSubcategory PSum a, PSubcategory PSum b) =>
Term s ((PSum a :--> b) :--> (PSum a :--> PSum b))
pextend = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PSum a :--> b)
f Term s (PSum a)
t -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). Term s a -> PSum a s
PSum forall a b. (a -> b) -> a -> b
$ Term s (PSum a :--> b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PSum a)
t

-- | @since 1.0.0
instance PComonad PSum where
  pextract :: forall (a :: PType) (s :: S).
PSubcategory PSum a =>
Term s (PSum a :--> a)
pextract = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PSum a)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PSum Term s a
t' <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PSum a)
t
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Term s a
t'

-- | @since 1.0.0
instance PApply PSum where
  pliftA2 :: forall (a :: PType) (b :: PType) (c :: PType) (s :: S).
(PSubcategory PSum a, PSubcategory PSum b, PSubcategory PSum c) =>
Term
  s ((a :--> (b :--> c)) :--> (PSum a :--> (PSum b :--> PSum c)))
pliftA2 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
f Term s (PSum a)
xs Term s (PSum b)
ys -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PSum Term s a
tx <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PSum a)
xs
      PSum Term s b
ty <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PSum b)
ys
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). Term s a -> PSum a s
PSum forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tx forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
ty

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

-- | @since 1.2.0
instance (PBoring a) => PBoring (PSum a) where
  pboring :: forall (s :: S). Term s (PSum a)
pboring = forall (f :: PType -> PType) (a :: PType) (s :: S).
(PApplicative f, PSubcategory f a) =>
Term s (a :--> f a)
ppure forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S). PBoring a => Term s a
pboring