Mercurial > hg > Members > Moririn

comparison hoareRedBlackTree.agda @ 580:99429fdb3b8b

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 18:08:26 +0900
parents 821d04c0770b
children 09e9e8fd7568
comparison
equal deleted inserted replaced
579:821d04c0770b 580:99429fdb3b8b
56 right : Maybe (Node a ) 56 right : Maybe (Node a )
57 left : Maybe (Node a ) 57 left : Maybe (Node a )
58 color : Color {n} 58 color : Color {n}
59 open Node 59 open Node
60 60
61 record RedBlackTree {n m : Level } (a : Set n) : Set (m Level.⊔ n) where 61 record RedBlackTree {n : Level } (a : Set n) : Set n where
62 field 62 field
63 root : Maybe (Node a ) 63 root : Maybe (Node a )
64 nodeStack : SingleLinkedStack (Node a ) 64 nodeStack : SingleLinkedStack (Node a )
65 -- compare : k → k → Tri A B C 65 -- compare : k → k → Tri A B C
66 -- <-cmp 66 -- <-cmp
71 ---- 71 ----
72 -- find node potition to insert or to delete, the path will be in the stack 72 -- find node potition to insert or to delete, the path will be in the stack
73 -- 73 --
74 74
75 {-# TERMINATING #-} 75 {-# TERMINATING #-}
76 findNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} {m} a → (Node a ) → (RedBlackTree {n} {m} a → t) → t 76 findNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
77 findNode {n} {m} {a} {t} tree n0 next with root tree 77 findNode {n} {m} {a} {t} tree n0 next with root tree
78 findNode {n} {m} {a} {t} tree n0 next | nothing = next tree 78 findNode {n} {m} {a} {t} tree n0 next | nothing = next tree
79 findNode {n} {m} {a} {t} tree n0 next | just x with <-cmp (key x) (key n0) 79 findNode {n} {m} {a} {t} tree n0 next | just x with <-cmp (key x) (key n0)
80 findNode {n} {m} {a} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree 80 findNode {n} {m} {a} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
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) 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)
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) 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)
83 83
84 84
85 findNode1 : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} {m} a → (Node a ) → (RedBlackTree {n} {m} a → t) → t 85 findNode1 : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
86 findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree) 86 findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
87 module FindNode where 87 module FindNode where
88 findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t 88 findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t
89 findNode2 nothing st = next record { root = nothing ; nodeStack = st } 89 findNode2 nothing st = next record { root = nothing ; nodeStack = st }
90 findNode2 (just x) st with <-cmp (key n0) (key x) 90 findNode2 (just x) st with <-cmp (key n0) (key x)
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 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ) 111 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
112 → RedBlackTree {n} {m} a 112 → RedBlackTree {n} a
113 createEmptyRedBlackTreeℕ a b = record { 113 createEmptyRedBlackTreeℕ a b = record {
114 root = nothing 114 root = nothing
115 ; nodeStack = emptySingleLinkedStack 115 ; nodeStack = emptySingleLinkedStack
116 } 116 }
117 117
118 popAllNode1 : {n : Level } {a : Set n} → SingleLinkedStack (Node a ) → Node a → Maybe (Node a) 118 findNodeLeft : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → Set
119 popAllNode1 [] r = nothing 119 findNodeLeft x t original = {!!}
120 popAllNode1 (x ∷ t) r with popAllNode1 t r 120 findNodeRight : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → Set
121 ... | ttt = {!!} 121 findNodeRight x t original = {!!}
122 122
123 popAllnode : {n m : Level } {a : Set n} → RedBlackTree {n} {m} a → RedBlackTree {n} {m} a → Set 123 data findNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → Set n where
124 popAllnode {n} {m} {a} now original = {!!} 124 FNI-Last : (now : RedBlackTree {n} a ) → findNodeInvariant [] now
125 125 FNI-Left : (x : Node a) (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a )
126 record findNodeInvariant {n m : Level } {a : Set n} {t : Set m} (now original : RedBlackTree {n} {m} a ) : Set (m Level.⊔ n) where 126 → findNodeInvariant ( x ∷ t ) original → findNodeLeft x t original → findNodeInvariant t original
127 field 127 FNI-Right : (x : Node a) (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a )
128 tree+stack : popAllnode now original 128 → findNodeInvariant ( x ∷ t ) original → findNodeRight x t original → findNodeInvariant t original
129 129
130 130
131 131
132 132
133