Mercurial > hg > Gears > GearsAgda

comparison hoareRedBlackTree.agda @ 583:d18df2e6135d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add replaceNode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 03 Nov 2019 08:53:00 +0900
parents 1a5dd71199f1
children 7e551cef35d7
comparison
equal deleted inserted replaced
582:1a5dd71199f1 583:d18df2e6135d
106 test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } ) 106 test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
107 node001 ( λ tree → tree ) 107 node001 ( λ tree → tree )
108 test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } ) 108 test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
109 node001 ( λ tree → tree ) 109 node001 ( λ tree → tree )
110 110
111 replaceNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
112 replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } )
113 module FindNodeR where
114 replaceNode1 : (Maybe (Node a )) → Node a
115 replaceNode1 nothing = record n0 { left = nothing ; right = nothing }
116 replaceNode1 (just x) = record n0 { left = left x ; right = right x }
117 replaceNode2 : SingleLinkedStack (Node a ) → (Node a → t) → t
118 replaceNode2 [] next = next ( replaceNode1 (root tree) )
119 replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0)
120 replaceNode2 (x ∷ st) next | tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) )
121 replaceNode2 (x ∷ st) next | tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) )
122 replaceNode2 (x ∷ st) next | tri> ¬a ¬b c = replaceNode2 st ( λ new → next ( record x { right = right new } ) )
123
124 insertNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
125 insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next )
126
111 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ) 127 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
112 → RedBlackTree {n} a 128 → RedBlackTree {n} a
113 createEmptyRedBlackTreeℕ a b = record { 129 createEmptyRedBlackTreeℕ a b = record {
114 root = nothing 130 root = nothing
115 ; nodeStack = emptySingleLinkedStack 131 ; nodeStack = emptySingleLinkedStack
141 ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? ) 157 ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
142 ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) ) 158 ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )
143 ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) ) 159 ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )
144 160
145 161
162 replaceNodeH : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → {!!} → t) → {!!} → t
163 replaceNodeH = {!!}
146 164