blob: f795d27c00f642795c3bb5908c598c058c33e660 (
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
|
(.module:
[lux #*
[abstract
[equivalence (#+ Equivalence)]
[monad (#+ do)]
{[0 #spec]
[/
["$." monoid]]}]
[data
[number
["n" nat]]
["." text ("#@." equivalence)]]
[math
["." random (#+ Random)]]
["_" test (#+ Test)]]
{1
["." /]})
(def: #export test
Test
(do {@ random.monad}
[expected random.nat
f0 (:: @ map n.+ random.nat)
f1 (:: @ map n.* random.nat)
dummy random.nat
extra (|> random.nat (random.filter (|>> (n.= expected) not)))]
(<| (_.covering /._)
($_ _.and
(let [equivalence (: (Equivalence (-> Nat Nat))
(structure
(def: (= left right)
(n.= (left extra)
(right extra)))))
generator (: (Random (-> Nat Nat))
(:: @ map n.- random.nat))]
(_.with-cover [/.monoid]
($monoid.spec equivalence /.monoid generator)))
(_.cover [/.identity]
(n.= expected
(/.identity expected)))
(_.cover [/.compose]
(n.= (f0 (f1 expected))
((/.compose f0 f1) expected)))
(_.cover [/.constant]
(n.= expected
((/.constant expected) dummy)))
(_.cover [/.flip]
(let [outcome ((/.flip n.-) expected extra)]
(and (n.= (n.- extra expected)
outcome)
(not (n.= (n.- expected extra)
outcome)))))
(_.cover [/.apply]
(n.= (f0 extra)
(/.apply extra f0)))
))))
|
