Mercurial > hg > Members > Moririn
diff RedBlackTree.agda @ 575:73fc32092b64
push local rbtree
| author | ryokka |
|---|---|
| date | Fri, 01 Nov 2019 17:42:51 +0900 |
| parents | a6aa2ff5fea4 |
| children | 0ddfa505d612 |
line wrap: on
line diff
--- a/RedBlackTree.agda Thu Aug 16 18:22:08 2018 +0900 +++ b/RedBlackTree.agda Fri Nov 01 17:42:51 2019 +0900 @@ -1,24 +1,33 @@ module RedBlackTree where + +open import Level hiding (zero) + +open import Data.Nat hiding (compare) +open import Data.Nat.Properties as NatProp +open import Data.Maybe +open import Data.Bool +open import Data.Empty + +open import Relation.Binary +open import Relation.Binary.PropositionalEquality + open import stack -open import Level hiding (zero) -open import Relation.Binary -open import Data.Nat.Properties as NatProp record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where field - putImpl : treeImpl -> a -> (treeImpl -> t) -> t - getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t + putImpl : treeImpl → a → (treeImpl → t) → t + getImpl : treeImpl → (treeImpl → Maybe a → t) → t open TreeMethods record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where field tree : treeImpl treeMethods : TreeMethods {n} {m} {a} {t} treeImpl - putTree : a -> (Tree treeImpl -> t) -> t - putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) - getTree : (Tree treeImpl -> Maybe a -> t) -> t - getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) + putTree : a → (Tree treeImpl → t) → t + putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} )) + getTree : (Tree treeImpl → Maybe a → t) → t + getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d ) open Tree @@ -26,220 +35,256 @@ Red : Color Black : Color -data CompareResult {n : Level } : Set n where - LT : CompareResult - GT : CompareResult - EQ : CompareResult -record Node {n : Level } (a k : Set n) : Set n where +record Node {n : Level } (a : Set n) (k : ℕ) : Set n where inductive field - key : k + key : ℕ value : a right : Maybe (Node a k) left : Maybe (Node a k) color : Color {n} open Node -record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where +record RedBlackTree {n m : Level } {t : Set m} (a : Set n) (k : ℕ) : Set (m Level.⊔ n) where field root : Maybe (Node a k) nodeStack : SingleLinkedStack (Node a k) - compare : k -> k -> CompareResult {n} + -- compare : k → k → Tri A B C open RedBlackTree open SingleLinkedStack --- +compTri : ( x y : ℕ ) -> Tri ( x < y ) ( x ≡ y ) ( x > y ) +compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder) + where open import Relation.Binary + -- put new node at parent node, and rebuild tree to the top -- {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html -replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t +replaceNode : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s ( - \s parent -> replaceNode1 s parent) + \s parent → replaceNode1 s parent) module ReplaceNode where - replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t - replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } ) - replaceNode1 s (Just n1) with compare tree (key n1) (key n0) - ... | EQ = replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next - ... | GT = replaceNode tree s ( record n1 { left = Just n0 } ) next - ... | LT = replaceNode tree s ( record n1 { right = Just n0 } ) next + replaceNode1 : SingleLinkedStack (Node a k) → Maybe ( Node a k ) → t + replaceNode1 s nothing = next ( record tree { root = just (record n0 { color = Black}) } ) + replaceNode1 s (just n1) with compTri (key n1) (key n0) + replaceNode1 s (just n1) | tri< lt ¬eq ¬gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next + replaceNode1 s (just n1) | tri≈ ¬lt eq ¬gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { left = just n0 } ) next + replaceNode1 s (just n1) | tri> ¬lt ¬eq gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { right = just n0 } ) next -rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> - (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t -rotateRight {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext) +rotateRight : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → + (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t +rotateRight {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 → rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext) where - rotateRight1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> - (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t + rotateRight1 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → + (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0 - ... | Nothing = rotateNext tree s Nothing n0 - ... | Just n1 with parent - ... | Nothing = rotateNext tree s (Just n1 ) n0 - ... | Just parent1 with left parent1 - ... | Nothing = rotateNext tree s (Just n1) Nothing - ... | Just leftParent with compare tree (key n1) (key leftParent) - ... | EQ = rotateNext tree s (Just n1) parent - ... | _ = rotateNext tree s (Just n1) parent + ... | nothing = rotateNext tree s nothing n0 + ... | just n1 with parent + ... | nothing = rotateNext tree s (just n1 ) n0 + ... | just parent1 with left parent1 + ... | nothing = rotateNext tree s (just n1) nothing + ... | just leftParent with compTri (key n1) (key leftParent) + rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri< a₁ ¬b ¬c = rotateNext tree s (just n1) parent + rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri≈ ¬a b ¬c = rotateNext tree s (just n1) parent + rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri> ¬a ¬b c = rotateNext tree s (just n1) parent -rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> - (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t -rotateLeft {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext) +rotateLeft : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → + (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t +rotateLeft {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 → rotateLeft1 tree s n0 parent rotateNext) where - rotateLeft1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> - (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t + rotateLeft1 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → + (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0 - ... | Nothing = rotateNext tree s Nothing n0 - ... | Just n1 with parent - ... | Nothing = rotateNext tree s (Just n1) Nothing - ... | Just parent1 with right parent1 - ... | Nothing = rotateNext tree s (Just n1) Nothing - ... | Just rightParent with compare tree (key n1) (key rightParent) - ... | EQ = rotateNext tree s (Just n1) parent - ... | _ = rotateNext tree s (Just n1) parent + ... | nothing = rotateNext tree s nothing n0 + ... | just n1 with parent + ... | nothing = rotateNext tree s (just n1) nothing + ... | just parent1 with right parent1 + ... | nothing = rotateNext tree s (just n1) nothing + ... | just rightParent with compTri (key n1) (key rightParent) + rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri< a₁ ¬b ¬c = rotateNext tree s (just n1) parent + rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri≈ ¬a b ¬c = rotateNext tree s (just n1) parent + rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri> ¬a ¬b c = rotateNext tree s (just n1) parent + -- ... | EQ = rotateNext tree s (just n1) parent + -- ... | _ = rotateNext tree s (just n1) parent {-# TERMINATING #-} -insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t -insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next) +insertCase5 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t +insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent → insertCase51 tree s n0 parent grandParent next) where - insertCase51 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k -> t) -> t + insertCase51 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → Maybe (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t insertCase51 {n} {m} {t} {a} {k} tree s n0 parent grandParent next with n0 - ... | Nothing = next tree - ... | Just n1 with parent | grandParent - ... | Nothing | _ = next tree - ... | _ | Nothing = next tree - ... | Just parent1 | Just grandParent1 with left parent1 | left grandParent1 - ... | Nothing | _ = next tree - ... | _ | Nothing = next tree - ... | Just leftParent1 | Just leftGrandParent1 - with compare tree (key n1) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1) - ... | EQ | EQ = rotateRight tree s n0 parent - (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next) - ... | _ | _ = rotateLeft tree s n0 parent - (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next) + ... | nothing = next tree + ... | just n1 with parent | grandParent + ... | nothing | _ = next tree + ... | _ | nothing = next tree + ... | just parent1 | just grandParent1 with left parent1 | left grandParent1 + ... | nothing | _ = next tree + ... | _ | nothing = next tree + ... | just leftParent1 | just leftGrandParent1 + with compTri (key n1) (key leftParent1) | compTri (key leftParent1) (key leftGrandParent1) + ... | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1 = rotateRight tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next) + ... | _ | _ = rotateLeft tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next) + -- ... | EQ | EQ = rotateRight tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next) + -- ... | _ | _ = rotateLeft tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next) -insertCase4 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t +insertCase4 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next with (right parent) | (left grandParent) -... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next -... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next -... | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent) -... | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent) - (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next)) -... | _ | _ = insertCase41 tree s n0 parent grandParent next +... | nothing | _ = insertCase5 tree s (just n0) parent grandParent next +... | _ | nothing = insertCase5 tree s (just n0) parent grandParent next +... | just rightParent | just leftGrandParent with compTri (key n0) (key rightParent) | compTri (key parent) (key leftGrandParent) -- (key n0) (key rightParent) | (key parent) (key leftGrandParent) +-- ... | EQ | EQ = popSingleLinkedStack s (\ s n1 → rotateLeft tree s (left n0) (just grandParent) +-- (\ tree s n0 parent → insertCase5 tree s n0 rightParent grandParent next)) +-- ... | _ | _ = insertCase41 tree s n0 parent grandParent next +... | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1 = popSingleLinkedStack s (\ s n1 → rotateLeft tree s (left n0) (just grandParent) (\ tree s n0 parent → insertCase5 tree s n0 rightParent grandParent next)) +... | _ | _ = insertCase41 tree s n0 parent grandParent next where - insertCase41 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t + insertCase41 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t insertCase41 {n} {m} {t} {a} {k} tree s n0 parent grandParent next - with (left parent) | (right grandParent) - ... | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next - ... | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next - ... | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent) - ... | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent) - (\ tree s n0 parent -> insertCase5 tree s n0 leftParent grandParent next)) - ... | _ | _ = insertCase5 tree s (Just n0) parent grandParent next + with (left parent) | (right grandParent) + ... | nothing | _ = insertCase5 tree s (just n0) parent grandParent next + ... | _ | nothing = insertCase5 tree s (just n0) parent grandParent next + ... | just leftParent | just rightGrandParent with compTri (key n0) (key leftParent) | compTri (key parent) (key rightGrandParent) + ... | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1 = popSingleLinkedStack s (\ s n1 → rotateRight tree s (right n0) (just grandParent) (\ tree s n0 parent → insertCase5 tree s n0 leftParent grandParent next)) + ... | _ | _ = insertCase5 tree s (just n0) parent grandParent next + -- ... | EQ | EQ = popSingleLinkedStack s (\ s n1 → rotateRight tree s (right n0) (just grandParent) + -- (\ tree s n0 parent → insertCase5 tree s n0 leftParent grandParent next)) + -- ... | _ | _ = insertCase5 tree s (just n0) parent grandParent next -colorNode : {n : Level } {a k : Set n} -> Node a k -> Color -> Node a k +colorNode : {n : Level } {a : Set n} {k : ℕ} → Node a k → Color → Node a k colorNode old c = record old { color = c } {-# TERMINATING #-} -insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t +insertNode : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t insertNode {n} {m} {t} {a} {k} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0) where - insertCase1 : Node a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t -- placed here to allow mutual recursion + insertCase1 : Node a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t -- placed here to allow mutual recursion -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html - insertCase3 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t + insertCase3 : SingleLinkedStack (Node a k) → 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 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 parent grandParent next - ... | _ with color uncle - ... | Red = pop2SingleLinkedStack s ( \s p0 p1 -> insertCase1 ( - record grandParent { color = Red ; left = Just ( record parent { color = Black } ) ; right = Just ( record uncle { color = Black } ) }) s p0 p1 ) - ... | Black = insertCase4 tree s n0 parent grandParent next - insertCase2 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t + ... | nothing | nothing = insertCase4 tree s n0 parent grandParent next + ... | nothing | just uncle = insertCase4 tree s n0 parent grandParent next + ... | just uncle | _ with compTri ( key uncle ) ( key parent ) + insertCase3 s n0 parent grandParent | just uncle | _ | tri≈ ¬a b ¬c = insertCase4 tree s n0 parent grandParent next + insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c with color uncle + insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c | Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 ( + record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 ) + insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c | Black = insertCase4 tree s n0 parent grandParent next + insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c with color uncle + insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c | Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 ( record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 ) + insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c | Black = insertCase4 tree s n0 parent grandParent next + -- ... | EQ = insertCase4 tree s n0 parent grandParent next + -- ... | _ with color uncle + -- ... | Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 ( + -- record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 ) + -- ... | Black = insertCase4 tree s n0 parent grandParent next --!! + insertCase2 : SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → t insertCase2 s n0 parent grandParent with color parent ... | Black = replaceNode tree s n0 next ... | Red = insertCase3 s n0 parent grandParent - insertCase1 n0 s Nothing Nothing = next tree - insertCase1 n0 s Nothing (Just grandParent) = next tree - insertCase1 n0 s (Just parent) Nothing = replaceNode tree s (colorNode n0 Black) next - insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent + insertCase1 n0 s nothing nothing = next tree + insertCase1 n0 s nothing (just grandParent) = next tree + insertCase1 n0 s (just parent) nothing = replaceNode tree s (colorNode n0 Black) next + insertCase1 n0 s (just parent) (just grandParent) = insertCase2 s n0 parent grandParent ---- -- find node potition to insert or to delete, the path will be in the stack --- -findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t -findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1) +-- +findNode : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Node a k) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t +findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s → findNode1 s n1) module FindNode where - findNode2 : SingleLinkedStack (Node a k) -> (Maybe (Node a k)) -> t - findNode2 s Nothing = next tree s n0 - findNode2 s (Just n) = findNode tree s n0 n next - findNode1 : SingleLinkedStack (Node a k) -> (Node a k) -> t - findNode1 s n1 with (compare tree (key n0) (key n1)) - ... | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n0 } ) ) - ... | GT = findNode2 s (right n1) - ... | LT = findNode2 s (left n1) + findNode2 : SingleLinkedStack (Node a k) → (Maybe (Node a k)) → t + findNode2 s nothing = next tree s n0 + findNode2 s (just n) = findNode tree s n0 n next + findNode1 : SingleLinkedStack (Node a k) → (Node a k) → t + findNode1 s n1 with (compTri (key n0) (key n1)) + findNode1 s n1 | tri< a ¬b ¬c = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) ) + findNode1 s n1 | tri≈ ¬a b ¬c = findNode2 s (right n1) + findNode1 s n1 | tri> ¬a ¬b c = findNode2 s (left n1) + -- ... | EQ = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) ) + -- ... | GT = findNode2 s (right n1) + -- ... | LT = findNode2 s (left n1) + + + + +leafNode : {n : Level } { a : Set n } → a → (k : ℕ) → (Node a k) +leafNode v k1 = record { key = k1 ; value = v ; right = nothing ; left = nothing ; color = Red } + +putRedBlackTree : {n m : Level} {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → {!!} → {!!} → (RedBlackTree {n} {m} {t} a k → t) → t +putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next with (root tree) +putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | nothing = next (record tree {root = just (leafNode {!!} {!!}) }) +putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode {!!} {!!}) n2 (λ tree1 s n1 → insertNode tree1 s n1 next)) +-- putRedBlackTree {n} {m} {t} {a} {k} tree value k1 next with (root tree) +-- ... | nothing = next (record tree {root = just (leafNode k1 value) }) +-- ... | just n2 = clearSingleLinkedStack (nodeStack tree) (\ s → findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 → insertNode tree1 s n1 next)) + + +-- getRedBlackTree : {n m : Level } {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} {A} a k → k → (RedBlackTree {n} {m} {t} {A} a k → (Maybe (Node a k)) → t) → t +-- getRedBlackTree {_} {_} {t} {a} {k} tree k1 cs = checkNode (root tree) +-- module GetRedBlackTree where -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html +-- search : Node a k → t +-- checkNode : Maybe (Node a k) → t +-- checkNode nothing = cs tree nothing +-- checkNode (just n) = search n +-- search n with compTri k1 (key n) +-- search n | tri< a ¬b ¬c = checkNode (left n) +-- search n | tri≈ ¬a b ¬c = cs tree (just n) +-- search n | tri> ¬a ¬b c = checkNode (right n) + -leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k -leafNode k1 value = record { - key = k1 ; - value = value ; - right = Nothing ; - left = Nothing ; - color = Red - } +-- compareT : {A B C : Set } → ℕ → ℕ → Tri A B C +-- compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder) x y +-- compareT x y | tri< a ¬b ¬c = tri< {!!} {!!} {!!} +-- compareT x y | tri≈ ¬a b ¬c = {!!} +-- compareT x y | tri> ¬a ¬b c = {!!} +-- -- ... | tri≈ a b c = {!!} +-- -- ... | tri< a b c = {!!} +-- -- ... | tri> a b c = {!!} -putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t -putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) -... | Nothing = next (record tree {root = Just (leafNode k1 value) }) -... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) +-- compare2 : (x y : ℕ ) → CompareResult {Level.zero} +-- compare2 zero zero = EQ +-- compare2 (suc _) zero = GT +-- compare2 zero (suc _) = LT +-- compare2 (suc x) (suc y) = compare2 x y -getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> (RedBlackTree {n} {m} {t} a k -> (Maybe (Node a k)) -> t) -> t -getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree) - module GetRedBlackTree where -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html - search : Node a k -> t - checkNode : Maybe (Node a k) -> t - checkNode Nothing = cs tree Nothing - checkNode (Just n) = search n - search n with compare tree k1 (key n) - search n | LT = checkNode (left n) - search n | GT = checkNode (right n) - search n | EQ = cs tree (Just n) - -open import Data.Nat hiding (compare) +-- -- putUnblanceTree : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} {A} a k → k → a → (RedBlackTree {n} {m} {t} {A} a k → t) → t +-- -- putUnblanceTree {n} {m} {A} {a} {k} {t} tree k1 value next with (root tree) +-- -- ... | nothing = next (record tree {root = just (leafNode k1 value) }) +-- -- ... | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next)) -compareℕ : ℕ → ℕ → CompareResult {Level.zero} -compareℕ x y with Data.Nat.compare x y -... | less _ _ = LT -... | equal _ = EQ -... | greater _ _ = GT +-- -- checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool +-- -- checkT nothing _ = false +-- -- checkT (just n) x with compTri (value n) x +-- -- ... | tri≈ _ _ _ = true +-- -- ... | _ = false -compareT : ℕ → ℕ → CompareResult {Level.zero} -compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) x y -... | tri≈ _ _ _ = EQ -... | tri< _ _ _ = LT -... | tri> _ _ _ = GT - -compare2 : (x y : ℕ ) -> CompareResult {Level.zero} -compare2 zero zero = EQ -compare2 (suc _) zero = GT -compare2 zero (suc _) = LT -compare2 (suc x) (suc y) = compare2 x y - -putUnblanceTree : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → (RedBlackTree {n} {m} {t} a k → t) → t -putUnblanceTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) -... | Nothing = next (record tree {root = Just (leafNode k1 value) }) -... | Just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next)) +-- -- checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (just n) x ≡ true +-- -- checkEQ x n refl with compTri (value n) x +-- -- ... | tri≈ _ refl _ = refl +-- -- ... | tri> _ neq gt = ⊥-elim (neq refl) +-- -- ... | tri< lt neq _ = ⊥-elim (neq refl) -createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ -createEmptyRedBlackTreeℕ {m} a {t} = record { - root = Nothing +createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ) + → RedBlackTree {n} {m} {t} a b +createEmptyRedBlackTreeℕ a b = record { + root = nothing ; nodeStack = emptySingleLinkedStack - ; compare = compareT + -- ; nodeComp = λ x x₁ → {!!} + } - + +-- ( x y : ℕ ) -> Tri ( x < y ) ( x ≡ y ) ( x > y ) + +-- test = (λ x → (createEmptyRedBlackTreeℕ x x) + +ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0 + +-- tes = putRedBlackTree {_} {_} {_} (createEmptyRedBlackTreeℕ {_} {_} {_} 3 3) 2 2 (λ t → t)