Mercurial > hg > Gears > GearsAgda

changeset 577:ac2293378d7a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
modify findNode1
author ryokka
date Fri, 01 Nov 2019 20:02:55 +0900
parents 40d01b368e34
children 7bacba816277
files hoareRedBlackTree.agda
diffstat 1 files changed, 7 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/hoareRedBlackTree.agda	Fri Nov 01 19:12:52 2019 +0900
+++ b/hoareRedBlackTree.agda	Fri Nov 01 20:02:55 2019 +0900
@@ -76,34 +76,17 @@
 
 
 findNode1 : {n m  : Level } {a : Set n} {k : ℕ} {t : Set m}  → RedBlackTree {n} {m} {t}   a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
-findNode1 {n} {m} {a} {k} {t} tree n0 next = findNode2 (root tree) (nodeStack tree) n0 {!!}
-  where
-    findNode2 : (Maybe (Node a k)) → SingleLinkedStack (Node a k) → Node a k → (Maybe (Node a k) → SingleLinkedStack (Node a k) → t) → t
-    findNode2 nothing st n0 next = next nothing st
-    findNode2 (just x) st n0 next with (<-cmp (key n0) (key x))
-    findNode2 (just x) st n0 next | tri≈ ¬a b ¬c = {!!}
-    findNode2 (just x) st n0 next | tri< a ¬b ¬c = {!!}
-    findNode2 (just x) st n0 next | tri> ¬a ¬b c = {!!}
+findNode1 {n} {m} {a} {k} {t} tree n0 next = pushSingleLinkedStack (nodeStack tree) n0 (λ st → findNode3 st n0)
+  module FindNode where
+    findNode2 : (Maybe (Node a k)) → SingleLinkedStack (Node a k) → t
+    findNode2 nothing st = next tree
+    findNode2 (just x) st = findNode1 (record {root = just x ; nodeStack = st}) x next
 
     findNode3 : SingleLinkedStack (Node a k) → Node a k → t
     findNode3 s1 n1 with (<-cmp (key n0) (key n1))
     findNode3 s1 n1 | tri≈ ¬a b ¬c = next (record {root = root tree ; nodeStack = s1})
-    findNode3 s1 n1 | tri< a ¬b ¬c = pushSingleLinkedStack (nodeStack tree) n1 (λ s → findNode2 (left n1) s n0 {!!})
-    findNode3 s1 n1 | tri> ¬a ¬b c = {!!}
-
--- 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
-  --   findNode2 s (just n) = findNode tree s n0 n next
-  --   findNode1 : SingleLinkedStack (Node a k) → (Node a k)  → t
-  --   findNode1 s n1 with (<-cmp (key n0) (key n1))
-  --   findNode1 s n1 | tri< a ¬b ¬c = findNode2 s (right 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 (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)
+    findNode3 s1 n1 | tri< a ¬b ¬c = findNode2 (right n1) s1
+    findNode3 s1 n1 | tri> ¬a ¬b c = findNode2 (left n1) s1
 
 
 createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
@@ -111,8 +94,5 @@
 createEmptyRedBlackTreeℕ a b = record {
         root = nothing
      ;  nodeStack = emptySingleLinkedStack
-     -- ;  nodeComp = λ x x₁ → {!!}
    }
 
-
-test = findNode (createEmptyRedBlackTreeℕ {!!} 1)