Mercurial > hg > Gears > GearsAgda

changeset 589:37f5826ca7d2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minor fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 06 Dec 2019 13:01:53 +0900
parents 8627d35d4bff
children 7c424dd0945d
files hoareBinaryTree.agda hoareRedBlackTree.agda
diffstat 2 files changed, 26 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Thu Dec 05 20:38:54 2019 +0900
+++ b/hoareBinaryTree.agda	Fri Dec 06 13:01:53 2019 +0900
@@ -75,13 +75,15 @@
 
 test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s (s≤s z≤n))))
 
-bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' ℕ tn ) → List (bt'-path A ) → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
-bt-find' key (bt'-leaf key₁) stack next = {!!}
+bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A )
+    → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
+bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack  -- no key found
 bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁
-bt-find' {n} {m} {A} {t} key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c =
-         bt-find' {n} {m} {A} {t} key tree ( (bt'-left {n} {A} key {key₁} {!!} {!!}  )  ∷ stack)  next
-bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next {!!} stack
-bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = {!!}
+bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c =
+         bt-find' key tree ( (bt'-left key {key₁} tr a )  ∷ stack)  next
+bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack
+bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = 
+         bt-find' key tree ( (bt'-right key {key₁} tr c )  ∷ stack)  next
 
 
 bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' ℕ tn ) → List (bt'-path A ) → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
--- a/hoareRedBlackTree.agda	Thu Dec 05 20:38:54 2019 +0900
+++ b/hoareRedBlackTree.agda	Fri Dec 06 13:01:53 2019 +0900
@@ -617,43 +617,27 @@
 findNodeRight x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
 findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))
 
+data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (node :  Maybe (Node a) ) → Set n where
+   fni-stackEmpty  : (now :  Maybe (Node a) ) → FindNodeInvariant [] now 
+   fni-treeEmpty  : (st : SingleLinkedStack (Node a))  → FindNodeInvariant st nothing
+   fni-Left  : (x : Node a) (st : SingleLinkedStack (Node a)) (node :  Maybe (Node a ))
+      →  FindNodeInvariant ( x ∷ st ) node → findNodeLeft x st →  FindNodeInvariant st node
+   fni-Right  : (x : Node a) (st : SingleLinkedStack (Node a)) (node :  Maybe (Node a ))
+      →  FindNodeInvariant ( x ∷ st ) node → findNodeRight x st →  FindNodeInvariant st node 
 findNodeLoop : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
 findNodeLoop x st = ((findNodeRight x st) ∨ (findNodeLeft x st))
 
-
-
-data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set n where
-   fni-stackEmpty  : (now :  RedBlackTree {n}  a ) → FindNodeInvariant [] now
-   fni-treeEmpty  : (st : SingleLinkedStack (Node a))  → FindNodeInvariant st record { root = nothing ; nodeStack = st }
-   fni-Left  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
-      →  FindNodeInvariant ( x ∷ st ) original → findNodeLeft x st →  FindNodeInvariant st original
-   fni-Right  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
-      →  FindNodeInvariant ( x ∷ st ) original → findNodeRight x st →  FindNodeInvariant st original
-   -- fni-loop  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → FindNodeInvariant st original
-
-
--- findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
---      → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t )
---      → ( FindNodeInvariant (nodeStack tree)  tree) → t
--- findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) n0 prev
---   module FindNodeH where
---     findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → Node a → FindNodeInvariant s tree  → t
---     findNode2h nothing st n0 prev = next record { root = nothing ; nodeStack = st } prev
---     findNode2h (just x) st n0 prev with <-cmp (key n0) (key x)
---     ... | tri≈ ¬lt eq ¬gt = next (record {root = just x ; nodeStack = st }) prev -- ( fni-Last ? )
---     ... | tri< lt ¬eq ¬gt = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 n0 (fni-Left x s1 tree ({!!}) (lproof x s1 )) )
--- b        where
---           nextInvaliant : (t)
---           nextInvaliant = next tree {!!}
---           lproof : (x : Node a) → (s1 : SingleLinkedStack (Node a)) → findNodeLeft x s1 --→ (n0 : Node a)
---           lproof ns [] with left ns | right ns
---           lproof ns [] | just x | just x₁ = {!!}
---           lproof ns [] | just x | nothing =  {!!}
---           lproof ns [] | nothing | just x = {!!}
---           lproof ns [] | nothing | nothing = record { proj1 = refl ; proj2 = refl }
---           lproof ns (x ∷ ss) = {!!}
-
---     ... | tri> ¬lt ¬eq gt = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 n0 (fni-Right x s1 tree ({!!}) {!!}) )
+findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
+     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) (root new ) → t ) 
+     → ( FindNodeInvariant (nodeStack tree)  (root tree) ) → t
+findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
+  module FindNodeH where
+    findNode2h : (new : Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s new → t
+    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } prev
+    findNode2h (just x) st prev with <-cmp (key n0) (key x)
+    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) prev
+    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 {!!} {!!} {!!}) )
+    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 {!!} {!!} {!!}) )
 
 
 -- replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t