Mercurial > hg > Gears > GearsAgda
changeset 575:73fc32092b64
push local rbtree
| author | ryokka |
|---|---|
| date | Fri, 01 Nov 2019 17:42:51 +0900 |
| parents | 70b09cbefd45 |
| children | 40d01b368e34 |
| files | RedBlackTree.agda Todo.txt redBlackTreeHoare.agda redBlackTreeTest.agda stack.agda |
| diffstat | 5 files changed, 846 insertions(+), 343 deletions(-) [+] |
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)
--- a/Todo.txt Thu Aug 16 18:22:08 2018 +0900 +++ b/Todo.txt Fri Nov 01 17:42:51 2019 +0900 @@ -1,3 +1,5 @@ + + Sun May 6 17:54:50 JST 2018 do1 a $ \b -> do2 b next を、do1 と do2 に分離することはできる? @@ -44,3 +46,11 @@ gotoを用いてモデル検査と証明の組み合わせを実現する +Wed Aug 27 17:52:00 JST 2019 + + 別で定義した TriCotomos や \=? などの Relation の関数を + Agdaで定義してあるものに置き換える,まとめる + + HoareLogic をベースにした SingleLinkedStack の作成 + + HoareLogic ベースの Tree の証明
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/redBlackTreeHoare.agda Fri Nov 01 17:42:51 2019 +0900 @@ -0,0 +1,290 @@ +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 + +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 +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 ) + +open Tree + +data Color {n : Level } : Set n where + Red : Color + Black : Color + + +record Node {n : Level } (a : Set n) (k : ℕ) : Set n where + inductive + field + 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 : Set n) (k : ℕ) : Set (m Level.⊔ n) where + field + root : Maybe (Node a k) + nodeStack : SingleLinkedStack (Node a k) + -- 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 : 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) + 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 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 : 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 : 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 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 : 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 : 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 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 : 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 : 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 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 : 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 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 : 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 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 : 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 : 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 + -- 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 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 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 + +---- +-- find node potition to insert or to delete, the path will be in the stack +-- +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 (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) + + + +-- 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 = {!!} + +-- 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 : 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)) + +-- -- checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool +-- -- checkT nothing _ = false +-- -- checkT (just n) x with compTri (value n) x +-- -- ... | tri≈ _ _ _ = true +-- -- ... | _ = false + +-- -- 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ℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ) + → RedBlackTree {n} {m} {t} a b +createEmptyRedBlackTreeℕ a b = record { + root = nothing + ; nodeStack = emptySingleLinkedStack + -- ; 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)
--- a/redBlackTreeTest.agda Thu Aug 16 18:22:08 2018 +0900 +++ b/redBlackTreeTest.agda Fri Nov 01 17:42:51 2019 +0900 @@ -1,17 +1,21 @@ module redBlackTreeTest where -open import RedBlackTree -open import stack open import Level hiding (zero) renaming ( suc to succ ) open import Data.Empty - +open import Data.List +open import Data.Maybe +open import Data.Bool open import Data.Nat +open import Data.Nat.Properties as NatProp + open import Relation.Nullary - +open import Relation.Binary open import Algebra -open import Data.Nat.Properties as NatProp + +open import RedBlackTree +open import stack open Tree open Node @@ -20,197 +24,350 @@ -- tests -putTree1 : {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 +putTree1 : {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 putTree1 {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)) +... | 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)) open import Relation.Binary.PropositionalEquality open import Relation.Binary.Core open import Function -check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} -check1 Nothing _ = False -check1 (Just n) x with Data.Nat.compare (value n) x -... | equal _ = True -... | _ = False +-- check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool +-- check1 nothing _ = false +-- check1 (just n) x with Data.Nat.compare (value n) x +-- ... | equal _ = true +-- ... | _ = false -check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} -check2 Nothing _ = False -check2 (Just n) x with compare2 (value n) x -... | EQ = True -... | _ = False +check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool +check2 nothing _ = false +check2 (just n) x with compare2 (value n) x +... | EQ = true +... | _ = false -test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True )) -test1 = refl +test1 : {m : Level} {A B C : Set} → putTree1 {Level.zero} {succ Level.zero} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ {!!} {!!} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true )) +test1 = {!!} -test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( - λ t → putTree1 t 2 2 ( - λ t → getRedBlackTree t 1 ( - λ t x → check2 x 1 ≡ True ))) -test2 = refl +-- test2 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( +-- λ t → putTree1 t 2 2 ( +-- λ t → getRedBlackTree t 1 ( +-- λ t x → check2 {m} x 1 ≡ true ))) +-- test2 = refl -open ≡-Reasoning -test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 - $ λ t → putTree1 t 2 2 - $ λ t → putTree1 t 3 3 - $ λ t → putTree1 t 4 4 - $ λ t → getRedBlackTree t 1 - $ λ t x → check2 x 1 ≡ True -test3 = begin - check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1 - ≡⟨ refl ⟩ - True - ∎ +-- open ≡-Reasoning +-- test3 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 +-- $ λ t → putTree1 t 2 2 +-- $ λ t → putTree1 t 3 3 +-- $ λ t → putTree1 t 4 4 +-- $ λ t → getRedBlackTree t 1 +-- $ λ t x → check2 {m} x 1 ≡ true +-- test3 {m} = begin +-- check2 {m} (just (record {key = 1 ; value = 1 ; color = Black ; left = nothing ; right = just (leafNode 2 2)})) 1 +-- ≡⟨ refl ⟩ +-- true +-- ∎ -test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 - $ λ t → putTree1 t 2 2 - $ λ t → putTree1 t 3 3 - $ λ t → putTree1 t 4 4 - $ λ t → getRedBlackTree t 4 - $ λ t x → x +-- test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 +-- $ λ t → putTree1 t 2 2 +-- $ λ t → putTree1 t 3 3 +-- $ λ t → putTree1 t 4 4 +-- $ λ t → getRedBlackTree t 4 +-- $ λ t x → x --- test5 : Maybe (Node ℕ ℕ) -test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 - $ λ t → putTree1 t 6 6 - $ λ t0 → clearSingleLinkedStack (nodeStack t0) - $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 ) - $ λ t1 s n1 → replaceNode t1 s n1 - $ λ t → getRedBlackTree t 3 - -- $ λ t x → SingleLinkedStack.top (stack s) - -- $ λ t x → n1 - $ λ t x → root t - where - findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t - findNode1 t s n1 Nothing next = next t s n1 - findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next +-- -- test5 : Maybe (Node ℕ ℕ) +-- test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 +-- $ λ t → putTree1 t 6 6 +-- $ λ t0 → clearSingleLinkedStack (nodeStack t0) +-- $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 ) +-- $ λ t1 s n1 → replaceNode t1 s n1 +-- $ λ t → getRedBlackTree t 3 +-- -- $ λ t x → SingleLinkedStack.top (stack s) +-- -- $ λ t x → n1 +-- $ λ t x → root t +-- where +-- findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t +-- findNode1 t s n1 nothing next = next t s n1 +-- findNode1 t s n1 ( just n2 ) next = findNode t s n1 n2 next --- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t → --- putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) --- test51 = refl +-- -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t → +-- -- putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ just (record { key = 1; value = 1; left = just (record { key = 2 ; value = 2 } ); right = nothing} ) +-- -- test51 = refl -test6 : Maybe (Node ℕ ℕ) -test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) +-- test6 : Maybe (Node ℕ ℕ) +-- test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) -test7 : Maybe (Node ℕ ℕ) -test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t)) - where - tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} - k1 = 1 - n2 = leafNode 0 0 - value1 = 1 +-- test7 : Maybe (Node ℕ ℕ) +-- test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t)) +-- where +-- tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} +-- k1 = 1 +-- n2 = leafNode 0 0 +-- value1 = 1 -test8 : Maybe (Node ℕ ℕ) -test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 - $ λ t → putTree1 t 2 2 (λ t → root t) +-- test8 : Maybe (Node ℕ ℕ) +-- test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 +-- $ λ t → putTree1 t 2 2 (λ t → root t) -test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True )) -test9 = refl - -test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( - λ t → putRedBlackTree t 2 2 ( - λ t → getRedBlackTree t 1 ( - λ t x → check2 x 1 ≡ True ))) -test10 = refl +-- test9 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true )) +-- test9 = refl -test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 - $ λ t → putRedBlackTree t 2 2 - $ λ t → putRedBlackTree t 3 3 - $ λ t → getRedBlackTree t 2 - $ λ t x → root t +-- test10 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( +-- λ t → putRedBlackTree t 2 2 ( +-- λ t → getRedBlackTree t 1 ( +-- λ t x → check2 {m} x 1 ≡ true ))) +-- test10 = refl - -redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ -redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT } +-- test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 +-- $ λ t → putRedBlackTree t 2 2 +-- $ λ t → putRedBlackTree t 3 3 +-- $ λ t → getRedBlackTree t 2 +-- $ λ t x → root t compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y ) -compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) +compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder) where open import Relation.Binary -checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} -checkT Nothing _ = False -checkT (Just n) x with compTri (value n) x -... | tri≈ _ _ _ = True -... | _ = False +checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool +checkT nothing _ = false +checkT (just n) x with compTri (value n) x +... | tri≈ _ _ _ = true +... | _ = false -checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (Just n) x ≡ True +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) -checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq -checkEQ' x y refl with x ≟ y -... | yes refl = refl -... | no neq = ⊥-elim ( neq refl ) +-- checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq +-- checkEQ' x y refl with x ≟ y +-- ... | yes refl = refl +-- ... | no neq = ⊥-elim ( neq refl ) --- search -> checkEQ --- findNode -> search +redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} {A B C : Set Level.zero } → RedBlackTree {Level.zero} {m} {t} {A} {B} {C} a ℕ +redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; nodeComp = λ x x₁ → {!!} } -- record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compTri } + + open stack.SingleLinkedStack open stack.Element {-# TERMINATING #-} -inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool {l} -inStack n s with ( top s ) -... | Nothing = True -... | Just n1 with compTri (key n) (key (datum n1)) -... | tri> _ neq _ = inStack n ( record { top = next n1 } ) -... | tri< _ neq _ = inStack n ( record { top = next n1 } ) -... | tri≈ _ refl _ = False +inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool +inStack {l} n s with ( top s ) +... | nothing = true +... | just n1 with compTri (key n) (key (datum n1)) +... | tri> _ neq _ = inStack {l} n ( record { top = next n1 } ) +... | tri< _ neq _ = inStack {l} n ( record { top = next n1 } ) +... | tri≈ _ refl _ = false record StackTreeInvariant ( n : Node ℕ ℕ ) - ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where + ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where field - sti : replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT x1 (value n) ≡ True) - notInStack : inStack n s ≡ True → ⊥ + sti : {m : Level} → replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT {m} x1 (value n) ≡ true) + notInStack : {m : Level} → inStack {m} n s ≡ true → ⊥ open StackTreeInvariant -putTest1 : (n : Maybe (Node ℕ ℕ)) - → (k : ℕ) (x : ℕ) - → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)) -putTest1 n k x with n -... | Just n1 = lemma0 - where - upelem : (eleN : Element (Node ℕ ℕ)) -> (Node ℕ ℕ) - upelem eleN = n1 - tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ - tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT } - lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s) - → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))) - lemma2 s STI with compTri k (key n1) - ... | tri≈ le refl gt = lemma5 s ( tree0 s ) n1 - where - lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → ( t : RedBlackTree ℕ ℕ ) → ( n : Node ℕ ℕ ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) } ) - ( \ s1 _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → - GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) ) - lemma5 s t n with (top s) - ... | Just n2 with compTri k k - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) - ... | tri≈ _ refl _ = ⊥-elim (notInStack STI ({!!})) - lemma5 s t n | Nothing with compTri k k - ... | tri≈ _ refl _ = checkEQ x _ refl - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) - ... | tri> le eq gt = sti ( record { sti = {!!} ; notInStack = {!!} } ) - ... | tri< le eq gt = {!!} - lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))) - lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!} ; notInStack = {!!} } ) -... | Nothing = lemma1 - where - lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { - key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k - ( λ t x1 → checkT x1 x ≡ True) - lemma1 with compTri k k - ... | tri≈ _ refl _ = checkEQ x _ refl - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) + +-- testn : {!!} +-- testn = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 +-- $ λ t → putTree1 t 1 1 +-- $ λ t → putTree1 t 3 3 (λ ta → record {root = root ta ; nodeStack = nodeStack ta }) + + +-- List と Node で書こうとしたがなんだかんだListに直したほうが楽そうだった + +nullNode = (record {key = 0 ; value = 0 ; right = nothing ; left = nothing ; color = Red}) + +-- treeTotal : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → (List ℕ → t) → t +-- treeTotal {m} {t} s tr next with (left tr) | (right tr) +-- treeTotal {m} {t} s tr next | nothing | nothing = next ((key tr) ∷ []) +-- treeTotal {m} {t} s tr next | nothing | just x = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li)) +-- treeTotal {m} {t} s tr next | just x | nothing = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li)) +-- treeTotal {m} {t} s tr next | just x | just x₁ = treeTotal {m} {t} s x (λ li1 → treeTotal {m} {t} s x₁ (λ li2 → next (s ++ li1 ++ li2))) +treeTotal : { n m : Level } {a : Set n} {t : Set m} → ( s : List a ) → ( tr : (Node a a) ) → List a +treeTotal {n} {m} {a} {t} s tr with (left tr) | (right tr) +treeTotal {n} {m} {a} {t} s tr | nothing | nothing = (key tr) ∷ [] +treeTotal {n} {m} {a} {t} s tr | nothing | just x = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x) +treeTotal {n} {m} {a} {t} s tr | just x | nothing = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x) +treeTotal {n} {m} {a} {t} s tr | just x | just x₁ = s ++ ((key tr) ∷ (treeTotal {n} {m} {a} {t} s x) ++ (treeTotal {n} {m} {a} {t} s x₁)) + + +-- treeTotalA : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → List ℕ + +-- (treeTotal {_} {ℕ} ([]) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} testn 5 5 {!!})))) + +-- exput : (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ ℕ))) (λ total → {!!})) ≡ {!!} +-- exput = {!!} + + +-- aaa = (treeTotal {_} {_} {ℕ} {_} (5 ∷ []) ((record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }))) + + +-- fuga = putTree1 {_} {_} {ℕ} {ℕ} (record {root = just (record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }) ; nodeStack = ( record {top = nothing}) ; compare = (λ x x₁ → EQ) }) 5 5 (λ aaa → aaa ) + +-- nontree ++ 2 :: [] + +-- piyo = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 ( λ t1 → findNode t1 (record {top = nothing}) (leafNode 2 2) (Data.Maybe.fromMaybe nullNode (root t1)) (λ tree stack node → {!!})) + + +-- exn2l : {!!} ≡ (treeTotal {_} {ℕ} ([]) (putTree1 {_} {_} {ℕ} {ℕ} {!!} 5 5 (λ t → {!!}))) -- (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root testn))) +-- exn2l = refl + + + + + +-- record FS {n m : Level } {a : Set n} {t : Set m} (oldTotal : List a) ( s : List a ) ( tr : (Node a a) ) : Set where +-- field +-- total : treeTotal {n} {m} {a} {t} s tr ≡ oldTotal +-- -- usage = FS.total -- relation + +-- data P { n m : Level } { t : Set m } : Set where +-- P₀ : (old : List ℕ) ( s : List ℕ ) → (tr : (Node ℕ ℕ) ) → FS {m} {t} old s tr → P + + + +-- ttt = putTree1 {_} {_} {ℕ} {ℕ} + +-- record TreeInterface {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set n where +-- field +-- tree : treeImpl +-- list : List ℕ +-- node : Node ℕ ℕ +-- putTreeHoare : (FS {_} {ℕ} list list node) → putTree1 {!!} {!!} {!!} {!!} + +stack2list : {n m : Level} {t : Set m} {a : Set n} → (s : SingleLinkedStack a) → List a +stack2list stack with top stack +stack2list stack | just x = (datum x) ∷ (elm2list {_} {_} {ℕ} x) + where + elm2list : {n m : Level} {t : Set m} {a : Set n} → (elm : (Element a)) → List a + elm2list el with next el + elm2list el | just x = (datum el) ∷ (elm2list {_} {_} {ℕ} x) + elm2list el | nothing = (datum el) ∷ [] +stack2list stack | nothing = [] + + +-- list2element : {n m : Level} {t : Set m} {a : Set n} → (l : List a) → Maybe (Element a) +-- list2element [] = nothing +-- list2element (x ∷ l) = just (cons x (list2element {_} {_} {ℕ} l)) + +-- ltest = list2element (1 ∷ 2 ∷ 3 ∷ []) + +list2stack : {n m : Level} {t : Set m} {a : Set n} {st : SingleLinkedStack a} → (l : List a) → SingleLinkedStack a +list2stack {n} {m} {t} {a} {s} (x ∷ l) = pushSingleLinkedStack s x (λ s1 → list2stack {n} {m} {t} {a} {s1} l ) +list2stack {n} {m} {t} {a} {s} [] = s + + + +-- stest = list2stack (1 ∷ 2 ∷ 3 ∷ []) + +open Node + +exfind : { m : Level } { t : Set m} → (dt : ℕ) → (node : (Node ℕ ℕ)) → (st : List ℕ) → findNode {_} {_} {ℕ} {ℕ} (redBlackInSomeState ℕ (just node)) (emptySingleLinkedStack) (leafNode dt dt) (node) (λ t1 st1 n1 → (( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ≡ ( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) )) +exfind dt node st with left node | right node +exfind dt node st | just x | just x₁ = {!!} +exfind dt node st | just x | nothing = {!!} +exfind dt node st | nothing | just x = {!!} +exfind dt node st | nothing | nothing with (compTri dt (key node)) +exfind dt node st | nothing | nothing | tri< a ¬b ¬c = {!!} +exfind dt node st | nothing | nothing | tri≈ ¬a b ¬c = {!!} +exfind dt node st | nothing | nothing | tri> ¬a ¬b c = {!!} + +-- exput : (ni : ℕ) → (tn : Node ℕ ℕ) → (ts : List ℕ) → (treeTotal {_} {ℕ} (ni ∷ ts) tn) +-- ≡ (treeTotal {_} {ℕ} (ts) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} (record { root = just tn } ) ni ni (λ tt → tt))))) +-- exput datum node [] with (right node) | (left node) +-- exput datum node [] | nothing | nothing = {!!} +-- exput datum node [] | just x | just x₁ = {!!} +-- exput datum node [] | just x | nothing = {!!} +-- exput datum node [] | nothing | just x = {!!} +-- exput datum node (x ∷ stack₁) = {!!} + + +-- proofTree : {n m : Level} {t : Set m} {a : Set n} (old stackl : List ℕ) → (node : Node ℕ ℕ) → (FS {_} {ℕ} old stackl node) → (tree : RedBlackTree ℕ ℕ) → (key : ℕ) → findNode {{!!}} {{!!}} {{!!}} {{!!}} tree (list2stack {!!} (record {top = nothing})) (leafNode key key) node (λ tree1 stack1 datum → {!!}) +-- -- -- -- putTree1 tree key key (λ t → (FS {_} {ℕ} old stackl (Data.Maybe.fromMaybe nullNode (root tree))) ) +-- proofTree old stack node fs t k = {!!} + +-- FS は 証明そのものになると思ってたけど実は違いそう +-- oldTotal と 現在の node, stack の組み合わせを比較する +-- oldTotal はどうやって作る? >< +-- treeTotal は list と node を受け取って それの total を出すのでそれで作る(list に put するデータなどを入れることで適当に作れる) + +-- p : {n m : Level} {t : Set m} {a : Set n} → ( s : SingleLinkedStack ℕ ) ( tr : (Node ℕ ℕ) ) ( tree : RedBlackTree ℕ ℕ ) (k : ℕ) → (FS (treeTotal (k ∷ (stack2list s)) tr) (stack2list s) tr) → putTree1 tree k k (λ atree → FS (treeTotal (stack2list s) (Data.Maybe.fromMaybe (tr) (root atree))) {!!} {!!}) +-- p stack node tree key = {!!} + +-- tt = (FS {_} {ℕ} [] [] (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ {_} ℕ {ℕ})))) + +-- ttt : (a : P) → P +-- ttt a = P₀ {!!} {!!} (record { key = {!!} ; value = {!!} ; right = {!!} ; left = {!!} ; color = {!!} }) (record { total = {!!} }) + + +-- FS では stack tree をあわせた整合性を示したい +-- そのためには...? +-- stack は前の node (というか一段上)が入ってる +-- tree は現在の node がある + + + -- tr(Node ℕ ℕ) s (List (Node)) + -- 3 [] + -- / \ + -- 2 5 + -- / / \ + -- 1 4 6 + + -- search 6 (6 > 3) + -- tr(Node ℕ ℕ) s (List (Node)) + -- 5 just (node (1 2 nothing) 3 (4 5 6) + -- / \ [] + -- 4 6 + +-- search 6 (6 > 5) +-- tr(Node ℕ ℕ) s (List (Node)) +-- 6 just (node (4 5 6)) +-- just (node (1 2 nothing) 3 (4 5 6) +-- [] + +-- just 6 → true みたいな感じ + +-- stack に node ごと入れるのは間違い…？ +-- 一応非破壊な感じがする(新しく作り直してる) +-- どう釣り合いをとるか + +-- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t +-- stack+tree {n} stack mid org = st stack mid org where +-- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ) +-- st [] _ _ = nothing +-- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org) +-- st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org +-- st (x ∷ []) n n1 | _ | _ = nothing +-- st (x ∷ a) n n1 with st a n n1 +-- st (x ∷ a) n n1 | just x₁ = {!!} +-- st (x ∷ a) n n1 | nothing = nothing + + +-- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t +-- stack+tree {n} stack mid org cg = st stack mid org +-- where +-- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ) +-- st [] _ _ = nothing +-- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org) +-- st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org +-- st (x ∷ []) n n1 | _ | _ = nothing +-- st (x ∷ a) n n1 with st a n n1 +-- st (x ∷ a) n n1 | just x₁ = {!!} +-- st (x ∷ a) n n1 | nothing = nothing + +-- findNodePush : {n : Level} → (stack : List (Node ℕ ℕ)) → (mid : Node ℕ ℕ) → (org : Node ℕ ℕ) → stack+tree stack mid org ≡ just ? +-- → ? {return (? ∷ stack),mid'} → stack+tree (? ∷ stack) (mid') org ≡ just ? +-- findNodePush + +-- stack+tree が just だって言えたらよい +-- {}2 は orig の どっちかのNode +
--- a/stack.agda Thu Aug 16 18:22:08 2018 +0900 +++ b/stack.agda Fri Nov 01 17:42:51 2019 +0900 @@ -3,27 +3,28 @@ open import Relation.Binary.PropositionalEquality open import Relation.Binary.Core -open import Data.Nat +open import Data.Nat hiding (compare) +open import Data.Maybe ex : 1 + 2 ≡ 3 ex = refl -data Bool {n : Level } : Set n where - True : Bool - False : Bool +-- data Bool {n : Level } : Set n where +-- True : Bool +-- False : Bool -record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where - field - pi1 : a - pi2 : b +-- record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where +-- field +-- pi1 : a +-- pi2 : b -data _∨_ {n : Level } (a : Set n) (b : Set n): Set n where - pi1 : a -> a ∨ b - pi2 : b -> a ∨ b +-- data _∨_ {n : Level } (a : Set n) (b : Set n): Set n where +-- pi1 : a -> a ∨ b +-- pi2 : b -> a ∨ b -data Maybe {n : Level } (a : Set n) : Set n where - Nothing : Maybe a - Just : a -> Maybe a +-- data Maybe {n : Level } (a : Set n) : Set n where +-- nothing : Maybe a +-- just : a -> Maybe a record StackMethods {n m : Level } (a : Set n ) {t : Set m } (stackImpl : Set n ) : Set (m Level.⊔ n) where field @@ -87,51 +88,51 @@ pushSingleLinkedStack stack datum next = next stack1 where element = cons datum (top stack) - stack1 = record {top = Just element} + stack1 = record {top = just element} popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t popSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack1 (Just data1) +... | nothing = cs stack nothing +... | just d = cs stack1 (just data1) where data1 = datum d stack1 = record { top = (next d) } pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) -... | Nothing = cs stack Nothing Nothing -... | Just d = pop2SingleLinkedStack' {n} {m} stack cs +... | nothing = cs stack nothing nothing +... | just d = pop2SingleLinkedStack' {n} {m} stack cs where pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t pop2SingleLinkedStack' stack cs with (next d) - ... | Nothing = cs stack Nothing Nothing - ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1)) + ... | nothing = cs stack nothing nothing + ... | just d1 = cs (record {top = (next d1)}) (just (datum d)) (just (datum d1)) getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t getSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack (Just data1) +... | nothing = cs stack nothing +... | just d = cs stack (just data1) where data1 = datum d get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) -... | Nothing = cs stack Nothing Nothing -... | Just d = get2SingleLinkedStack' {n} {m} stack cs +... | nothing = cs stack nothing nothing +... | just d = get2SingleLinkedStack' {n} {m} stack cs where get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t get2SingleLinkedStack' stack cs with (next d) - ... | Nothing = cs stack Nothing Nothing - ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1)) + ... | nothing = cs stack nothing nothing + ... | just d1 = cs stack (just (datum d)) (just (datum d1)) clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t -clearSingleLinkedStack stack next = next (record {top = Nothing}) +clearSingleLinkedStack stack next = next (record {top = nothing}) emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a -emptySingleLinkedStack = record {top = Nothing} +emptySingleLinkedStack = record {top = nothing} ----- -- Basic stack implementations are specifications of a Stack