{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Plutarch.Internal.Semigroup (
  -- * Type classes
  PSemigroup (..),
  PMonoid (..),

  -- * Helper newtypes
  PAnd (..),
  POr (..),
  PXor (..),
) where

import Data.ByteString qualified as BS
import Data.Kind (Type)
import Data.Text qualified as Text
import GHC.Generics (Generic)
import Generics.SOP qualified as SOP
import Plutarch.Builtin.BLS (
  PBuiltinBLS12_381_G1_Element,
  PBuiltinBLS12_381_G2_Element,
  PBuiltinBLS12_381_MlResult,
 )
import Plutarch.Builtin.Bool (
  PBool (PFalse, PTrue),
  pif,
  pif',
  pnot,
 )
import Plutarch.Builtin.ByteString (
  PByteString,
  pandBS,
  pindexBS,
  plengthBS,
  porBS,
  ppadding,
  preplicateBS,
  pxorBS,
 )
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Builtin.String (PString)
import Plutarch.Builtin.Unit (PUnit, punit)
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Lift (
  DeriveNewtypePLiftable,
  PLiftable (AsHaskell),
  PLifted (PLifted),
  PlutusRepr,
 )
import Plutarch.Internal.Numeric (
  PNatural,
  PPositive,
  pbySquaringDefault,
  pdiv,
  pnaturalToPositiveCPS,
  pscaleNatural,
  pscalePositive,
  pzero,
  (#*),
  (#+),
 )
import Plutarch.Internal.Ord (POrd)
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PlutusType (PlutusType (PInner), pcon)
import Plutarch.Internal.Term (
  S,
  Term,
  plet,
  punsafeBuiltin,
  punsafeConstantInternal,
  (#),
  (#$),
 )
import Plutarch.Repr.Newtype (DeriveNewtypePlutusType (DeriveNewtypePlutusType))
import Plutarch.Unsafe (punsafeDowncast)
import PlutusCore qualified as PLC
import Universe (Includes)

{- | = Laws

The only mandatory law is that '#<>' must be associative:

@x #<> (y #<> z)@ @=@ @(x #<> y) #<> z@

If you define 'pstimes', ensure the following also hold:

1. @pstimes pone x@ @=@ @x@
2. @(pstimes p1 x) #<> (pstimes p2 x)@ @=@ @pstimes (p1 #+ p2) x@
3. @pstimes p1 (pstimes p2 x)@ @=@ @pstimes (p1 #* p2) x@

The default implementation automatically ensures these laws hold.

@since 1.10.0
-}
class PSemigroup (a :: S -> Type) where
  (#<>) :: forall (s :: S). Term s a -> Term s a -> Term s a
  default (#<>) ::
    forall (s :: S).
    PSemigroup (PInner a) =>
    Term s a ->
    Term s a ->
    Term s a
  Term s a
x #<> Term s a
y = Term s (PInner a) -> Term s a
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner a) -> Term s a) -> Term s (PInner a) -> Term s a
forall a b. (a -> b) -> a -> b
$ Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s a
x Term s (PInner a) -> Term s (PInner a) -> Term s (PInner a)
forall (s :: S).
Term s (PInner a) -> Term s (PInner a) -> Term s (PInner a)
forall (a :: PType) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
#<> Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s a
y
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S). Term s PPositive -> Term s a -> Term s a
  pstimes Term s PPositive
p Term s a
x = (forall (s :: S). Term s a -> Term s a -> Term s a)
-> Term s a -> Term s PPositive -> Term s a
forall (a :: PType) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s a -> Term s PPositive -> Term s a
pbySquaringDefault Term s' a -> Term s' a -> Term s' a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: PType) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
(#<>) Term s a
x Term s PPositive
p

infixr 6 #<>

-- | @since 1.10.0
instance PSemigroup PUnit where
  {-# INLINEABLE (#<>) #-}
  Term s PUnit
x #<> :: forall (s :: S). Term s PUnit -> Term s PUnit -> Term s PUnit
#<> Term s PUnit
y = Term s PUnit -> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
x ((Term s PUnit -> Term s PUnit) -> Term s PUnit)
-> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall a b. (a -> b) -> a -> b
$ \Term s PUnit
_ -> Term s PUnit -> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
y ((Term s PUnit -> Term s PUnit) -> Term s PUnit)
-> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall a b. (a -> b) -> a -> b
$ Term s PUnit -> Term s PUnit -> Term s PUnit
forall a b. a -> b -> a
const Term s PUnit
forall (s :: S). Term s PUnit
punit
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S). Term s PPositive -> Term s PUnit -> Term s PUnit
pstimes Term s PPositive
p Term s PUnit
x = Term s PPositive
-> (Term s PPositive -> Term s PUnit) -> Term s PUnit
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
p ((Term s PPositive -> Term s PUnit) -> Term s PUnit)
-> (Term s PPositive -> Term s PUnit) -> Term s PUnit
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
_ -> Term s PUnit -> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
x ((Term s PUnit -> Term s PUnit) -> Term s PUnit)
-> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall a b. (a -> b) -> a -> b
$ Term s PUnit -> Term s PUnit -> Term s PUnit
forall a b. a -> b -> a
const Term s PUnit
forall (s :: S). Term s PUnit
punit

-- | @since 1.10.0
instance PSemigroup PString where
  {-# INLINEABLE (#<>) #-}
  Term s PString
x #<> :: forall (s :: S). Term s PString -> Term s PString -> Term s PString
#<> Term s PString
y = DefaultFun -> Term s (PString :--> (PString :--> PString))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.AppendString Term s (PString :--> (PString :--> PString))
-> Term s PString -> Term s (PString :--> PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PString
x Term s (PString :--> PString) -> Term s PString -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PString
y

-- | @since 1.10.0
instance PSemigroup PByteString where
  {-# INLINEABLE (#<>) #-}
  Term s PByteString
x #<> :: forall (s :: S).
Term s PByteString -> Term s PByteString -> Term s PByteString
#<> Term s PByteString
y = DefaultFun
-> Term s (PByteString :--> (PByteString :--> PByteString))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.AppendByteString Term s (PByteString :--> (PByteString :--> PByteString))
-> Term s PByteString -> Term s (PByteString :--> PByteString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
x Term s (PByteString :--> PByteString)
-> Term s PByteString -> Term s PByteString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
y
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive -> Term s PByteString -> Term s PByteString
pstimes Term s PPositive
p Term s PByteString
bs = Term s PByteString
-> (Term s PByteString -> Term s PByteString) -> Term s PByteString
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PByteString
bs ((Term s PByteString -> Term s PByteString) -> Term s PByteString)
-> (Term s PByteString -> Term s PByteString) -> Term s PByteString
forall a b. (a -> b) -> a -> b
$ \Term s PByteString
bs' ->
    Term s PBool
-> Term s PByteString -> Term s PByteString -> Term s PByteString
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s (PByteString :--> PInteger)
forall (s :: S). Term s (PByteString :--> PInteger)
plengthBS Term s (PByteString :--> PInteger)
-> Term s PByteString -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
bs' Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
1)
      (Term s (PInteger :--> (PByte :--> PByteString))
forall (s :: S). Term s (PInteger :--> (PByte :--> PByteString))
preplicateBS Term s (PInteger :--> (PByte :--> PByteString))
-> Term s PInteger -> Term s (PByte :--> PByteString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
p Term s (PByte :--> PByteString)
-> Term s PByte -> Term s PByteString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PByteString :--> (PInteger :--> PByte))
forall (s :: S). Term s (PByteString :--> (PInteger :--> PByte))
pindexBS Term s (PByteString :--> (PInteger :--> PByte))
-> Term s PByteString -> Term s (PInteger :--> PByte)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
bs' Term s (PInteger :--> PByte) -> Term s PInteger -> Term s PByte
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
0)
      ((forall (s :: S).
 Term s PByteString -> Term s PByteString -> Term s PByteString)
-> Term s PByteString -> Term s PPositive -> Term s PByteString
forall (a :: PType) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s a -> Term s PPositive -> Term s a
pbySquaringDefault Term s' PByteString -> Term s' PByteString -> Term s' PByteString
forall (s :: S).
Term s PByteString -> Term s PByteString -> Term s PByteString
forall (a :: PType) (s :: S).
PSemigroup a =>
Term s a -> Term s a -> Term s a
(#<>) Term s PByteString
bs' Term s PPositive
p)

{- | BLS points form a group technically, but a @PGroup@ notion would be too
niche to be useful. Unlike other types which could be semigroups (or monoids)
in many ways, BLS points have only one (essentially their additive
instances), so we can provide these.

@since 1.10.0
-}
instance PSemigroup PBuiltinBLS12_381_G1_Element where
  {-# INLINEABLE (#<>) #-}
  #<> :: forall (s :: S).
Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
(#<>) = Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S).
Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
forall (a :: PType) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+)
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
pstimes Term s PPositive
p Term s PBuiltinBLS12_381_G1_Element
x = Term s PBuiltinBLS12_381_G1_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S).
Term s PBuiltinBLS12_381_G1_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G1_Element
forall (a :: PType) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s PBuiltinBLS12_381_G1_Element
x Term s PPositive
p

-- | @since 1.10.0
instance PSemigroup PBuiltinBLS12_381_G2_Element where
  {-# INLINEABLE (#<>) #-}
  #<> :: forall (s :: S).
Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
(#<>) = Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S).
Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
forall (a :: PType) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+)
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
pstimes Term s PPositive
p Term s PBuiltinBLS12_381_G2_Element
x = Term s PBuiltinBLS12_381_G2_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S).
Term s PBuiltinBLS12_381_G2_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G2_Element
forall (a :: PType) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s PBuiltinBLS12_381_G2_Element
x Term s PPositive
p

{- | Since multiplication of Miller loop results exists, they are technically
semigroups, though confusingly in a /different/ way to BLS curve points.

@since 1.10.0
-}
instance PSemigroup PBuiltinBLS12_381_MlResult where
  {-# INLINEABLE (#<>) #-}
  #<> :: forall (s :: S).
Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
(#<>) = Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
forall (s :: S).
Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
(#*)

{- | = Laws

1. @pmempty #<> x@ @=@ @x #<> pmempty@ @=@ @x@
2. @pstimes n pmempty@ @=@ @pmempty@

If you define 'pmtimes', ensure the following as well:

3. @pmtimes (ppositiveToNatural # p) x@ @=@
   @pstimes p x@
4. @pmtimes pzero x@ @=@ @pmempty@

The default implementation of 'pmtimes' ensures these laws hold.

@since 1.10.0
-}
class PSemigroup a => PMonoid (a :: S -> Type) where
  pmempty :: forall (s :: S). Term s a
  default pmempty ::
    forall (s :: S).
    PMonoid (PInner a) =>
    Term s a
  pmempty = Term s (PInner a) -> Term s a
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast Term s (PInner a)
forall (s :: S). Term s (PInner a)
forall (a :: PType) (s :: S). PMonoid a => Term s a
pmempty
  {-# INLINEABLE pmtimes #-}
  pmtimes :: forall (s :: S). Term s PNatural -> Term s a -> Term s a
  pmtimes Term s PNatural
n Term s a
x = Term s a
-> (Term s PPositive -> Term s a) -> Term s PNatural -> Term s a
forall (a :: PType) (s :: S).
Term s a
-> (Term s PPositive -> Term s a) -> Term s PNatural -> Term s a
pnaturalToPositiveCPS Term s a
forall (s :: S). Term s a
forall (a :: PType) (s :: S). PMonoid a => Term s a
pmempty (Term s PPositive -> Term s a -> Term s a
forall (s :: S). Term s PPositive -> Term s a -> Term s a
forall (a :: PType) (s :: S).
PSemigroup a =>
Term s PPositive -> Term s a -> Term s a
`pstimes` Term s a
x) Term s PNatural
n

-- | @since 1.10.0
instance PMonoid PUnit where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s PUnit
pmempty = Term s PUnit
forall (s :: S). Term s PUnit
punit
  {-# INLINEABLE pmtimes #-}
  pmtimes :: forall (s :: S). Term s PNatural -> Term s PUnit -> Term s PUnit
pmtimes Term s PNatural
n Term s PUnit
x = Term s PNatural
-> (Term s PNatural -> Term s PUnit) -> Term s PUnit
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PNatural
n ((Term s PNatural -> Term s PUnit) -> Term s PUnit)
-> (Term s PNatural -> Term s PUnit) -> Term s PUnit
forall a b. (a -> b) -> a -> b
$ \Term s PNatural
_ -> Term s PUnit -> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
x ((Term s PUnit -> Term s PUnit) -> Term s PUnit)
-> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall a b. (a -> b) -> a -> b
$ Term s PUnit -> Term s PUnit -> Term s PUnit
forall a b. a -> b -> a
const Term s PUnit
forall (s :: S). Term s PUnit
punit

-- | @since 1.10.0
instance PMonoid PString where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s PString
pmempty = Some @Type (ValueOf DefaultUni) -> Term s PString
forall (s :: S) (a :: PType).
Some @Type (ValueOf DefaultUni) -> Term s a
punsafeConstantInternal (Some @Type (ValueOf DefaultUni) -> Term s PString)
-> Some @Type (ValueOf DefaultUni) -> Term s PString
forall a b. (a -> b) -> a -> b
$ Text -> Some @Type (ValueOf DefaultUni)
forall a (uni :: Type -> Type).
Contains @Type uni a =>
a -> Some @Type (ValueOf uni)
PLC.someValue Text
Text.empty

-- | @since 1.10.0
instance PMonoid PByteString where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s PByteString
pmempty = Some @Type (ValueOf DefaultUni) -> Term s PByteString
forall (s :: S) (a :: PType).
Some @Type (ValueOf DefaultUni) -> Term s a
punsafeConstantInternal (Some @Type (ValueOf DefaultUni) -> Term s PByteString)
-> Some @Type (ValueOf DefaultUni) -> Term s PByteString
forall a b. (a -> b) -> a -> b
$ ByteString -> Some @Type (ValueOf DefaultUni)
forall a (uni :: Type -> Type).
Contains @Type uni a =>
a -> Some @Type (ValueOf uni)
PLC.someValue ByteString
BS.empty

-- | @since 1.10.0
instance PMonoid PBuiltinBLS12_381_G1_Element where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s PBuiltinBLS12_381_G1_Element
pmempty = Term s PBuiltinBLS12_381_G1_Element
forall (s :: S). Term s PBuiltinBLS12_381_G1_Element
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero
  {-# INLINEABLE pmtimes #-}
  pmtimes :: forall (s :: S).
Term s PNatural
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
pmtimes Term s PNatural
n Term s PBuiltinBLS12_381_G1_Element
x = Term s PBuiltinBLS12_381_G1_Element
-> Term s PNatural -> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S).
Term s PBuiltinBLS12_381_G1_Element
-> Term s PNatural -> Term s PBuiltinBLS12_381_G1_Element
forall (a :: PType) (s :: S).
PAdditiveMonoid a =>
Term s a -> Term s PNatural -> Term s a
pscaleNatural Term s PBuiltinBLS12_381_G1_Element
x Term s PNatural
n

-- | @since 1.10.0
instance PMonoid PBuiltinBLS12_381_G2_Element where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s PBuiltinBLS12_381_G2_Element
pmempty = Term s PBuiltinBLS12_381_G2_Element
forall (s :: S). Term s PBuiltinBLS12_381_G2_Element
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero
  {-# INLINEABLE pmtimes #-}
  pmtimes :: forall (s :: S).
Term s PNatural
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
pmtimes Term s PNatural
n Term s PBuiltinBLS12_381_G2_Element
x = Term s PBuiltinBLS12_381_G2_Element
-> Term s PNatural -> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S).
Term s PBuiltinBLS12_381_G2_Element
-> Term s PNatural -> Term s PBuiltinBLS12_381_G2_Element
forall (a :: PType) (s :: S).
PAdditiveMonoid a =>
Term s a -> Term s PNatural -> Term s a
pscaleNatural Term s PBuiltinBLS12_381_G2_Element
x Term s PNatural
n

{- | Wrapper for types which have logical AND semantics somehow.

@since 1.10.0
-}
newtype PAnd (a :: S -> Type) (s :: S)
  = PAnd (Term s a)
  deriving stock
    ( -- | @since 1.10.0
      (forall x. PAnd a s -> Rep (PAnd a s) x)
-> (forall x. Rep (PAnd a s) x -> PAnd a s) -> Generic (PAnd a s)
forall x. Rep (PAnd a s) x -> PAnd a s
forall x. PAnd a s -> Rep (PAnd a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (s :: S) x. Rep (PAnd a s) x -> PAnd a s
forall (a :: PType) (s :: S) x. PAnd a s -> Rep (PAnd a s) x
$cfrom :: forall (a :: PType) (s :: S) x. PAnd a s -> Rep (PAnd a s) x
from :: forall x. PAnd a s -> Rep (PAnd a s) x
$cto :: forall (a :: PType) (s :: S) x. Rep (PAnd a s) x -> PAnd a s
to :: forall x. Rep (PAnd a s) x -> PAnd a s
Generic
    )
  deriving anyclass
    ( -- | @since 1.10.0
      All @[Type] (SListI @Type) (Code (PAnd a s))
All @[Type] (SListI @Type) (Code (PAnd a s)) =>
(PAnd a s -> Rep (PAnd a s))
-> (Rep (PAnd a s) -> PAnd a s) -> Generic (PAnd a s)
Rep (PAnd a s) -> PAnd a s
PAnd a s -> Rep (PAnd a s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: PType) (s :: S).
All @[Type] (SListI @Type) (Code (PAnd a s))
forall (a :: PType) (s :: S). Rep (PAnd a s) -> PAnd a s
forall (a :: PType) (s :: S). PAnd a s -> Rep (PAnd a s)
$cfrom :: forall (a :: PType) (s :: S). PAnd a s -> Rep (PAnd a s)
from :: PAnd a s -> Rep (PAnd a s)
$cto :: forall (a :: PType) (s :: S). Rep (PAnd a s) -> PAnd a s
to :: Rep (PAnd a s) -> PAnd a s
SOP.Generic
    , -- | @since 1.10.0
      (forall (s :: S).
 Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool)
-> PEq (PAnd a)
forall (s :: S). Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
forall (a :: PType) (s :: S).
PEq a =>
Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
$c#== :: forall (a :: PType) (s :: S).
PEq a =>
Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
#== :: forall (s :: S). Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
PEq
    , -- | @since 1.10.0
      PEq (PAnd a)
PEq (PAnd a) =>
(forall (s :: S).
 Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool)
-> (forall (s :: S).
    Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool)
-> (forall (s :: S).
    Term s (PAnd a) -> Term s (PAnd a) -> Term s (PAnd a))
-> (forall (s :: S).
    Term s (PAnd a) -> Term s (PAnd a) -> Term s (PAnd a))
-> POrd (PAnd a)
forall (s :: S). Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
forall (s :: S).
Term s (PAnd a) -> Term s (PAnd a) -> Term s (PAnd a)
forall (t :: PType).
PEq t =>
(forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> POrd t
forall (a :: PType). POrd a => PEq (PAnd a)
forall (a :: PType) (s :: S).
POrd a =>
Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
forall (a :: PType) (s :: S).
POrd a =>
Term s (PAnd a) -> Term s (PAnd a) -> Term s (PAnd a)
$c#<= :: forall (a :: PType) (s :: S).
POrd a =>
Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
#<= :: forall (s :: S). Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
$c#< :: forall (a :: PType) (s :: S).
POrd a =>
Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
#< :: forall (s :: S). Term s (PAnd a) -> Term s (PAnd a) -> Term s PBool
$cpmax :: forall (a :: PType) (s :: S).
POrd a =>
Term s (PAnd a) -> Term s (PAnd a) -> Term s (PAnd a)
pmax :: forall (s :: S).
Term s (PAnd a) -> Term s (PAnd a) -> Term s (PAnd a)
$cpmin :: forall (a :: PType) (s :: S).
POrd a =>
Term s (PAnd a) -> Term s (PAnd a) -> Term s (PAnd a)
pmin :: forall (s :: S).
Term s (PAnd a) -> Term s (PAnd a) -> Term s (PAnd a)
POrd
    )
  deriving
    ( -- | @since 1.10.0
      (forall (s :: S). PAnd a s -> Term s (PInner (PAnd a)))
-> (forall (s :: S) (b :: PType).
    Term s (PInner (PAnd a)) -> (PAnd a s -> Term s b) -> Term s b)
-> PlutusType (PAnd a)
forall (s :: S). PAnd a s -> Term s (PInner (PAnd a))
forall (s :: S) (b :: PType).
Term s (PInner (PAnd a)) -> (PAnd a s -> Term s b) -> Term s b
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). PAnd a s -> Term s (PInner (PAnd a))
forall (a :: PType) (s :: S) (b :: PType).
Term s (PInner (PAnd a)) -> (PAnd a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: PType) (s :: S). PAnd a s -> Term s (PInner (PAnd a))
pcon' :: forall (s :: S). PAnd a s -> Term s (PInner (PAnd a))
$cpmatch' :: forall (a :: PType) (s :: S) (b :: PType).
Term s (PInner (PAnd a)) -> (PAnd a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PAnd a)) -> (PAnd a s -> Term s b) -> Term s b
PlutusType
    )
    via (DeriveNewtypePlutusType (PAnd a))

-- | @since 1.10.0
deriving via
  DeriveNewtypePLiftable (PAnd a) (AsHaskell a)
  instance
    (PLiftable a, PLC.DefaultUni `Includes` PlutusRepr a) => PLiftable (PAnd a)

-- | @since 1.10.0
instance PSemigroup (PAnd PBool) where
  {-# INLINEABLE (#<>) #-}
  Term s (PAnd PBool)
x #<> :: forall (s :: S).
Term s (PAnd PBool) -> Term s (PAnd PBool) -> Term s (PAnd PBool)
#<> Term s (PAnd PBool)
y = Term s (PBool :--> (PAnd PBool :--> (PAnd PBool :--> PAnd PBool)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (PAnd PBool :--> (PAnd PBool :--> PAnd PBool)))
-> Term s PBool
-> Term s (PAnd PBool :--> (PAnd PBool :--> PAnd PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAnd PBool) -> Term s (PInner (PAnd PBool))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PAnd PBool)
x Term s (PAnd PBool :--> (PAnd PBool :--> PAnd PBool))
-> Term s (PAnd PBool) -> Term s (PAnd PBool :--> PAnd PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAnd PBool)
y Term s (PAnd PBool :--> PAnd PBool)
-> Term s (PAnd PBool) -> Term s (PAnd PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAnd PBool)
x

  -- \| 'PBool' is idempotent under AND.
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive -> Term s (PAnd PBool) -> Term s (PAnd PBool)
pstimes Term s PPositive
p Term s (PAnd PBool)
x = Term s PPositive
-> (Term s PPositive -> Term s (PAnd PBool)) -> Term s (PAnd PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
p ((Term s PPositive -> Term s (PAnd PBool)) -> Term s (PAnd PBool))
-> (Term s PPositive -> Term s (PAnd PBool)) -> Term s (PAnd PBool)
forall a b. (a -> b) -> a -> b
$ Term s (PAnd PBool) -> Term s PPositive -> Term s (PAnd PBool)
forall a b. a -> b -> a
const Term s (PAnd PBool)
x

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

{- | This uses padding semantics as specified in CIP-122, as this allows a
'PMonoid' instance as well.

@since 1.10.0
-}
instance PSemigroup (PAnd PByteString) where
  {-# INLINEABLE (#<>) #-}
  Term s (PAnd PByteString)
x #<> :: forall (s :: S).
Term s (PAnd PByteString)
-> Term s (PAnd PByteString) -> Term s (PAnd PByteString)
#<> Term s (PAnd PByteString)
y = Term s (PInner (PAnd PByteString)) -> Term s (PAnd PByteString)
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner (PAnd PByteString)) -> Term s (PAnd PByteString))
-> Term s (PInner (PAnd PByteString)) -> Term s (PAnd PByteString)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
forall (s :: S).
Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
pandBS Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
-> Term s PLogicOpSemantics
-> Term s (PByteString :--> (PByteString :--> PByteString))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PLogicOpSemantics
forall (s :: S). Term s PLogicOpSemantics
ppadding Term s (PByteString :--> (PByteString :--> PByteString))
-> Term s PByteString -> Term s (PByteString :--> PByteString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAnd PByteString) -> Term s (PInner (PAnd PByteString))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PAnd PByteString)
x Term s (PByteString :--> PByteString)
-> Term s PByteString -> Term s PByteString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAnd PByteString) -> Term s (PInner (PAnd PByteString))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PAnd PByteString)
y

  -- \| 'PByteString' is idempotent under AND regardless of semantics.
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive
-> Term s (PAnd PByteString) -> Term s (PAnd PByteString)
pstimes Term s PPositive
p Term s (PAnd PByteString)
x = Term s PPositive
-> (Term s PPositive -> Term s (PAnd PByteString))
-> Term s (PAnd PByteString)
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
p ((Term s PPositive -> Term s (PAnd PByteString))
 -> Term s (PAnd PByteString))
-> (Term s PPositive -> Term s (PAnd PByteString))
-> Term s (PAnd PByteString)
forall a b. (a -> b) -> a -> b
$ Term s (PAnd PByteString)
-> Term s PPositive -> Term s (PAnd PByteString)
forall a b. a -> b -> a
const Term s (PAnd PByteString)
x

-- | @since 1.10.0
instance PMonoid (PAnd PByteString) where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s (PAnd PByteString)
pmempty = PAnd PByteString s -> Term s (PAnd PByteString)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PAnd PByteString s -> Term s (PAnd PByteString))
-> (Term s PByteString -> PAnd PByteString s)
-> Term s PByteString
-> Term s (PAnd PByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PByteString -> PAnd PByteString s
forall (a :: PType) (s :: S). Term s a -> PAnd a s
PAnd (Term s PByteString -> Term s (PAnd PByteString))
-> Term s PByteString -> Term s (PAnd PByteString)
forall a b. (a -> b) -> a -> b
$ Term s PByteString
forall a. Monoid a => a
mempty

{- | Wrapper for types which have logical OR semantics somehow.

@since 1.10.0
-}
newtype POr (a :: S -> Type) (s :: S)
  = POr (Term s a)
  deriving stock
    ( -- | @since 1.10.0
      (forall x. POr a s -> Rep (POr a s) x)
-> (forall x. Rep (POr a s) x -> POr a s) -> Generic (POr a s)
forall x. Rep (POr a s) x -> POr a s
forall x. POr a s -> Rep (POr a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (s :: S) x. Rep (POr a s) x -> POr a s
forall (a :: PType) (s :: S) x. POr a s -> Rep (POr a s) x
$cfrom :: forall (a :: PType) (s :: S) x. POr a s -> Rep (POr a s) x
from :: forall x. POr a s -> Rep (POr a s) x
$cto :: forall (a :: PType) (s :: S) x. Rep (POr a s) x -> POr a s
to :: forall x. Rep (POr a s) x -> POr a s
Generic
    )
  deriving anyclass
    ( -- | @since 1.10.0
      All @[Type] (SListI @Type) (Code (POr a s))
All @[Type] (SListI @Type) (Code (POr a s)) =>
(POr a s -> Rep (POr a s))
-> (Rep (POr a s) -> POr a s) -> Generic (POr a s)
Rep (POr a s) -> POr a s
POr a s -> Rep (POr a s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: PType) (s :: S).
All @[Type] (SListI @Type) (Code (POr a s))
forall (a :: PType) (s :: S). Rep (POr a s) -> POr a s
forall (a :: PType) (s :: S). POr a s -> Rep (POr a s)
$cfrom :: forall (a :: PType) (s :: S). POr a s -> Rep (POr a s)
from :: POr a s -> Rep (POr a s)
$cto :: forall (a :: PType) (s :: S). Rep (POr a s) -> POr a s
to :: Rep (POr a s) -> POr a s
SOP.Generic
    , -- | @since 1.10.0
      (forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s PBool)
-> PEq (POr a)
forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s PBool
forall (a :: PType) (s :: S).
PEq a =>
Term s (POr a) -> Term s (POr a) -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
$c#== :: forall (a :: PType) (s :: S).
PEq a =>
Term s (POr a) -> Term s (POr a) -> Term s PBool
#== :: forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s PBool
PEq
    , -- | @since 1.10.0
      PEq (POr a)
PEq (POr a) =>
(forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s PBool)
-> (forall (s :: S).
    Term s (POr a) -> Term s (POr a) -> Term s PBool)
-> (forall (s :: S).
    Term s (POr a) -> Term s (POr a) -> Term s (POr a))
-> (forall (s :: S).
    Term s (POr a) -> Term s (POr a) -> Term s (POr a))
-> POrd (POr a)
forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s PBool
forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s (POr a)
forall (t :: PType).
PEq t =>
(forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> POrd t
forall (a :: PType). POrd a => PEq (POr a)
forall (a :: PType) (s :: S).
POrd a =>
Term s (POr a) -> Term s (POr a) -> Term s PBool
forall (a :: PType) (s :: S).
POrd a =>
Term s (POr a) -> Term s (POr a) -> Term s (POr a)
$c#<= :: forall (a :: PType) (s :: S).
POrd a =>
Term s (POr a) -> Term s (POr a) -> Term s PBool
#<= :: forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s PBool
$c#< :: forall (a :: PType) (s :: S).
POrd a =>
Term s (POr a) -> Term s (POr a) -> Term s PBool
#< :: forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s PBool
$cpmax :: forall (a :: PType) (s :: S).
POrd a =>
Term s (POr a) -> Term s (POr a) -> Term s (POr a)
pmax :: forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s (POr a)
$cpmin :: forall (a :: PType) (s :: S).
POrd a =>
Term s (POr a) -> Term s (POr a) -> Term s (POr a)
pmin :: forall (s :: S). Term s (POr a) -> Term s (POr a) -> Term s (POr a)
POrd
    )
  deriving
    ( -- | @since 1.10.0
      (forall (s :: S). POr a s -> Term s (PInner (POr a)))
-> (forall (s :: S) (b :: PType).
    Term s (PInner (POr a)) -> (POr a s -> Term s b) -> Term s b)
-> PlutusType (POr a)
forall (s :: S). POr a s -> Term s (PInner (POr a))
forall (s :: S) (b :: PType).
Term s (PInner (POr a)) -> (POr a s -> Term s b) -> Term s b
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). POr a s -> Term s (PInner (POr a))
forall (a :: PType) (s :: S) (b :: PType).
Term s (PInner (POr a)) -> (POr a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: PType) (s :: S). POr a s -> Term s (PInner (POr a))
pcon' :: forall (s :: S). POr a s -> Term s (PInner (POr a))
$cpmatch' :: forall (a :: PType) (s :: S) (b :: PType).
Term s (PInner (POr a)) -> (POr a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (POr a)) -> (POr a s -> Term s b) -> Term s b
PlutusType
    )
    via (DeriveNewtypePlutusType (POr a))

-- | @since 1.10.0
deriving via
  DeriveNewtypePLiftable (POr a) (AsHaskell a)
  instance
    (PLiftable a, PLC.DefaultUni `Includes` PlutusRepr a) => PLiftable (POr a)

-- | @since 1.10.0
instance PSemigroup (POr PBool) where
  {-# INLINEABLE (#<>) #-}
  Term s (POr PBool)
x #<> :: forall (s :: S).
Term s (POr PBool) -> Term s (POr PBool) -> Term s (POr PBool)
#<> Term s (POr PBool)
y = Term s PBool
-> Term s (POr PBool) -> Term s (POr PBool) -> Term s (POr PBool)
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s (POr PBool) -> Term s (PInner (POr PBool))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (POr PBool)
x) Term s (POr PBool)
x Term s (POr PBool)
y

  -- \| 'PBool' is idempotent under OR.
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive -> Term s (POr PBool) -> Term s (POr PBool)
pstimes Term s PPositive
p Term s (POr PBool)
x = Term s PPositive
-> (Term s PPositive -> Term s (POr PBool)) -> Term s (POr PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
p ((Term s PPositive -> Term s (POr PBool)) -> Term s (POr PBool))
-> (Term s PPositive -> Term s (POr PBool)) -> Term s (POr PBool)
forall a b. (a -> b) -> a -> b
$ Term s (POr PBool) -> Term s PPositive -> Term s (POr PBool)
forall a b. a -> b -> a
const Term s (POr PBool)
x

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

{- | This uses padding semantics as specified in CIP-122, as this allows a
'PMonoid' instance as well.

@since 1.10.0
-}
instance PSemigroup (POr PByteString) where
  {-# INLINEABLE (#<>) #-}
  Term s (POr PByteString)
x #<> :: forall (s :: S).
Term s (POr PByteString)
-> Term s (POr PByteString) -> Term s (POr PByteString)
#<> Term s (POr PByteString)
y = Term s (PInner (POr PByteString)) -> Term s (POr PByteString)
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner (POr PByteString)) -> Term s (POr PByteString))
-> Term s (PInner (POr PByteString)) -> Term s (POr PByteString)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
forall (s :: S).
Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
porBS Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
-> Term s PLogicOpSemantics
-> Term s (PByteString :--> (PByteString :--> PByteString))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PLogicOpSemantics
forall (s :: S). Term s PLogicOpSemantics
ppadding Term s (PByteString :--> (PByteString :--> PByteString))
-> Term s PByteString -> Term s (PByteString :--> PByteString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (POr PByteString) -> Term s (PInner (POr PByteString))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (POr PByteString)
x Term s (PByteString :--> PByteString)
-> Term s PByteString -> Term s PByteString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (POr PByteString) -> Term s (PInner (POr PByteString))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (POr PByteString)
y

  -- \| 'PByteString' is idempotent under OR regardless of semantics.
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive
-> Term s (POr PByteString) -> Term s (POr PByteString)
pstimes Term s PPositive
p Term s (POr PByteString)
x = Term s PPositive
-> (Term s PPositive -> Term s (POr PByteString))
-> Term s (POr PByteString)
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
p ((Term s PPositive -> Term s (POr PByteString))
 -> Term s (POr PByteString))
-> (Term s PPositive -> Term s (POr PByteString))
-> Term s (POr PByteString)
forall a b. (a -> b) -> a -> b
$ Term s (POr PByteString)
-> Term s PPositive -> Term s (POr PByteString)
forall a b. a -> b -> a
const Term s (POr PByteString)
x

-- | @since 1.10.0
instance PMonoid (POr PByteString) where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s (POr PByteString)
pmempty = POr PByteString s -> Term s (POr PByteString)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (POr PByteString s -> Term s (POr PByteString))
-> (Term s PByteString -> POr PByteString s)
-> Term s PByteString
-> Term s (POr PByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PByteString -> POr PByteString s
forall (a :: PType) (s :: S). Term s a -> POr a s
POr (Term s PByteString -> Term s (POr PByteString))
-> Term s PByteString -> Term s (POr PByteString)
forall a b. (a -> b) -> a -> b
$ Term s PByteString
forall a. Monoid a => a
mempty

{- | Wrapper for types which have logical XOR semantics somehow.

@since 1.10.0
-}
newtype PXor (a :: S -> Type) (s :: S)
  = PXor (Term s a)
  deriving stock
    ( -- | @since 1.10.0
      (forall x. PXor a s -> Rep (PXor a s) x)
-> (forall x. Rep (PXor a s) x -> PXor a s) -> Generic (PXor a s)
forall x. Rep (PXor a s) x -> PXor a s
forall x. PXor a s -> Rep (PXor a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (s :: S) x. Rep (PXor a s) x -> PXor a s
forall (a :: PType) (s :: S) x. PXor a s -> Rep (PXor a s) x
$cfrom :: forall (a :: PType) (s :: S) x. PXor a s -> Rep (PXor a s) x
from :: forall x. PXor a s -> Rep (PXor a s) x
$cto :: forall (a :: PType) (s :: S) x. Rep (PXor a s) x -> PXor a s
to :: forall x. Rep (PXor a s) x -> PXor a s
Generic
    )
  deriving anyclass
    ( -- | @since 1.10.0
      All @[Type] (SListI @Type) (Code (PXor a s))
All @[Type] (SListI @Type) (Code (PXor a s)) =>
(PXor a s -> Rep (PXor a s))
-> (Rep (PXor a s) -> PXor a s) -> Generic (PXor a s)
Rep (PXor a s) -> PXor a s
PXor a s -> Rep (PXor a s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: PType) (s :: S).
All @[Type] (SListI @Type) (Code (PXor a s))
forall (a :: PType) (s :: S). Rep (PXor a s) -> PXor a s
forall (a :: PType) (s :: S). PXor a s -> Rep (PXor a s)
$cfrom :: forall (a :: PType) (s :: S). PXor a s -> Rep (PXor a s)
from :: PXor a s -> Rep (PXor a s)
$cto :: forall (a :: PType) (s :: S). Rep (PXor a s) -> PXor a s
to :: Rep (PXor a s) -> PXor a s
SOP.Generic
    , -- | @since 1.10.0
      (forall (s :: S).
 Term s (PXor a) -> Term s (PXor a) -> Term s PBool)
-> PEq (PXor a)
forall (s :: S). Term s (PXor a) -> Term s (PXor a) -> Term s PBool
forall (a :: PType) (s :: S).
PEq a =>
Term s (PXor a) -> Term s (PXor a) -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
$c#== :: forall (a :: PType) (s :: S).
PEq a =>
Term s (PXor a) -> Term s (PXor a) -> Term s PBool
#== :: forall (s :: S). Term s (PXor a) -> Term s (PXor a) -> Term s PBool
PEq
    , -- | @since 1.10.0
      PEq (PXor a)
PEq (PXor a) =>
(forall (s :: S).
 Term s (PXor a) -> Term s (PXor a) -> Term s PBool)
-> (forall (s :: S).
    Term s (PXor a) -> Term s (PXor a) -> Term s PBool)
-> (forall (s :: S).
    Term s (PXor a) -> Term s (PXor a) -> Term s (PXor a))
-> (forall (s :: S).
    Term s (PXor a) -> Term s (PXor a) -> Term s (PXor a))
-> POrd (PXor a)
forall (s :: S). Term s (PXor a) -> Term s (PXor a) -> Term s PBool
forall (s :: S).
Term s (PXor a) -> Term s (PXor a) -> Term s (PXor a)
forall (t :: PType).
PEq t =>
(forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> POrd t
forall (a :: PType). POrd a => PEq (PXor a)
forall (a :: PType) (s :: S).
POrd a =>
Term s (PXor a) -> Term s (PXor a) -> Term s PBool
forall (a :: PType) (s :: S).
POrd a =>
Term s (PXor a) -> Term s (PXor a) -> Term s (PXor a)
$c#<= :: forall (a :: PType) (s :: S).
POrd a =>
Term s (PXor a) -> Term s (PXor a) -> Term s PBool
#<= :: forall (s :: S). Term s (PXor a) -> Term s (PXor a) -> Term s PBool
$c#< :: forall (a :: PType) (s :: S).
POrd a =>
Term s (PXor a) -> Term s (PXor a) -> Term s PBool
#< :: forall (s :: S). Term s (PXor a) -> Term s (PXor a) -> Term s PBool
$cpmax :: forall (a :: PType) (s :: S).
POrd a =>
Term s (PXor a) -> Term s (PXor a) -> Term s (PXor a)
pmax :: forall (s :: S).
Term s (PXor a) -> Term s (PXor a) -> Term s (PXor a)
$cpmin :: forall (a :: PType) (s :: S).
POrd a =>
Term s (PXor a) -> Term s (PXor a) -> Term s (PXor a)
pmin :: forall (s :: S).
Term s (PXor a) -> Term s (PXor a) -> Term s (PXor a)
POrd
    )
  deriving
    ( -- | @since 1.10.0
      (forall (s :: S). PXor a s -> Term s (PInner (PXor a)))
-> (forall (s :: S) (b :: PType).
    Term s (PInner (PXor a)) -> (PXor a s -> Term s b) -> Term s b)
-> PlutusType (PXor a)
forall (s :: S). PXor a s -> Term s (PInner (PXor a))
forall (s :: S) (b :: PType).
Term s (PInner (PXor a)) -> (PXor a s -> Term s b) -> Term s b
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). PXor a s -> Term s (PInner (PXor a))
forall (a :: PType) (s :: S) (b :: PType).
Term s (PInner (PXor a)) -> (PXor a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: PType) (s :: S). PXor a s -> Term s (PInner (PXor a))
pcon' :: forall (s :: S). PXor a s -> Term s (PInner (PXor a))
$cpmatch' :: forall (a :: PType) (s :: S) (b :: PType).
Term s (PInner (PXor a)) -> (PXor a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PXor a)) -> (PXor a s -> Term s b) -> Term s b
PlutusType
    )
    via (DeriveNewtypePlutusType (PXor a))

-- | @since 1.10.0
deriving via
  DeriveNewtypePLiftable (PXor a) (AsHaskell a)
  instance
    (PLiftable a, PLC.DefaultUni `Includes` PlutusRepr a) => PLiftable (PXor a)

-- | @since 1.10.0
instance PSemigroup (PXor PBool) where
  {-# INLINEABLE (#<>) #-}
  Term s (PXor PBool)
x #<> :: forall (s :: S).
Term s (PXor PBool) -> Term s (PXor PBool) -> Term s (PXor PBool)
#<> Term s (PXor PBool)
y = Term s (PBool :--> (PXor PBool :--> (PXor PBool :--> PXor PBool)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (PXor PBool :--> (PXor PBool :--> PXor PBool)))
-> Term s PBool
-> Term s (PXor PBool :--> (PXor PBool :--> PXor PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PXor PBool) -> Term s (PInner (PXor PBool))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PXor PBool)
x Term s (PXor PBool :--> (PXor PBool :--> PXor PBool))
-> Term s (PXor PBool) -> Term s (PXor PBool :--> PXor PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (PXor PBool s -> Term s (PXor PBool)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PXor PBool s -> Term s (PXor PBool))
-> (Term s PBool -> PXor PBool s)
-> Term s PBool
-> Term s (PXor PBool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PBool -> PXor PBool s
forall (a :: PType) (s :: S). Term s a -> PXor a s
PXor (Term s PBool -> Term s (PXor PBool))
-> Term s PBool -> Term s (PXor PBool)
forall a b. (a -> b) -> a -> b
$ Term s (PBool :--> PBool)
forall (s :: S). Term s (PBool :--> PBool)
pnot Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PXor PBool) -> Term s (PInner (PXor PBool))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PXor PBool)
y) Term s (PXor PBool :--> PXor PBool)
-> Term s (PXor PBool) -> Term s (PXor PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PXor PBool)
y

  -- \| Because XOR is self-inverting, there are only two outcomes: either the
  -- argument (if the exponent is odd) or 'PFalse' (if it's even).
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive -> Term s (PXor PBool) -> Term s (PXor PBool)
pstimes = Term s PBool
-> Term s PPositive -> Term s (PXor PBool) -> Term s (PXor PBool)
forall (a :: PType) (b :: PType) (s :: S).
((PInner a :: PType) ~ (PInteger :: PType)) =>
Term s b -> Term s a -> Term s (PXor b) -> Term s (PXor b)
pxortimes (PBool s -> Term s PBool
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse)

-- | @since 1.10.0
instance PMonoid (PXor PBool) where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s (PXor PBool)
pmempty = PXor PBool s -> Term s (PXor PBool)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PXor PBool s -> Term s (PXor PBool))
-> (PBool s -> PXor PBool s) -> PBool s -> Term s (PXor PBool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PBool -> PXor PBool s
forall (a :: PType) (s :: S). Term s a -> PXor a s
PXor (Term s PBool -> PXor PBool s)
-> (PBool s -> Term s PBool) -> PBool s -> PXor PBool s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PBool s -> Term s PBool
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PBool s -> Term s (PXor PBool)) -> PBool s -> Term s (PXor PBool)
forall a b. (a -> b) -> a -> b
$ PBool s
forall (s :: S). PBool s
PFalse
  {-# INLINEABLE pmtimes #-}
  pmtimes :: forall (s :: S).
Term s PNatural -> Term s (PXor PBool) -> Term s (PXor PBool)
pmtimes = Term s PBool
-> Term s PNatural -> Term s (PXor PBool) -> Term s (PXor PBool)
forall (a :: PType) (b :: PType) (s :: S).
((PInner a :: PType) ~ (PInteger :: PType)) =>
Term s b -> Term s a -> Term s (PXor b) -> Term s (PXor b)
pxortimes (PBool s -> Term s PBool
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse)

{- | This uses padding semantics as specified in CIP-122, as this allows a
'PMonoid' instance as well.

@since 1.10.0
-}
instance PSemigroup (PXor PByteString) where
  {-# INLINEABLE (#<>) #-}
  Term s (PXor PByteString)
x #<> :: forall (s :: S).
Term s (PXor PByteString)
-> Term s (PXor PByteString) -> Term s (PXor PByteString)
#<> Term s (PXor PByteString)
y = Term s (PInner (PXor PByteString)) -> Term s (PXor PByteString)
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner (PXor PByteString)) -> Term s (PXor PByteString))
-> Term s (PInner (PXor PByteString)) -> Term s (PXor PByteString)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
forall (s :: S).
Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
pxorBS Term
  s
  (PLogicOpSemantics
   :--> (PByteString :--> (PByteString :--> PByteString)))
-> Term s PLogicOpSemantics
-> Term s (PByteString :--> (PByteString :--> PByteString))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PLogicOpSemantics
forall (s :: S). Term s PLogicOpSemantics
ppadding Term s (PByteString :--> (PByteString :--> PByteString))
-> Term s PByteString -> Term s (PByteString :--> PByteString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PXor PByteString) -> Term s (PInner (PXor PByteString))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PXor PByteString)
x Term s (PByteString :--> PByteString)
-> Term s PByteString -> Term s PByteString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PXor PByteString) -> Term s (PInner (PXor PByteString))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PXor PByteString)
y

  -- \| Because XOR is self-inverting, there are only two outcomes: either the
  -- argument (if the exponent is odd) or the empty 'PByteString' (if it isn't).
  {-# INLINEABLE pstimes #-}
  pstimes :: forall (s :: S).
Term s PPositive
-> Term s (PXor PByteString) -> Term s (PXor PByteString)
pstimes = Term s PByteString
-> Term s PPositive
-> Term s (PXor PByteString)
-> Term s (PXor PByteString)
forall (a :: PType) (b :: PType) (s :: S).
((PInner a :: PType) ~ (PInteger :: PType)) =>
Term s b -> Term s a -> Term s (PXor b) -> Term s (PXor b)
pxortimes Term s PByteString
forall a. Monoid a => a
mempty

-- | @since 1.10.0
instance PMonoid (PXor PByteString) where
  {-# INLINEABLE pmempty #-}
  pmempty :: forall (s :: S). Term s (PXor PByteString)
pmempty = PXor PByteString s -> Term s (PXor PByteString)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PXor PByteString s -> Term s (PXor PByteString))
-> (Term s PByteString -> PXor PByteString s)
-> Term s PByteString
-> Term s (PXor PByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PByteString -> PXor PByteString s
forall (a :: PType) (s :: S). Term s a -> PXor a s
PXor (Term s PByteString -> Term s (PXor PByteString))
-> Term s PByteString -> Term s (PXor PByteString)
forall a b. (a -> b) -> a -> b
$ Term s PByteString
forall a. Monoid a => a
mempty

-- Helpers

pxortimes ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  PInner a ~ PInteger =>
  Term s b ->
  Term s a ->
  Term s (PXor b) ->
  Term s (PXor b)
pxortimes :: forall (a :: PType) (b :: PType) (s :: S).
((PInner a :: PType) ~ (PInteger :: PType)) =>
Term s b -> Term s a -> Term s (PXor b) -> Term s (PXor b)
pxortimes Term s b
def Term s a
x =
  Term s PBool
-> Term s (PXor b) -> Term s (PXor b) -> Term s (PXor b)
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
    ((Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s a
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
2) Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0)
    (PXor b s -> Term s (PXor b)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PXor b s -> Term s (PXor b))
-> (Term s b -> PXor b s) -> Term s b -> Term s (PXor b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s b -> PXor b s
forall (a :: PType) (s :: S). Term s a -> PXor a s
PXor (Term s b -> Term s (PXor b)) -> Term s b -> Term s (PXor b)
forall a b. (a -> b) -> a -> b
$ Term s b
def)