blob: 0a6fcf69813e82482b7963b4f2dea73eb22e3f23 (
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
|
(.module:
[lux #*
data/text/format
["_" test (#+ Test)]
[control
[monad (#+ do)]
{[0 #test]
[/
["$." equivalence]
["$." functor (#+ Injection)]]}]
[data
["." maybe]
[number
["." 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 /.Stack)))
(do r.monad
[size gen-nat
sample (r.stack size gen-nat)
new-top gen-nat]
($_ _.and
($equivalence.spec (/.equivalence nat.equivalence) (r.stack size r.nat))
($functor.spec ..injection /.equivalence /.functor)
(_.test "Can query the size of a stack."
(n/= size (/.size sample)))
(_.test "Can peek inside non-empty stacks."
(case (/.peek sample)
#.None (/.empty? sample)
(#.Some _) (not (/.empty? sample))))
(_.test (format "Popping empty stacks doesn't change anything."
"But, if they're non-empty, the top of the stack is removed.")
(case (/.size sample)
0 (case (/.pop sample)
#.None
(/.empty? sample)
(#.Some _)
false)
expected (case (/.pop sample)
(#.Some sample')
(and (n/= expected (/.size sample'))
(not (/.empty? sample)))
#.None
false)))
(_.test "Pushing onto a stack always increases it by 1, adding a new value at the top."
(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))))
))))
|
