Mercurial > hg > Gears > GearsAgda

comparison hoareRedBlackTree.agda @ 576:40d01b368e34

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Temporary Push
author ryokka
date Fri, 01 Nov 2019 19:12:52 +0900
parents
children ac2293378d7a
comparison
equal deleted inserted replaced
575:73fc32092b64 576:40d01b368e34
1 module hoareRedBlackTree where
2
3
4 open import Level hiding (zero)
5
6 open import Data.Nat hiding (compare)
7 open import Data.Nat.Properties as NatProp
8 open import Data.Maybe
9 open import Data.Bool
10 open import Data.Empty
11
12 open import Relation.Binary
13 open import Relation.Binary.PropositionalEquality
14
15 open import stack
16
17
18
19 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
20 field
21 putImpl : treeImpl → a → (treeImpl → t) → t
22 getImpl : treeImpl → (treeImpl → Maybe a → t) → t
23 open TreeMethods
24
25 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
26 field
27 tree : treeImpl
28 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
29 putTree : a → (Tree treeImpl → t) → t
30 putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
31 getTree : (Tree treeImpl → Maybe a → t) → t
32 getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )
33
34 open Tree
35
36 data Color {n : Level } : Set n where
37 Red : Color
38 Black : Color
39
40
41 record Node {n : Level } (a : Set n) (k : ℕ) : Set n where
42 inductive
43 field
44 key : ℕ
45 value : a
46 right : Maybe (Node a k)
47 left : Maybe (Node a k)
48 color : Color {n}
49 open Node
50
51 record RedBlackTree {n m : Level } {t : Set m} (a : Set n) (k : ℕ) : Set (m Level.⊔ n) where
52 field
53 root : Maybe (Node a k)
54 nodeStack : SingleLinkedStack (Node a k)
55 -- compare : k → k → Tri A B C
56 -- <-cmp
57
58 open RedBlackTree
59
60 open SingleLinkedStack
61
62
63
64 ----
65 -- find node potition to insert or to delete, the path will be in the stack
66 --
67
68 {-# TERMINATING #-}
69 findNode : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
70 findNode {n} {m} {a} {k} {t} tree n0 next with root tree
71 findNode {n} {m} {a} {k} {t} tree n0 next | nothing = next tree
72 findNode {n} {m} {a} {k} {t} tree n0 next | just x with <-cmp (key x) (key n0)
73 findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
74 findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
75 findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
76
77
78 findNode1 : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
79 findNode1 {n} {m} {a} {k} {t} tree n0 next = findNode2 (root tree) (nodeStack tree) n0 {!!}
80 where
81 findNode2 : (Maybe (Node a k)) → SingleLinkedStack (Node a k) → Node a k → (Maybe (Node a k) → SingleLinkedStack (Node a k) → t) → t
82 findNode2 nothing st n0 next = next nothing st
83 findNode2 (just x) st n0 next with (<-cmp (key n0) (key x))
84 findNode2 (just x) st n0 next | tri≈ ¬a b ¬c = {!!}
85 findNode2 (just x) st n0 next | tri< a ¬b ¬c = {!!}
86 findNode2 (just x) st n0 next | tri> ¬a ¬b c = {!!}
87
88 findNode3 : SingleLinkedStack (Node a k) → Node a k → t
89 findNode3 s1 n1 with (<-cmp (key n0) (key n1))
90 findNode3 s1 n1 | tri≈ ¬a b ¬c = next (record {root = root tree ; nodeStack = s1})
91 findNode3 s1 n1 | tri< a ¬b ¬c = pushSingleLinkedStack (nodeStack tree) n1 (λ s → findNode2 (left n1) s n0 {!!})
92 findNode3 s1 n1 | tri> ¬a ¬b c = {!!}
93
94 -- pushSingleLinkedStack s n1 (\ s → findNode1 s n1)
95 -- module FindNode where
96 -- findNode2 : SingleLinkedStack (Node a k) → (Maybe (Node a k)) → t
97 -- findNode2 s nothing = next tree
98 -- findNode2 s (just n) = findNode tree s n0 n next
99 -- findNode1 : SingleLinkedStack (Node a k) → (Node a k) → t
100 -- findNode1 s n1 with (<-cmp (key n0) (key n1))
101 -- findNode1 s n1 | tri< a ¬b ¬c = findNode2 s (right n1)
102 -- findNode1 s n1 | tri≈ ¬a b ¬c = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
103 -- findNode1 s n1 | tri> ¬a ¬b c = findNode2 s (left n1)
104 -- ... | EQ = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
105 -- ... | GT = findNode2 s (right n1)
106 -- ... | LT = findNode2 s (left n1)
107
108
109 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
110 → RedBlackTree {n} {m} {t} a b
111 createEmptyRedBlackTreeℕ a b = record {
112 root = nothing
113 ; nodeStack = emptySingleLinkedStack
114 -- ; nodeComp = λ x x₁ → {!!}
115 }
116
117
118 test = findNode (createEmptyRedBlackTreeℕ {!!} 1)