blob: c377fccc3141cb75f0bd4d47f7b46d8128820441 (
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
|
(.module:
[lux #*
data/text/format
["_" test (#+ Test)]
[control
[monad (#+ do)]
{[0 #test]
[/
["$." equivalence]
["$." functor (#+ Injection)]]}]
[data
[number
["." nat]]]
[math
["r" random]]]
{1
["." /]})
(def: injection
(Injection /.Queue)
(|>> list /.from-list))
(def: #export test
Test
(<| (_.context (%name (name-of /.Queue)))
(do r.monad
[size (:: @ map (n/% 100) r.nat)
sample (r.queue size r.nat)
non-member (|> r.nat
(r.filter (|>> (/.member? nat.equivalence sample) not)))]
($_ _.and
($equivalence.spec (/.equivalence nat.equivalence) (r.queue size r.nat))
($functor.spec ..injection /.equivalence /.functor)
(_.test "I can query the size of a queue (and empty queues have size 0)."
(if (n/= 0 size)
(/.empty? sample)
(n/= size (/.size sample))))
(_.test "Enqueueing and dequeing affects the size of queues."
(and (n/= (inc size) (/.size (/.push non-member sample)))
(or (/.empty? sample)
(n/= (dec size) (/.size (/.pop sample))))
(n/= size (/.size (/.pop (/.push non-member sample))))))
(_.test "Transforming to/from list can't change the queue."
(let [(^open "/;.") (/.equivalence nat.equivalence)]
(|> sample
/.to-list /.from-list
(/;= sample))))
(_.test "I can always peek at a non-empty queue."
(case (/.peek sample)
#.None (/.empty? sample)
(#.Some _) #1))
(_.test "I can query whether an element belongs to a queue."
(and (not (/.member? nat.equivalence sample non-member))
(/.member? nat.equivalence (/.push non-member sample)
non-member)
(case (/.peek sample)
#.None
(/.empty? sample)
(#.Some first)
(and (/.member? nat.equivalence sample first)
(not (/.member? nat.equivalence (/.pop sample) first))))))
))))
|
