blob: 40dd3f60f385061efb0c17b3346e0c043f4796b6 (
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
|
(.require
[library
[lux (.except)
["_" test (.only Test)]
[abstract
[monad (.only do)]
[\\specification
["$[0]" functor (.only Injection Comparison)]
["$[0]" apply]
["$[0]" monad]]]
[math
["[0]" random]
[number
["n" nat]]]]]
[\\library
["[0]" / (.only Thread)
[//
["[0]" io]]]])
(def (injection value)
(Injection (All (_ a !) (Thread ! a)))
(at /.monad in value))
(def comparison
(Comparison (All (_ a !) (Thread ! a)))
(function (_ == left right)
(== (/.result left) (/.result right))))
(def .public test
Test
(do random.monad
[sample random.nat
factor random.nat]
(<| (_.covering /._)
(all _.and
(_.for [/.Thread]
(all _.and
(_.coverage [/.result]
(n.= sample
(|> sample
(at /.monad in)
/.result)))
(_.coverage [/.io]
(n.= sample
(|> sample
(at /.monad in)
/.io
io.run!)))
(_.for [/.functor]
($functor.spec ..injection ..comparison /.functor))
(_.for [/.apply]
($apply.spec ..injection ..comparison /.apply))
(_.for [/.monad]
($monad.spec ..injection ..comparison /.monad))
))
(_.for [/.Box /.box]
(all _.and
(_.coverage [/.read!]
(n.= sample
(/.result (is (All (_ !) (Thread ! Nat))
(do /.monad
[box (/.box sample)]
(/.read! box))))))
(_.coverage [/.write!]
(n.= factor
(/.result (is (All (_ !) (Thread ! Nat))
(do /.monad
[box (/.box sample)
_ (/.write! factor box)]
(/.read! box))))))
(_.coverage [/.update!]
(n.= (n.* factor sample)
(/.result (is (All (_ !) (Thread ! Nat))
(do /.monad
[box (/.box sample)
[old new] (/.update! (n.* factor) box)]
(in new))))))))
))))
|