Mercurial > hg > Gears > GearsAgda

annotate hoareRedBlackTree.agda @ 579:821d04c0770b

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 17:34:46 +0900
parents 7bacba816277
children 99429fdb3b8b
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
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
9 open import Data.Bool
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
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
61 record RedBlackTree {n m : Level } (a : Set n) : Set (m Level.⊔ 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 #-}
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
76 findNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} {m} a → (Node a ) → (RedBlackTree {n} {m} a → t) → t
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
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
85 findNode1 : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} {m} a → (Node a ) → (RedBlackTree {n} {m} a → t) → t
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
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
111 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
112 → RedBlackTree {n} {m} a
576
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
113 createEmptyRedBlackTreeℕ a b = record {
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
114 root = nothing
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
115 ; nodeStack = emptySingleLinkedStack
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
116 }
40d01b368e34 Temporary Push
ryokka
parents:
diff changeset
117
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
118 popAllNode1 : {n : Level } {a : Set n} → SingleLinkedStack (Node a ) → Node a → Maybe (Node a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
119 popAllNode1 [] r = nothing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
120 popAllNode1 (x ∷ t) r with popAllNode1 t r
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
121 ... | ttt = {!!}
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
122
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
123 popAllnode : {n m : Level } {a : Set n} → RedBlackTree {n} {m} a → RedBlackTree {n} {m} a → Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
124 popAllnode {n} {m} {a} now original = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
125
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
126 record findNodeInvariant {n m : Level } {a : Set n} {t : Set m} (now original : RedBlackTree {n} {m} a ) : Set (m Level.⊔ n) where
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
127 field
579
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 578
diff changeset
128 tree+stack : popAllnode now original
578
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
129
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
130
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
131
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
132
7bacba816277 use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 577
diff changeset
133