|
576
|
1 module RedBlackTreeHoare where
|
|
575
|
2
|
|
|
3
|
|
|
4 open import Level hiding (zero)
|
|
|
5
|
|
|
6 open import Data.Nat hiding (compare)
|
|
|
7 open import Data.Nat.Properties as NatProp
|
|
|
8 open import Data.Maybe
|
|
|
9 open import Data.Bool
|
|
|
10 open import Data.Empty
|
|
|
11
|
|
|
12 open import Relation.Binary
|
|
|
13 open import Relation.Binary.PropositionalEquality
|
|
|
14
|
|
|
15 open import stack
|
|
|
16
|
|
|
17 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
|
|
|
18 field
|
|
|
19 putImpl : treeImpl → a → (treeImpl → t) → t
|
|
|
20 getImpl : treeImpl → (treeImpl → Maybe a → t) → t
|
|
|
21 open TreeMethods
|
|
|
22
|
|
|
23 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
|
|
|
24 field
|
|
|
25 tree : treeImpl
|
|
|
26 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
|
|
|
27 putTree : a → (Tree treeImpl → t) → t
|
|
|
28 putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
|
|
|
29 getTree : (Tree treeImpl → Maybe a → t) → t
|
|
|
30 getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )
|
|
|
31
|
|
|
32 open Tree
|
|
|
33
|
|
|
34 data Color {n : Level } : Set n where
|
|
|
35 Red : Color
|
|
|
36 Black : Color
|
|
|
37
|
|
|
38
|
|
|
39 record Node {n : Level } (a : Set n) (k : ℕ) : Set n where
|
|
|
40 inductive
|
|
|
41 field
|
|
|
42 key : ℕ
|
|
|
43 value : a
|
|
|
44 right : Maybe (Node a k)
|
|
|
45 left : Maybe (Node a k)
|
|
|
46 color : Color {n}
|
|
|
47 open Node
|
|
|
48
|
|
|
49 record RedBlackTree {n m : Level } {t : Set m} (a : Set n) (k : ℕ) : Set (m Level.⊔ n) where
|
|
|
50 field
|
|
|
51 root : Maybe (Node a k)
|
|
|
52 nodeStack : SingleLinkedStack (Node a k)
|
|
|
53 -- compare : k → k → Tri A B C
|
|
576
|
54 -- <-cmp
|
|
575
|
55
|
|
|
56 open RedBlackTree
|
|
|
57
|
|
|
58 open SingleLinkedStack
|
|
|
59
|
|
|
60 compTri : ( x y : ℕ ) -> Tri ( x < y ) ( x ≡ y ) ( x > y )
|
|
|
61 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder)
|
|
|
62 where open import Relation.Binary
|
|
|
63
|
|
|
64 -- put new node at parent node, and rebuild tree to the top
|
|
|
65 --
|
|
|
66 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
|
|
|
67 replaceNode : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
|
68 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s (
|
|
|
69 \s parent → replaceNode1 s parent)
|
|
|
70 module ReplaceNode where
|
|
|
71 replaceNode1 : SingleLinkedStack (Node a k) → Maybe ( Node a k ) → t
|
|
|
72 replaceNode1 s nothing = next ( record tree { root = just (record n0 { color = Black}) } )
|
|
|
73 replaceNode1 s (just n1) with compTri (key n1) (key n0)
|
|
|
74 replaceNode1 s (just n1) | tri< lt ¬eq ¬gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next
|
|
|
75 replaceNode1 s (just n1) | tri≈ ¬lt eq ¬gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { left = just n0 } ) next
|
|
|
76 replaceNode1 s (just n1) | tri> ¬lt ¬eq gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { right = just n0 } ) next
|
|
|
77
|
|
|
78
|
|
|
79 rotateRight : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) →
|
|
|
80 (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t
|
|
|
81 rotateRight {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 → rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext)
|
|
|
82 where
|
|
|
83 rotateRight1 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) →
|
|
|
84 (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t
|
|
|
85 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0
|
|
|
86 ... | nothing = rotateNext tree s nothing n0
|
|
|
87 ... | just n1 with parent
|
|
|
88 ... | nothing = rotateNext tree s (just n1 ) n0
|
|
|
89 ... | just parent1 with left parent1
|
|
|
90 ... | nothing = rotateNext tree s (just n1) nothing
|
|
|
91 ... | just leftParent with compTri (key n1) (key leftParent)
|
|
|
92 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri< a₁ ¬b ¬c = rotateNext tree s (just n1) parent
|
|
|
93 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri≈ ¬a b ¬c = rotateNext tree s (just n1) parent
|
|
|
94 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri> ¬a ¬b c = rotateNext tree s (just n1) parent
|
|
|
95
|
|
|
96
|
|
|
97 rotateLeft : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) →
|
|
|
98 (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t
|
|
|
99 rotateLeft {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 → rotateLeft1 tree s n0 parent rotateNext)
|
|
|
100 where
|
|
|
101 rotateLeft1 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) →
|
|
|
102 (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t
|
|
|
103 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0
|
|
|
104 ... | nothing = rotateNext tree s nothing n0
|
|
|
105 ... | just n1 with parent
|
|
|
106 ... | nothing = rotateNext tree s (just n1) nothing
|
|
|
107 ... | just parent1 with right parent1
|
|
|
108 ... | nothing = rotateNext tree s (just n1) nothing
|
|
|
109 ... | just rightParent with compTri (key n1) (key rightParent)
|
|
|
110 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri< a₁ ¬b ¬c = rotateNext tree s (just n1) parent
|
|
|
111 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri≈ ¬a b ¬c = rotateNext tree s (just n1) parent
|
|
|
112 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri> ¬a ¬b c = rotateNext tree s (just n1) parent
|
|
|
113 -- ... | EQ = rotateNext tree s (just n1) parent
|
|
|
114 -- ... | _ = rotateNext tree s (just n1) parent
|
|
|
115
|
|
|
116 {-# TERMINATING #-}
|
|
|
117 insertCase5 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
|
118 insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent → insertCase51 tree s n0 parent grandParent next)
|
|
|
119 where
|
|
|
120 insertCase51 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → Maybe (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
|
121 insertCase51 {n} {m} {t} {a} {k} tree s n0 parent grandParent next with n0
|
|
|
122 ... | nothing = next tree
|
|
|
123 ... | just n1 with parent | grandParent
|
|
|
124 ... | nothing | _ = next tree
|
|
|
125 ... | _ | nothing = next tree
|
|
|
126 ... | just parent1 | just grandParent1 with left parent1 | left grandParent1
|
|
|
127 ... | nothing | _ = next tree
|
|
|
128 ... | _ | nothing = next tree
|
|
|
129 ... | just leftParent1 | just leftGrandParent1
|
|
|
130 with compTri (key n1) (key leftParent1) | compTri (key leftParent1) (key leftGrandParent1)
|
|
|
131 ... | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1 = rotateRight tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
|
|
|
132 ... | _ | _ = rotateLeft tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
|
|
|
133 -- ... | EQ | EQ = rotateRight tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
|
|
|
134 -- ... | _ | _ = rotateLeft tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
|
|
|
135
|
|
|
136 insertCase4 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
|
137 insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next
|
|
|
138 with (right parent) | (left grandParent)
|
|
|
139 ... | nothing | _ = insertCase5 tree s (just n0) parent grandParent next
|
|
|
140 ... | _ | nothing = insertCase5 tree s (just n0) parent grandParent next
|
|
|
141 ... | just rightParent | just leftGrandParent with compTri (key n0) (key rightParent) | compTri (key parent) (key leftGrandParent) -- (key n0) (key rightParent) | (key parent) (key leftGrandParent)
|
|
|
142 -- ... | EQ | EQ = popSingleLinkedStack s (\ s n1 → rotateLeft tree s (left n0) (just grandParent)
|
|
|
143 -- (\ tree s n0 parent → insertCase5 tree s n0 rightParent grandParent next))
|
|
|
144 -- ... | _ | _ = insertCase41 tree s n0 parent grandParent next
|
|
|
145 ... | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1 = popSingleLinkedStack s (\ s n1 → rotateLeft tree s (left n0) (just grandParent) (\ tree s n0 parent → insertCase5 tree s n0 rightParent grandParent next))
|
|
|
146 ... | _ | _ = insertCase41 tree s n0 parent grandParent next
|
|
|
147 where
|
|
|
148 insertCase41 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
|
149 insertCase41 {n} {m} {t} {a} {k} tree s n0 parent grandParent next
|
|
|
150 with (left parent) | (right grandParent)
|
|
|
151 ... | nothing | _ = insertCase5 tree s (just n0) parent grandParent next
|
|
|
152 ... | _ | nothing = insertCase5 tree s (just n0) parent grandParent next
|
|
|
153 ... | just leftParent | just rightGrandParent with compTri (key n0) (key leftParent) | compTri (key parent) (key rightGrandParent)
|
|
|
154 ... | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1 = popSingleLinkedStack s (\ s n1 → rotateRight tree s (right n0) (just grandParent) (\ tree s n0 parent → insertCase5 tree s n0 leftParent grandParent next))
|
|
|
155 ... | _ | _ = insertCase5 tree s (just n0) parent grandParent next
|
|
|
156 -- ... | EQ | EQ = popSingleLinkedStack s (\ s n1 → rotateRight tree s (right n0) (just grandParent)
|
|
|
157 -- (\ tree s n0 parent → insertCase5 tree s n0 leftParent grandParent next))
|
|
|
158 -- ... | _ | _ = insertCase5 tree s (just n0) parent grandParent next
|
|
|
159
|
|
|
160 colorNode : {n : Level } {a : Set n} {k : ℕ} → Node a k → Color → Node a k
|
|
|
161 colorNode old c = record old { color = c }
|
|
|
162
|
|
|
163 {-# TERMINATING #-}
|
|
|
164 insertNode : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
|
165 insertNode {n} {m} {t} {a} {k} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0)
|
|
|
166 where
|
|
|
167 insertCase1 : Node a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t -- placed here to allow mutual recursion
|
|
|
168 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
|
|
|
169 insertCase3 : SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → t
|
|
|
170 insertCase3 s n0 parent grandParent with left grandParent | right grandParent
|
|
|
171 ... | nothing | nothing = insertCase4 tree s n0 parent grandParent next
|
|
|
172 ... | nothing | just uncle = insertCase4 tree s n0 parent grandParent next
|
|
|
173 ... | just uncle | _ with compTri ( key uncle ) ( key parent )
|
|
|
174 insertCase3 s n0 parent grandParent | just uncle | _ | tri≈ ¬a b ¬c = insertCase4 tree s n0 parent grandParent next
|
|
|
175 insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c with color uncle
|
|
|
176 insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c | Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 (
|
|
|
177 record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 )
|
|
|
178 insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c | Black = insertCase4 tree s n0 parent grandParent next
|
|
|
179 insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c with color uncle
|
|
|
180 insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c | Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 ( record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 )
|
|
|
181 insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c | Black = insertCase4 tree s n0 parent grandParent next
|
|
|
182 -- ... | EQ = insertCase4 tree s n0 parent grandParent next
|
|
|
183 -- ... | _ with color uncle
|
|
|
184 -- ... | Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 (
|
|
|
185 -- record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 )
|
|
|
186 -- ... | Black = insertCase4 tree s n0 parent grandParent next --!!
|
|
|
187 insertCase2 : SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → t
|
|
|
188 insertCase2 s n0 parent grandParent with color parent
|
|
|
189 ... | Black = replaceNode tree s n0 next
|
|
|
190 ... | Red = insertCase3 s n0 parent grandParent
|
|
|
191 insertCase1 n0 s nothing nothing = next tree
|
|
|
192 insertCase1 n0 s nothing (just grandParent) = next tree
|
|
|
193 insertCase1 n0 s (just parent) nothing = replaceNode tree s (colorNode n0 Black) next
|
|
|
194 insertCase1 n0 s (just parent) (just grandParent) = insertCase2 s n0 parent grandParent
|
|
|
195
|
|
576
|
196
|
|
575
|
197 ----
|
|
|
198 -- find node potition to insert or to delete, the path will be in the stack
|
|
|
199 --
|
|
|
200 findNode : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Node a k) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t
|
|
|
201 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s → findNode1 s n1)
|
|
|
202 module FindNode where
|
|
|
203 findNode2 : SingleLinkedStack (Node a k) → (Maybe (Node a k)) → t
|
|
|
204 findNode2 s nothing = next tree s n0
|
|
|
205 findNode2 s (just n) = findNode tree s n0 n next
|
|
|
206 findNode1 : SingleLinkedStack (Node a k) → (Node a k) → t
|
|
|
207 findNode1 s n1 with (compTri (key n0) (key n1))
|
|
|
208 findNode1 s n1 | tri< a ¬b ¬c = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
|
|
|
209 findNode1 s n1 | tri≈ ¬a b ¬c = findNode2 s (right n1)
|
|
|
210 findNode1 s n1 | tri> ¬a ¬b c = findNode2 s (left n1)
|
|
|
211 -- ... | EQ = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
|
|
|
212 -- ... | GT = findNode2 s (right n1)
|
|
|
213 -- ... | LT = findNode2 s (left n1)
|
|
|
214
|
|
|
215
|
|
|
216
|
|
|
217
|
|
|
218 leafNode : {n : Level } { a : Set n } → a → (k : ℕ) → (Node a k)
|
|
|
219 leafNode v k1 = record { key = k1 ; value = v ; right = nothing ; left = nothing ; color = Red }
|
|
|
220
|
|
|
221 putRedBlackTree : {n m : Level} {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → {!!} → {!!} → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
|
222 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next with (root tree)
|
|
|
223 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | nothing = next (record tree {root = just (leafNode {!!} {!!}) })
|
|
|
224 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode {!!} {!!}) n2 (λ tree1 s n1 → insertNode tree1 s n1 next))
|
|
|
225 -- putRedBlackTree {n} {m} {t} {a} {k} tree value k1 next with (root tree)
|
|
|
226 -- ... | nothing = next (record tree {root = just (leafNode k1 value) })
|
|
|
227 -- ... | just n2 = clearSingleLinkedStack (nodeStack tree) (\ s → findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 → insertNode tree1 s n1 next))
|
|
|
228
|
|
|
229
|
|
|
230 -- getRedBlackTree : {n m : Level } {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} {A} a k → k → (RedBlackTree {n} {m} {t} {A} a k → (Maybe (Node a k)) → t) → t
|
|
|
231 -- getRedBlackTree {_} {_} {t} {a} {k} tree k1 cs = checkNode (root tree)
|
|
|
232 -- module GetRedBlackTree where -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html
|
|
|
233 -- search : Node a k → t
|
|
|
234 -- checkNode : Maybe (Node a k) → t
|
|
|
235 -- checkNode nothing = cs tree nothing
|
|
|
236 -- checkNode (just n) = search n
|
|
|
237 -- search n with compTri k1 (key n)
|
|
|
238 -- search n | tri< a ¬b ¬c = checkNode (left n)
|
|
|
239 -- search n | tri≈ ¬a b ¬c = cs tree (just n)
|
|
|
240 -- search n | tri> ¬a ¬b c = checkNode (right n)
|
|
|
241
|
|
|
242
|
|
|
243
|
|
|
244 -- compareT : {A B C : Set } → ℕ → ℕ → Tri A B C
|
|
|
245 -- compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder) x y
|
|
|
246 -- compareT x y | tri< a ¬b ¬c = tri< {!!} {!!} {!!}
|
|
|
247 -- compareT x y | tri≈ ¬a b ¬c = {!!}
|
|
|
248 -- compareT x y | tri> ¬a ¬b c = {!!}
|
|
|
249 -- -- ... | tri≈ a b c = {!!}
|
|
|
250 -- -- ... | tri< a b c = {!!}
|
|
|
251 -- -- ... | tri> a b c = {!!}
|
|
|
252
|
|
|
253 -- compare2 : (x y : ℕ ) → CompareResult {Level.zero}
|
|
|
254 -- compare2 zero zero = EQ
|
|
|
255 -- compare2 (suc _) zero = GT
|
|
|
256 -- compare2 zero (suc _) = LT
|
|
|
257 -- compare2 (suc x) (suc y) = compare2 x y
|
|
|
258
|
|
|
259 -- -- putUnblanceTree : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} {A} a k → k → a → (RedBlackTree {n} {m} {t} {A} a k → t) → t
|
|
|
260 -- -- putUnblanceTree {n} {m} {A} {a} {k} {t} tree k1 value next with (root tree)
|
|
|
261 -- -- ... | nothing = next (record tree {root = just (leafNode k1 value) })
|
|
|
262 -- -- ... | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next))
|
|
|
263
|
|
|
264 -- -- checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool
|
|
|
265 -- -- checkT nothing _ = false
|
|
|
266 -- -- checkT (just n) x with compTri (value n) x
|
|
|
267 -- -- ... | tri≈ _ _ _ = true
|
|
|
268 -- -- ... | _ = false
|
|
|
269
|
|
|
270 -- -- checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (just n) x ≡ true
|
|
|
271 -- -- checkEQ x n refl with compTri (value n) x
|
|
|
272 -- -- ... | tri≈ _ refl _ = refl
|
|
|
273 -- -- ... | tri> _ neq gt = ⊥-elim (neq refl)
|
|
|
274 -- -- ... | tri< lt neq _ = ⊥-elim (neq refl)
|
|
|
275
|
|
|
276
|
|
|
277 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
|
|
|
278 → RedBlackTree {n} {m} {t} a b
|
|
|
279 createEmptyRedBlackTreeℕ a b = record {
|
|
|
280 root = nothing
|
|
|
281 ; nodeStack = emptySingleLinkedStack
|
|
|
282 -- ; nodeComp = λ x x₁ → {!!}
|
|
|
283
|
|
|
284 }
|
|
|
285
|
|
|
286 -- ( x y : ℕ ) -> Tri ( x < y ) ( x ≡ y ) ( x > y )
|
|
|
287
|
|
|
288 -- test = (λ x → (createEmptyRedBlackTreeℕ x x)
|
|
|
289
|
|
576
|
290 -- ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0
|
|
575
|
291
|
|
|
292 -- tes = putRedBlackTree {_} {_} {_} (createEmptyRedBlackTreeℕ {_} {_} {_} 3 3) 2 2 (λ t → t)
|
