blob: 501791b082a8cc02e700d8b8f9f7eed00703b3c3 (
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
|
(.using
[library
[lux "*"
["_" test {"+" Test}]
[abstract
[monad {"+" do}]
[\\specification
[functor
["$[0]" contravariant]]]]
[data
["[0]" bit ("[1]#[0]" equivalence)]]
[math
["[0]" random {"+" Random}]
[number
["n" nat]
["i" int]]]]]
[\\library
["[0]" / {"+" Equivalence}]])
(def: .public test
Test
(do random.monad
[leftN random.nat
rightN random.nat
leftI random.int
rightI random.int
sample random.nat
different (|> random.nat (random.only (|>> (n.= sample) not)))
.let [equivalence (is (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 /._)
(all _.and
(_.for [/.functor]
($contravariant.spec equivalence n.equivalence /.functor))
(_.cover [/.rec]
(let [equivalence (is (Equivalence (List Nat))
(/.rec (function (_ equivalence)
(implementation
(def: (= left right)
(case [left right]
[{.#End} {.#End}]
true
[{.#Item leftH lefT} {.#Item 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))))))
))))
|
