{-# LANGUAGE UndecidableInstances #-}

module Plutarch.Pair (PPair (..)) where

import Data.Kind (Type)
import GHC.Generics (Generic)
import Generics.SOP qualified as SOP
import Plutarch.Internal.Eq (PEq)
import Plutarch.Internal.PlutusType (PlutusType, pcon, pmatch)
import Plutarch.Internal.Semigroup (
  PMonoid (pmempty),
  PSemigroup (pstimes, (#<>)),
 )
import Plutarch.Internal.Show (PShow)
import Plutarch.Internal.Term (S, Term)
import Plutarch.Repr.SOP (DeriveAsSOPStruct (DeriveAsSOPStruct))

{- |
  Plutus encoding of Pairs.

  Note: This is represented differently than 'BuiltinPair'. It is SoP encoded.
-}
data PPair (a :: S -> Type) (b :: S -> Type) (s :: S)
  = PPair (Term s a) (Term s b)
  deriving stock
    ( -- | @since 1.10.0
      (forall x. PPair a b s -> Rep (PPair a b s) x)
-> (forall x. Rep (PPair a b s) x -> PPair a b s)
-> Generic (PPair a b s)
forall x. Rep (PPair a b s) x -> PPair a b s
forall x. PPair a b s -> Rep (PPair a b s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (b :: S -> Type) (s :: S) x.
Rep (PPair a b s) x -> PPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S) x.
PPair a b s -> Rep (PPair a b s) x
$cfrom :: forall (a :: S -> Type) (b :: S -> Type) (s :: S) x.
PPair a b s -> Rep (PPair a b s) x
from :: forall x. PPair a b s -> Rep (PPair a b s) x
$cto :: forall (a :: S -> Type) (b :: S -> Type) (s :: S) x.
Rep (PPair a b s) x -> PPair a b s
to :: forall x. Rep (PPair a b s) x -> PPair a b s
Generic
    )
  deriving anyclass
    ( -- | @since 1.10.0
      All @[Type] (SListI @Type) (Code (PPair a b s))
All @[Type] (SListI @Type) (Code (PPair a b s)) =>
(PPair a b s -> Rep (PPair a b s))
-> (Rep (PPair a b s) -> PPair a b s) -> Generic (PPair a b s)
Rep (PPair a b s) -> PPair a b s
PPair a b s -> Rep (PPair a b s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
All @[Type] (SListI @Type) (Code (PPair a b s))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Rep (PPair a b s) -> PPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PPair a b s -> Rep (PPair a b s)
$cfrom :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PPair a b s -> Rep (PPair a b s)
from :: PPair a b s -> Rep (PPair a b s)
$cto :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Rep (PPair a b s) -> PPair a b s
to :: Rep (PPair a b s) -> PPair a b s
SOP.Generic
    , -- | @since 1.10.0
      (forall (s :: S).
 Term s (PPair a b) -> Term s (PPair a b) -> Term s PBool)
-> PEq (PPair a b)
forall (s :: S).
Term s (PPair a b) -> Term s (PPair a b) -> Term s PBool
forall (t :: S -> Type).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PEq a, PEq b) =>
Term s (PPair a b) -> Term s (PPair a b) -> Term s PBool
$c#== :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PEq a, PEq b) =>
Term s (PPair a b) -> Term s (PPair a b) -> Term s PBool
#== :: forall (s :: S).
Term s (PPair a b) -> Term s (PPair a b) -> Term s PBool
PEq
    , -- | @since 1.10.0
      (forall (s :: S). Bool -> Term s (PPair a b) -> Term s PString)
-> PShow (PPair a b)
forall (s :: S). Bool -> Term s (PPair a b) -> Term s PString
forall (t :: S -> Type).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PShow a, PShow b) =>
Bool -> Term s (PPair a b) -> Term s PString
$cpshow' :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PShow a, PShow b) =>
Bool -> Term s (PPair a b) -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s (PPair a b) -> Term s PString
PShow
    )

-- | @since 1.10.0
deriving via
  DeriveAsSOPStruct (PPair a b)
  instance
    PlutusType (PPair a b)

-- | @since 1.10.0
instance
  (PSemigroup a, PSemigroup b) =>
  PSemigroup (PPair a b)
  where
  {-# INLINEABLE (#<>) #-}
  Term s (PPair a b)
x #<> :: forall (s :: S).
Term s (PPair a b) -> Term s (PPair a b) -> Term s (PPair a b)
#<> Term s (PPair a b)
y = Term s (PPair a b)
-> (PPair a b s -> Term s (PPair a b)) -> Term s (PPair 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 (PPair a b)
x ((PPair a b s -> Term s (PPair a b)) -> Term s (PPair a b))
-> (PPair a b s -> Term s (PPair a b)) -> Term s (PPair a b)
forall a b. (a -> b) -> a -> b
$ \(PPair Term s a
x1 Term s b
x2) ->
    Term s (PPair a b)
-> (PPair a b s -> Term s (PPair a b)) -> Term s (PPair 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 (PPair a b)
y ((PPair a b s -> Term s (PPair a b)) -> Term s (PPair a b))
-> (PPair a b s -> Term s (PPair a b)) -> Term s (PPair a b)
forall a b. (a -> b) -> a -> b
$ \(PPair Term s a
y1 Term s b
y2) ->
      PPair a b s -> Term s (PPair a b)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a b s -> Term s (PPair a b))
-> (Term s b -> PPair a b s) -> Term s b -> Term s (PPair a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s b -> PPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair (Term s a
x1 Term s a -> Term s a -> Term s a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> Term s a
y1) (Term s b -> Term s (PPair a b)) -> Term s b -> Term s (PPair a b)
forall a b. (a -> b) -> a -> b
$ (Term s b
x2 Term s b -> Term s b -> Term s b
forall (s :: S). Term s b -> Term s b -> Term s b
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> Term s b
y2)
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive -> Term s (PPair a b) -> Term s (PPair a b)
pstimes Term s PPositive
p Term s (PPair a b)
x = Term s (PPair a b)
-> (PPair a b s -> Term s (PPair a b)) -> Term s (PPair 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 (PPair a b)
x ((PPair a b s -> Term s (PPair a b)) -> Term s (PPair a b))
-> (PPair a b s -> Term s (PPair a b)) -> Term s (PPair a b)
forall a b. (a -> b) -> a -> b
$ \(PPair Term s a
x1 Term s b
x2) ->
    PPair a b s -> Term s (PPair a b)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a b s -> Term s (PPair a b))
-> (Term s b -> PPair a b s) -> Term s b -> Term s (PPair a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s b -> PPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair (Term s PPositive -> Term s a -> Term s a
forall (s :: S). Term s PPositive -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s PPositive -> Term s a -> Term s a
pstimes Term s PPositive
p Term s a
x1) (Term s b -> Term s (PPair a b)) -> Term s b -> Term s (PPair a b)
forall a b. (a -> b) -> a -> b
$ Term s PPositive -> Term s b -> Term s b
forall (s :: S). Term s PPositive -> Term s b -> Term s b
forall (a :: S -> Type) (s :: S).
PSemigroup a =>
Term s PPositive -> Term s a -> Term s a
pstimes Term s PPositive
p Term s b
x2

-- | @since 1.10.0
instance
  (PMonoid a, PMonoid b) =>
  PMonoid (PPair a b)
  where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s (PPair a b)
pmempty = PPair a b s -> Term s (PPair a b)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a b s -> Term s (PPair a b))
-> (Term s b -> PPair a b s) -> Term s b -> Term s (PPair a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s b -> PPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PMonoid a => Term s a
pmempty (Term s b -> Term s (PPair a b)) -> Term s b -> Term s (PPair a b)
forall a b. (a -> b) -> a -> b
$ Term s b
forall (s :: S). Term s b
forall (a :: S -> Type) (s :: S). PMonoid a => Term s a
pmempty