blob: 5d929527e121d761615217d723deee1b638704e0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
(.module:
[lux #*
data/text/format
["_" test (#+ Test)]
["r" math/random]
[abstract/monad (#+ do)]
[data
["." product]
["." bit ("#@." equivalence)]
["." error]]
["." type ("#@." equivalence)]]
{1
["." /]})
(def: %3 (/.modulus +3))
(`` (type: Mod3 (~~ (:of %3))))
(def: modulusR
(r.Random Int)
(|> r.int
(:: r.monad map (i/% +1000))
(r.filter (|>> (i/= +0) not))))
(def: valueR
(r.Random Int)
(|> r.int (:: r.monad map (i/% +1000))))
(def: (modR modulus)
(All [m] (-> (/.Modulus m) (r.Random [Int (/.Mod m)])))
(do r.monad
[raw valueR]
(wrap [raw (/.mod modulus raw)])))
(def: value
(All [m] (-> (/.Mod m) Int))
(|>> /.un-mod product.left))
(def: (comparison m/? i/?)
(All [m]
(-> (-> (/.Mod m) (/.Mod m) Bit)
(-> Int Int Bit)
(-> (/.Mod m) (/.Mod m) Bit)))
(function (_ param subject)
(bit@= (m/? param subject)
(i/? (value param)
(value subject)))))
(def: (arithmetic modulus m/! i/!)
(All [m]
(-> (/.Modulus m)
(-> (/.Mod m) (/.Mod m) (/.Mod m))
(-> Int Int Int)
(-> (/.Mod m) (/.Mod m) Bit)))
(function (_ param subject)
(|> (i/! (value param)
(value subject))
(/.mod modulus)
(/.m/= (m/! param subject)))))
(def: #export test
Test
(<| (_.context (%name (name-of /.Mod)))
(do r.monad
[_normalM modulusR
_alternativeM (|> modulusR (r.filter (|>> (i/= _normalM) not)))
#let [normalM (|> _normalM /.from-int error.assume)
alternativeM (|> _alternativeM /.from-int error.assume)]
[_param param] (modR normalM)
[_subject subject] (modR normalM)
#let [copyM (|> normalM /.to-int /.from-int error.assume)]]
($_ _.and
(_.test "Every modulus has a unique type, even if the numeric value is the same as another."
(and (type@= (:of normalM)
(:of normalM))
(not (type@= (:of normalM)
(:of alternativeM)))
(not (type@= (:of normalM)
(:of copyM)))))
(_.test "Can extract the original integer from the modulus."
(i/= _normalM
(/.to-int normalM)))
(_.test "Can compare mod'ed values."
(and (/.m/= subject subject)
((comparison /.m/= i/=) param subject)
((comparison /.m/< i/<) param subject)
((comparison /.m/<= i/<=) param subject)
((comparison /.m/> i/>) param subject)
((comparison /.m/>= i/>=) param subject)))
(_.test "Mod'ed values are ordered."
(and (bit@= (/.m/< param subject)
(not (/.m/>= param subject)))
(bit@= (/.m/> param subject)
(not (/.m/<= param subject)))
(bit@= (/.m/= param subject)
(not (or (/.m/< param subject)
(/.m/> param subject))))))
(_.test "Can do arithmetic."
(and ((arithmetic normalM /.m/+ i/+) param subject)
((arithmetic normalM /.m/- i/-) param subject)
((arithmetic normalM /.m/* i/*) param subject)))
(_.test "Can sometimes find multiplicative inverse."
(case (/.inverse subject)
(#.Some subject^-1)
(|> subject
(/.m/* subject^-1)
(/.m/= (/.mod normalM +1)))
#.None
true))
(_.test "Can encode/decode to text."
(let [(^open "mod/.") (/.codec normalM)]
(case (|> subject mod/encode mod/decode)
(#error.Success output)
(/.m/= subject output)
(#error.Failure error)
false)))
(_.test "Can equalize 2 moduli if they are equal."
(case (/.equalize (/.mod normalM _subject)
(/.mod copyM _param))
(#error.Success paramC)
(/.m/= param paramC)
(#error.Failure error)
false))
(_.test "Cannot equalize 2 moduli if they are the different."
(case (/.equalize (/.mod normalM _subject)
(/.mod alternativeM _param))
(#error.Success paramA)
false
(#error.Failure error)
true))
(_.test "All numbers are congruent to themselves."
(/.congruent? normalM _subject _subject))
(_.test "If 2 numbers are congruent under a modulus, then they must also be equal under the same modulus."
(bit@= (/.congruent? normalM _param _subject)
(/.m/= param subject)))
))))
|
