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

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

import Data.Coerce (coerce)
import Data.Functor.Const (Const)
import Data.Text (pack)
import GHC.Generics (Generic)
import Plutarch.Builtin (PAsData, PData, PIsData, pdata)
import Plutarch.Builtin.Bool (pif)
import Plutarch.Integer (PInteger, PIntegral)
import Plutarch.Internal.Eq (PEq)
import Plutarch.Internal.Lift (DeriveNewtypePLiftable, PLiftable, PLifted (PLifted))
import Plutarch.Internal.Newtype (PlutusTypeNewtype)
import Plutarch.Internal.Ord (POrd, PPartialOrd ((#<=)))
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  DerivePlutusType (DPTStrat),
  PlutusType,
  pcon,
 )
import Plutarch.Internal.Term (
  S,
  Term,
  phoistAcyclic,
  plet,
  pthrow,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Internal.TermCont (runTermCont, tcont)
import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Num (PNum (pfromInteger, (#-)))
import Plutarch.Show (PShow, pshow)
import Plutarch.Trace (ptraceInfoError)
import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'), ptryFrom)
import Prettyprinter (Pretty)
import Test.QuickCheck (
  Arbitrary,
  CoArbitrary,
  Function (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 PBool)
-> (forall (s :: S).
    Term s PPositive -> Term s PPositive -> Term s PBool)
-> PPartialOrd 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)
-> (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
$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
$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
PPartialOrd
    , PPartialOrd PPositive
PPartialOrd PPositive =>
(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 PPositive
forall (t :: PType).
PPartialOrd t =>
(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
$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
    , (forall (s :: S).
 Term s (PPositive :--> (PPositive :--> PPositive)))
-> (forall (s :: S).
    Term s (PPositive :--> (PPositive :--> PPositive)))
-> (forall (s :: S).
    Term s (PPositive :--> (PPositive :--> PPositive)))
-> (forall (s :: S).
    Term s (PPositive :--> (PPositive :--> PPositive)))
-> PIntegral PPositive
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
$cpdiv :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
pdiv :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
$cpmod :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
pmod :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
$cpquot :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
pquot :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
$cprem :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
prem :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
PIntegral
    , (forall (s :: S). Bool -> Term s PPositive -> Term s PString)
-> PShow PPositive
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
$cpshow' :: forall (s :: S). Bool -> Term s PPositive -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s PPositive -> Term s PString
PShow
    )

instance DerivePlutusType PPositive where
  type DPTStrat _ = PlutusTypeNewtype

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

instance PNum PPositive where
  Term s PPositive
x #- :: forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
#- Term s PPositive
y = Term s (PInteger :--> PPositive)
forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive Term s (PInteger :--> PPositive)
-> Term s PInteger -> Term s PPositive
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 (PInner PPositive)
-> Term s (PInner PPositive) -> Term s (PInner PPositive)
forall (s :: S).
Term s (PInner PPositive)
-> Term s (PInner PPositive) -> Term s (PInner PPositive)
forall (a :: PType) (s :: S).
PNum a =>
Term s a -> Term s a -> Term s a
#- Term s PPositive -> Term s (PInner PPositive)
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 =
        Text -> Term s PPositive
forall (s :: S) (a :: PType). HasCallStack => Text -> Term s a
pthrow (Text -> Term s PPositive) -> Text -> Term s PPositive
forall a b. (a -> b) -> a -> b
$
          Text
"PPositive.pfromInteger: encountered non positive: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
pack (Integer -> String
forall a. Show a => a -> String
show Integer
x)
    | Bool
otherwise = PPositive s -> Term s PPositive
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PPositive s -> Term s PPositive)
-> PPositive s -> Term s 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 -> PPositive s) -> Term s PInteger -> PPositive s
forall a b. (a -> b) -> a -> b
$ Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
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 = TermCont
  @r
  s
  (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
-> ((Term s PPositive,
     Reduce (PTryFromExcess PInteger PPositive s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
 -> ((Term s PPositive,
      Reduce (PTryFromExcess PInteger PPositive s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
-> ((Term s PPositive,
     Reduce (PTryFromExcess PInteger PPositive s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
-> TermCont
     @r
     s
     (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PInteger :--> PPositive)
forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive Term s (PInteger :--> PPositive)
-> Term s PInteger -> Term s PPositive
forall (s :: S) (a :: PType) (b :: PType).
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 x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x)
-> (forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b)
-> Generic (Flip @k @k f a b)
forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x
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
$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
from :: forall 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
to :: forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b
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 = TermCont
  @r
  s
  (Term s (PAsData PPositive),
   Reduce (PTryFromExcess PData (PAsData PPositive) s))
-> ((Term s (PAsData PPositive),
     Reduce (PTryFromExcess PData (PAsData PPositive) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PPositive),
    Reduce (PTryFromExcess PData (PAsData PPositive) s))
 -> ((Term s (PAsData PPositive),
      Reduce (PTryFromExcess PData (PAsData PPositive) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PPositive),
      Reduce (PTryFromExcess PData (PAsData PPositive) s))
-> ((Term s (PAsData PPositive),
     Reduce (PTryFromExcess PData (PAsData PPositive) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    (Term s (PAsData PInteger)
_, Term s PInteger
i) <- (((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
 -> Term s r)
-> TermCont @r s (Term s (PAsData PInteger), Term s PInteger)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
  -> Term s r)
 -> TermCont @r s (Term s (PAsData PInteger), Term s PInteger))
-> (((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
    -> Term s r)
-> TermCont @r s (Term s (PAsData PInteger), Term s PInteger)
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 <- ((Term s PPositive -> Term s r) -> Term s r)
-> TermCont @r s (Term s PPositive)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PPositive -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PPositive))
-> (Term s PPositive -> (Term s PPositive -> Term s r) -> Term s r)
-> Term s PPositive
-> TermCont @r s (Term s PPositive)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PPositive -> (Term s PPositive -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PPositive -> TermCont @r s (Term s PPositive))
-> Term s PPositive -> TermCont @r s (Term s PPositive)
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> PPositive)
forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive Term s (PInteger :--> PPositive)
-> Term s PInteger -> Term s PPositive
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
i
    Term s (PAsData PPositive)
resData <- ((Term s (PAsData PPositive) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PAsData PPositive))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PAsData PPositive) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PAsData PPositive)))
-> (Term s (PAsData PPositive)
    -> (Term s (PAsData PPositive) -> Term s r) -> Term s r)
-> Term s (PAsData PPositive)
-> TermCont @r s (Term s (PAsData PPositive))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData PPositive)
-> (Term s (PAsData PPositive) -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PAsData PPositive)
 -> TermCont @r s (Term s (PAsData PPositive)))
-> Term s (PAsData PPositive)
-> TermCont @r s (Term s (PAsData PPositive))
forall a b. (a -> b) -> a -> b
$ Term s PPositive -> Term s (PAsData PPositive)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PPositive
res
    (Term s (PAsData PPositive), Term s PPositive)
-> TermCont @r s (Term s (PAsData PPositive), Term s PPositive)
forall a. a -> TermCont @r s a
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 (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0)
      (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

-- | Partial version of 'PPositive'. Errors if argument is zero.
ptryPositive :: 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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0)
      (Term s PString -> Term s PPositive
forall (a :: PType) (s :: S). Term s PString -> Term s a
ptraceInfoError (Term s PString -> Term s PPositive)
-> Term s PString -> Term s PPositive
forall a b. (a -> b) -> a -> b
$ Term s PString
"ptryPositive: building with non positive: " Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PInteger -> Term s PString
forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow Term s PInteger
i)
      (Term s PPositive -> Term s PPositive)
-> Term s PPositive -> Term s PPositive
forall a b. (a -> b) -> a -> b
$ PPositive s -> Term s PPositive
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon
      (PPositive s -> Term s PPositive)
-> PPositive s -> Term s 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

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

-- | @since WIP
deriving via (QuickCheck.Positive Integer) instance Arbitrary Positive

-- | @since WIP
deriving via Integer instance CoArbitrary Positive

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

-- | @since WIP
deriving via Integer instance Pretty Positive

-- | @since WIP
mkPositive :: Integer -> Maybe Positive
mkPositive :: Integer -> Maybe Positive
mkPositive Integer
n
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Positive -> Maybe Positive
forall a. a -> Maybe a
Just (Positive -> Maybe Positive) -> Positive -> Maybe Positive
forall a b. (a -> b) -> a -> b
$ Integer -> Positive
UnsafeMkPositive Integer
n
  | Bool
otherwise = Maybe Positive
forall a. Maybe a
Nothing