blob: 520fa141c740056b3c8b865fe23b34afb3f2e98c (
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
|
(.module:
[lux #*
["_" test (#+ Test)]
[abstract
[monad (#+ do)]
[\spec
[functor
["$." contravariant]]]]
[data
["." bit ("#\." equivalence)]]
[math
["." random (#+ Random)]
[number
["n" nat]
["i" int]]]]
[\\
["." / (#+ Equivalence)]])
(def: #export test
Test
(do random.monad
[leftN random.nat
rightN random.nat
leftI random.int
rightI random.int
sample random.nat
different (|> random.nat (random.filter (|>> (n.= sample) not)))
#let [equivalence (: (Equivalence (Equivalence Nat))
(implementation
(def: (= left right)
(and (bit\= (\ left = leftN leftN)
(\ right = leftN leftN))
(bit\= (\ left = rightN rightN)
(\ right = rightN rightN))
(bit\= (\ left = leftN rightN)
(\ right = leftN rightN))))))]]
(<| (_.covering /._)
($_ _.and
(_.for [/.functor]
($contravariant.spec equivalence n.equivalence /.functor))
(_.cover [/.rec]
(let [equivalence (: (Equivalence (List Nat))
(/.rec (function (_ equivalence)
(implementation
(def: (= left right)
(case [left right]
[#.Nil #.Nil]
true
[(#.Cons leftH lefT) (#.Cons rightH rightT)]
(and (n.= leftH rightH)
(\ equivalence = lefT rightT))
_
false))))))]
(and (\ equivalence = (list sample sample) (list sample sample))
(not (\ equivalence = (list sample sample) (list sample)))
(not (\ equivalence = (list sample sample) (list different different))))))
))))
|
