Skip to content

Commit

Permalink
Use PPositive rather than PNonZero for PRational
Browse files Browse the repository at this point in the history
  • Loading branch information
TotallyNotChase committed Jul 12, 2022
1 parent 74b01ac commit 8a5973e
Show file tree
Hide file tree
Showing 10 changed files with 142 additions and 141 deletions.
78 changes: 0 additions & 78 deletions Plutarch/NonZero.hs

This file was deleted.

79 changes: 79 additions & 0 deletions Plutarch/Positive.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

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

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

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

import Plutarch.Maybe (PMaybe (PJust, PNothing))

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

newtype PPositive s = PPositive (Term s PInteger)
deriving stock (Generic)
deriving anyclass (PlutusType, PIsData, PEq, POrd, PIntegral, PShow)
instance DerivePlutusType PPositive where type DPTStrat _ = PlutusTypeNewtype

instance PNum PPositive where
x #- y = ptryPositive #$ pto x #- pto y

pfromInteger x
| x <= 0 = pthrow "PPositive.pfromInteger: encountered non positive"
| otherwise = pcon $ PPositive $ pfromInteger x

instance PTryFrom PInteger PPositive where
type PTryFromExcess PInteger PPositive = Const ()
ptryFrom' opq = runTermCont $ pure (ptryPositive # opq, ())

newtype Flip f a b = Flip (f b a) deriving stock (Generic)

instance PTryFrom PData (PAsData PPositive) where
type PTryFromExcess PData (PAsData PPositive) = Flip Term PPositive
ptryFrom' opq = runTermCont $ do
(_, i) <- tcont $ ptryFrom @(PAsData PInteger) opq
res <- tcont . plet $ ptryPositive # i
resData <- tcont . plet $ pdata res
pure (resData, res)

