blob: 9c526d0df7beb3f24e72b000e6d75201b67d9ae8 (
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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
(.module:
[lux #*
[abstract
[equivalence (#+ Equivalence)]
[monad (#+ do Monad)]]
[data
["." maybe]
[number
["n" nat ("#\." interval)]]
[collection
["." tree #_
["#" finger (#+ Tree)]]]]
[type (#+ :by-example)
[abstract (#+ abstract: :abstraction :representation)]]])
(type: #export Priority
Nat)
(def: #export max Priority n\top)
(def: #export min Priority n\bottom)
(def: builder
(tree.builder n.maximum))
(def: :@:
(:by-example [@]
{(tree.Builder @ Priority)
..builder}
@))
(abstract: #export (Queue a)
(Maybe (Tree :@: Priority a))
(def: #export empty
Queue
(:abstraction #.None))
(def: #export (peek queue)
(All [a] (-> (Queue a) (Maybe a)))
(do maybe.monad
[tree (:representation queue)]
(tree.search (n.= (tree.tag tree))
tree)))
(def: #export (size queue)
(All [a] (-> (Queue a) Nat))
(case (:representation queue)
#.None
0
(#.Some tree)
(loop [node tree]
(case (tree.root node)
(0 #0 _)
1
(0 #1 [left right])
(n.+ (recur left) (recur right))))))
(def: #export (member? equivalence queue member)
(All [a] (-> (Equivalence a) (Queue a) a Bit))
(case (:representation queue)
#.None
false
(#.Some tree)
(loop [node tree]
(case (tree.root node)
(0 #0 reference)
(:: equivalence = reference member)
(0 #1 [left right])
(or (recur left)
(recur right))))))
(def: #export (pop queue)
(All [a] (-> (Queue a) (Queue a)))
(:abstraction
(do maybe.monad
[tree (:representation queue)
#let [highest-priority (tree.tag tree)]]
(loop [node tree]
(case (tree.root node)
(0 #0 reference)
(if (n.= highest-priority (tree.tag node))
#.None
(#.Some node))
(0 #1 left right)
(if (n.= highest-priority (tree.tag left))
(case (recur left)
#.None
(#.Some right)
(#.Some =left)
(#.Some (:: ..builder branch =left right)))
(case (recur right)
#.None
(#.Some left)
(#.Some =right)
(#.Some (:: ..builder branch left =right)))))))))
(def: #export (push priority value queue)
(All [a] (-> Priority a (Queue a) (Queue a)))
(let [addition (:: ..builder leaf priority value)]
(:abstraction
(case (:representation queue)
#.None
(#.Some addition)
(#.Some tree)
(#.Some (:: ..builder branch tree addition))))))
)
(def: #export empty?
(All [a] (-> (Queue a) Bit))
(|>> ..size (n.= 0)))
|
