|
576
|
1 module hoareRedBlackTree where
|
|
|
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
|
|
|
18
|
|
|
19 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
|
|
|
20 field
|
|
|
21 putImpl : treeImpl → a → (treeImpl → t) → t
|
|
|
22 getImpl : treeImpl → (treeImpl → Maybe a → t) → t
|
|
|
23 open TreeMethods
|
|
|
24
|
|
|
25 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
|
|
|
26 field
|
|
|
27 tree : treeImpl
|
|
|
28 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
|
|
|
29 putTree : a → (Tree treeImpl → t) → t
|
|
|
30 putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
|
|
|
31 getTree : (Tree treeImpl → Maybe a → t) → t
|
|
|
32 getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )
|
|
|
33
|
|
|
34 open Tree
|
|
|
35
|
|
|
36 data Color {n : Level } : Set n where
|
|
|
37 Red : Color
|
|
|
38 Black : Color
|
|
|
39
|
|
|
40
|
|
|
41 record Node {n : Level } (a : Set n) (k : ℕ) : Set n where
|
|
|
42 inductive
|
|
|
43 field
|
|
|
44 key : ℕ
|
|
|
45 value : a
|
|
|
46 right : Maybe (Node a k)
|
|
|
47 left : Maybe (Node a k)
|
|
|
48 color : Color {n}
|
|
|
49 open Node
|
|
|
50
|
|
|
51 record RedBlackTree {n m : Level } {t : Set m} (a : Set n) (k : ℕ) : Set (m Level.⊔ n) where
|
|
|
52 field
|
|
|
53 root : Maybe (Node a k)
|
|
|
54 nodeStack : SingleLinkedStack (Node a k)
|
|
|
55 -- compare : k → k → Tri A B C
|
|
|
56 -- <-cmp
|
|
|
57
|
|
|
58 open RedBlackTree
|
|
|
59
|
|
|
60 open SingleLinkedStack
|
|
|
61
|
|
|
62
|
|
|
63
|
|
|
64 ----
|
|
|
65 -- find node potition to insert or to delete, the path will be in the stack
|
|
|
66 --
|
|
|
67
|
|
|
68 {-# TERMINATING #-}
|
|
|
69 findNode : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
|
70 findNode {n} {m} {a} {k} {t} tree n0 next with root tree
|
|
|
71 findNode {n} {m} {a} {k} {t} tree n0 next | nothing = next tree
|
|
|
72 findNode {n} {m} {a} {k} {t} tree n0 next | just x with <-cmp (key x) (key n0)
|
|
|
73 findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
|
|
|
74 findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
|
|
|
75 findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
|
|
|
76
|
|
|
77
|
|
|
78 findNode1 : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
|
|
577
|
79 findNode1 {n} {m} {a} {k} {t} tree n0 next = pushSingleLinkedStack (nodeStack tree) n0 (λ st → findNode3 st n0)
|
|
|
80 module FindNode where
|
|
|
81 findNode2 : (Maybe (Node a k)) → SingleLinkedStack (Node a k) → t
|
|
|
82 findNode2 nothing st = next tree
|
|
|
83 findNode2 (just x) st = findNode1 (record {root = just x ; nodeStack = st}) x next
|
|
576
|
84
|
|
|
85 findNode3 : SingleLinkedStack (Node a k) → Node a k → t
|
|
|
86 findNode3 s1 n1 with (<-cmp (key n0) (key n1))
|
|
|
87 findNode3 s1 n1 | tri≈ ¬a b ¬c = next (record {root = root tree ; nodeStack = s1})
|
|
577
|
88 findNode3 s1 n1 | tri< a ¬b ¬c = findNode2 (right n1) s1
|
|
|
89 findNode3 s1 n1 | tri> ¬a ¬b c = findNode2 (left n1) s1
|
|
576
|
90
|
|
|
91
|
|
|
92 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
|
|
|
93 → RedBlackTree {n} {m} {t} a b
|
|
|
94 createEmptyRedBlackTreeℕ a b = record {
|
|
|
95 root = nothing
|
|
|
96 ; nodeStack = emptySingleLinkedStack
|
|
|
97 }
|
|
|
98
|