-- | Build a 'PPositive' from a 'PInteger'. Yields 'PNothing' if argument is zero.
ppositive :: Term s (PInteger :--> PMaybe PPositive)
ppositive = phoistAcyclic $
plam $ \i ->
pif
(i #<= 0)
(pcon PNothing)
$ pcon . PJust . pcon $ PPositive i

-- | Partial version of 'PPositive'. Errors if argument is zero.
ptryPositive :: Term s (PInteger :--> PPositive)
ptryPositive = phoistAcyclic $
plam $ \i ->
pif
(i #<= 0)
(ptraceError "ptryPositive: building with non positive")
$ pcon $ PPositive i
16 changes: 8 additions & 8 deletions Plutarch/Rational.hs
Original file line number Diff line number Diff line change
Expand Up @@ -50,9 +50,9 @@ import Plutarch.Builtin (
import Plutarch.Integer (PInteger, pdiv, pmod)
import Plutarch.Lift (pconstant)
import Plutarch.List (pcons, phead, plength, pnil, ptail)
import Plutarch.NonZero (PNonZero, ptryNonZero)
import Plutarch.Num (PNum, pabs, pfromInteger, pnegate, psignum, (#*), (#+), (#-))
import Plutarch.Pair (PPair (PPair))
import Plutarch.Positive (PPositive, ptryPositive)
import Plutarch.Show (PShow, pshow, pshow')
import Plutarch.TermCont (tcont, unTermCont)
import Plutarch.Trace (ptraceError)
Expand All @@ -65,7 +65,7 @@ class PFractional (a :: PType) where
pfromRational :: Term s (PRational :--> a)

data PRational s
= PRational (Term s PInteger) (Term s PNonZero)
= PRational (Term s PInteger) (Term s PPositive)
deriving stock (Generic)
deriving anyclass (PlutusType, PEq)

Expand Down Expand Up @@ -109,14 +109,14 @@ instance PIsData PRational where

newtype Flip f a b = Flip (f b a) deriving stock (Generic)

-- | NOTE: This instance produces a verified 'PNonZero' as the excess output.
-- | NOTE: This instance produces a verified 'PPositive' as the excess output.
instance PTryFrom PData (PAsData PRational) where
type PTryFromExcess PData (PAsData PRational) = Flip Term PNonZero
type PTryFromExcess PData (PAsData PRational) = Flip Term PPositive
ptryFrom' opq = runTermCont $ do
(_, ld) <- tcont $ ptryFrom @(PAsData (PBuiltinList PData)) opq
tcont $ \f -> pif (plength # ld #== 2) (f ()) (ptraceError "ptryFrom(PRational): data list length should be 2")
(_, denm) <- tcont $ ptryFrom @(PAsData PInteger) $ phead #$ ptail # ld
res <- tcont . plet $ ptryNonZero # denm
res <- tcont . plet $ ptryPositive # denm
pure (punsafeCoerce opq, res)

instance POrd PRational where
Expand Down Expand Up @@ -217,14 +217,14 @@ instance PFractional PRational where
phoistAcyclic $
plam $ \x ->
pmatch x $ \(PRational xn xd) ->
pcon $ PRational (pto xd) $ ptryNonZero # xn
pcon $ PRational (pto xd) $ ptryPositive # xn

x' #/ y' =
phoistAcyclic
( plam $ \x y -> unTermCont $ do
PRational xn xd <- tcont $ pmatch x
PRational yn yd <- tcont $ pmatch y
denm <- tcont . plet $ ptryNonZero #$ pto xd * yn
denm <- tcont . plet $ ptryPositive #$ pto xd * yn
pure $ preduce #$ pcon $ PRational (xn * pto yd) denm
)
# x'
Expand Down Expand Up @@ -267,7 +267,7 @@ pmax = phoistAcyclic $ plam $ \a b -> pif (a #<= b) b a
pnumerator :: Term s (PRational :--> PInteger)
pnumerator = phoistAcyclic $ plam $ \x -> pmatch x $ \(PRational n _) -> n

pdenominator :: Term s (PRational :--> PNonZero)
pdenominator :: Term s (PRational :--> PPositive)
pdenominator = phoistAcyclic $ plam $ \x -> pmatch x $ \(PRational _ d) -> d

pfromInteger :: Term s (PInteger :--> PRational)
Expand Down
10 changes: 5 additions & 5 deletions plutarch-test/goldens/data-verif.bench.golden
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,13 @@ erroneous.A { test := Integer, test2 := Integer } /= { test := String, test2 :=
erroneous.Map Int String /= Map Int Int {"exBudgetCPU":733650,"exBudgetMemory":548,"scriptSizeBytes":165}
erroneous.PDataSum constr 2 {"exBudgetCPU":700994,"exBudgetMemory":230,"scriptSizeBytes":197}
erroneous.PDataSum wrong record type {"exBudgetCPU":990483,"exBudgetMemory":232,"scriptSizeBytes":256}
erroneous.[ByteString] (with length == 2) /= PRational {"exBudgetCPU":1656457,"exBudgetMemory":554,"scriptSizeBytes":231}
erroneous.[Integer] (with length == 0) /= PRational {"exBudgetCPU":761999,"exBudgetMemory":230,"scriptSizeBytes":193}
erroneous.[Integer] (with length == 3) /= PRational {"exBudgetCPU":2227517,"exBudgetMemory":524,"scriptSizeBytes":239}
erroneous.[Integer] (with length == 2, with 0 denominator) /= PRational {"exBudgetCPU":2156288,"exBudgetMemory":524,"scriptSizeBytes":225}
erroneous.[ByteString] (with length == 2) /= PRational {"exBudgetCPU":1656457,"exBudgetMemory":554,"scriptSizeBytes":246}
erroneous.[Integer] (with length == 0) /= PRational {"exBudgetCPU":761999,"exBudgetMemory":230,"scriptSizeBytes":208}
erroneous.[Integer] (with length == 3) /= PRational {"exBudgetCPU":2227517,"exBudgetMemory":524,"scriptSizeBytes":254}
erroneous.[Integer] (with length == 2, with 0 denominator) /= PRational {"exBudgetCPU":2152752,"exBudgetMemory":524,"scriptSizeBytes":240}
working.(String, String) == (String, String) {"exBudgetCPU":4806613,"exBudgetMemory":14428,"scriptSizeBytes":123}
working.[String] == [String] {"exBudgetCPU":4994603,"exBudgetMemory":16904,"scriptSizeBytes":114}
working.[Integer] (with length == 2) == PRational {"exBudgetCPU":9654221,"exBudgetMemory":28350,"scriptSizeBytes":385}
working.[Integer] (with length == 2) == PRational {"exBudgetCPU":9650685,"exBudgetMemory":28350,"scriptSizeBytes":400}
working.A { test := Integer, test2 := Integer } == { test := Integer, test2 := Integer } {"exBudgetCPU":2950183,"exBudgetMemory":9876,"scriptSizeBytes":122}
working.A { test := Integer, test2 := Integer } == [Integer] {"exBudgetCPU":2950183,"exBudgetMemory":9876,"scriptSizeBytes":122}
working.A { test := String, test2 := Integer } == { test := String, test2 := Integer } {"exBudgetCPU":3007046,"exBudgetMemory":10176,"scriptSizeBytes":128}
Expand Down
Loading

0 comments on commit 8a5973e

Please sign in to comment.