Mercurial > hg > Gears > GearsAgda
diff RedBlackTree.agda @ 525:0696b9846415
write rotateRithg. but not working now
author | ryokka |
---|---|
date | Mon, 08 Jan 2018 18:23:55 +0900 |
parents | 8fbc3ef749b6 |
children | c2d236418459 |
line wrap: on
line diff
--- a/RedBlackTree.agda Fri Jan 05 17:23:06 2018 +0900 +++ b/RedBlackTree.agda Mon Jan 08 18:23:55 2018 +0900 @@ -66,8 +66,13 @@ ... | GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next ... | EQ = next tree -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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t -rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!} +-- 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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t +-- rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with parent +-- ... | Nothing = insertCase5 tree s n0 parent grandParent next +-- ... | Just parent with compare tree (key n0) (key (left parent))) +-- | EQ = insetCase5 tree s n0 parent grandParent next +-- | _ = insetCase5 tree s n0 parent grandParent next + 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 -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}