blob: 2d269d30015f1f24297aec11c8046943132a5cff (
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
|
(.using
[library
[lux "*"
["_" test {"+" Test}]
[abstract
[predicate {"+" Predicate}]
[monad {"+" do}]]
[control
["[0]" maybe ("[1]#[0]" monad)]]
[data
[collection
["[0]" list ("[1]#[0]" functor)]]]
[math
["[0]" random]
[number
["n" nat]]]]]
[\\library
["[0]" /]])
(def: _refiner
(/.refiner (n.> 123)))
(def: _type
(/.type _refiner))
(def: .public test
Test
(<| (_.covering /._)
(_.for [/.Refined])
(do [! random.monad]
[raw random.nat
modulus (# ! each (|>> (n.% 10) (n.+ 2)) random.nat)
.let [predicate (is (Predicate Nat)
(|>> (n.% modulus) (n.= 0)))]
total_raws (# ! each (|>> (n.% 20) ++) random.nat)
raws (random.list total_raws random.nat)]
($_ _.and
(_.for [/.Refiner]
($_ _.and
(_.cover [/.refiner]
(case (/.refiner predicate raw)
{.#Some refined}
(predicate raw)
{.#None}
(not (predicate raw))))
(_.cover [/.predicate]
(|> (/.refiner predicate modulus)
(maybe#each (|>> /.predicate (same? predicate)))
(maybe.else false)))
))
(_.cover [/.value]
(|> (/.refiner predicate modulus)
(maybe#each (|>> /.value (n.= modulus)))
(maybe.else false)))
(_.cover [/.lifted]
(and (|> (/.refiner predicate modulus)
(maybe#each (/.lifted (n.+ modulus)))
maybe#conjoint
(maybe#each (|>> /.value (n.= (n.+ modulus modulus))))
(maybe.else false))
(|> (/.refiner predicate modulus)
(maybe#each (/.lifted (n.+ (++ modulus))))
maybe#conjoint
(maybe#each (|>> /.value (n.= (n.+ modulus (++ modulus)))))
(maybe.else false)
not)))
(_.cover [/.only]
(let [expected (list.only predicate raws)
actual (/.only (/.refiner predicate) raws)]
(and (n.= (list.size expected)
(list.size actual))
(# (list.equivalence n.equivalence) =
expected
(list#each /.value actual)))))
(_.cover [/.partition]
(let [expected (list.only predicate raws)
[actual alternative] (/.partition (/.refiner predicate) raws)]
(and (n.= (list.size expected)
(list.size actual))
(n.= (n.- (list.size expected) total_raws)
(list.size alternative))
(# (list.equivalence n.equivalence) =
expected
(list#each /.value actual)))))
(_.cover [/.type]
(exec (is (Maybe .._type)
(.._refiner raw))
true))
))))
|
