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

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

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

  -- * Functions
  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

-- | @since WIP
newtype PPositive (s :: S) = PPositive (Term s PInteger)
  deriving stock
    ( -- | @since WIP
      (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 WIP
      (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
    , -- | @since WIP
      (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
    , -- | @since WIP
      (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
    , -- | @since WIP
      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
    )

-- | @since WIP
instance DerivePlutusType PPositive where
  type DPTStrat _ = PlutusTypeNewtype

-- | @since WIP
deriving via
  DeriveNewtypePLiftable PPositive PInteger Positive
  instance
    PLiftable PPositive

-- | @since WIP
newtype Positive = UnsafeMkPositive {Positive -> Integer
getPositive :: Integer}
  deriving stock
    ( -- | @since WIP
      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
    , -- | @since WIP
      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 WIP
      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 WIP
      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 WIP
      (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 WIP
      (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 WIP
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

{- | The addition operation.

= 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 WIP
-}
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 #-}

  -- | This defaults to exponentiation-by-squaring, which in general is the best
  -- we can do.
  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

-- | @since WIP
infix 6 #+

-- | @since WIP
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

-- | @since WIP
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

-- | @since WIP
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

-- | @since WIP
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

{- | The notion of zero, as well as a (kind of) reversal of 'pscalePositive',
similar to floor division by positive integers.

= Laws

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

@since WIP
-}
class PAdditiveSemigroup a => PAdditiveMonoid (a :: S -> Type) where
  pzero :: forall (s :: S). Term s a

-- | @since WIP
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

-- | @since WIP
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

-- | @since WIP
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

{- | 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 WIP
-}
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)
      )

-- | @since WIP
infix 6 #-

-- | @since WIP
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

-- | @since WIP
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

-- | @since WIP
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

{- | 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)@ @=@
   @pscalePositive # x # (n #+ m)@
5. @ppowPositive # (ppowPositive # x # n) # m@ @=@
   @pscalePositive # 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 WIP
-}
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

-- | @since WIP
infix 6 #*

-- | @since WIP
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

-- | @since WIP
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

{- | The notion of one (multiplicative identity).

= Laws

1. @pone #* x@ @=@ @x@ (@pone@ is the left identity of @#*@)
2. @x #* pone@ @=@ @x@ (@pone@ is the right identity of @#*@)

@since WIP
-}
class PMultiplicativeSemigroup a => PMultiplicativeMonoid (a :: S -> Type) where
  pone :: forall (s :: S). Term s a

-- | @since WIP
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

-- | @since WIP
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 zero.

@since WIP
-}
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)

-- | Build a 'PPositive' from a 'PInteger'. Yields 'PNothing' if argument is zero.
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

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

= Important note

This implementation assumes that the operation argument is associative.

@since WIP
-}
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 ->
  -- We know that we can never have a value less than 1 for e, due to the type
  -- constraint. Thus, we make two assumptions:
  --
  -- 1. The stopping condition is equality to 1
  -- 2. The exponent is never negative
  --
  -- This allows us to use `pquot` and `prem` instead of `pdiv` and `pmod`,
  -- which is a bit faster.
  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
    )

{- | = 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 WIP
-}
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

-- | @since WIP
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 WIP
-}
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

-- | @since WIP
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)

-- 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 :: 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

-- | @since WIP
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

-- | @since WIP
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

-- | @since WIP
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

-- | @since WIP
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