annotate RedBlackTree.agda @ 532:ccf98ed4a4f7

fix red black tree
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Jan 2018 23:56:42 +0900
parents f6060e1bf900
children 2d6ccbf429ad
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
417
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
1 module RedBlackTree where
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
2
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
3 open import stack
511
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
4 open import Level
417
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
5
511
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
6 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
7 field
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
8 putImpl : treeImpl -> a -> (treeImpl -> t) -> t
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
9 getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
10 open TreeMethods
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
11
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
12 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
417
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
13 field
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
14 tree : treeImpl
513
f2a3acc766b5 fix RedBlackTree.agda
ryokka
parents: 512
diff changeset
15 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
f2a3acc766b5 fix RedBlackTree.agda
ryokka
parents: 512
diff changeset
16 putTree : a -> (Tree treeImpl -> t) -> t
511
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
17 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
513
f2a3acc766b5 fix RedBlackTree.agda
ryokka
parents: 512
diff changeset
18 getTree : (Tree treeImpl -> Maybe a -> t) -> t
511
044c25475ed4 fix stack.agda
mir3636
parents: 478
diff changeset
19 getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
427
07ccd411ad70 fix interface in agda
ryokka
parents: 425
diff changeset
20
478
0223c07c3946 fix stack.agda
ryokka
parents: 428
diff changeset
21 open Tree
0223c07c3946 fix stack.agda
ryokka
parents: 428
diff changeset
22
513
f2a3acc766b5 fix RedBlackTree.agda
ryokka
parents: 512
diff changeset
23 data Color {n : Level } : Set n where
425
ea6353b6c4ef Add findNode to RedBlackTree.agda
innparusu
parents: 417
diff changeset
24 Red : Color
ea6353b6c4ef Add findNode to RedBlackTree.agda
innparusu
parents: 417
diff changeset
25 Black : Color
ea6353b6c4ef Add findNode to RedBlackTree.agda
innparusu
parents: 417
diff changeset
26
512
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
27 data CompareResult {n : Level } : Set n where
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
28 LT : CompareResult
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
29 GT : CompareResult
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
30 EQ : CompareResult
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
31
513
f2a3acc766b5 fix RedBlackTree.agda
ryokka
parents: 512
diff changeset
32 record Node {n : Level } (a k : Set n) : Set n where
f2a3acc766b5 fix RedBlackTree.agda
ryokka
parents: 512
diff changeset
33 inductive
425
ea6353b6c4ef Add findNode to RedBlackTree.agda
innparusu
parents: 417
diff changeset
34 field
512
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
35 key : k
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
36 value : a
513
f2a3acc766b5 fix RedBlackTree.agda
ryokka
parents: 512
diff changeset
37 right : Maybe (Node a k)
f2a3acc766b5 fix RedBlackTree.agda
ryokka
parents: 512
diff changeset
38 left : Maybe (Node a k)
514
f86da73d611e fix RedBlackTree.agda
ryokka
parents: 513
diff changeset
39 color : Color {n}
512
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
40 open Node
425
ea6353b6c4ef Add findNode to RedBlackTree.agda
innparusu
parents: 417
diff changeset
41
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
42 record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
417
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
43 field
514
f86da73d611e fix RedBlackTree.agda
ryokka
parents: 513
diff changeset
44 root : Maybe (Node a k)
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
45 nodeStack : Stack {n} {m} (Node a k) {t} si
514
f86da73d611e fix RedBlackTree.agda
ryokka
parents: 513
diff changeset
46 compare : k -> k -> CompareResult {n}
425
ea6353b6c4ef Add findNode to RedBlackTree.agda
innparusu
parents: 417
diff changeset
47
417
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
48 open RedBlackTree
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
49
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
50 open Stack
512
95865cab040a fix RedBlackTree.agda
mir3636
parents: 511
diff changeset
51
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
52 --
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
53 -- put new node at parent node, and rebuild tree to the top
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
54 --
519
0a723e418b2a add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 518
diff changeset
55 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
56 replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
57 replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
58 \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
59 where
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
60 replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t
529
c9be3631cc41 fix insertCase4
ryokka
parents: 528
diff changeset
61 replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )
c9be3631cc41 fix insertCase4
ryokka
parents: 528
diff changeset
62 replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )
c9be3631cc41 fix insertCase4
ryokka
parents: 528
diff changeset
63 replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
64 replaceNode1 s (Just grandParent) result with result
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
65 ... | LT = replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
66 ... | GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
529
c9be3631cc41 fix insertCase4
ryokka
parents: 528
diff changeset
67 ... | EQ = next tree
478
0223c07c3946 fix stack.agda
ryokka
parents: 428
diff changeset
68
525
0696b9846415 write rotateRithg. but not working now
ryokka
parents: 523
diff changeset
69
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
70 rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) ->
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
71 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
72 rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext = getStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext)
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
73 where
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
74 rotateRight1 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) ->
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
75 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
76 rotateRight1 {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext with n0
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
77 ... | Nothing = rotateNext tree s Nothing n0
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
78 ... | Just n1 with parent
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
79 ... | Nothing = rotateNext tree s (Just n1 ) n0
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
80 ... | Just parent1 with left parent1
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
81 ... | Nothing = rotateNext tree s (Just n1) Nothing
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
82 ... | Just leftParent with compare tree (key n1) (key leftParent)
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
83 ... | EQ = rotateNext tree s (Just n1) parent
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
84 ... | _ = rotateNext tree s (Just n1) parent
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
85
519
0a723e418b2a add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 518
diff changeset
86
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
87 rotateLeft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) ->
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
88 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
89 rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext = getStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext)
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
90 where
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
91 rotateLeft1 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) ->
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
92 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
93 rotateLeft1 {n} {m} {t} {a} {k} {si} tree s n0 parent rotateNext with n0
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
94 ... | Nothing = rotateNext tree s Nothing n0
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
95 ... | Just n1 with parent
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
96 ... | Nothing = rotateNext tree s (Just n1) Nothing
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
97 ... | Just parent1 with right parent1
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
98 ... | Nothing = rotateNext tree s (Just n1) Nothing
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
99 ... | Just rightParent with compare tree (key n1) (key rightParent)
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
100 ... | EQ = rotateNext tree s (Just n1) parent
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
101 ... | _ = rotateNext tree s (Just n1) parent
519
0a723e418b2a add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 518
diff changeset
102
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
103 {-# TERMINATING #-}
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
104 insertCase5 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
105 insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = pop2Stack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next)
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
106 where
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
107 insertCase51 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
108 insertCase51 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with n0
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
109 ... | Nothing = next tree
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
110 ... | Just n1 with parent | grandParent
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
111 ... | Nothing | _ = next tree
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
112 ... | _ | Nothing = next tree
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
113 ... | Just parent1 | Just grandParent1 with left parent1 | left grandParent1
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
114 ... | Nothing | _ = next tree
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
115 ... | _ | Nothing = next tree
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
116 ... | Just leftParent1 | Just leftGrandParent1
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
117 with compare tree (key n1) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1)
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
118 ... | EQ | EQ = rotateRight tree s n0 parent
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
119 (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next)
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
120 ... | _ | _ = rotateLeft tree s n0 parent
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
121 (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next)
519
0a723e418b2a add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 518
diff changeset
122
528
7719f40e1367 fix insertCase4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 527
diff changeset
123 insertCase4 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
527
a829a367cf7d add insertCase4
ryokka
parents: 526
diff changeset
124 insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next
528
7719f40e1367 fix insertCase4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 527
diff changeset
125 with (right parent) | (left grandParent)
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
126 ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
127 ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next
528
7719f40e1367 fix insertCase4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 527
diff changeset
128 ... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent)
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
129 ... | EQ | EQ = popStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent)
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
130 (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next))
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
131 ... | _ | _ = insertCase41 tree s n0 parent grandParent next
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
132 where
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
133 insertCase41 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
134 insertCase41 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
135 with (left parent) | (right grandParent)
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
136 ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
137 ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next
530
63f3df7f5448 add insertCase41, insertCase5
ryokka
parents: 529
diff changeset
138 ... | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent)
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
139 ... | EQ | EQ = popStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent)
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
140 (\ tree s n0 parent -> insertCase5 tree s n0 leftParent grandParent next))
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
141 ... | _ | _ = insertCase5 tree s (Just n0) parent grandParent next
527
a829a367cf7d add insertCase4
ryokka
parents: 526
diff changeset
142
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
143 colorNode : {n : Level } {a k : Set n} -> Node a k -> Color -> Node a k
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
144 colorNode old c = record old { color = c }
527
a829a367cf7d add insertCase4
ryokka
parents: 526
diff changeset
145
519
0a723e418b2a add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 518
diff changeset
146 {-# TERMINATING #-}
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
147 insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
148 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (insertCase1 n0)
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
149 where
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
150 insertCase1 : Node a k -> Stack (Node a k) si -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion
519
0a723e418b2a add some more directives in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 518
diff changeset
151 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
152 insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
153 insertCase3 s n0 parent grandParent with left grandParent | right grandParent
528
7719f40e1367 fix insertCase4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 527
diff changeset
154 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
7719f40e1367 fix insertCase4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 527
diff changeset
155 ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
156 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent )
528
7719f40e1367 fix insertCase4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 527
diff changeset
157 ... | EQ = insertCase4 tree s n0 parent grandParent next
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
158 ... | _ with color uncle
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
159 ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 (
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
160 record grandParent { color = Red ; left = Just ( record parent { color = Black } ) ; right = Just ( record uncle { color = Black } ) }) s p0 p1 )
528
7719f40e1367 fix insertCase4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 527
diff changeset
161 ... | Black = insertCase4 tree s n0 parent grandParent next
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
162 insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
163 insertCase2 s n0 parent grandParent with color parent
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
164 ... | Black = replaceNode tree s parent n0 next
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
165 ... | Red = insertCase3 s n0 parent grandParent
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
166 insertCase1 n0 s Nothing Nothing = next tree
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
167 insertCase1 n0 s Nothing (Just grandParent) = next tree
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
168 insertCase1 n0 s (Just parent) Nothing = replaceNode tree s parent (colorNode n0 Black) next
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
169 insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
528
7719f40e1367 fix insertCase4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 527
diff changeset
170
531
f6060e1bf900 add clearStack
ryokka
parents: 530
diff changeset
171 ----
f6060e1bf900 add clearStack
ryokka
parents: 530
diff changeset
172 -- find node potition to insert or to delete, the pass will be in the stack
f6060e1bf900 add clearStack
ryokka
parents: 530
diff changeset
173 --
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
174 findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
175 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
417
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
176 where
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
177 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
178 findNode2 s Nothing = next tree s n0
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
179 findNode2 s (Just n) = findNode tree s n0 n next
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
180 findNode1 : Stack (Node a k) si -> (Node a k) -> t
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
181 findNode1 s n1 with (compare tree (key n0) (key n1))
529
c9be3631cc41 fix insertCase4
ryokka
parents: 528
diff changeset
182 ... | EQ = next tree s n0
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
183 ... | GT = findNode2 s (right n1)
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
184 ... | LT = findNode2 s (left n1)
425
ea6353b6c4ef Add findNode to RedBlackTree.agda
innparusu
parents: 417
diff changeset
185
ea6353b6c4ef Add findNode to RedBlackTree.agda
innparusu
parents: 417
diff changeset
186
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
187 leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
188 leafNode k1 value = record {
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
189 key = k1 ;
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
190 value = value ;
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
191 right = Nothing ;
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
192 left = Nothing ;
532
ccf98ed4a4f7 fix red black tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
193 color = Red
518
c9f90f573efe add more reblack tree in agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
194 }
417
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
195
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
196 putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
197 putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
198 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
531
f6060e1bf900 add clearStack
ryokka
parents: 530
diff changeset
199 ... | Just n2 = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
200
522
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
201 getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
202 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
417
24c98ca207f4 add RedBlackTree.agda
mir3636
parents:
diff changeset
203 where
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
204 checkNode : Maybe (Node a k) -> t
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
205 checkNode Nothing = cs tree Nothing
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
206 checkNode (Just n) = search n
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
207 where
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
208 search : Node a k -> t
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
209 search n with compare tree k1 (key n)
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
210 search n | LT = checkNode (left n)
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
211 search n | GT = checkNode (right n)
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 514
diff changeset
212 search n | EQ = cs tree (Just n)