Mercurial > hg > Gears > GearsAgda

comparison RedBlackTree.agda @ 528:7719f40e1367

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix insertCase4
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Jan 2018 07:57:52 +0900
parents a829a367cf7d
children c9be3631cc41
comparison
equal deleted inserted replaced
527:a829a367cf7d 528:7719f40e1367
88 ... | _ = rotateNext tree s n0 parent grandParent 88 ... | _ = rotateNext tree s n0 parent grandParent
89 89
90 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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t 90 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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
91 insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!} 91 insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
92 92
93 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 -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t 93 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
94 insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next 94 insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next
95 with parent | grandParent 95 with (right parent) | (left grandParent)
96 ... | Nothing | _ = {!!}
97 ... | _ | Nothing = {!!}
98 ... | Just parent1 | Just grandParent1
99 with (right parent1) | (left grandParent1)
100 ... | Nothing | _ = {!!} 96 ... | Nothing | _ = {!!}
101 ... | _ | Nothing = {!!} 97 ... | _ | Nothing = {!!}
102 ... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent1) (key leftGrandParent) 98 ... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent)
103 ... | EQ | EQ = {!!} 99 ... | EQ | EQ = {!!}
104 ... | _ | _ = {!!} 100 ... | _ | _ = {!!}
105
106
107
108 101
109 102
110 {-# TERMINATING #-} 103 {-# TERMINATING #-}
111 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 104 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
112 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 ) 105 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
113 where 106 where
114 insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion 107 insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion
115 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html 108 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
116 insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t 109 insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
117 insertCase3 s n0 parent grandParent with left grandParent | right grandParent 110 insertCase3 s n0 parent grandParent with left grandParent | right grandParent
118 ... | Nothing | Nothing = insertCase4 tree s n0 Nothing Nothing next 111 ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
119 ... | Nothing | Just uncle = insertCase4 tree s n0 Nothing (Just uncle) next 112 ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next
120 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent ) 113 ... | Just uncle | _ with compare tree ( key uncle ) ( key parent )
121 ... | EQ = insertCase4 tree s n0 (Just uncle) {!!} next 114 ... | EQ = insertCase4 tree s n0 parent grandParent next
122 ... | _ with color uncle 115 ... | _ with color uncle
123 ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( 116 ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s (
124 record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 ) 117 record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
125 ... | Black = insertCase4 tree s n0 (Just uncle) {!!} next 118 ... | Black = insertCase4 tree s n0 parent grandParent next
126 insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t 119 insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
127 insertCase2 s n0 parent grandParent with color parent 120 insertCase2 s n0 parent grandParent with color parent
128 ... | Black = replaceNode tree s grandParent n0 next 121 ... | Black = replaceNode tree s grandParent n0 next
129 ... | Red = insertCase3 s n0 parent grandParent 122 ... | Red = insertCase3 s n0 parent grandParent
130 insertCase1 s n0 Nothing Nothing = next tree 123 insertCase1 s n0 Nothing Nothing = next tree
131 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next 124 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
132 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next 125 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
133 insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent 126 insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
134 where 127
135 128
136 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 129 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
137 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1) 130 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
138 where 131 where
139 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t 132 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t