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

module Plutarch.Positive (PPositive, ppositive, ptryPositive) where

import Data.Functor.Const (Const)
import Data.Text (pack)
import GHC.Generics (Generic)

import Plutarch.Bool (PEq, POrd, PPartialOrd, pif, (#<=))
import Plutarch.Builtin (PAsData, PData, PIsData, pdata)
import Plutarch.Integer (PInteger, PIntegral)

import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Show (PShow, pshow)

import Plutarch (
  DerivePlutusType (DPTStrat),
  PlutusType,
  PlutusTypeNewtype,
  Term,
  TermCont (runTermCont),
  pcon,
  phoistAcyclic,
  plam,
  plet,
  pthrow,
  pto,
  (#),
  (#$),
  type (:-->),
 )
import Plutarch.Num (PNum (pfromInteger, (#-)))
import Plutarch.TermCont (tcont)
import Plutarch.Trace (ptraceError)
import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'), ptryFrom)

newtype PPositive s = PPositive (Term s PInteger)
  deriving stock (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
$cto :: forall (s :: S) x. Rep (PPositive s) x -> PPositive s
$cfrom :: forall (s :: S) x. PPositive s -> Rep (PPositive s) x
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
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
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PPositive) -> (PPositive s -> Term s b) -> Term s b
$cpmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PPositive) -> (PPositive s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PPositive s -> Term s (PInner PPositive)
$cpcon' :: forall (s :: S). PPositive s -> Term s (PInner PPositive)
PlutusType, 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
pdataImpl :: forall (s :: S). Term s PPositive -> Term s PData
$cpdataImpl :: forall (s :: S). Term s PPositive -> Term s PData
pfromDataImpl :: forall (s :: S). Term s (PAsData PPositive) -> Term s PPositive
$cpfromDataImpl :: forall (s :: S). Term s (PAsData PPositive) -> Term s PPositive
PIsData, 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
#== :: 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
PEq, PEq PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PBool
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)
-> PPartialOrd t
#< :: 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
$c#<= :: forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PBool
PPartialOrd, PPartialOrd PPositive
forall (t :: PType). PPartialOrd t -> POrd t
POrd, forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
forall (a :: PType).
(forall (s :: S). Term s (a :--> (a :--> a)))
-> (forall (s :: S). Term s (a :--> (a :--> a)))
-> (forall (s :: S). Term s (a :--> (a :--> a)))
-> (forall (s :: S). Term s (a :--> (a :--> a)))
-> PIntegral a
prem :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
$cprem :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
pquot :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
$cpquot :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
pmod :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
$cpmod :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
pdiv :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
$cpdiv :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
PIntegral, forall (s :: S). Bool -> Term s PPositive -> Term s PString
forall (t :: PType).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
pshow' :: forall (s :: S). Bool -> Term s PPositive -> Term s PString
$cpshow' :: forall (s :: S). Bool -> Term s PPositive -> Term s PString
PShow)
instance DerivePlutusType PPositive where type DPTStrat _ = PlutusTypeNewtype

instance PNum PPositive where
  Term s PPositive
x #- :: forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
#- Term s PPositive
y = forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
x forall (a :: PType) (s :: S).
PNum a =>
Term s a -> Term s a -> Term s a
#- forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
y

  pfromInteger :: forall (s :: S). Integer -> Term s PPositive
pfromInteger Integer
x
    | Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
0 =
        forall (s :: S) (a :: PType). HasCallStack => Text -> Term s a
pthrow forall a b. (a -> b) -> a -> b
$
          Text
"PPositive.pfromInteger: encountered non positive: " forall a. Semigroup a => a -> a -> a
<> String -> Text
pack (forall a. Show a => a -> String
show Integer
x)
    | Bool
otherwise = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PPositive s
PPositive forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PNum a => Integer -> Term s a
pfromInteger Integer
x

instance PTryFrom PInteger PPositive where
  type PTryFromExcess PInteger PPositive = Const ()
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PInteger
-> ((Term s PPositive,
     Reduce (PTryFromExcess PInteger PPositive s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PInteger
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
opq, ())

newtype Flip f a b = Flip (f b a) deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
$cto :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
$cfrom :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
Generic)

instance PTryFrom PData (PAsData PPositive) where
  type PTryFromExcess PData (PAsData PPositive) = Flip Term PPositive
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData PPositive),
     Reduce (PTryFromExcess PData (PAsData PPositive) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    (Term s (PAsData PInteger)
_, Term s PInteger
i) <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PInteger) Term s PData
opq
    Term s PPositive
res <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
i
    Term s (PAsData PPositive)
resData <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PPositive
res
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PAsData PPositive)
resData, Term s PPositive
res)

-- | 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 (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PInteger
i ->
    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
i forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0)
      (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (s :: S). PMaybe a s
PNothing)
      forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). Term s a -> PMaybe a s
PJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon
      forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PPositive s
PPositive Term s PInteger
i

-- | Partial version of 'PPositive'. Errors if argument is zero.
ptryPositive :: Term s (PInteger :--> PPositive)
ptryPositive :: forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PInteger
i ->
    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
i forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0)
      (forall (s :: S) (a :: PType). Term s PString -> Term s a
ptraceError forall a b. (a -> b) -> a -> b
$ Term s PString
"ptryPositive: building with non positive: " forall a. Semigroup a => a -> a -> a
<> forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow Term s PInteger
i)
      forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon
      forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> PPositive s
PPositive Term s PInteger
i