blob: 9a0b91b99c3c1bb62292c1da731959244d6842c4 (
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
|
(.module:
[library
[lux "*"
["[0]" meta]
[abstract
[monad {"+" [do]}]]
[control
["[0]" try {"+" [Try]}]
["[0]" exception {"+" [exception:]}]
[parser
["<[0]>" code]]]
[macro
[syntax {"+" [syntax:]}]
["[0]" code]]
[math
[number
["i" int]]]
[type
abstract]]])
(exception: .public zero_cannot_be_a_modulus)
(abstract: .public (Modulus %)
Int
(def: .public (modulus value)
(Ex (_ %) (-> Int (Try (Modulus %))))
(if (i.= +0 value)
(exception.except ..zero_cannot_be_a_modulus [])
{try.#Success (:abstraction value)}))
(def: .public divisor
(All (_ %) (-> (Modulus %) Int))
(|>> :representation))
(def: .public (= reference subject)
(All (_ %r %s) (-> (Modulus %r) (Modulus %s) Bit))
(i.= (:representation reference)
(:representation subject)))
(def: .public (congruent? modulus reference subject)
(All (_ %) (-> (Modulus %) Int Int Bit))
(|> subject
(i.- reference)
(i.% (:representation modulus))
(i.= +0)))
)
(syntax: .public (literal [divisor <code>.int])
(meta.lifted
(do try.monad
[_ (..modulus divisor)]
(in (list (` ((~! try.trusted) (..modulus (~ (code.int divisor))))))))))
|
