blob: cf69e9243a682ebfd7771e36db987fee8e0fbacb (
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
|
(.module:
[library
[lux #*
["_" test (#+ Test)]
[abstract
[predicate (#+ Predicate)]
[monad (#+ do)]]
[control
["." maybe ("#\." monad)]]
[data
[collection
["." list ("#\." functor)]]]
[math
["." random]
[number
["n" nat]]]]]
[\\library
["." /]])
(def: _refiner
(/.refiner (n.> 123)))
(def: _type
(/.type _refiner))
(def: .public test
Test
(<| (_.covering /._)
(_.for [/.Refined])
(do {! random.monad}
[raw random.nat
modulus (\ ! map (|>> (n.% 10) (n.+ 2)) random.nat)
.let [predicate (: (Predicate Nat)
(|>> (n.% modulus) (n.= 0)))]
total_raws (\ ! map (|>> (n.% 20) inc) 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\map (|>> /.predicate (same? predicate)))
(maybe.else false)))
))
(_.cover [/.value]
(|> (/.refiner predicate modulus)
(maybe\map (|>> /.value (n.= modulus)))
(maybe.else false)))
(_.cover [/.lifted]
(and (|> (/.refiner predicate modulus)
(maybe\map (/.lifted (n.+ modulus)))
maybe\join
(maybe\map (|>> /.value (n.= (n.+ modulus modulus))))
(maybe.else false))
(|> (/.refiner predicate modulus)
(maybe\map (/.lifted (n.+ (inc modulus))))
maybe\join
(maybe\map (|>> /.value (n.= (n.+ modulus (inc 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\map /.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\map /.value actual)))))
(_.cover [/.type]
(exec (: (Maybe .._type)
(.._refiner raw))
true))
))))
|
