Mercurial > hg > Gears > GearsAgda

comparison hoareRedBlackTree.agda @ 584:7e551cef35d7

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 Sun, 03 Nov 2019 09:27:51 +0900
parents d18df2e6135d
children 42e8cf963c5c
comparison
equal deleted inserted replaced
583:d18df2e6135d 584:7e551cef35d7
137 findNodeRight : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n 137 findNodeRight : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n
138 findNodeRight x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing ) 138 findNodeRight x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing )
139 findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h)) 139 findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))
140 140
141 data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → Set n where 141 data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → Set n where
142 fni-Top : (now : RedBlackTree {n} a ) → FindNodeInvariant [] now 142 fni-stackEmpty : (now : RedBlackTree {n} a ) → FindNodeInvariant [] now
143 fni-Left : (x : Node a) (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) 143 fni-treeEmpty : (st : SingleLinkedStack (Node a)) → FindNodeInvariant st record { root = nothing ; nodeStack = st }
144 → FindNodeInvariant ( x ∷ t ) original → findNodeLeft x t → FindNodeInvariant t original 144 fni-Left : (x : Node a) (st : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a )
145 fni-Right : (x : Node a) (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) 145 → FindNodeInvariant ( x ∷ st ) original → findNodeLeft x st → FindNodeInvariant st original
146 → FindNodeInvariant ( x ∷ t ) original → findNodeRight x t → FindNodeInvariant t original 146 fni-Right : (x : Node a) (st : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a )
147 → FindNodeInvariant ( x ∷ st ) original → findNodeRight x st → FindNodeInvariant st original
147 148
148 149
149 findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a ) 150 findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a )
150 → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) tree → t ) 151 → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) tree → t )
151 → ( FindNodeInvariant (nodeStack tree) tree) → t 152 → ( FindNodeInvariant (nodeStack tree) tree) → t
152 findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev 153 findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
153 module FindNodeH where 154 module FindNodeH where
154 findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree → t 155 findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree → t
155 findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!} 156 findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!}
156 findNode2h (just x) st prev with <-cmp (key n0) (key x) 157 findNode2h (just x) st prev with <-cmp (key n0) (key x)
157 ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? ) 158 ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
158 ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) ) 159 ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )
159 ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) ) 160 ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )
160 161
161 162
162 replaceNodeH : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → {!!} → t) → {!!} → t 163 -- replaceNodeH : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → {!!} → t) → {!!} → t
163 replaceNodeH = {!!} 164 -- replaceNodeH = {!!}
164 165