-
Notifications
You must be signed in to change notification settings - Fork 64
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Plutarch Numeric hierarchy #160
base: staging
Are you sure you want to change the base?
Changes from 7 commits
d676dd9
3f29c5a
1f797e7
9454d09
faa289b
658b60d
95ea57b
a1e173b
beeb9d6
d3fe282
ff1b3a5
c444c4e
7969137
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -228,15 +228,15 @@ instance PIsData PBool where | |
(phoistAcyclic $ plam toBool) # pforgetData x | ||
where | ||
toBool :: Term s PData -> Term s PBool | ||
toBool d = pfstBuiltin # (pasConstr # d) #== 1 | ||
toBool d = pfstBuiltin # (pasConstr # d) #== pconstant 1 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why? |
||
|
||
pdata x = | ||
(phoistAcyclic $ plam toData) # x | ||
where | ||
toData :: Term s PBool -> Term s (PAsData PBool) | ||
toData b = | ||
punsafeBuiltin PLC.ConstrData | ||
# (pif' # b # 1 # (0 :: Term s PInteger)) | ||
# (pif' # b # pconstant 1 # (pconstant 0 :: Term s PInteger)) | ||
# nil | ||
|
||
nil :: Term s (PBuiltinList PData) | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -36,7 +36,15 @@ import Plutarch.Builtin ( | |
psndBuiltin, | ||
) | ||
import Plutarch.Integer (PInteger) | ||
import Plutarch.Lift (PConstant, PConstantRepr, PConstanted, PLift, pconstantFromRepr, pconstantToRepr) | ||
import Plutarch.Lift ( | ||
PConstant, | ||
PConstantRepr, | ||
PConstanted, | ||
PLift, | ||
pconstant, | ||
pconstantFromRepr, | ||
pconstantToRepr, | ||
) | ||
import Plutarch.List (punsafeIndex) | ||
import Plutarch.Prelude | ||
import qualified Plutus.V1.Ledger.Api as Ledger | ||
|
@@ -66,13 +74,16 @@ punDataRepr = phoistAcyclic $ | |
plet (pasConstr #$ pasData t) $ \d -> | ||
(punsafeCoerce $ psndBuiltin # d :: Term _ (PDataList def)) | ||
|
||
pindexDataRepr :: (KnownNat n) => Proxy n -> Term s (PDataRepr (def : defs) :--> PDataList (IndexList n (def : defs))) | ||
pindexDataRepr :: | ||
(KnownNat n) => | ||
Proxy n -> | ||
Term s (PDataRepr (def : defs) :--> PDataList (IndexList n (def : defs))) | ||
pindexDataRepr n = phoistAcyclic $ | ||
plam $ \t -> | ||
plet (pasConstr #$ pasData t) $ \d -> | ||
let i :: Term _ PInteger = pfstBuiltin # d | ||
in pif | ||
(i #== fromInteger (natVal n)) | ||
(i #== pconstant (natVal n)) | ||
(punsafeCoerce $ psndBuiltin # d :: Term _ (PDataList _)) | ||
perror | ||
|
||
|
@@ -84,7 +95,7 @@ pindexDataList n = | |
punsafeIndex @PBuiltinList @PData # ind | ||
where | ||
ind :: Term s PInteger | ||
ind = fromInteger $ natVal n | ||
ind = pconstant $ natVal n | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why? |
||
|
||
data DataReprHandlers (out :: PType) (def :: [[PType]]) (s :: S) where | ||
DRHNil :: DataReprHandlers out '[] s | ||
|
@@ -132,7 +143,7 @@ pmatchDataRepr d handlers = | |
then go common (idx + 1) rest constr | ||
else | ||
pif | ||
(fromInteger idx #== constr) | ||
(pconstant idx #== constr) | ||
handler | ||
$ go common (idx + 1) rest constr | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,7 +1,15 @@ | ||
{-# LANGUAGE UndecidableInstances #-} | ||
{-# OPTIONS_GHC -Wno-orphans #-} | ||
|
||
module Plutarch.Integer (PInteger, PIntegral (..)) where | ||
module Plutarch.Integer ( | ||
PInteger, | ||
ppowInteger, | ||
(#^), | ||
pdivideInteger, | ||
pmodInteger, | ||
pquotientInteger, | ||
premainderInteger, | ||
) where | ||
|
||
import Plutarch (punsafeBuiltin) | ||
import Plutarch.Bool (PEq, POrd, pif, (#<), (#<=), (#==)) | ||
|
@@ -12,6 +20,19 @@ import Plutarch.Lift ( | |
PUnsafeLiftDecl, | ||
pconstant, | ||
) | ||
import Plutarch.Numeric ( | ||
PAdditiveGroup ((#-)), | ||
PAdditiveMonoid (pzero), | ||
PAdditiveSemigroup ((#+)), | ||
PEuclideanClosed (pdivMod), | ||
PMultiplicativeGroup (preciprocal), | ||
PMultiplicativeMonoid (pone), | ||
PMultiplicativeSemigroup ((#*)), | ||
pdiv, | ||
peven, | ||
pnegate, | ||
) | ||
import Plutarch.Pair (PPair (PPair)) | ||
import Plutarch.Prelude | ||
import qualified PlutusCore as PLC | ||
|
||
|
@@ -21,37 +42,89 @@ data PInteger s | |
instance PUnsafeLiftDecl PInteger where type PLifted PInteger = Integer | ||
deriving via (DerivePConstantViaCoercible Integer PInteger Integer) instance (PConstant Integer) | ||
|
||
class PIntegral a where | ||
pdiv :: Term s (a :--> a :--> a) | ||
pmod :: Term s (a :--> a :--> a) | ||
pquot :: Term s (a :--> a :--> a) | ||
prem :: Term s (a :--> a :--> a) | ||
|
||
instance PIntegral PInteger where | ||
pdiv = punsafeBuiltin PLC.DivideInteger | ||
pmod = punsafeBuiltin PLC.ModInteger | ||
pquot = punsafeBuiltin PLC.QuotientInteger | ||
prem = punsafeBuiltin PLC.RemainderInteger | ||
|
||
instance PEq PInteger where | ||
x #== y = punsafeBuiltin PLC.EqualsInteger # x # y | ||
|
||
instance POrd PInteger where | ||
x #<= y = punsafeBuiltin PLC.LessThanEqualsInteger # x # y | ||
x #< y = punsafeBuiltin PLC.LessThanInteger # x # y | ||
|
||
instance Num (Term s PInteger) where | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why remove this instance? |
||
x + y = punsafeBuiltin PLC.AddInteger # x # y | ||
x - y = punsafeBuiltin PLC.SubtractInteger # x # y | ||
x * y = punsafeBuiltin PLC.MultiplyInteger # x # y | ||
abs x' = plet x' $ \x -> pif (x #<= -1) (negate x) x | ||
negate x = 0 - x | ||
signum x' = plet x' $ \x -> | ||
pif | ||
(x #== 0) | ||
0 | ||
$ pif | ||
(x #<= 0) | ||
(-1) | ||
1 | ||
fromInteger = pconstant | ||
instance PAdditiveSemigroup PInteger where | ||
x #+ y = punsafeBuiltin PLC.AddInteger # x # y | ||
|
||
instance PAdditiveMonoid PInteger where | ||
pzero = phoistAcyclic (pconstant 0) | ||
|
||
instance PAdditiveGroup PInteger where | ||
x #- y = punsafeBuiltin PLC.SubtractInteger # x # y | ||
|
||
instance PMultiplicativeSemigroup PInteger where | ||
x #* y = punsafeBuiltin PLC.MultiplyInteger # x # y | ||
|
||
instance PMultiplicativeMonoid PInteger where | ||
pone = phoistAcyclic (pconstant 1) | ||
|
||
instance PEuclideanClosed PInteger where | ||
pdivMod = | ||
phoistAcyclic | ||
( plam $ \x y -> | ||
pif | ||
(y #== pzero) | ||
(pcon $ PPair pzero x) | ||
( pcon $ | ||
PPair | ||
(punsafeBuiltin PLC.QuotientInteger # x # y) | ||
(punsafeBuiltin PLC.RemainderInteger # x # y) | ||
) | ||
) | ||
|
||
-- | Raise by an 'Integer' power. | ||
ppowInteger :: PMultiplicativeGroup a => Term s a -> Term s PInteger -> Term s a | ||
ppowInteger a int = | ||
phoistAcyclic | ||
( plam $ \x i -> | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. do-syntax please There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We can't actually use do-syntax, because it breaks GHC 8.10.7... |
||
plet i $ \i' -> | ||
plet x $ \x' -> | ||
pif (i' #== pzero) pone $ | ||
pif (i' #== pone) x' $ | ||
plet (pexpBySquaring # x') $ \sqX -> | ||
pif | ||
(i' #< pzero) | ||
(preciprocal $ sqX #$ pnegate i') | ||
(sqX # i') | ||
) | ||
# a | ||
# int | ||
|
||
-- | Operator version of 'ppowInteger'. | ||
(#^) :: (PMultiplicativeGroup a) => Term s a -> Term s PInteger -> Term s a | ||
(#^) = ppowInteger | ||
|
||
infixr 8 #^ | ||
|
||
pdivideInteger :: Term s (PInteger :--> PInteger :--> PInteger) | ||
pdivideInteger = punsafeBuiltin PLC.DivideInteger | ||
|
||
pmodInteger :: Term s (PInteger :--> PInteger :--> PInteger) | ||
pmodInteger = punsafeBuiltin PLC.ModInteger | ||
|
||
pquotientInteger :: Term s (PInteger :--> PInteger :--> PInteger) | ||
pquotientInteger = punsafeBuiltin PLC.QuotientInteger | ||
|
||
premainderInteger :: Term s (PInteger :--> PInteger :--> PInteger) | ||
premainderInteger = punsafeBuiltin PLC.RemainderInteger | ||
|
||
-- Helpers | ||
|
||
-- We secretly know that i is always positive. | ||
pexpBySquaring :: | ||
forall s a. | ||
(PMultiplicativeMonoid a) => | ||
Term s (a :--> PInteger :--> a) | ||
pexpBySquaring = pfix #$ plam f | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This isn't hoisted. |
||
where | ||
f :: Term s (a :--> PInteger :--> a) -> Term s a -> Term s PInteger -> Term s a | ||
f self acc i = | ||
pif (i #== pone) acc $ | ||
plet (self # (acc #* acc) # (pdiv i (pconstant 2))) $ \x -> | ||
pif (peven # i) x (acc #* x) |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -43,6 +43,12 @@ import Plutarch (PInner, PlutusType, pcon', pmatch') | |
import Plutarch.Bool (PBool (PFalse, PTrue), PEq, pif, (#&&), (#==), (#||)) | ||
import Plutarch.Integer (PInteger) | ||
import Plutarch.Lift (pconstant) | ||
import Plutarch.Numeric ( | ||
PAdditiveGroup ((#-)), | ||
PAdditiveMonoid (pzero), | ||
PAdditiveSemigroup ((#+)), | ||
PMultiplicativeMonoid (pone), | ||
) | ||
import Plutarch.Pair (PPair (PPair)) | ||
import Plutarch.Prelude | ||
|
||
|
@@ -154,8 +160,8 @@ plength :: PIsListLike list a => Term s (list a :--> PInteger) | |
plength = phoistAcyclic $ | ||
plam $ \xs -> | ||
let go :: PIsListLike list a => Term s (list a :--> PInteger :--> PInteger) | ||
go = (pfix #$ plam $ \self ls n -> pelimList (\_ xs -> self # xs # n + 1) n ls) | ||
in go # xs # 0 | ||
go = (pfix #$ plam $ \self ls n -> pelimList (\_ xs -> self # xs # n #+ pone) n ls) | ||
in go # xs # pzero | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why? |
||
|
||
{- | | ||
Unsafely index a BuiltinList, | ||
|
@@ -166,9 +172,9 @@ punsafeIndex = phoistAcyclic $ | |
pfix #$ plam $ | ||
\self n xs -> | ||
pif | ||
(n #== 0) | ||
(n #== pzero) | ||
(phead # xs) | ||
(self # (n - 1) #$ ptail # xs) | ||
(self # (n #- pone) #$ ptail # xs) | ||
|
||
-------------------------------------------------------------------------------- | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
?