blob: 763f1836dfa038560d0cb60de14e73bf0696d735 (
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
119
120
121
122
123
124
125
126
127
128
|
(.module:
[library
[lux #*
[abstract
[equivalence (#+ Equivalence)]
[monad (#+ do)]]
[data
["." maybe]
[collection
["." tree #_
["#" finger (#+ Tree)]]]]
[math
[number
["n" nat ("#\." interval)]]]
[type (#+ :by_example)
[abstract (#+ abstract: :abstraction :representation)]]]])
(type: .public Priority
Nat)
(def: .public max
Priority
n\top)
(def: .public min
Priority
n\bottom)
(def: builder
(tree.builder n.maximum))
(def: :@:
(:by_example [@]
(tree.Builder @ Priority)
..builder
@))
(abstract: .public (Queue a)
{}
(Maybe (Tree :@: Priority a))
(def: .public empty
Queue
(:abstraction #.None))
(def: .public (peek queue)
(All [a] (-> (Queue a) (Maybe a)))
(do maybe.monad
[tree (:representation queue)]
(tree.one (n.= (tree.tag tree))
tree)))
(def: .public (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: .public (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: .public (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: .public (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: .public empty?
(All [a] (-> (Queue a) Bit))
(|>> ..size (n.= 0)))
|
