blob: a8a2ceeeb81c160f5fe8d3b3c9527f4e54728924 (
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
|
(.module:
[lux #*
["%" data/text/format (#+ format)]
["_" test (#+ Test)]
[abstract
[monad (#+ do)]
{[0 #spec]
[/
["$." equivalence]
["$." functor (#+ Injection)]]}]
[data
["." maybe]
[number
["n" nat]]]
[math
["r" random]]]
{1
["." /]})
(def: (injection value)
(Injection /.Stack)
(/.push value /.empty))
(def: gen-nat
(r.Random Nat)
(|> r.nat
(:: r.monad map (n.% 100))))
(def: #export test
Test
(<| (_.context (%.name (name-of /._)))
(do r.monad
[size gen-nat
sample (r.stack size gen-nat)
new-top gen-nat]
($_ _.and
($equivalence.spec (/.equivalence n.equivalence) (r.stack size r.nat))
($functor.spec ..injection /.equivalence /.functor)
(_.test (%.name (name-of /.size))
(n.= size (/.size sample)))
(_.test (%.name (name-of /.peek))
(case (/.peek sample)
#.None (/.empty? sample)
(#.Some _) (not (/.empty? sample))))
(_.test (%.name (name-of /.pop))
(case (/.size sample)
0 (case (/.pop sample)
#.None
(/.empty? sample)
(#.Some _)
false)
expected (case (/.pop sample)
(#.Some sample')
(and (n.= (dec expected) (/.size sample'))
(not (/.empty? sample)))
#.None
false)))
(_.test (%.name (name-of /.push))
(and (is? sample
(|> sample (/.push new-top) /.pop maybe.assume))
(n.= (inc (/.size sample))
(/.size (/.push new-top sample)))
(|> (/.push new-top sample) /.peek maybe.assume
(is? new-top))))
))))
|
