Mercurial > hg > Gears > GearsAgda
changeset 528:7719f40e1367
fix insertCase4
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 09 Jan 2018 07:57:52 +0900 |
| parents | a829a367cf7d |
| children | c9be3631cc41 |
| files | RedBlackTree.agda |
| diffstat | 1 files changed, 8 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/RedBlackTree.agda Mon Jan 08 19:43:49 2018 +0900 +++ b/RedBlackTree.agda Tue Jan 09 07:57:52 2018 +0900 @@ -90,23 +90,16 @@ 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 insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!} -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 +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 insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next - with parent | grandParent -... | Nothing | _ = {!!} -... | _ | Nothing = {!!} -... | Just parent1 | Just grandParent1 - with (right parent1) | (left grandParent1) + with (right parent) | (left grandParent) ... | Nothing | _ = {!!} ... | _ | Nothing = {!!} -... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent1) (key leftGrandParent) +... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent) ... | EQ | EQ = {!!} ... | _ | _ = {!!} - - - {-# TERMINATING #-} 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 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 ) @@ -115,14 +108,14 @@ -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t insertCase3 s n0 parent grandParent with left grandParent | right grandParent - ... | Nothing | Nothing = insertCase4 tree s n0 Nothing Nothing next - ... | Nothing | Just uncle = insertCase4 tree s n0 Nothing (Just uncle) next + ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next + ... | Nothing | Just uncle = insertCase4 tree s n0 parent grandParent next ... | Just uncle | _ with compare tree ( key uncle ) ( key parent ) - ... | EQ = insertCase4 tree s n0 (Just uncle) {!!} next + ... | EQ = insertCase4 tree s n0 parent grandParent next ... | _ with color uncle ... | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 ) - ... | Black = insertCase4 tree s n0 (Just uncle) {!!} next + ... | Black = insertCase4 tree s n0 parent grandParent next insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t insertCase2 s n0 parent grandParent with color parent ... | Black = replaceNode tree s grandParent n0 next @@ -131,7 +124,7 @@ insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent - where + 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 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)