Mercurial > hg > Members > Moririn

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
1 module hoareRedBlackTree where
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
2
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
3
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
4 open import Level hiding (zero)
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
5
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
6 open import Data.Nat hiding (compare)
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
7 open import Data.Nat.Properties as NatProp
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
8 open import Data.Maybe
581
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
9 -- open import Data.Bool
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
10 open import Data.Empty
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
11 open import Data.List
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
12
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
13 open import Relation.Binary
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
14 open import Relation.Binary.PropositionalEquality
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
15 open import logic
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
16
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
17
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
18 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
19 field
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
20 putImpl : treeImpl → a → (treeImpl → t) → t
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
21 getImpl : treeImpl → (treeImpl → Maybe a → t) → t
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
22 open TreeMethods
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
23
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
24 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
25 field
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
26 tree : treeImpl
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
27 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
28 putTree : a → (Tree treeImpl → t) → t
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
29 putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
30 getTree : (Tree treeImpl → Maybe a → t) → t
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
31 getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
32
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
33 open Tree
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
34
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
35 SingleLinkedStack = List
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
36
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
37 emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
38 emptySingleLinkedStack = []
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
39
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
40 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
41 pushSingleLinkedStack stack datum next = next ( datum ∷ stack )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
42
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
43 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
44 popSingleLinkedStack [] cs = cs [] nothing
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
45 popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1)
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
46
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
47 data Color {n : Level } : Set n where
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
48 Red : Color
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
49 Black : Color
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
50
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
51 record Node {n : Level } (a : Set n) : Set n where
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
52 inductive
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
53 field
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
54 key : ℕ
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
55 value : a
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
56 right : Maybe (Node a )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
57 left : Maybe (Node a )
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
58 color : Color {n}
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
59 open Node
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
60
580
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 579
diff changeset
61 record RedBlackTree {n : Level } (a : Set n) : Set n where
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
62 field
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
63 root : Maybe (Node a )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
64 nodeStack : SingleLinkedStack (Node a )
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
65 -- compare : k → k → Tri A B C
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
66 -- <-cmp
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
67
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
68 open RedBlackTree
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
69
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
70
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
71 ----
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
72 -- find node potition to insert or to delete, the path will be in the stack
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
73 --
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
74
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
75 {-# TERMINATING #-}
580
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 579
diff changeset
76 findNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
77 findNode {n} {m} {a} {t} tree n0 next with root tree
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
78 findNode {n} {m} {a} {t} tree n0 next | nothing = next tree
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
79 findNode {n} {m} {a} {t} tree n0 next | just x with <-cmp (key x) (key n0)
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
80 findNode {n} {m} {a} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
81 findNode {n} {m} {a} {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
82 findNode {n} {m} {a} {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
83
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
84
580
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 579
diff changeset
85 findNode1 : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
86 findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
577
ac2293378d7a modify findNode1
ryokka
parents: 576
diff changeset
87 module FindNode where
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
88 findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
89 findNode2 nothing st = next record { root = nothing ; nodeStack = st }
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
90 findNode2 (just x) st with <-cmp (key n0) (key x)
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
91 ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st })
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
92 ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1)
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
93 ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1)
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
94
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
95 node001 : Node ℕ
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
96 node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black }
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
97 node002 : Node ℕ
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
98 node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black }
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
99 node003 : Node ℕ
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
100 node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black }
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
101
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
102 test001 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
103 node001 ( λ tree → tree )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
104 test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
105 node001 ( λ tree → tree )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
106 test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
107 node001 ( λ tree → tree )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
108 test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
109 node001 ( λ tree → tree )
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
110
583
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
111 replaceNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
112 replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } )
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
113 module FindNodeR where
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
114 replaceNode1 : (Maybe (Node a )) → Node a
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
115 replaceNode1 nothing = record n0 { left = nothing ; right = nothing }
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
116 replaceNode1 (just x) = record n0 { left = left x ; right = right x }
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
117 replaceNode2 : SingleLinkedStack (Node a ) → (Node a → t) → t
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
118 replaceNode2 [] next = next ( replaceNode1 (root tree) )
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
119 replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0)
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
120 replaceNode2 (x ∷ st) next | tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) )
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
121 replaceNode2 (x ∷ st) next | tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) )
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
122 replaceNode2 (x ∷ st) next | tri> ¬a ¬b c = replaceNode2 st ( λ new → next ( record x { right = right new } ) )
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
123
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
124 insertNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
125 insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next )
d18df2e6135d add replaceNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 582
diff changeset
126
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
127 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
580
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 579
diff changeset
128 → RedBlackTree {n} a
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
129 createEmptyRedBlackTreeℕ a b = record {
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
130 root = nothing
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
131 ; nodeStack = emptySingleLinkedStack
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
132 }
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
133
581
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
134 findNodeLeft : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
135 findNodeLeft x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
136 findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
137 findNodeRight : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
138 findNodeRight x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
139 findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
140
581
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
141 data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → Set n where
584
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
142 fni-stackEmpty : (now : RedBlackTree {n} a ) → FindNodeInvariant [] now
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
143 fni-treeEmpty : (st : SingleLinkedStack (Node a)) → FindNodeInvariant st record { root = nothing ; nodeStack = st }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
144 fni-Left : (x : Node a) (st : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
145 → FindNodeInvariant ( x ∷ st ) original → findNodeLeft x st → FindNodeInvariant st original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
146 fni-Right : (x : Node a) (st : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
147 → FindNodeInvariant ( x ∷ st ) original → findNodeRight x st → FindNodeInvariant st original
581
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
148
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
149
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
150 findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a )
582
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 581
diff changeset
151 → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) tree → t )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 581
diff changeset
152 → ( FindNodeInvariant (nodeStack tree) tree) → t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 581
diff changeset
153 findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
581
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
154 module FindNodeH where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
155 findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree → t
584
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
156 findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!}
581
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
157 findNode2h (just x) st prev with <-cmp (key n0) (key x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
158 ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
159 ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 580
diff changeset
160 ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
161
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
162
584
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
163 -- replaceNodeH : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → {!!} → t) → {!!} → t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 583
diff changeset
164 -- replaceNodeH = {!!}
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
165