11-- editorconfig-checker-disable-file
22{-# LANGUAGE OverloadedStrings #-}
33{-# LANGUAGE TupleSections #-}
4+ {-# LANGUAGE NoImplicitPrelude #-}
5+ {-# LANGUAGE TypeApplications #-}
46
57module Rational.Laws.Construction (constructionLaws ) where
68
79import Hedgehog (Gen , Property , assert , cover , property , (===) )
810import Hedgehog.Gen qualified as Gen
911import PlutusTx.Prelude qualified as Plutus
10- import PlutusTx.Ratio qualified as Ratio
11- import Prelude
12- import Rational.Laws.Helpers (forAllWithPP , genInteger , genIntegerPos , normalAndEquivalentToMaybe ,
12+ import PlutusTx.Ratio qualified as P
13+ import PlutusTx.Numeric qualified as P
14+ import PlutusTx.Enum qualified as P
15+ import PlutusTx.List qualified as P
16+ import Prelude hiding (succ , pred )
17+ import Rational.Laws.Helpers (forAllWithPP , genRational , genInteger , genIntegerPos , normalAndEquivalentToMaybe ,
1318 testCoverProperty )
1419import Test.Tasty (TestTree )
1520import Test.Tasty.Hedgehog (testPropertyNamed )
21+ import Data.Ratio qualified as GHC
1622
1723constructionLaws :: [TestTree ]
1824constructionLaws =
@@ -37,30 +43,57 @@ constructionLaws =
3743 " denominator (unsafeRatio x y) > 0"
3844 " propUnsafeRatioDenomPos"
3945 propUnsafeRatioDenomPos
40- ]
46+ , testPropertyNamed " succ(r)>r"
47+ " propSuccGt"
48+ propSuccGt
49+ , testPropertyNamed " pred(r)<r"
50+ " propPredLt"
51+ propPredLt
52+ , testPropertyNamed " fromEnum . toEnum n = n"
53+ " propFromToEnumId"
54+ propFromToEnumId
55+ , testPropertyNamed " denominator . toEnum = 1"
56+ " propDenomToEnum"
57+ propDenomToEnum
58+ , testPropertyNamed " n<=m ==> length(enumFromTo n m) = abs(n-m)+1"
59+ " propEnumFromToInteger"
60+ propEnumFromToInteger
61+ , testPropertyNamed " enumFromTo = GHC.enumFromTo"
62+ " propEnumFromToGHC"
63+ propEnumFromToGHC
64+ , testPropertyNamed " x/=y ==> enumFromThenTo x y x = [x]"
65+ " propEnumFromThenToLim"
66+ propEnumFromThenToLim
67+ , testPropertyNamed " x/=y ==> enumFromThenTo = GHC.enumFromThenTo"
68+ " propEnumFromThenToGHC"
69+ propEnumFromThenToGHC
70+ , testPropertyNamed " enumFromTo x y = enumFromThenTo x (x+1) y"
71+ " propEnumFromToThenTo"
72+ propEnumFromToThenTo
73+ ]
4174
4275propZeroDenom :: Property
4376propZeroDenom = property $ do
4477 x <- forAllWithPP genInteger
45- Ratio . ratio x Plutus. zero `normalAndEquivalentToMaybe` Nothing
78+ P . ratio x Plutus. zero `normalAndEquivalentToMaybe` Nothing
4679
4780propOneDenom :: Property
4881propOneDenom = property $ do
4982 x <- forAllWithPP genInteger
50- Ratio . ratio x Plutus. one `normalAndEquivalentToMaybe` (Just . Ratio .fromInteger $ x)
83+ P . ratio x Plutus. one `normalAndEquivalentToMaybe` (Just . P .fromInteger $ x)
5184
5285propRatioSelf :: Property
5386propRatioSelf = property $ do
5487 x <- forAllWithPP . Gen. filter (/= Plutus. zero) $ genInteger
55- Ratio . ratio x x `normalAndEquivalentToMaybe` Just Plutus. one
88+ P . ratio x x `normalAndEquivalentToMaybe` Just Plutus. one
5689
5790propRatioSign :: Property
5891propRatioSign = property $ do
5992 (n, d) <- forAllWithPP go
6093 cover 30 " zero numerator" $ n == 0
6194 cover 30 " same signs" $ signum n == signum d
6295 cover 30 " different signs" $ (signum n /= signum d) && n /= 0
63- let r = Ratio . ratio n d
96+ let r = P . ratio n d
6497 let signIndicator = Plutus. compare <$> r <*> pure Plutus. zero
6598 case (signum n, signum d) of
6699 (0 , _) -> signIndicator === Just Plutus. EQ
@@ -89,31 +122,88 @@ propConstructionAgreement :: Property
89122propConstructionAgreement = property $ do
90123 n <- forAllWithPP genInteger
91124 d <- forAllWithPP . Gen. filter (/= Plutus. zero) $ genInteger
92- Ratio . ratio n d `normalAndEquivalentToMaybe` (Just . Ratio . unsafeRatio n $ d)
125+ P . ratio n d `normalAndEquivalentToMaybe` (Just . P . unsafeRatio n $ d)
93126
94127propFromIntegerNum :: Property
95128propFromIntegerNum = property $ do
96129 x <- forAllWithPP genInteger
97- let r = Ratio .fromInteger x
98- Ratio . numerator r === x
130+ let r = P .fromInteger x
131+ P . numerator r === x
99132
100133propFromIntegerDen :: Property
101134propFromIntegerDen = property $ do
102135 x <- forAllWithPP genInteger
103- let r = Ratio .fromInteger x
104- Ratio . denominator r === Plutus. one
136+ let r = P .fromInteger x
137+ P . denominator r === Plutus. one
105138
106139propRatioScale :: Property
107140propRatioScale = property $ do
108141 x <- forAllWithPP genInteger
109142 y <- forAllWithPP genInteger
110143 z <- forAllWithPP . Gen. filter (/= Plutus. zero) $ genInteger
111- let lhs = Ratio . ratio x y
112- let rhs = Ratio . ratio (x Plutus. * z) (y Plutus. * z)
144+ let lhs = P . ratio x y
145+ let rhs = P . ratio (x Plutus. * z) (y Plutus. * z)
113146 lhs `normalAndEquivalentToMaybe` rhs
114147
115148propUnsafeRatioDenomPos :: Property
116149propUnsafeRatioDenomPos = property $ do
117150 n <- forAllWithPP genInteger
118151 d <- forAllWithPP $ Gen. filter (/= Plutus. zero) genInteger
119- assert $ Ratio. denominator (Ratio. unsafeRatio n d) > 0
152+ assert $ P. denominator (P. unsafeRatio n d) > 0
153+
154+ propSuccGt :: Property
155+ propSuccGt = property $ do
156+ n <- forAllWithPP genRational
157+ assert $ P. succ n > n
158+
159+ propPredLt :: Property
160+ propPredLt = property $ do
161+ n <- forAllWithPP genRational
162+ assert $ P. pred n < n
163+
164+ propDenomToEnum :: Property
165+ propDenomToEnum = property $ do
166+ n <- forAllWithPP genInteger
167+ P. denominator (P. toEnum n) === 1
168+
169+ propFromToEnumId :: Property
170+ propFromToEnumId = property $ do
171+ n <- forAllWithPP genInteger
172+ P. fromEnum @ P. Rational (P. toEnum n) === n
173+
174+ propEnumFromToInteger :: Property
175+ propEnumFromToInteger = property $ do
176+ n <- forAllWithPP genInteger
177+ m <- forAllWithPP $ Gen. filter (>= n) genInteger
178+ P. length (P. enumFromTo @ P. Rational (P. toEnum n) (P. toEnum m)) === abs (n - m) + 1
179+
180+ propEnumFromThenToLim :: Property
181+ propEnumFromThenToLim = property $ do
182+ x <- forAllWithPP genRational
183+ y <- forAllWithPP $ Gen. filter (/= x) genRational
184+ P. enumFromThenTo x y x === [x]
185+
186+ propEnumFromToGHC :: Property
187+ propEnumFromToGHC = property $ do
188+ x <- forAllWithPP genRational
189+ y <- forAllWithPP genRational
190+ fmap toGHC (P. enumFromTo x y) === enumFromTo (toGHC x) (toGHC y)
191+
192+ propEnumFromThenToGHC :: Property
193+ propEnumFromThenToGHC = property $ do
194+ x <- forAllWithPP genRational
195+ y <- forAllWithPP $ Gen. filter (/= x) genRational
196+ z <- forAllWithPP genRational
197+ fmap toGHC (P. enumFromThenTo x y z) === enumFromThenTo (toGHC x) (toGHC y) (toGHC z)
198+
199+ propEnumFromToThenTo :: Property
200+ propEnumFromToThenTo = property $ do
201+ x <- forAllWithPP genRational
202+ y <- forAllWithPP genRational
203+ P. enumFromTo x y === P. enumFromThenTo x (x P. + Plutus. one) y
204+
205+ {-| Converts a 'Rational' to a GHC 'Rational', preserving value. Does not
206+ work on-chain.
207+ -}
208+ toGHC :: P. Rational -> Rational
209+ toGHC r = P. numerator r GHC. % P. denominator r
0 commit comments