@@ -6,7 +6,8 @@ import Control.Monad.Eff.Console (CONSOLE, log)
6
6
import Control.Monad.Eff.Random (RANDOM )
7
7
import Control.Monad.Eff.Exception (EXCEPTION )
8
8
import Data.Rational (Rational , (%))
9
- import Test.StrongCheck (class Arbitrary , Result , quickCheck , (===))
9
+ import Test.StrongCheck (Result , quickCheck , (===))
10
+ import Test.StrongCheck.Arbitrary (class Arbitrary )
10
11
import Test.StrongCheck.Gen (chooseInt , suchThat )
11
12
12
13
@@ -16,15 +17,15 @@ instance arbitraryTestRational :: Arbitrary TestRational where
16
17
arbitrary = do
17
18
a <- chooseInt (-99.0 ) 99.0
18
19
b <- suchThat (chooseInt (-99.0 ) 99.0 ) (_ /= 0 )
19
- return $ TestRational $ a % b
20
+ pure $ TestRational $ a % b
20
21
21
22
newtype TestRatNonZero = TestRatNonZero Rational
22
23
23
24
instance arbitraryTestRatNonZero :: Arbitrary TestRatNonZero where
24
25
arbitrary = do
25
26
a <- suchThat (chooseInt (-99.0 ) 99.0 ) (_ /= 0 )
26
27
b <- suchThat (chooseInt (-99.0 ) 99.0 ) (_ /= 0 )
27
- return $ TestRatNonZero $ a % b
28
+ pure $ TestRatNonZero $ a % b
28
29
29
30
main :: forall eff . Eff (console :: CONSOLE , random :: RANDOM , err :: EXCEPTION | eff ) Unit
30
31
main = do
@@ -49,13 +50,13 @@ main = do
49
50
log " Checking 'Annihilation' law for Semiring"
50
51
quickCheck annihilation
51
52
53
+ log " Checking 'Additive inverse' law for Ring"
54
+ quickCheck additiveInverse
55
+
52
56
log " Checking 'Remainder' law for MuduloSemiring"
53
57
quickCheck remainder
54
58
55
- log " Checking 'Multiplicative inverse' law for DivisionRing"
56
- quickCheck multiplicativeInverse
57
-
58
- log " Checking 'Commutative multiplication' law for Num"
59
+ log " Checking 'Commutative multiplication' law for CommutativeRing"
59
60
quickCheck commutativeMultiplication
60
61
61
62
log " Checking 'Reflexivity' law for Ord"
@@ -65,6 +66,15 @@ main = do
65
66
log " Checking 'Transitivity' law for Ord"
66
67
quickCheck ordTransitivity
67
68
69
+ log " Checking 'Integral domain' law for EuclideanRing"
70
+ quickCheck integralDomain
71
+
72
+ log " Checking 'Multiplicative Euclidean function' law for EuclideanRing"
73
+ quickCheck multiplicativeEuclideanFunction
74
+
75
+ log " Checking 'Non-zero multiplicative inverse' law for Field"
76
+ quickCheck multiplicativeInverse
77
+
68
78
where
69
79
70
80
identity :: TestRational -> Result
@@ -94,6 +104,9 @@ main = do
94
104
annihilation :: TestRational -> Boolean
95
105
annihilation (TestRational a) = zero * a == a * zero && zero == a * zero
96
106
107
+ additiveInverse :: TestRational -> Boolean
108
+ additiveInverse (TestRational a) = a - a == (zero - a) + a && a - a == zero
109
+
97
110
ordReflexivity :: TestRational -> Boolean
98
111
ordReflexivity (TestRational a) = a <= a
99
112
@@ -103,11 +116,16 @@ main = do
103
116
remainder :: TestRatNonZero -> TestRatNonZero -> Result
104
117
remainder (TestRatNonZero a) (TestRatNonZero b) = a / b * b + (a `mod` b) === a
105
118
106
- multiplicativeInverse :: TestRatNonZero -> Result
107
- multiplicativeInverse (TestRatNonZero x) = (one / x) * x === one
108
-
109
119
commutativeMultiplication :: TestRational -> TestRational -> Result
110
120
commutativeMultiplication (TestRational a) (TestRational b) = a * b === b * a
111
121
112
122
ordTransitivity :: TestRational -> TestRational -> TestRational -> Boolean
113
123
ordTransitivity (TestRational a) (TestRational b) (TestRational c) = if a <= b && b <= c then a <= c else true
124
+
125
+ integralDomain :: TestRatNonZero -> TestRatNonZero -> Boolean
126
+ integralDomain (TestRatNonZero a) (TestRatNonZero b) = a * b /= zero
127
+
128
+ multiplicativeEuclideanFunction :: TestRatNonZero -> TestRatNonZero -> Boolean
129
+ multiplicativeEuclideanFunction (TestRatNonZero a) (TestRatNonZero b) = a == (a / b) * b + (a `mod` b)
130
+ multiplicativeInverse :: TestRational -> TestRational -> Boolean
131
+ multiplicativeInverse (TestRational a) (TestRational b) = a `mod` b == zero
0 commit comments