blob: b399fc342060cfd5f3c6be164e79515c7bfdf92e (
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
|
(.using
[library
[lux "*"
[abstract
[equivalence {"+" Equivalence}]
[monad {"+" do}]]
[control
["[0]" maybe]]
[data
[collection
["[0]" tree "_"
["[1]" finger {"+" Tree}]]]]
[math
[number
["n" nat ("[1]#[0]" interval)]]]
[type {"+" by_example}
[primitive {"+" primitive: 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
@))
(primitive: .public (Queue a)
(Maybe (Tree :@: Priority a))
(def: .public empty
Queue
(abstraction {.#None}))
(def: .public (front 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 (again [node tree])
(case (tree.root node)
{0 #0 _}
1
{0 #1 [left right]}
(n.+ (again left) (again right))))))
(def: .public (member? equivalence queue member)
(All (_ a) (-> (Equivalence a) (Queue a) a Bit))
(case (representation queue)
{.#None}
false
{.#Some tree}
(loop (again [node tree])
(case (tree.root node)
{0 #0 reference}
(# equivalence = reference member)
{0 #1 [left right]}
(or (again left)
(again right))))))
(def: .public (next queue)
(All (_ a) (-> (Queue a) (Queue a)))
(abstraction
(do maybe.monad
[tree (representation queue)
.let [highest_priority (tree.tag tree)]]
(loop (again [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 (again left)
{.#None}
{.#Some right}
{.#Some =left}
{.#Some (# ..builder branch =left right)})
(case (again right)
{.#None}
{.#Some left}
{.#Some =right}
{.#Some (# ..builder branch left =right)})))))))
(def: .public (end 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)))
|