blob: 260f5f51f4520837a527d14dd9a723c4fa0762f4 (
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
|
(.module:
[lux #*
["_" test (#+ Test)]
[abstract
[predicate (#+ Predicate)]
[monad (#+ do)]]
[data
["." maybe ("#\." monad)]
[collection
["." list ("#\." functor)]]]
[math
["." random]
[number
["n" nat]]]]
{1
["." /]})
(def: _refiner
(/.refinement (n.> 123)))
(def: _type
(/.type _refiner))
(def: #export 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 [/.refinement]
(case (/.refinement predicate raw)
(#.Some refined)
(predicate raw)
#.None
(not (predicate raw))))
(_.cover [/.predicate]
(|> (/.refinement predicate modulus)
(maybe\map (|>> /.predicate (is? predicate)))
(maybe.default false)))
))
(_.cover [/.un_refine]
(|> (/.refinement predicate modulus)
(maybe\map (|>> /.un_refine (n.= modulus)))
(maybe.default false)))
(_.cover [/.lift]
(and (|> (/.refinement predicate modulus)
(maybe\map (/.lift (n.+ modulus)))
maybe\join
(maybe\map (|>> /.un_refine (n.= (n.+ modulus modulus))))
(maybe.default false))
(|> (/.refinement predicate modulus)
(maybe\map (/.lift (n.+ (inc modulus))))
maybe\join
(maybe\map (|>> /.un_refine (n.= (n.+ modulus (inc modulus)))))
(maybe.default false)
not)))
(_.cover [/.filter]
(let [expected (list.filter predicate raws)
actual (/.filter (/.refinement predicate) raws)]
(and (n.= (list.size expected)
(list.size actual))
(\ (list.equivalence n.equivalence) =
expected
(list\map /.un_refine actual)))))
(_.cover [/.partition]
(let [expected (list.filter predicate raws)
[actual alternative] (/.partition (/.refinement 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 /.un_refine actual)))))
(_.cover [/.type]
(exec (: (Maybe .._type)
(.._refiner raw))
true))
))))
|
