Mercurial > hg > Gears > GearsAgda

changeset 581:09e9e8fd7568

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 Nov 2019 19:23:10 +0900
parents 99429fdb3b8b
children 1a5dd71199f1
files hoareRedBlackTree.agda
diffstat 1 files changed, 25 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/hoareRedBlackTree.agda	Sat Nov 02 18:08:26 2019 +0900
+++ b/hoareRedBlackTree.agda	Sat Nov 02 19:23:10 2019 +0900
@@ -6,7 +6,7 @@
 open import Data.Nat hiding (compare)
 open import Data.Nat.Properties as NatProp
 open import Data.Maybe
-open import Data.Bool
+-- open import Data.Bool
 open import Data.Empty
 open import Data.List
 
@@ -115,18 +115,31 @@
      ;  nodeStack = emptySingleLinkedStack
    }
 
-findNodeLeft : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}   a ) → Set
-findNodeLeft x t original = {!!}
-findNodeRight : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set
-findNodeRight x t original = {!!}
+findNodeLeft : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
+findNodeLeft x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
+findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h))
+findNodeRight : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
+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)) (original :  RedBlackTree {n}  a ) → Set n where
-   FNI-Last  : (now :  RedBlackTree {n}  a ) → findNodeInvariant [] now 
-   FNI-Left  : (x : Node a) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
-      →  findNodeInvariant ( x ∷ t ) original → findNodeLeft x t original  →  findNodeInvariant t original
-   FNI-Right  : (x : Node a) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
-      →  findNodeInvariant ( x ∷ t ) original → findNodeRight x t original  →  findNodeInvariant t original
+data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set n where
+   fni-Top  : (now :  RedBlackTree {n}  a ) → FindNodeInvariant [] now 
+   fni-Left  : (x : Node a) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
+      →  FindNodeInvariant ( x ∷ t ) original → findNodeLeft x t →  FindNodeInvariant t original
+   fni-Right  : (x : Node a) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
+      →  FindNodeInvariant ( x ∷ t ) original → findNodeRight x t →  FindNodeInvariant t original
+
+
+findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
+     → ( FindNodeInvariant (nodeStack tree)  tree)  → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t ) → t
+findNode1h {n} {m} {a} {t} tree n0 prev next = findNode2h (root tree) (nodeStack tree) prev
+  module FindNodeH where
+    findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree  → t
+    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!} -- ( fni-Last ? )
+    findNode2h (just x) st prev with <-cmp (key n0) (key x)
+    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
+    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )
+    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )
 
 
 
-