{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Plutarch.Internal.Numeric (
  -- * Types
  PPositive,
  Positive,
  PNatural,

  -- * Type classes
  PAdditiveSemigroup (..),
  PAdditiveMonoid (..),
  PAdditiveGroup (..),
  PMultiplicativeSemigroup (..),
  PMultiplicativeMonoid (..),
  PRing (..),
  PIntegralDomain (..),

  -- * Functions
  positiveToInteger,
  toPositiveAbs,
  ptryPositive,
  ppositive,
  ptryNatural,
  pnatural,
  ppositiveToNatural,
  pnaturalToPositiveCPS,
  pbySquaringDefault,
  pdiv,
  pmod,
  pquot,
  prem,
) where

import Data.Coerce (coerce)
import Data.Kind (Type)
import GHC.Generics (Generic)
import Generics.SOP qualified as SOP
import Numeric.Natural (Natural)
import Plutarch.Builtin.BLS (
  PBuiltinBLS12_381_G1_Element,
  PBuiltinBLS12_381_G2_Element,
  PBuiltinBLS12_381_MlResult,
  pbls12_381_G1_add,
  pbls12_381_G1_compressed_zero,
  pbls12_381_G1_neg,
  pbls12_381_G1_scalarMul,
  pbls12_381_G1_uncompress,
  pbls12_381_G2_add,
  pbls12_381_G2_compressed_zero,
  pbls12_381_G2_neg,
  pbls12_381_G2_scalarMul,
  pbls12_381_G2_uncompress,
  pbls12_381_mulMlResult,
 )
import Plutarch.Builtin.Bool (pcond, pif)
import Plutarch.Builtin.Integer (
  PInteger,
  paddInteger,
  pconstantInteger,
  pmultiplyInteger,
  pquotientInteger,
  premainderInteger,
  psubtractInteger,
 )
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Fix (pfix)
import Plutarch.Internal.IsData (PIsData)
import Plutarch.Internal.Lift (
  DeriveNewtypePLiftable,
  LiftError (OtherLiftError),
  PLiftable (
    AsHaskell,
    PlutusRepr,
    haskToRepr,
    plutToRepr,
    reprToHask,
    reprToPlut
  ),
  PLifted (PLifted),
  punsafeCoercePLifted,
 )
import Plutarch.Internal.Ord (POrd ((#<=)))
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  DeriveNewtypePlutusType (DeriveNewtypePlutusType),
  PlutusType (PInner),
  pcon,
 )
import Plutarch.Internal.Term (
  S,
  Term,
  perror,
  phoistAcyclic,
  plet,
  punsafeBuiltin,
  punsafeCoerce,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Internal.Trace (ptraceInfo)
import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Unsafe (punsafeDowncast)
import PlutusCore qualified as PLC
import Prettyprinter (Pretty)
import Test.QuickCheck (
  Arbitrary,
  CoArbitrary,
  Function,
  functionMap,
 )
import Test.QuickCheck qualified as QuickCheck

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

-- | @since 1.10.0
deriving via
  DeriveNewtypePLiftable PPositive Positive
  instance
    PLiftable PPositive

-- | @since 1.10.0
newtype Positive = UnsafeMkPositive {Positive -> Integer
getPositive :: Integer}
  deriving stock
    ( -- | @since 1.10.0
      Int -> Positive -> ShowS
[Positive] -> ShowS
Positive -> [Char]
(Int -> Positive -> ShowS)
-> (Positive -> [Char]) -> ([Positive] -> ShowS) -> Show Positive
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Positive -> ShowS
showsPrec :: Int -> Positive -> ShowS
$cshow :: Positive -> [Char]
show :: Positive -> [Char]
$cshowList :: [Positive] -> ShowS
showList :: [Positive] -> ShowS
Show
    , -- | @since 1.10.0
      Positive -> Positive -> Bool
(Positive -> Positive -> Bool)
-> (Positive -> Positive -> Bool) -> Eq Positive
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Positive -> Positive -> Bool
== :: Positive -> Positive -> Bool
$c/= :: Positive -> Positive -> Bool
/= :: Positive -> Positive -> Bool
Eq
    , -- | @since 1.10.0
      Eq Positive
Eq Positive =>
(Positive -> Positive -> Ordering)
-> (Positive -> Positive -> Bool)
-> (Positive -> Positive -> Bool)
-> (Positive -> Positive -> Bool)
-> (Positive -> Positive -> Bool)
-> (Positive -> Positive -> Positive)
-> (Positive -> Positive -> Positive)
-> Ord Positive
Positive -> Positive -> Bool
Positive -> Positive -> Ordering
Positive -> Positive -> Positive
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Positive -> Positive -> Ordering
compare :: Positive -> Positive -> Ordering
$c< :: Positive -> Positive -> Bool
< :: Positive -> Positive -> Bool
$c<= :: Positive -> Positive -> Bool
<= :: Positive -> Positive -> Bool
$c> :: Positive -> Positive -> Bool
> :: Positive -> Positive -> Bool
$c>= :: Positive -> Positive -> Bool
>= :: Positive -> Positive -> Bool
$cmax :: Positive -> Positive -> Positive
max :: Positive -> Positive -> Positive
$cmin :: Positive -> Positive -> Positive
min :: Positive -> Positive -> Positive
Ord
    )
  deriving
    ( -- | @since 1.10.0
      Gen Positive
Gen Positive -> (Positive -> [Positive]) -> Arbitrary Positive
Positive -> [Positive]
forall a. Gen a -> (a -> [a]) -> Arbitrary a
$carbitrary :: Gen Positive
arbitrary :: Gen Positive
$cshrink :: Positive -> [Positive]
shrink :: Positive -> [Positive]
Arbitrary
    )
    via QuickCheck.Positive Integer
  deriving
    ( -- | @since 1.10.0
      (forall b. Positive -> Gen b -> Gen b) -> CoArbitrary Positive
forall b. Positive -> Gen b -> Gen b
forall a. (forall b. a -> Gen b -> Gen b) -> CoArbitrary a
$ccoarbitrary :: forall b. Positive -> Gen b -> Gen b
coarbitrary :: forall b. Positive -> Gen b -> Gen b
CoArbitrary
    , -- | @since 1.10.0
      (forall ann. Positive -> Doc ann)
-> (forall ann. [Positive] -> Doc ann) -> Pretty Positive
forall ann. [Positive] -> Doc ann
forall ann. Positive -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
$cpretty :: forall ann. Positive -> Doc ann
pretty :: forall ann. Positive -> Doc ann
$cprettyList :: forall ann. [Positive] -> Doc ann
prettyList :: forall ann. [Positive] -> Doc ann
Pretty
    )
    via Integer

-- | @since 1.10.0
instance Function Positive where
  {-# INLINEABLE function #-}
  function :: forall b. (Positive -> b) -> Positive :-> b
function = forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
functionMap @Integer Positive -> Integer
forall a b. Coercible @Type a b => a -> b
coerce Integer -> Positive
forall a b. Coercible @Type a b => a -> b
coerce

{- | Converts negative 'Integer's into their absolute values, positive
'Integer's into their 'Positive' equivalents. Errors on 0.

@since 1.10.0
-}
toPositiveAbs :: Integer -> Positive
toPositiveAbs :: Integer -> Positive
toPositiveAbs Integer
i = Integer -> Positive
UnsafeMkPositive (Integer -> Positive) -> Integer -> Positive
forall a b. (a -> b) -> a -> b
$ case Integer -> Integer
forall a. Num a => a -> a
signum Integer
i of
  (Integer
-1) -> Integer -> Integer
forall a. Num a => a -> a
abs Integer
i
  Integer
0 -> [Char] -> Integer
forall a. HasCallStack => [Char] -> a
error [Char]
"toPositiveAbs: called with zero"
  Integer
_ -> Integer
i

-- | @since 1.10.0
positiveToInteger :: Positive -> Integer
positiveToInteger :: Positive -> Integer
positiveToInteger = Positive -> Integer
getPositive

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

-- | @since 1.10.0
instance PLiftable PNatural where
  type AsHaskell PNatural = Natural
  type PlutusRepr PNatural = Integer
  {-# INLINEABLE haskToRepr #-}
  haskToRepr :: AsHaskell PNatural -> PlutusRepr PNatural
haskToRepr = AsHaskell PNatural -> PlutusRepr PNatural
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINEABLE reprToHask #-}
  reprToHask :: PlutusRepr PNatural -> Either LiftError (AsHaskell PNatural)
reprToHask PlutusRepr PNatural
i = case PlutusRepr PNatural -> PlutusRepr PNatural
forall a. Num a => a -> a
signum PlutusRepr PNatural
i of
    (PlutusRepr PNatural
-1) -> LiftError -> Either LiftError (AsHaskell PNatural)
forall a b. a -> Either a b
Left (LiftError -> Either LiftError (AsHaskell PNatural))
-> LiftError -> Either LiftError (AsHaskell PNatural)
forall a b. (a -> b) -> a -> b
$ Text -> LiftError
OtherLiftError Text
"Negative input"
    PlutusRepr PNatural
_ -> AsHaskell PNatural -> Either LiftError (AsHaskell PNatural)
forall a b. b -> Either a b
Right (AsHaskell PNatural -> Either LiftError (AsHaskell PNatural))
-> (PlutusRepr PNatural -> AsHaskell PNatural)
-> PlutusRepr PNatural
-> Either LiftError (AsHaskell PNatural)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlutusRepr PNatural -> AsHaskell PNatural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (PlutusRepr PNatural -> Either LiftError (AsHaskell PNatural))
-> PlutusRepr PNatural -> Either LiftError (AsHaskell PNatural)
forall a b. (a -> b) -> a -> b
$ PlutusRepr PNatural
i
  {-# INLINEABLE reprToPlut #-}
  reprToPlut :: forall (s :: S). PlutusRepr PNatural -> PLifted s PNatural
reprToPlut = PLifted s PInteger -> PLifted s PNatural
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
PLifted s a -> PLifted s b
punsafeCoercePLifted (PLifted s PInteger -> PLifted s PNatural)
-> (PlutusRepr PNatural -> PLifted s PInteger)
-> PlutusRepr PNatural
-> PLifted s PNatural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S).
PLiftable a =>
PlutusRepr a -> PLifted s a
reprToPlut @PInteger (PlutusRepr PInteger -> PLifted s PInteger)
-> (PlutusRepr PNatural -> PlutusRepr PInteger)
-> PlutusRepr PNatural
-> PLifted s PInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlutusRepr PNatural -> PlutusRepr PInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINEABLE plutToRepr #-}
  plutToRepr :: (forall (s :: S). PLifted s PNatural)
-> Either LiftError (PlutusRepr PNatural)
plutToRepr forall (s :: S). PLifted s PNatural
t = forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). PLifted s a) -> Either LiftError (PlutusRepr a)
plutToRepr @PInteger (PLifted s PNatural -> PLifted s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
PLifted s a -> PLifted s b
punsafeCoercePLifted PLifted s PNatural
forall (s :: S). PLifted s PNatural
t)

{- | The addition operation, and the notion of scaling by a positive.

= Laws

1. @x #+ y@ @=@ @y #+ x@ (commutativity of @#+@)
2. @x #+ (y #+ z)@ @=@ @(x #+ y) #+ z@ (associativity of @#+@)

If you define a custom @pscalePositive@, ensure the following also hold:

3. @pscalePositive x pone@ @=@ @x@
4. @(pscalePositive x n) #+ (pscalePositive x m)@ @=@
   @pscalePositive x (n #+ m)@
5. @pscalePositive (pscalePositive x n) m@ @=@
   @pscalePositive x (n #* m)@

The default implementation ensures these laws are satisfied.

@since 1.10.0
-}
class PAdditiveSemigroup (a :: S -> Type) where
  (#+) :: forall (s :: S). Term s a -> Term s a -> Term s a
  default (#+) ::
    forall (s :: S).
    PAdditiveSemigroup (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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s a -> Term s (PInner a)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s a
y
  {-# INLINEABLE pscalePositive #-}

  -- | This defaults to exponentiation-by-squaring, which in general is the best
  -- we can do.
  pscalePositive ::
    forall (s :: S).
    Term s a ->
    Term s PPositive ->
    Term s a
  pscalePositive = (forall (s :: S). Term s a -> Term s a -> Term s a)
-> Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (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 :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+)

-- | @since 1.10.0
infix 6 #+

-- | @since 1.10.0
instance PAdditiveSemigroup PPositive where
  {-# INLINEABLE (#+) #-}
  Term s PPositive
x #+ :: forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
#+ Term s PPositive
y = Term s PInteger -> Term s PPositive
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s PInteger -> Term s PPositive)
-> Term s PInteger -> Term s PPositive
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
paddInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
y
  {-# INLINEABLE pscalePositive #-}
  pscalePositive :: forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
pscalePositive Term s PPositive
b Term s PPositive
e = Term s PPositive
b Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PPositive
e

-- | @since 1.10.0
instance PAdditiveSemigroup PNatural where
  {-# INLINEABLE (#+) #-}
  Term s PNatural
x #+ :: forall (s :: S).
Term s PNatural -> Term s PNatural -> Term s PNatural
#+ Term s PNatural
y = PNatural s -> Term s PNatural
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PNatural s -> Term s PNatural)
-> (Term s PInteger -> PNatural s)
-> Term s PInteger
-> Term s PNatural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> PNatural s
forall (s :: S). Term s PInteger -> PNatural s
PNatural (Term s PInteger -> Term s PNatural)
-> Term s PInteger -> Term s PNatural
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
paddInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s (PInner PNatural)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PNatural
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s (PInner PNatural)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PNatural
y
  {-# INLINEABLE pscalePositive #-}
  pscalePositive :: forall (s :: S).
Term s PNatural -> Term s PPositive -> Term s PNatural
pscalePositive Term s PNatural
b Term s PPositive
e = Term s PNatural
b Term s PNatural -> Term s PNatural -> Term s PNatural
forall (s :: S).
Term s PNatural -> Term s PNatural -> Term s PNatural
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PPositive -> Term s PNatural
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PPositive
e

-- | @since 1.10.0
instance PAdditiveSemigroup PInteger where
  {-# INLINEABLE (#+) #-}
  Term s PInteger
x #+ :: forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
#+ Term s PInteger
y = Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
paddInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y
  {-# INLINEABLE pscalePositive #-}
  pscalePositive :: forall (s :: S).
Term s PInteger -> Term s PPositive -> Term s PInteger
pscalePositive Term s PInteger
b Term s PPositive
e = Term s PInteger
b Term s PInteger -> Term s PInteger -> Term s PInteger
forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
e

-- | @since 1.10.0
instance PAdditiveSemigroup PBuiltinBLS12_381_G1_Element where
  {-# INLINEABLE (#+) #-}
  Term s PBuiltinBLS12_381_G1_Element
x #+ :: 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
y = Term
  s
  (PBuiltinBLS12_381_G1_Element
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
forall (s :: S).
Term
  s
  (PBuiltinBLS12_381_G1_Element
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
pbls12_381_G1_add Term
  s
  (PBuiltinBLS12_381_G1_Element
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
-> Term s PBuiltinBLS12_381_G1_Element
-> Term
     s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
x Term
  s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
y
  {-# INLINEABLE pscalePositive #-}
  pscalePositive :: forall (s :: S).
Term s PBuiltinBLS12_381_G1_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G1_Element
pscalePositive Term s PBuiltinBLS12_381_G1_Element
x Term s PPositive
p = Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
pbls12_381_G1_scalarMul Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
-> Term s PInteger
-> Term
     s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
p Term
  s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
x

-- | @since 1.10.0
instance PAdditiveSemigroup PBuiltinBLS12_381_G2_Element where
  {-# INLINEABLE (#+) #-}
  Term s PBuiltinBLS12_381_G2_Element
x #+ :: 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
y = Term
  s
  (PBuiltinBLS12_381_G2_Element
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
forall (s :: S).
Term
  s
  (PBuiltinBLS12_381_G2_Element
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
pbls12_381_G2_add Term
  s
  (PBuiltinBLS12_381_G2_Element
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
-> Term s PBuiltinBLS12_381_G2_Element
-> Term
     s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
x Term
  s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
y
  {-# INLINEABLE pscalePositive #-}
  pscalePositive :: forall (s :: S).
Term s PBuiltinBLS12_381_G2_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G2_Element
pscalePositive Term s PBuiltinBLS12_381_G2_Element
x Term s PPositive
p = Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
pbls12_381_G2_scalarMul Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
-> Term s PInteger
-> Term
     s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
p Term
  s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
x

{- | The notion of zero, as well as a way to scale by naturals.

= Laws

1. @pzero #+ x@ @=@ @x@ (@pzero@ is the identity of @#+@)
2. @pscalePositive pzero n@ @=@
   @pzero@ (@pzero@ does not scale up)

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

3. @pscaleNatural x (ppositiveToNatural # p)@ @=@
   @pscalePositive x p@
4. @pscaleNatural x pzero@ @=@ @pzero@

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

@since 1.10.0
-}
class PAdditiveSemigroup a => PAdditiveMonoid (a :: S -> Type) where
  pzero :: forall (s :: S). Term s a
  {-# INLINEABLE pscaleNatural #-}
  pscaleNatural ::
    forall (s :: S).
    Term s a ->
    Term s PNatural ->
    Term s a
  pscaleNatural Term s a
x Term s PNatural
n =
    Term s PNatural -> (Term s PNatural -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PNatural
n ((Term s PNatural -> Term s a) -> Term s a)
-> (Term s PNatural -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s PNatural
n' ->
      Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s PNatural
n' Term s PNatural -> Term s PNatural -> Term s PBool
forall (s :: S). Term s PNatural -> Term s PNatural -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PNatural
forall (s :: S). Term s PNatural
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
        Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero
        (Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s a
x (Term s PNatural -> Term s PPositive
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PNatural
n'))

-- | @since 1.10.0
instance PAdditiveMonoid PInteger where
  {-# INLINEABLE pzero #-}
  pzero :: forall (s :: S). Term s PInteger
pzero = Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
0
  {-# INLINEABLE pscaleNatural #-}
  pscaleNatural :: forall (s :: S).
Term s PInteger -> Term s PNatural -> Term s PInteger
pscaleNatural Term s PInteger
i Term s PNatural
n = Term s PInteger
i Term s PInteger -> Term s PInteger -> Term s PInteger
forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PNatural -> Term s PInteger
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PNatural
n

-- | @since 1.10.0
instance PAdditiveMonoid PNatural where
  {-# INLINEABLE pzero #-}
  pzero :: forall (s :: S). Term s PNatural
pzero = PNatural s -> Term s PNatural
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PNatural s -> Term s PNatural)
-> (Integer -> PNatural s) -> Integer -> Term s PNatural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> PNatural s
forall (s :: S). Term s PInteger -> PNatural s
PNatural (Term s PInteger -> PNatural s)
-> (Integer -> Term s PInteger) -> Integer -> PNatural s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger (Integer -> Term s PNatural) -> Integer -> Term s PNatural
forall a b. (a -> b) -> a -> b
$ Integer
0
  {-# INLINEABLE pscaleNatural #-}
  pscaleNatural :: forall (s :: S).
Term s PNatural -> Term s PNatural -> Term s PNatural
pscaleNatural Term s PNatural
n1 Term s PNatural
n2 = Term s PNatural
n1 Term s PNatural -> Term s PNatural -> Term s PNatural
forall (s :: S).
Term s PNatural -> Term s PNatural -> Term s PNatural
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PNatural
n2

-- | @since 1.10.0
instance PAdditiveMonoid PBuiltinBLS12_381_G1_Element where
  {-# INLINEABLE pzero #-}
  pzero :: forall (s :: S). Term s PBuiltinBLS12_381_G1_Element
pzero = Term s (PByteString :--> PBuiltinBLS12_381_G1_Element)
forall (s :: S).
Term s (PByteString :--> PBuiltinBLS12_381_G1_Element)
pbls12_381_G1_uncompress Term s (PByteString :--> PBuiltinBLS12_381_G1_Element)
-> Term s PByteString -> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
forall (s :: S). Term s PByteString
pbls12_381_G1_compressed_zero
  {-# INLINEABLE pscaleNatural #-}
  pscaleNatural :: forall (s :: S).
Term s PBuiltinBLS12_381_G1_Element
-> Term s PNatural -> Term s PBuiltinBLS12_381_G1_Element
pscaleNatural Term s PBuiltinBLS12_381_G1_Element
x Term s PNatural
n = Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
pbls12_381_G1_scalarMul Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
-> Term s PInteger
-> Term
     s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s (PInner PNatural)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PNatural
n Term
  s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
x

-- | @since 1.10.0
instance PAdditiveMonoid PBuiltinBLS12_381_G2_Element where
  {-# INLINEABLE pzero #-}
  pzero :: forall (s :: S). Term s PBuiltinBLS12_381_G2_Element
pzero = Term s (PByteString :--> PBuiltinBLS12_381_G2_Element)
forall (s :: S).
Term s (PByteString :--> PBuiltinBLS12_381_G2_Element)
pbls12_381_G2_uncompress Term s (PByteString :--> PBuiltinBLS12_381_G2_Element)
-> Term s PByteString -> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
forall (s :: S). Term s PByteString
pbls12_381_G2_compressed_zero
  {-# INLINEABLE pscaleNatural #-}
  pscaleNatural :: forall (s :: S).
Term s PBuiltinBLS12_381_G2_Element
-> Term s PNatural -> Term s PBuiltinBLS12_381_G2_Element
pscaleNatural Term s PBuiltinBLS12_381_G2_Element
x Term s PNatural
n = Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
pbls12_381_G2_scalarMul Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
-> Term s PInteger
-> Term
     s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s (PInner PNatural)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PNatural
n Term
  s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
x

{- | The notion of additive inverses, and the subtraction operation.

= Laws

If you define @pnegate@, the following laws must hold:

1. @(pnegate # x) #+ x@ @=@ @pzero@ (@pnegate@ is an additive inverse)
2. @pnegate #$ pnegate # x@ @=@ @x@ (@pnegate@ is self-inverting)

If you define @#-@, the following law must hold:

3. @x #- x@ @=@ @pzero@

Additionally, the following \'consistency laws\' must hold. Default
implementations of both @pnegate@ and @#-@ uphold these.

4. @pnegate # x@ @=@ @pzero #- x@
5. @x #- y@ @=@ @x #+ (pnegate # y)@

Lastly, if you define a custom @pscaleInteger@, the following laws
must hold:

6. @pscaleInteger x pzero@ @=@ @pzero@
7. @pscaleInteger x (pnegate # y)@ @=@
   @pnegate # (pscaleInteger x y)@

@since 1.10.0
-}
class PAdditiveMonoid a => PAdditiveGroup (a :: S -> Type) where
  {-# MINIMAL pnegate | (#-) #-}
  {-# INLINEABLE pnegate #-}
  pnegate :: forall (s :: S). Term s (a :--> a)
  pnegate = (forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a)
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s a) -> Term s (a :--> a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a) -> Term s (c :--> a)
plam ((Term s a -> Term s a) -> Term s (a :--> a))
-> (Term s a -> Term s a) -> Term s (a :--> a)
forall a b. (a -> b) -> a -> b
$ \Term s a
x -> Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero 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).
PAdditiveGroup a =>
Term s a -> Term s a -> Term s a
#- Term s a
x
  {-# INLINEABLE (#-) #-}
  (#-) :: forall (s :: S). Term s a -> Term s a -> Term s a
  Term s a
x' #- Term s a
y' = Term s (a :--> (a :--> a))
forall (s' :: S). Term s' (a :--> (a :--> a))
inner Term s (a :--> (a :--> a)) -> Term s a -> Term s (a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x' Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y'
    where
      inner :: forall (s' :: S). Term s' (a :--> a :--> a)
      inner :: forall (s' :: S). Term s' (a :--> (a :--> a))
inner = (forall (s' :: S). Term s' (a :--> (a :--> a)))
-> Term s' (a :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (a :--> (a :--> a)))
 -> Term s' (a :--> (a :--> a)))
-> (forall (s' :: S). Term s' (a :--> (a :--> a)))
-> Term s' (a :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a)))
-> (Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s a
y ->
        Term s a
x 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).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y)
  {-# INLINEABLE pscaleInteger #-}
  pscaleInteger ::
    forall (s :: S).
    Term s a ->
    Term s PInteger ->
    Term s a
  pscaleInteger Term s a
b Term s PInteger
e =
    Term s PInteger -> (Term s PInteger -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PInteger
e ((Term s PInteger -> Term s a) -> Term s a)
-> (Term s PInteger -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
e' ->
      Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s PInteger
e' Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
        Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero
        ( Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s PInteger
e' Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
            (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s a
b (Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: S -> Type). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
e')))
            (Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s a
b (Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: S -> Type). Term s (PInner a) -> Term s a
punsafeDowncast Term s PInteger
Term s (PInner PPositive)
e'))
        )

-- | @since 1.10.0
infix 6 #-

-- | @since 1.10.0
instance PAdditiveGroup PInteger where
  {-# INLINEABLE (#-) #-}
  Term s PInteger
x #- :: forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
#- Term s PInteger
y = Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
psubtractInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y
  {-# INLINEABLE pscaleInteger #-}
  pscaleInteger :: forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
pscaleInteger = Term s PInteger -> Term s PInteger -> Term s PInteger
forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
(#*)

-- | @since 1.10.0
instance PAdditiveGroup PBuiltinBLS12_381_G1_Element where
  {-# INLINEABLE pnegate #-}
  pnegate :: forall (s :: S).
Term
  s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
pnegate = Term
  s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
forall (s :: S).
Term
  s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
pbls12_381_G1_neg
  {-# INLINEABLE pscaleInteger #-}
  pscaleInteger :: forall (s :: S).
Term s PBuiltinBLS12_381_G1_Element
-> Term s PInteger -> Term s PBuiltinBLS12_381_G1_Element
pscaleInteger Term s PBuiltinBLS12_381_G1_Element
b Term s PInteger
e = Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
pbls12_381_G1_scalarMul Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G1_Element
         :--> PBuiltinBLS12_381_G1_Element))
-> Term s PInteger
-> Term
     s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
e Term
  s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
b

-- | @since 1.10.0
instance PAdditiveGroup PBuiltinBLS12_381_G2_Element where
  {-# INLINEABLE pnegate #-}
  pnegate :: forall (s :: S).
Term
  s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
pnegate = Term
  s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
forall (s :: S).
Term
  s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
pbls12_381_G2_neg
  {-# INLINEABLE pscaleInteger #-}
  pscaleInteger :: forall (s :: S).
Term s PBuiltinBLS12_381_G2_Element
-> Term s PInteger -> Term s PBuiltinBLS12_381_G2_Element
pscaleInteger Term s PBuiltinBLS12_381_G2_Element
b Term s PInteger
e = Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
pbls12_381_G2_scalarMul Term
  s
  (PInteger
   :--> (PBuiltinBLS12_381_G2_Element
         :--> PBuiltinBLS12_381_G2_Element))
-> Term s PInteger
-> Term
     s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
e Term
  s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
b

{- | The multiplication operation.

= Laws

1. @x #* (y #* z)@ @=@ @(x #* y) #* z@ (associativity of @#*@)

If you define a custom @ppowPositive@, ensure the following also hold:

3. @ppowPositive x pone@ @=@ @x@
4. @(ppowPositive x n) #* (ppowPositive x m)@ @=@
   @ppowPositive x (n #+ m)@
5. @ppowPositive (ppowPositive x n) m@ @=@
   @ppowPositive x (n #* m)@

The default implementation ensures these laws are satisfied.

= Note

Unlike 'PAdditiveSemigroup', the multiplication operation doesn't need to be
commutative. Currently, all Plutarch-provided instances are, but this need
not be true for other instances.

@since 1.10.0
-}
class PMultiplicativeSemigroup (a :: S -> Type) where
  {-# INLINEABLE (#*) #-}
  (#*) :: forall (s :: S). Term s a -> Term s a -> Term s a
  default (#*) ::
    forall (s :: S).
    PMultiplicativeSemigroup (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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s a -> Term s (PInner a)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s a
y
  {-# INLINEABLE ppowPositive #-}
  ppowPositive ::
    forall (s :: S).
    Term s a ->
    Term s PPositive ->
    Term s a
  ppowPositive = (forall (s :: S). Term s a -> Term s a -> Term s a)
-> Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (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 :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
(#*)

-- | @since 1.10.0
infix 6 #*

-- | @since 1.10.0
instance PMultiplicativeSemigroup PPositive where
  {-# INLINEABLE (#*) #-}
  Term s PPositive
x #* :: forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
#* Term s PPositive
y = Term s PInteger -> Term s PPositive
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s PInteger -> Term s PPositive)
-> Term s PInteger -> Term s PPositive
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmultiplyInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
y

-- | @since 1.10.0
instance PMultiplicativeSemigroup PNatural where
  {-# INLINEABLE (#*) #-}
  Term s PNatural
x #* :: forall (s :: S).
Term s PNatural -> Term s PNatural -> Term s PNatural
#* Term s PNatural
y = PNatural s -> Term s PNatural
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PNatural s -> Term s PNatural)
-> (Term s PInteger -> PNatural s)
-> Term s PInteger
-> Term s PNatural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> PNatural s
forall (s :: S). Term s PInteger -> PNatural s
PNatural (Term s PInteger -> Term s PNatural)
-> Term s PInteger -> Term s PNatural
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmultiplyInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s (PInner PNatural)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PNatural
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s (PInner PNatural)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PNatural
y

-- | @since 1.10.0
instance PMultiplicativeSemigroup PInteger where
  {-# INLINEABLE (#*) #-}
  Term s PInteger
x #* :: forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
#* Term s PInteger
y = Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmultiplyInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y

-- | @since 1.10.0
instance PMultiplicativeSemigroup PBuiltinBLS12_381_MlResult where
  {-# INLINEABLE (#*) #-}
  Term s PBuiltinBLS12_381_MlResult
x #* :: forall (s :: S).
Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
#* Term s PBuiltinBLS12_381_MlResult
y = Term
  s
  (PBuiltinBLS12_381_MlResult
   :--> (PBuiltinBLS12_381_MlResult :--> PBuiltinBLS12_381_MlResult))
forall (s :: S).
Term
  s
  (PBuiltinBLS12_381_MlResult
   :--> (PBuiltinBLS12_381_MlResult :--> PBuiltinBLS12_381_MlResult))
pbls12_381_mulMlResult Term
  s
  (PBuiltinBLS12_381_MlResult
   :--> (PBuiltinBLS12_381_MlResult :--> PBuiltinBLS12_381_MlResult))
-> Term s PBuiltinBLS12_381_MlResult
-> Term
     s (PBuiltinBLS12_381_MlResult :--> PBuiltinBLS12_381_MlResult)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_MlResult
x Term s (PBuiltinBLS12_381_MlResult :--> PBuiltinBLS12_381_MlResult)
-> Term s PBuiltinBLS12_381_MlResult
-> Term s PBuiltinBLS12_381_MlResult
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_MlResult
y

{- | The notion of one (multiplicative identity), and exponentiation by
 - naturals.

= Laws

1. @pone #* x@ @=@ @x@ (@pone@ is the left identity of @#*@)
2. @x #* pone@ @=@ @x@ (@pone@ is the right identity of @#*@)
3. @ppowPositive pone p@ @=@ @pone@ (@pone@ does not scale up)

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

4. @ppowNatural x (ppositiveToNatural # p)@ @=@
   @ppowPositive x p@
5. @ppowNatural x pzero@ @=@ @pone@

@since 1.10.0
-}
class PMultiplicativeSemigroup a => PMultiplicativeMonoid (a :: S -> Type) where
  pone :: forall (s :: S). Term s a
  {-# INLINEABLE ppowNatural #-}
  ppowNatural ::
    forall (s :: S).
    Term s a ->
    Term s PNatural ->
    Term s a
  ppowNatural Term s a
x Term s PNatural
n = Term s PNatural -> (Term s PNatural -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PNatural
n ((Term s PNatural -> Term s a) -> Term s a)
-> (Term s PNatural -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s PNatural
n' ->
    Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PNatural
n' Term s PNatural -> Term s PNatural -> Term s PBool
forall (s :: S). Term s PNatural -> Term s PNatural -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PNatural
forall (s :: S). Term s PNatural
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
      Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone
      (Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s PPositive -> Term s a
ppowPositive Term s a
x (PPositive s -> Term s PPositive
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s PInteger -> PPositive s
forall (s :: S). Term s PInteger -> PPositive s
PPositive (Term s PInteger -> PPositive s) -> Term s PInteger -> PPositive s
forall a b. (a -> b) -> a -> b
$ Term s PNatural -> Term s (PInner PNatural)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PNatural
n')))

-- | @since 1.10.0
instance PMultiplicativeMonoid PPositive where
  {-# INLINEABLE pone #-}
  pone :: forall (s :: S). Term s PPositive
pone = Term s PInteger -> Term s PPositive
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s PInteger -> Term s PPositive)
-> Term s PInteger -> Term s PPositive
forall a b. (a -> b) -> a -> b
$ Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
1

-- | @since 1.10.0
instance PMultiplicativeMonoid PNatural where
  {-# INLINEABLE pone #-}
  pone :: forall (s :: S). Term s PNatural
pone = PNatural s -> Term s PNatural
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PNatural s -> Term s PNatural)
-> (Term s PInteger -> PNatural s)
-> Term s PInteger
-> Term s PNatural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> PNatural s
forall (s :: S). Term s PInteger -> PNatural s
PNatural (Term s PInteger -> Term s PNatural)
-> Term s PInteger -> Term s PNatural
forall a b. (a -> b) -> a -> b
$ Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
1

-- | @since 1.10.0
instance PMultiplicativeMonoid PInteger where
  {-# INLINEABLE pone #-}
  pone :: forall (s :: S). Term s PInteger
pone = Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
1

{- | Partial version of 'ppositive'. Errors if argument is not positive.

@since 1.10.0
-}
ptryPositive :: forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive :: forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive = (forall (s :: S). Term s (PInteger :--> PPositive))
-> Term s (PInteger :--> PPositive)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> PPositive))
 -> Term s (PInteger :--> PPositive))
-> (forall (s :: S). Term s (PInteger :--> PPositive))
-> Term s (PInteger :--> PPositive)
forall a b. (a -> b) -> a -> b
$
  (Term s PInteger -> Term s PPositive)
-> Term s (PInteger :--> PPositive)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PPositive) -> Term s (c :--> PPositive)
plam ((Term s PInteger -> Term s PPositive)
 -> Term s (PInteger :--> PPositive))
-> (Term s PInteger -> Term s PPositive)
-> Term s (PInteger :--> PPositive)
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
i ->
    Term s PBool
-> Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
i Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
0)
      (Term s PString -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
Term s PString -> Term s a -> Term s a
ptraceInfo Term s PString
"ptryPositive: building with non positive" Term s PPositive
forall (s :: S) (a :: S -> Type). Term s a
perror)
      (Term s PInteger -> Term s PPositive
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PInteger
i)

-- | Build a 'PPositive' from a 'PInteger'. Yields 'PNothing' if argument is not positive.
ppositive :: Term s (PInteger :--> PMaybe PPositive)
ppositive :: forall (s :: S). Term s (PInteger :--> PMaybe PPositive)
ppositive = (forall (s :: S). Term s (PInteger :--> PMaybe PPositive))
-> Term s (PInteger :--> PMaybe PPositive)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> PMaybe PPositive))
 -> Term s (PInteger :--> PMaybe PPositive))
-> (forall (s :: S). Term s (PInteger :--> PMaybe PPositive))
-> Term s (PInteger :--> PMaybe PPositive)
forall a b. (a -> b) -> a -> b
$
  (Term s PInteger -> Term s (PMaybe PPositive))
-> Term s (PInteger :--> PMaybe PPositive)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PMaybe PPositive))
-> Term s (c :--> PMaybe PPositive)
plam ((Term s PInteger -> Term s (PMaybe PPositive))
 -> Term s (PInteger :--> PMaybe PPositive))
-> (Term s PInteger -> Term s (PMaybe PPositive))
-> Term s (PInteger :--> PMaybe PPositive)
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
i ->
    Term s PBool
-> Term s (PMaybe PPositive)
-> Term s (PMaybe PPositive)
-> Term s (PMaybe PPositive)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
i Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
0)
      (PMaybe PPositive s -> Term s (PMaybe PPositive)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe PPositive s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)
      (Term s (PMaybe PPositive) -> Term s (PMaybe PPositive))
-> Term s (PMaybe PPositive) -> Term s (PMaybe PPositive)
forall a b. (a -> b) -> a -> b
$ PMaybe PPositive s -> Term s (PMaybe PPositive)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe PPositive s -> Term s (PMaybe PPositive))
-> (PPositive s -> PMaybe PPositive s)
-> PPositive s
-> Term s (PMaybe PPositive)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PPositive -> PMaybe PPositive s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust (Term s PPositive -> PMaybe PPositive s)
-> (PPositive s -> Term s PPositive)
-> PPositive s
-> PMaybe PPositive s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PPositive s -> Term s PPositive
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon
      (PPositive s -> Term s (PMaybe PPositive))
-> PPositive s -> Term s (PMaybe PPositive)
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> PPositive s
forall (s :: S). Term s PInteger -> PPositive s
PPositive Term s PInteger
i

{- | A default implementation of exponentiation-by-squaring with a
strictly-positive exponent.

= Important note

This implementation assumes that the operation argument is associative.

@since 1.10.0
-}
pbySquaringDefault ::
  forall (a :: S -> Type) (s :: S).
  (forall (s' :: S). Term s' a -> Term s' a -> Term s' a) ->
  Term s a ->
  Term s PPositive ->
  Term s a
pbySquaringDefault :: forall (a :: S -> Type) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s a -> Term s PPositive -> Term s a
pbySquaringDefault forall (s' :: S). Term s' a -> Term s' a -> Term s' a
f Term s a
b Term s PPositive
e = Term s (a :--> (PPositive :--> a))
forall (s'' :: S). Term s'' (a :--> (PPositive :--> a))
go Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
b Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
e
  where
    go :: forall (s'' :: S). Term s'' (a :--> PPositive :--> a)
    go :: forall (s'' :: S). Term s'' (a :--> (PPositive :--> a))
go = (forall (s'' :: S). Term s'' (a :--> (PPositive :--> a)))
-> Term s'' (a :--> (PPositive :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s'' :: S). Term s'' (a :--> (PPositive :--> a)))
 -> Term s'' (a :--> (PPositive :--> a)))
-> (forall (s'' :: S). Term s'' (a :--> (PPositive :--> a)))
-> Term s'' (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
   :--> (a :--> (PPositive :--> a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
   :--> (a :--> (PPositive :--> a)))
-> Term
     s ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
-> Term s (a :--> (PPositive :--> a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (a :--> (PPositive :--> a))
 -> Term s a -> Term s PPositive -> Term s a)
-> Term
     s ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s PPositive -> Term s a)
-> Term s (c :--> (a :--> (PPositive :--> a)))
plam ((Term s (a :--> (PPositive :--> a))
  -> Term s a -> Term s PPositive -> Term s a)
 -> Term
      s ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a))))
-> (Term s (a :--> (PPositive :--> a))
    -> Term s a -> Term s PPositive -> Term s a)
-> Term
     s ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (PPositive :--> a))
self Term s a
b Term s PPositive
e -> Term s PPositive -> (Term s PPositive -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
e ((Term s PPositive -> Term s a) -> Term s a)
-> (Term s PPositive -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
e' ->
      Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
e' Term s (PInner PPositive)
-> Term s (PInner PPositive) -> Term s PBool
forall (s :: S).
Term s (PInner PPositive)
-> Term s (PInner PPositive) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
1)
        Term s a
b
        ( Term s a -> (Term s a -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (a :--> (PPositive :--> a))
self Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
b Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: S -> Type). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pquotientInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
e' Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
2)) ((Term s a -> Term s a) -> Term s a)
-> (Term s a -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s a
below ->
            Term s a -> (Term s a -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s a -> Term s a -> Term s a
forall (s' :: S). Term s' a -> Term s' a -> Term s' a
f Term s a
below Term s a
below) ((Term s a -> Term s a) -> Term s a)
-> (Term s a -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s a
res ->
              Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (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))
premainderInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
e' Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
2) Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
1)
                (Term s a -> Term s a -> Term s a
forall (s' :: S). Term s' a -> Term s' a -> Term s' a
f Term s a
b Term s a
res)
                Term s a
res
        )

{- | = Laws

1. @pfromInteger 0@ @=@ @pzero@
2. @pfromInteger 1@ @=@ @pone@
3. @pfromInteger (x + y)@ @=@ @pfromInteger x #+ pfromInteger y@
4. @pfromInteger (x * y)@ @=@ @pfromInteger x #* pfromInteger y@

Additionally, the following \'interaction laws\' must hold between the
instances of 'PAdditiveGroup' and 'PMultiplicativeMonoid' for @a@:

5. @x #* (y #+ z)@ @=@ @(x #* y) #+ (x #* z)@ (@#*@ left-distributes over
   @#+@)
6. @(y #+ z) #* x@ @=@ @(y #* x) #+ (z #* x)@ (@#*@ right-distributes over
   @#+@)

@since 1.10.0
-}
class
  (PAdditiveGroup a, PMultiplicativeMonoid a) =>
  PRing (a :: S -> Type)
  where
  pfromInteger :: forall (s :: S). Integer -> Term s a
  default pfromInteger :: forall (s :: S). PRing (PInner a) => Integer -> Term s a
  pfromInteger Integer
x = Term s (PInner a) -> Term s a
forall (s :: S) (a :: S -> Type). 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
$ Integer -> Term s (PInner a)
forall (s :: S). Integer -> Term s (PInner a)
forall (a :: S -> Type) (s :: S). PRing a => Integer -> Term s a
pfromInteger Integer
x

-- | @since 1.10.0
instance PRing PInteger where
  {-# INLINEABLE pfromInteger #-}
  pfromInteger :: forall (s :: S). Integer -> Term s PInteger
pfromInteger = Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger

{- | = Laws

= Pedantry note

Technically, the requirements here are too strong: we demand an /ordered/
ring, which integral domains don't necessarily have to be. However, in our
case, our hand is forced by expected semantics: in abstract algebra, both the
absolute value and the signum are real numbers (which are always totally
ordered) but in our case, both must be elements of the integral domain
itself. Thus, in order for the laws to make any sense, we have to ensure a
total order on the integral domain. Since all of our integral domains are
\'at least as big\' as the integers, this doesn't pose a huge problem.

@since 1.10.0
-}
class (PRing a, POrd a) => PIntegralDomain (a :: S -> Type) where
  {-# INLINEABLE psignum #-}
  psignum :: forall (s :: S). Term s (a :--> a)
  default psignum :: forall (s :: S). Term s (a :--> a)
  psignum = (forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a)
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s a) -> Term s (a :--> a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a) -> Term s (c :--> a)
plam ((Term s a -> Term s a) -> Term s (a :--> a))
-> (Term s a -> Term s a) -> Term s (a :--> a)
forall a b. (a -> b) -> a -> b
$ \Term s a
x ->
    [(Term s PBool, Term s a)] -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
[(Term s PBool, Term s a)] -> Term s a -> Term s a
pcond
      [ (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero, Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
      , (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero, Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone)
      ]
      Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone
  {-# INLINEABLE pabs #-}
  pabs :: forall (s :: S). Term s (a :--> a)
  default pabs :: forall (s :: S). Term s (a :--> a)
  pabs = (forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a))
-> (forall (s :: S). Term s (a :--> a)) -> Term s (a :--> a)
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s a) -> Term s (a :--> a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a) -> Term s (c :--> a)
plam ((Term s a -> Term s a) -> Term s (a :--> a))
-> (Term s a -> Term s a) -> Term s (a :--> a)
forall a b. (a -> b) -> a -> b
$ \Term s a
x ->
    Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
      (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x)
      Term s a
x

-- | @since 1.10.0
instance PIntegralDomain PInteger where
  {-# INLINEABLE psignum #-}
  psignum :: forall (s :: S). Term s (PInteger :--> PInteger)
psignum = (forall (s :: S). Term s (PInteger :--> PInteger))
-> Term s (PInteger :--> PInteger)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> PInteger))
 -> Term s (PInteger :--> PInteger))
-> (forall (s :: S). Term s (PInteger :--> PInteger))
-> Term s (PInteger :--> PInteger)
forall a b. (a -> b) -> a -> b
$ (Term s PInteger -> Term s PInteger)
-> Term s (PInteger :--> PInteger)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger) -> Term s (c :--> PInteger)
plam ((Term s PInteger -> Term s PInteger)
 -> Term s (PInteger :--> PInteger))
-> (Term s PInteger -> Term s PInteger)
-> Term s (PInteger :--> PInteger)
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
x ->
    [(Term s PBool, Term s PInteger)]
-> Term s PInteger -> Term s PInteger
forall (a :: S -> Type) (s :: S).
[(Term s PBool, Term s a)] -> Term s a -> Term s a
pcond
      [ (Term s PInteger
x Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
0, Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
0)
      , (Term s PInteger
x Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
0, Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger (Integer
-1))
      ]
      (Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
1)

-- orphan instance, but only visibly orphan when importing internal modules
instance PIntegralDomain a => Num (Term s a) where
  {-# INLINEABLE (+) #-}
  + :: Term s a -> Term s a -> Term s a
(+) = 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).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+)
  {-# INLINEABLE (-) #-}
  - :: Term s a -> Term s a -> Term s a
(-) = 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).
PAdditiveGroup a =>
Term s a -> Term s a -> Term s a
(#-)
  {-# INLINEABLE (*) #-}
  * :: Term s a -> Term s a -> Term s a
(*) = 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).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
(#*)
  {-# INLINEABLE abs #-}
  abs :: Term s a -> Term s a
abs Term s a
x = Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
pabs Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x
  {-# INLINEABLE negate #-}
  negate :: Term s a -> Term s a
negate Term s a
x = Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x
  {-# INLINEABLE signum #-}
  signum :: Term s a -> Term s a
signum Term s a
x = Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
psignum Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x
  {-# INLINEABLE fromInteger #-}
  fromInteger :: Integer -> Term s a
fromInteger = Integer -> Term s a
forall (s :: S). Integer -> Term s a
forall (a :: S -> Type) (s :: S). PRing a => Integer -> Term s a
pfromInteger

-- | @since 1.10.0
pdiv :: forall (s :: S). Term s (PInteger :--> PInteger :--> PInteger)
pdiv :: forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv = DefaultFun -> Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S) (a :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.DivideInteger

-- | @since 1.10.0
pmod :: forall (s :: S). Term s (PInteger :--> PInteger :--> PInteger)
pmod :: forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmod = DefaultFun -> Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S) (a :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ModInteger

-- | @since 1.10.0
pquot :: forall (s :: S). Term s (PInteger :--> PInteger :--> PInteger)
pquot :: forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pquot = DefaultFun -> Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S) (a :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.QuotientInteger

-- | @since 1.10.0
prem :: forall (s :: S). Term s (PInteger :--> PInteger :--> PInteger)
prem :: forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
prem = DefaultFun -> Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S) (a :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.RemainderInteger

{- | Specialized form of @pmaybe@ for 'PNatural'. Given a default, and a way to
turn a 'PPositive' into an answer, produce the default when given 'pzero',
and apply the function otherwise.

@since 1.10.0
-}
pnaturalToPositiveCPS ::
  forall (a :: S -> Type) (s :: S).
  Term s a ->
  (Term s PPositive -> Term s a) ->
  Term s PNatural ->
  Term s a
pnaturalToPositiveCPS :: forall (a :: S -> Type) (s :: S).
Term s a
-> (Term s PPositive -> Term s a) -> Term s PNatural -> Term s a
pnaturalToPositiveCPS Term s a
def Term s PPositive -> Term s a
f Term s PNatural
n = Term s PNatural -> (Term s PNatural -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PNatural
n ((Term s PNatural -> Term s a) -> Term s a)
-> (Term s PNatural -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s PNatural
n' ->
  Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
    (Term s PNatural
n' Term s PNatural -> Term s PNatural -> Term s PBool
forall (s :: S). Term s PNatural -> Term s PNatural -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PNatural
forall (s :: S). Term s PNatural
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
    Term s a
def
    (Term s PPositive -> Term s a
f (Term s PPositive -> Term s a)
-> (Term s PNatural -> Term s PPositive)
-> Term s PNatural
-> Term s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PNatural -> Term s PPositive
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s PNatural -> Term s a) -> Term s PNatural -> Term s a
forall a b. (a -> b) -> a -> b
$ Term s PNatural
n)

{- | Partial version of 'pnatural'. Errors if argument is negative.

@since 1.10.0
-}
ptryNatural :: forall (s :: S). Term s (PInteger :--> PNatural)
ptryNatural :: forall (s :: S). Term s (PInteger :--> PNatural)
ptryNatural = (forall (s :: S). Term s (PInteger :--> PNatural))
-> Term s (PInteger :--> PNatural)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> PNatural))
 -> Term s (PInteger :--> PNatural))
-> (forall (s :: S). Term s (PInteger :--> PNatural))
-> Term s (PInteger :--> PNatural)
forall a b. (a -> b) -> a -> b
$ (Term s PInteger -> Term s PNatural)
-> Term s (PInteger :--> PNatural)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PNatural) -> Term s (c :--> PNatural)
plam ((Term s PInteger -> Term s PNatural)
 -> Term s (PInteger :--> PNatural))
-> (Term s PInteger -> Term s PNatural)
-> Term s (PInteger :--> PNatural)
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
i ->
  Term s PBool
-> Term s PNatural -> Term s PNatural -> Term s PNatural
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
    (Term s PInteger
i Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger (Integer
-1))
    (Term s PString -> Term s PNatural -> Term s PNatural
forall (a :: S -> Type) (s :: S).
Term s PString -> Term s a -> Term s a
ptraceInfo Term s PString
"ptryNatural: building with negative" Term s PNatural
forall (s :: S) (a :: S -> Type). Term s a
perror)
    (PNatural s -> Term s PNatural
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PNatural s -> Term s PNatural)
-> (Term s PInteger -> PNatural s)
-> Term s PInteger
-> Term s PNatural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> PNatural s
forall (s :: S). Term s PInteger -> PNatural s
PNatural (Term s PInteger -> Term s PNatural)
-> Term s PInteger -> Term s PNatural
forall a b. (a -> b) -> a -> b
$ Term s PInteger
i)

{- | Build a 'PNatural' from a 'PInteger'. Yields 'PNothing' if given a negative
value.

@since 1.10.0
-}
pnatural :: forall (s :: S). Term s (PInteger :--> PMaybe PNatural)
pnatural :: forall (s :: S). Term s (PInteger :--> PMaybe PNatural)
pnatural = (forall (s :: S). Term s (PInteger :--> PMaybe PNatural))
-> Term s (PInteger :--> PMaybe PNatural)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> PMaybe PNatural))
 -> Term s (PInteger :--> PMaybe PNatural))
-> (forall (s :: S). Term s (PInteger :--> PMaybe PNatural))
-> Term s (PInteger :--> PMaybe PNatural)
forall a b. (a -> b) -> a -> b
$ (Term s PInteger -> Term s (PMaybe PNatural))
-> Term s (PInteger :--> PMaybe PNatural)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PMaybe PNatural))
-> Term s (c :--> PMaybe PNatural)
plam ((Term s PInteger -> Term s (PMaybe PNatural))
 -> Term s (PInteger :--> PMaybe PNatural))
-> (Term s PInteger -> Term s (PMaybe PNatural))
-> Term s (PInteger :--> PMaybe PNatural)
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
i ->
  Term s PBool
-> Term s (PMaybe PNatural)
-> Term s (PMaybe PNatural)
-> Term s (PMaybe PNatural)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
    (Term s PInteger
i Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger (Integer
-1))
    (PMaybe PNatural s -> Term s (PMaybe PNatural)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe PNatural s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)
    (PMaybe PNatural s -> Term s (PMaybe PNatural)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe PNatural s -> Term s (PMaybe PNatural))
-> (Term s PInteger -> PMaybe PNatural s)
-> Term s PInteger
-> Term s (PMaybe PNatural)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PNatural -> PMaybe PNatural s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust (Term s PNatural -> PMaybe PNatural s)
-> (Term s PInteger -> Term s PNatural)
-> Term s PInteger
-> PMaybe PNatural s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PNatural s -> Term s PNatural
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PNatural s -> Term s PNatural)
-> (Term s PInteger -> PNatural s)
-> Term s PInteger
-> Term s PNatural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> PNatural s
forall (s :: S). Term s PInteger -> PNatural s
PNatural (Term s PInteger -> Term s (PMaybe PNatural))
-> Term s PInteger -> Term s (PMaybe PNatural)
forall a b. (a -> b) -> a -> b
$ Term s PInteger
i)

{- | \'Relax\' a 'PPositive' to 'PNatural'. This uses 'punsafeCoerce'
underneath, but because any positive is also a natural, is safe.

@since 1.10.0
-}
ppositiveToNatural :: forall (s :: S). Term s (PPositive :--> PNatural)
ppositiveToNatural :: forall (s :: S). Term s (PPositive :--> PNatural)
ppositiveToNatural = (forall (s :: S). Term s (PPositive :--> PNatural))
-> Term s (PPositive :--> PNatural)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PPositive :--> PNatural))
 -> Term s (PPositive :--> PNatural))
-> (forall (s :: S). Term s (PPositive :--> PNatural))
-> Term s (PPositive :--> PNatural)
forall a b. (a -> b) -> a -> b
$ (Term s PPositive -> Term s PNatural)
-> Term s (PPositive :--> PNatural)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PNatural) -> Term s (c :--> PNatural)
plam ((Term s PPositive -> Term s PNatural)
 -> Term s (PPositive :--> PNatural))
-> (Term s PPositive -> Term s PNatural)
-> Term s (PPositive :--> PNatural)
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
x -> Term s PPositive -> Term s PNatural
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PPositive
x