blob: 30cc94613a317d280fa385af196cfeb7b28aead8 (
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
|
(.using
[library
[lux (.except)
[abstract
[equivalence (.only Equivalence)]
[monad (.only do)]]
[control
["[0]" maybe]]
[data
[collection
["[0]" tree
["[1]" finger (.only Tree)]]]]
[math
[number
["n" nat (.open: "[1]#[0]" interval)]]]
[type (.only by_example)
[primitive (.only 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 [@]
(is (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}
(at 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 (at ..builder branch =left right)})
(case (again right)
{.#None}
{.#Some left}
{.#Some =right}
{.#Some (at ..builder branch left =right)})))))))
(def .public (end priority value queue)
(All (_ a) (-> Priority a (Queue a) (Queue a)))
(let [addition (at ..builder leaf priority value)]
(abstraction
(case (representation queue)
{.#None}
{.#Some addition}
{.#Some tree}
{.#Some (at ..builder branch tree addition)}))))
)
(def .public empty?
(All (_ a) (-> (Queue a) Bit))
(|>> ..size (n.= 0)))
|
