blob: f4b78086497ca4bd7c83b31dcb6145c7be8ec6ae (
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
|
(.module:
[lux #*
["_" test (#+ Test)]
[abstract
[monad (#+ do)]
["." predicate]
{[0 #spec]
[/
["$." equivalence]]}]
[math
["." random (#+ Random)]
[number
["n" nat]]]]
{1
["." / (#+ Bits)]})
(def: (size min max)
(-> Nat Nat (Random Nat))
(|> random.nat
(\ random.monad map (|>> (n.% (inc max)) (n.max min)))))
(def: #export random
(Random Bits)
(do {! random.monad}
[size (\ ! map (n.% 1,000) random.nat)]
(case size
0 (wrap /.empty)
_ (do {! random.monad}
[idx (|> random.nat (\ ! map (n.% size)))]
(wrap (/.set idx /.empty))))))
(def: #export test
Test
(<| (_.covering /._)
(_.for [/.Bits])
($_ _.and
(_.for [/.equivalence]
($equivalence.spec /.equivalence ..random))
(do random.monad
[sample ..random]
(_.cover [/.empty? /.size]
(if (/.empty? sample)
(n.= 0 (/.size sample))
(n.> 0 (/.size sample)))))
(_.cover [/.empty]
(/.empty? /.empty))
(do {! random.monad}
[size (\ ! map (|>> (n.% 1,000) inc) random.nat)
idx (\ ! map (n.% size) random.nat)
sample ..random]
($_ _.and
(_.cover [/.get /.set]
(and (|> /.empty (/.get idx) not)
(|> /.empty (/.set idx) (/.get idx))))
(_.cover [/.clear]
(|> /.empty (/.set idx) (/.clear idx) (/.get idx) not))
(_.cover [/.flip]
(and (|> /.empty (/.flip idx) (/.get idx))
(|> /.empty (/.flip idx) (/.flip idx) (/.get idx) not)))
(_.cover [/.Chunk /.capacity /.chunk-size]
(and (n.= 0 (/.capacity /.empty))
(|> /.empty (/.set idx) /.capacity
(n.- idx)
(predicate.unite (n.>= 0)
(n.< /.chunk-size)))
(let [grown (/.flip idx /.empty)]
(and (n.> 0 (/.capacity grown))
(is? /.empty (/.flip idx grown))))))
(_.cover [/.intersects?]
(and (not (/.intersects? /.empty
/.empty))
(/.intersects? (/.set idx /.empty)
(/.set idx /.empty))
(not (/.intersects? (/.set (inc idx) /.empty)
(/.set idx /.empty)))
(not (/.intersects? sample (/.not sample)))))
(_.cover [/.not]
(and (is? /.empty (/.not /.empty))
(or (is? /.empty sample)
(and (not (\ /.equivalence = sample (/.not sample)))
(\ /.equivalence = sample (/.not (/.not sample)))))))
(_.cover [/.xor]
(and (is? /.empty (/.xor sample sample))
(n.= (/.size (/.xor sample (/.not sample)))
(/.capacity sample))))
(_.cover [/.or]
(and (\ /.equivalence = sample (/.or sample sample))
(n.= (/.size (/.or sample (/.not sample)))
(/.capacity sample))))
(_.cover [/.and]
(and (\ /.equivalence = sample (/.and sample sample))
(is? /.empty (/.and sample (/.not sample)))))
)))))
|
