blob: 6710ef7c6882b3034f1247a61c4073afd087eb11 (
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:
[library
[lux #*
["_" test (#+ Test)]
[abstract
[monad (#+ do)]
["." predicate]
[\\specification
["$." equivalence]]]
[math
["." random (#+ Random)]
[number
["n" nat]]]]]
[\\library
["." / (#+ Bits)]])
(def: (size min max)
(-> Nat Nat (Random Nat))
(|> random.nat
(\ random.monad map (|>> (n.% (inc max)) (n.max min)))))
(def: .public random
(Random Bits)
(do {! random.monad}
[size (\ ! map (n.% 1,000) random.nat)]
(case size
0 (in /.empty)
_ (do {! random.monad}
[idx (|> random.nat (\ ! map (n.% size)))]
(in (/.one idx /.empty))))))
(def: .public 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 [/.bit /.one]
(and (|> /.empty (/.bit idx) not)
(|> /.empty (/.one idx) (/.bit idx))))
(_.cover [/.zero]
(|> /.empty (/.one idx) (/.zero idx) (/.bit idx) not))
(_.cover [/.flipped]
(and (|> /.empty (/.flipped idx) (/.bit idx))
(|> /.empty (/.flipped idx) (/.flipped idx) (/.bit idx) not)))
(_.cover [/.Chunk /.capacity /.chunk_size]
(and (n.= 0 (/.capacity /.empty))
(|> /.empty (/.one idx) /.capacity
(n.- idx)
(predicate.or (n.>= 0)
(n.< /.chunk_size)))
(let [grown (/.flipped idx /.empty)]
(and (n.> 0 (/.capacity grown))
(same? /.empty (/.flipped idx grown))))))
(_.cover [/.intersects?]
(and (not (/.intersects? /.empty
/.empty))
(/.intersects? (/.one idx /.empty)
(/.one idx /.empty))
(not (/.intersects? (/.one (inc idx) /.empty)
(/.one idx /.empty)))
(not (/.intersects? sample (/.not sample)))))
(_.cover [/.not]
(and (same? /.empty (/.not /.empty))
(or (same? /.empty sample)
(and (not (\ /.equivalence = sample (/.not sample)))
(\ /.equivalence = sample (/.not (/.not sample)))))))
(_.cover [/.xor]
(and (same? /.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))
(same? /.empty (/.and sample (/.not sample)))))
)))))
|
