{-# LANGUAGE QuantifiedConstraints #-}

module Plutarch.Extra.Numeric (peven, (#^)) where

import Plutarch.Extra.TermCont (pletC)
import Plutarch.Num (PNum)

-- | @since 1.0.0
peven ::
  forall (a :: S -> Type) (s :: S).
  (PIntegral a, PEq a, PNum a) =>
  Term s (a :--> PBool)
peven :: forall (a :: S -> Type) (s :: S).
(PIntegral a, PEq a, PNum a) =>
Term s (a :--> PBool)
peven = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> (forall (a :: S -> Type) (s :: S).
PIntegral a =>
Term s (a :--> (a :--> a))
prem forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
2) forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
0

ppowIntegral ::
  forall (s :: S) (n :: S -> Type) (e :: S -> Type).
  (PNum n, PNum e, PEq e, PIntegral e) =>
  Term s (n :--> e :--> n)
ppowIntegral :: forall (s :: S) (n :: S -> Type) (e :: S -> Type).
(PNum n, PNum e, PEq e, PIntegral e) =>
Term s (n :--> (e :--> n))
ppowIntegral =
  forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s n
x Term s e
n ->
      forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s e
n forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s e
0) Term s n
1 forall a b. (a -> b) -> a -> b
$ forall {s :: S}. Term s (n :--> (e :--> n))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s n
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s e
n
  where
    go :: Term s (n :--> (e :--> n))
go = forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (n :--> (e :--> n))
self Term s n
x Term s e
n ->
      forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s e
n forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s e
1) Term s n
x forall a b. (a -> b) -> a -> b
$
        forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
          Term s n
next <- forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC forall a b. (a -> b) -> a -> b
$ Term s (n :--> (e :--> n))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s n
x forall a. Num a => a -> a -> a
* Term s n
x) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (a :: S -> Type) (s :: S).
PIntegral a =>
Term s (a :--> (a :--> a))
pdiv forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s e
n forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s e
2)
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
              (forall (a :: S -> Type) (s :: S).
(PIntegral a, PEq a, PNum a) =>
Term s (a :--> PBool)
peven forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s e
n)
              Term s n
next
              (Term s n
x forall a. Num a => a -> a -> a
* Term s n
next)

{- | Power to a 'PIntegral' exponent. Exponent must be @>= 0@. Only use this if
 the exponent isn't statically known!

 Performance note: Haskell '(^)' already works for Plutarch if the exponent is
 'Integral' (can just be 'Int' or 'Integer', if known statically), and the base
 is in 'Num', which is the case for most/all Plutarch numeric types. It probably
 performs better, due to the exponent calculations being done ahead of time.

 Performance note: When working with `PRational', you most likely want to use
 the 'Plutarch.Extra.PRationalNoReduce' wrapper to prevent reducing after each
 internal multiplication.

 @since 3.12.2
-}
(#^) ::
  forall (s :: S) (n :: S -> Type) (e :: S -> Type).
  (PNum n, PNum e, PEq e, PIntegral e) =>
  Term s n ->
  Term s e ->
  Term s n
Term s n
n #^ :: forall (s :: S) (n :: S -> Type) (e :: S -> Type).
(PNum n, PNum e, PEq e, PIntegral e) =>
Term s n -> Term s e -> Term s n
#^ Term s e
e = forall (s :: S) (n :: S -> Type) (e :: S -> Type).
(PNum n, PNum e, PEq e, PIntegral e) =>
Term s (n :--> (e :--> n))
ppowIntegral forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s n
n forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s e
e

infixr 8 #^