{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Plutarch.Internal.Numeric (
PPositive,
Positive,
PAdditiveSemigroup (..),
PAdditiveMonoid (..),
PAdditiveGroup (..),
PMultiplicativeSemigroup (..),
PMultiplicativeMonoid (..),
PRing (..),
PIntegralDomain (..),
ptryPositive,
ppositive,
pbySquaringDefault,
pdiv,
pmod,
pquot,
prem,
) where
import Data.Coerce (coerce)
import Data.Kind (Type)
import GHC.Generics (Generic)
import Plutarch.Builtin.BLS (
PBuiltinBLS12_381_G1_Element,
PBuiltinBLS12_381_G2_Element,
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,
)
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,
PLiftable,
PLifted (PLifted),
)
import Plutarch.Internal.Newtype (PlutusTypeNewtype)
import Plutarch.Internal.Ord (POrd ((#<=)))
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
DerivePlutusType (DPTStrat),
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
newtype PPositive (s :: S) = PPositive (Term s PInteger)
deriving stock
(
(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
(
(forall (s :: S). PPositive s -> Term s (PInner PPositive))
-> (forall (s :: S) (b :: PType).
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 :: PType).
Term s (PInner PPositive) -> (PPositive s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
$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 :: PType).
Term s (PInner PPositive) -> (PPositive s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PPositive) -> (PPositive s -> Term s b) -> Term s b
PlutusType
,
(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 :: PType).
(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
,
(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 :: PType).
(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
,
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 :: PType).
PEq t =>
(forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> POrd t
$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
)
instance DerivePlutusType PPositive where
type DPTStrat _ = PlutusTypeNewtype
deriving via
DeriveNewtypePLiftable PPositive PInteger Positive
instance
PLiftable PPositive
newtype Positive = UnsafeMkPositive {Positive -> Integer
getPositive :: Integer}
deriving stock
(
Int -> Positive -> ShowS
[Positive] -> ShowS
Positive -> String
(Int -> Positive -> ShowS)
-> (Positive -> String) -> ([Positive] -> ShowS) -> Show Positive
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Positive -> ShowS
showsPrec :: Int -> Positive -> ShowS
$cshow :: Positive -> String
show :: Positive -> String
$cshowList :: [Positive] -> ShowS
showList :: [Positive] -> ShowS
Show
,
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
,
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
(
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
(
(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
,
(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
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
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 :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner a) -> Term s a) -> Term s (PInner a) -> Term s a
forall a b. (a -> b) -> a -> b
$ Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s a
x Term s (PInner a) -> Term s (PInner a) -> Term s (PInner a)
forall (s :: S).
Term s (PInner a) -> Term s (PInner a) -> Term s (PInner a)
forall (a :: PType) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s a
y
{-# INLINEABLE pscalePositive #-}
pscalePositive ::
forall (s :: S).
Term s (a :--> PPositive :--> a)
pscalePositive = (forall (s :: S). Term s (a :--> (PPositive :--> a)))
-> Term s (a :--> (PPositive :--> a))
forall (a :: PType) (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 -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PPositive -> Term s a)
-> Term s (c :--> (PPositive :--> a))
plam ((Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a)))
-> (Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
b Term s PPositive
e ->
(forall (s :: S). Term s a -> Term s a -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall (a :: PType) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s (a :--> (PPositive :--> a))
pbySquaringDefault Term s' a -> Term s' a -> Term s' a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: PType) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+) Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
e
infix 6 #+
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 :: PType) (a :: PType) (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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
y
{-# INLINEABLE pscalePositive #-}
pscalePositive :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
pscalePositive = DefaultFun -> Term s (PPositive :--> (PPositive :--> PPositive))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MultiplyInteger
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y
{-# INLINEABLE pscalePositive #-}
pscalePositive :: forall (s :: S). Term s (PInteger :--> (PPositive :--> PInteger))
pscalePositive = DefaultFun -> Term s (PInteger :--> (PPositive :--> PInteger))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MultiplyInteger
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element))
pscalePositive = (forall (s :: S).
Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element)))
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element)))
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element)))
-> (forall (s :: S).
Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element)))
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element))
forall a b. (a -> b) -> a -> b
$ (Term s PBuiltinBLS12_381_G1_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G1_Element)
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c
-> Term s PPositive -> Term s PBuiltinBLS12_381_G1_Element)
-> Term s (c :--> (PPositive :--> PBuiltinBLS12_381_G1_Element))
plam ((Term s PBuiltinBLS12_381_G1_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G1_Element)
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element)))
-> (Term s PBuiltinBLS12_381_G1_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G1_Element)
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PPositive :--> PBuiltinBLS12_381_G1_Element))
forall a b. (a -> b) -> a -> b
$ \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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
p Term
s (PBuiltinBLS12_381_G1_Element :--> PBuiltinBLS12_381_G1_Element)
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
x
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element))
pscalePositive = (forall (s :: S).
Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element)))
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element)))
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element)))
-> (forall (s :: S).
Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element)))
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element))
forall a b. (a -> b) -> a -> b
$ (Term s PBuiltinBLS12_381_G2_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G2_Element)
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c
-> Term s PPositive -> Term s PBuiltinBLS12_381_G2_Element)
-> Term s (c :--> (PPositive :--> PBuiltinBLS12_381_G2_Element))
plam ((Term s PBuiltinBLS12_381_G2_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G2_Element)
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element)))
-> (Term s PBuiltinBLS12_381_G2_Element
-> Term s PPositive -> Term s PBuiltinBLS12_381_G2_Element)
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PPositive :--> PBuiltinBLS12_381_G2_Element))
forall a b. (a -> b) -> a -> b
$ \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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
p Term
s (PBuiltinBLS12_381_G2_Element :--> PBuiltinBLS12_381_G2_Element)
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
x
class PAdditiveSemigroup a => PAdditiveMonoid (a :: S -> Type) where
pzero :: forall (s :: S). Term s a
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
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
forall (s :: S). Term s PByteString
pbls12_381_G1_compressed_zero
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
forall (s :: S). Term s PByteString
pbls12_381_G2_compressed_zero
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 :: PType) (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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 :: PType) (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 :: PType) (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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 :: PType) (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 :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y)
{-# INLINEABLE pscaleInteger #-}
pscaleInteger :: forall (s :: S). Term s (a :--> PInteger :--> a)
pscaleInteger = (forall (s :: S). Term s (a :--> (PInteger :--> a)))
-> Term s (a :--> (PInteger :--> a))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (a :--> (PInteger :--> a)))
-> Term s (a :--> (PInteger :--> a)))
-> (forall (s :: S). Term s (a :--> (PInteger :--> a)))
-> Term s (a :--> (PInteger :--> a))
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s PInteger -> Term s a)
-> Term s (a :--> (PInteger :--> a))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PInteger -> Term s a)
-> Term s (c :--> (PInteger :--> a))
plam ((Term s a -> Term s PInteger -> Term s a)
-> Term s (a :--> (PInteger :--> a)))
-> (Term s a -> Term s PInteger -> Term s a)
-> Term s (a :--> (PInteger :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
b Term s PInteger
e ->
Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: PType) (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 :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero)
Term s a
forall (s :: S). Term s a
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero
( Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: PType) (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 :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero)
(Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (a :--> (PPositive :--> a))
forall (s :: S). Term s (a :--> (PPositive :--> a))
forall (a :: PType) (s :: S).
PAdditiveSemigroup a =>
Term s (a :--> (PPositive :--> a))
pscalePositive Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner PPositive :--> PInner PPositive)
forall (s :: S). Term s (PInner PPositive :--> PInner PPositive)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (PInner PPositive :--> PInner PPositive)
-> Term s (PInner PPositive) -> Term s (PInner PPositive)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
Term s (PInner PPositive)
e))
(Term s (a :--> (PPositive :--> a))
forall (s :: S). Term s (a :--> (PPositive :--> a))
forall (a :: PType) (s :: S).
PAdditiveSemigroup a =>
Term s (a :--> (PPositive :--> a))
pscalePositive Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast Term s PInteger
Term s (PInner PPositive)
e)
)
infix 6 #-
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y
{-# INLINEABLE pscaleInteger #-}
pscaleInteger :: forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pscaleInteger = Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmultiplyInteger
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
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element))
pscaleInteger = (forall (s :: S).
Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element)))
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element)))
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element)))
-> (forall (s :: S).
Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element)))
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element))
forall a b. (a -> b) -> a -> b
$ (Term s PBuiltinBLS12_381_G1_Element
-> Term s PInteger -> Term s PBuiltinBLS12_381_G1_Element)
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c
-> Term s PInteger -> Term s PBuiltinBLS12_381_G1_Element)
-> Term s (c :--> (PInteger :--> PBuiltinBLS12_381_G1_Element))
plam ((Term s PBuiltinBLS12_381_G1_Element
-> Term s PInteger -> Term s PBuiltinBLS12_381_G1_Element)
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element)))
-> (Term s PBuiltinBLS12_381_G1_Element
-> Term s PInteger -> Term s PBuiltinBLS12_381_G1_Element)
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PInteger :--> PBuiltinBLS12_381_G1_Element))
forall a b. (a -> b) -> a -> b
$ \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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
b
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
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element))
pscaleInteger = (forall (s :: S).
Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element)))
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element)))
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element)))
-> (forall (s :: S).
Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element)))
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element))
forall a b. (a -> b) -> a -> b
$ (Term s PBuiltinBLS12_381_G2_Element
-> Term s PInteger -> Term s PBuiltinBLS12_381_G2_Element)
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c
-> Term s PInteger -> Term s PBuiltinBLS12_381_G2_Element)
-> Term s (c :--> (PInteger :--> PBuiltinBLS12_381_G2_Element))
plam ((Term s PBuiltinBLS12_381_G2_Element
-> Term s PInteger -> Term s PBuiltinBLS12_381_G2_Element)
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element)))
-> (Term s PBuiltinBLS12_381_G2_Element
-> Term s PInteger -> Term s PBuiltinBLS12_381_G2_Element)
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PInteger :--> PBuiltinBLS12_381_G2_Element))
forall a b. (a -> b) -> a -> b
$ \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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
b
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 :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner a) -> Term s a) -> Term s (PInner a) -> Term s a
forall a b. (a -> b) -> a -> b
$ Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s a
x Term s (PInner a) -> Term s (PInner a) -> Term s (PInner a)
forall (s :: S).
Term s (PInner a) -> Term s (PInner a) -> Term s (PInner a)
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s a
y
{-# INLINEABLE ppowPositive #-}
ppowPositive ::
forall (s :: S).
Term s (a :--> PPositive :--> a)
ppowPositive = (forall (s :: S). Term s (a :--> (PPositive :--> a)))
-> Term s (a :--> (PPositive :--> a))
forall (a :: PType) (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 -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PPositive -> Term s a)
-> Term s (c :--> (PPositive :--> a))
plam ((Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a)))
-> (Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s PPositive
p ->
(forall (s :: S). Term s a -> Term s a -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall (a :: PType) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s (a :--> (PPositive :--> a))
pbySquaringDefault Term s' a -> Term s' a -> Term s' a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
(#*) Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
p
infix 6 #*
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 :: PType) (a :: PType) (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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
y
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y
class PMultiplicativeSemigroup a => PMultiplicativeMonoid (a :: S -> Type) where
pone :: forall (s :: S). Term s a
instance PMultiplicativeMonoid PPositive where
{-# INLINEABLE pone #-}
pone :: forall (s :: S). Term s PPositive
pone = Term s PInteger -> Term s PPositive
forall (b :: PType) (a :: PType) (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
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
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 :: PType) (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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 :: PType) (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 :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero)
(Term s PString -> Term s PPositive -> Term s PPositive
forall (a :: PType) (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 :: PType). Term s a
perror)
(Term s PInteger -> Term s PPositive
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s PInteger
i)
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 :: PType) (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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 :: PType) (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 :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero)
(PMaybe PPositive s -> Term s (PMaybe PPositive)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe PPositive s
forall (a :: PType) (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 :: PType) (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 :: PType) (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 :: PType) (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
pbySquaringDefault ::
forall (a :: S -> Type) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a) ->
Term s (a :--> PPositive :--> a)
pbySquaringDefault :: forall (a :: PType) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s (a :--> (PPositive :--> a))
pbySquaringDefault forall (s' :: S). Term s' a -> Term s' a -> Term s' a
f = ClosedTerm (a :--> (PPositive :--> a))
-> Term s (a :--> (PPositive :--> a))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PPositive :--> a))
-> Term s (a :--> (PPositive :--> a)))
-> ClosedTerm (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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 PBool -> Term s a -> Term s a -> Term s a
forall (a :: PType) (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 :: PType). 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 :: PType) (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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: PType). 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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
e Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# 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 :: PType) (b :: PType).
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 :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
((Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
premainderInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). 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 :: PType) (b :: PType).
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 :: PType) (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
)
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 :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner a) -> Term s a) -> Term s (PInner a) -> Term s a
forall a b. (a -> b) -> a -> b
$ Integer -> Term s (PInner a)
forall (s :: S). Integer -> Term s (PInner a)
forall (a :: PType) (s :: S). PRing a => Integer -> Term s a
pfromInteger Integer
x
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
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 :: PType) (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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 :: PType) (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 :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
forall (s :: S). Term s a
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero, Term s a
forall (s :: S). Term s a
forall (a :: PType) (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 :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
forall (s :: S). Term s a
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero, Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
forall (s :: S). Term s a
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone)
]
Term s a
forall (s :: S). Term s a
forall (a :: PType) (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 :: PType) (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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 :: PType) (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 :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
forall (s :: S). Term s a
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero)
(Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x)
Term s a
x
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 :: PType) (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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 :: PType) (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 :: PType) (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 :: PType) (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)
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 :: PType) (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 :: PType) (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 :: PType) (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 :: PType) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
pabs Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
psignum Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (s :: S). PRing a => Integer -> Term s a
pfromInteger
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 :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.DivideInteger
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 :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ModInteger
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 :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.QuotientInteger
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 :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.RemainderInteger