Members/Moririn: RedBlackTree.agda annotate

annotate RedBlackTree.agda @ 589:37f5826ca7d2

minor fix

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 06 Dec 2019 13:01:53 +0900
parents	0ddfa505d612
children	8df36383ced0

rev	line source
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	1 module RedBlackTree where
24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	2
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	3
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	4 open import Level hiding (zero)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	5
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	6 open import Data.Nat hiding (compare)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	7 open import Data.Nat.Properties as NatProp
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	8 open import Data.Maybe
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	9 open import Data.Bool
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	10 open import Data.Empty
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	11
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	12 open import Relation.Binary
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	13 open import Relation.Binary.PropositionalEquality
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	14
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	15 open import stack
564 40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 551 diff changeset	16
511 044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	17 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	18 field
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	19 putImpl : treeImpl → a → (treeImpl → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	20 getImpl : treeImpl → (treeImpl → Maybe a → t) → t
511 044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	21 open TreeMethods
044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	22
044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	23 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	24 field
24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	25 tree : treeImpl
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	26 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	27 putTree : a → (Tree treeImpl → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	28 putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	29 getTree : (Tree treeImpl → Maybe a → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	30 getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )
427 07ccd411ad70 fix interface in agda ryokka parents: 425 diff changeset	31
478 0223c07c3946 fix stack.agda ryokka parents: 428 diff changeset	32 open Tree
0223c07c3946 fix stack.agda ryokka parents: 428 diff changeset	33
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	34 data Color {n : Level } : Set n where
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	35 Red : Color
ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	36 Black : Color
ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	37
512 95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	38
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	39 record Node {n : Level } (a : Set n) (k : ℕ) : Set n where
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	40 inductive
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	41 field
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	42 key : ℕ
512 95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	43 value : a
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	44 right : Maybe (Node a k)
f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	45 left : Maybe (Node a k)
514 f86da73d611e fix RedBlackTree.agda ryokka parents: 513 diff changeset	46 color : Color {n}
512 95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	47 open Node
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	48
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	49 record RedBlackTree {n m : Level } {t : Set m} (a : Set n) (k : ℕ) : Set (m Level.⊔ n) where
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	50 field
514 f86da73d611e fix RedBlackTree.agda ryokka parents: 513 diff changeset	51 root : Maybe (Node a k)
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	52 nodeStack : SingleLinkedStack (Node a k)
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	53 -- compare : k → k → Tri A B C
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	54
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	55 open RedBlackTree
24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	56
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	57 open SingleLinkedStack
512 95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	58
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	59 compTri : ( x y : ℕ ) -> Tri ( x < y ) ( x ≡ y ) ( x > y )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	60 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	61 where open import Relation.Binary
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	62
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	63 -- put new node at parent node, and rebuild tree to the top
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	64 --
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	65 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	66 replaceNode : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	67 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s (
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	68 \s parent → replaceNode1 s parent)
570 a6aa2ff5fea4 separate clearStack ryokka parents: 564 diff changeset	69 module ReplaceNode where
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	70 replaceNode1 : SingleLinkedStack (Node a k) → Maybe ( Node a k ) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	71 replaceNode1 s nothing = next ( record tree { root = just (record n0 { color = Black}) } )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	72 replaceNode1 s (just n1) with compTri (key n1) (key n0)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	73 replaceNode1 s (just n1) \| tri< lt ¬eq ¬gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	74 replaceNode1 s (just n1) \| tri≈ ¬lt eq ¬gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { left = just n0 } ) next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	75 replaceNode1 s (just n1) \| tri> ¬lt ¬eq gt = replaceNode {n} {m} {t} {a} {k} tree s ( record n1 { right = just n0 } ) next
478 0223c07c3946 fix stack.agda ryokka parents: 428 diff changeset	76
525 0696b9846415 write rotateRithg. but not working now ryokka parents: 523 diff changeset	77
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	78 rotateRight : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) →
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	79 (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	80 rotateRight {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 → rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext)
530 63f3df7f5448 add insertCase41, insertCase5 ryokka parents: 529 diff changeset	81 where
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	82 rotateRight1 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) →
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	83 (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	84 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	85 ... \| nothing = rotateNext tree s nothing n0
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	86 ... \| just n1 with parent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	87 ... \| nothing = rotateNext tree s (just n1 ) n0
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	88 ... \| just parent1 with left parent1
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	89 ... \| nothing = rotateNext tree s (just n1) nothing
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	90 ... \| just leftParent with compTri (key n1) (key leftParent)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	91 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext \| just n1 \| just parent1 \| just leftParent \| tri< a₁ ¬b ¬c = rotateNext tree s (just n1) parent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	92 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext \| just n1 \| just parent1 \| just leftParent \| tri≈ ¬a b ¬c = rotateNext tree s (just n1) parent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	93 rotateRight1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext \| just n1 \| just parent1 \| just leftParent \| tri> ¬a ¬b c = rotateNext tree s (just n1) parent
530 63f3df7f5448 add insertCase41, insertCase5 ryokka parents: 529 diff changeset	94
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	95
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	96 rotateLeft : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) →
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	97 (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	98 rotateLeft {n} {m} {t} {a} {k} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 → rotateLeft1 tree s n0 parent rotateNext)
530 63f3df7f5448 add insertCase41, insertCase5 ryokka parents: 529 diff changeset	99 where
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	100 rotateLeft1 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) →
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	101 (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t) → t
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	102 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext with n0
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	103 ... \| nothing = rotateNext tree s nothing n0
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	104 ... \| just n1 with parent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	105 ... \| nothing = rotateNext tree s (just n1) nothing
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	106 ... \| just parent1 with right parent1
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	107 ... \| nothing = rotateNext tree s (just n1) nothing
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	108 ... \| just rightParent with compTri (key n1) (key rightParent)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	109 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext \| just n1 \| just parent1 \| just rightParent \| tri< a₁ ¬b ¬c = rotateNext tree s (just n1) parent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	110 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext \| just n1 \| just parent1 \| just rightParent \| tri≈ ¬a b ¬c = rotateNext tree s (just n1) parent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	111 rotateLeft1 {n} {m} {t} {a} {k} tree s n0 parent rotateNext \| just n1 \| just parent1 \| just rightParent \| tri> ¬a ¬b c = rotateNext tree s (just n1) parent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	112 -- ... \| EQ = rotateNext tree s (just n1) parent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	113 -- ... \| _ = rotateNext tree s (just n1) parent
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	114
530 63f3df7f5448 add insertCase41, insertCase5 ryokka parents: 529 diff changeset	115 {-# TERMINATING #-}
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	116 insertCase5 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	117 insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent → insertCase51 tree s n0 parent grandParent next)
530 63f3df7f5448 add insertCase41, insertCase5 ryokka parents: 529 diff changeset	118 where
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	119 insertCase51 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → Maybe (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	120 insertCase51 {n} {m} {t} {a} {k} tree s n0 parent grandParent next with n0
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	121 ... \| nothing = next tree
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	122 ... \| just n1 with parent \| grandParent
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	123 ... \| nothing \| _ = next tree
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	124 ... \| _ \| nothing = next tree
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	125 ... \| just parent1 \| just grandParent1 with left parent1 \| left grandParent1
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	126 ... \| nothing \| _ = next tree
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	127 ... \| _ \| nothing = next tree
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	128 ... \| just leftParent1 \| just leftGrandParent1
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	129 with compTri (key n1) (key leftParent1) \| compTri (key leftParent1) (key leftGrandParent1)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	130 ... \| tri≈ ¬a b ¬c \| tri≈ ¬a1 b1 ¬c1 = rotateRight tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	131 ... \| _ \| _ = rotateLeft tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	132 -- ... \| EQ \| EQ = rotateRight tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	133 -- ... \| _ \| _ = rotateLeft tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	134
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	135 insertCase4 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	136 insertCase4 {n} {m} {t} {a} {k} tree s n0 parent grandParent next
528 7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	137 with (right parent) \| (left grandParent)
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	138 ... \| nothing \| _ = insertCase5 tree s (just n0) parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	139 ... \| _ \| nothing = insertCase5 tree s (just n0) parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	140 ... \| just rightParent \| just leftGrandParent with compTri (key n0) (key rightParent) \| compTri (key parent) (key leftGrandParent) -- (key n0) (key rightParent) \| (key parent) (key leftGrandParent)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	141 -- ... \| EQ \| EQ = popSingleLinkedStack s (\ s n1 → rotateLeft tree s (left n0) (just grandParent)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	142 -- (\ tree s n0 parent → insertCase5 tree s n0 rightParent grandParent next))
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	143 -- ... \| _ \| _ = insertCase41 tree s n0 parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	144 ... \| tri≈ ¬a b ¬c \| tri≈ ¬a1 b1 ¬c1 = popSingleLinkedStack s (\ s n1 → rotateLeft tree s (left n0) (just grandParent) (\ tree s n0 parent → insertCase5 tree s n0 rightParent grandParent next))
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	145 ... \| _ \| _ = insertCase41 tree s n0 parent grandParent next
530 63f3df7f5448 add insertCase41, insertCase5 ryokka parents: 529 diff changeset	146 where
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	147 insertCase41 : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	148 insertCase41 {n} {m} {t} {a} {k} tree s n0 parent grandParent next
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	149 with (left parent) \| (right grandParent)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	150 ... \| nothing \| _ = insertCase5 tree s (just n0) parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	151 ... \| _ \| nothing = insertCase5 tree s (just n0) parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	152 ... \| just leftParent \| just rightGrandParent with compTri (key n0) (key leftParent) \| compTri (key parent) (key rightGrandParent)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	153 ... \| tri≈ ¬a b ¬c \| tri≈ ¬a1 b1 ¬c1 = popSingleLinkedStack s (\ s n1 → rotateRight tree s (right n0) (just grandParent) (\ tree s n0 parent → insertCase5 tree s n0 leftParent grandParent next))
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	154 ... \| _ \| _ = insertCase5 tree s (just n0) parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	155 -- ... \| EQ \| EQ = popSingleLinkedStack s (\ s n1 → rotateRight tree s (right n0) (just grandParent)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	156 -- (\ tree s n0 parent → insertCase5 tree s n0 leftParent grandParent next))
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	157 -- ... \| _ \| _ = insertCase5 tree s (just n0) parent grandParent next
527 a829a367cf7d add insertCase4 ryokka parents: 526 diff changeset	158
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	159 colorNode : {n : Level } {a : Set n} {k : ℕ} → Node a k → Color → Node a k
532 ccf98ed4a4f7 fix red black tree Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 531 diff changeset	160 colorNode old c = record old { color = c }
527 a829a367cf7d add insertCase4 ryokka parents: 526 diff changeset	161
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	162 {-# TERMINATING #-}
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	163 insertNode : {n m : Level } {t : Set m } {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → (RedBlackTree {n} {m} {t} a k → t) → t
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	164 insertNode {n} {m} {t} {a} {k} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0)
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	165 where
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	166 insertCase1 : Node a k → SingleLinkedStack (Node a k) → Maybe (Node a k) → Maybe (Node a k) → t -- placed here to allow mutual recursion
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	167 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	168 insertCase3 : SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → t
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	169 insertCase3 s n0 parent grandParent with left grandParent \| right grandParent
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	170 ... \| nothing \| nothing = insertCase4 tree s n0 parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	171 ... \| nothing \| just uncle = insertCase4 tree s n0 parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	172 ... \| just uncle \| _ with compTri ( key uncle ) ( key parent )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	173 insertCase3 s n0 parent grandParent \| just uncle \| _ \| tri≈ ¬a b ¬c = insertCase4 tree s n0 parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	174 insertCase3 s n0 parent grandParent \| just uncle \| _ \| tri< a ¬b ¬c with color uncle
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	175 insertCase3 s n0 parent grandParent \| just uncle \| _ \| tri< a ¬b ¬c \| Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 (
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	176 record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	177 insertCase3 s n0 parent grandParent \| just uncle \| _ \| tri< a ¬b ¬c \| Black = insertCase4 tree s n0 parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	178 insertCase3 s n0 parent grandParent \| just uncle \| _ \| tri> ¬a ¬b c with color uncle
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	179 insertCase3 s n0 parent grandParent \| just uncle \| _ \| tri> ¬a ¬b c \| Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 ( record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	180 insertCase3 s n0 parent grandParent \| just uncle \| _ \| tri> ¬a ¬b c \| Black = insertCase4 tree s n0 parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	181 -- ... \| EQ = insertCase4 tree s n0 parent grandParent next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	182 -- ... \| _ with color uncle
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	183 -- ... \| Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1 (
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	184 -- record grandParent { color = Red ; left = just ( record parent { color = Black } ) ; right = just ( record uncle { color = Black } ) }) s p0 p1 )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	185 -- ... \| Black = insertCase4 tree s n0 parent grandParent next --!!
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	186 insertCase2 : SingleLinkedStack (Node a k) → Node a k → Node a k → Node a k → t
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	187 insertCase2 s n0 parent grandParent with color parent
538 5c001e8ba0d5 add redBlackTreeTest.agda test5,test51. but not work ryokka parents: 537 diff changeset	188 ... \| Black = replaceNode tree s n0 next
532 ccf98ed4a4f7 fix red black tree Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 531 diff changeset	189 ... \| Red = insertCase3 s n0 parent grandParent
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	190 insertCase1 n0 s nothing nothing = next tree
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	191 insertCase1 n0 s nothing (just grandParent) = next tree
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	192 insertCase1 n0 s (just parent) nothing = replaceNode tree s (colorNode n0 Black) next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	193 insertCase1 n0 s (just parent) (just grandParent) = insertCase2 s n0 parent grandParent
528 7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	194
531 f6060e1bf900 add clearStack ryokka parents: 530 diff changeset	195 ----
549 bc3208d510cd add some Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 545 diff changeset	196 -- find node potition to insert or to delete, the path will be in the stack
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	197 --
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	198 findNode : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Node a k) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	199 findNode {n} {m} {a} {k} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s → findNode1 s n1)
570 a6aa2ff5fea4 separate clearStack ryokka parents: 564 diff changeset	200 module FindNode where
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	201 findNode2 : SingleLinkedStack (Node a k) → (Maybe (Node a k)) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	202 findNode2 s nothing = next tree s n0
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	203 findNode2 s (just n) = findNode tree s n0 n next
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	204 findNode1 : SingleLinkedStack (Node a k) → (Node a k) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	205 findNode1 s n1 with (compTri (key n0) (key n1))
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	206 findNode1 s n1 \| tri< a ¬b ¬c = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	207 findNode1 s n1 \| tri≈ ¬a b ¬c = findNode2 s (right n1)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	208 findNode1 s n1 \| tri> ¬a ¬b c = findNode2 s (left n1)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	209 -- ... \| EQ = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	210 -- ... \| GT = findNode2 s (right n1)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	211 -- ... \| LT = findNode2 s (left n1)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	212
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	213
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	214
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	215
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	216 leafNode : {n : Level } { a : Set n } → a → (k : ℕ) → (Node a k)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	217 leafNode v k1 = record { key = k1 ; value = v ; right = nothing ; left = nothing ; color = Red }
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	218
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 575 diff changeset	219 putRedBlackTree : {n m : Level} {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → ℕ → ℕ → (RedBlackTree {n} {m} {t} a k → t) → t
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	220 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next with (root tree)
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 575 diff changeset	221 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next \| nothing = next (record tree {root = just (leafNode val k1) })
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	222 putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next \| just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode {!!} {!!}) n2 (λ tree1 s n1 → insertNode tree1 s n1 next))
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	223 -- putRedBlackTree {n} {m} {t} {a} {k} tree value k1 next with (root tree)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	224 -- ... \| nothing = next (record tree {root = just (leafNode k1 value) })
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	225 -- ... \| just n2 = clearSingleLinkedStack (nodeStack tree) (\ s → findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 → insertNode tree1 s n1 next))
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	226
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	227
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	228 -- getRedBlackTree : {n m : Level } {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} {A} a k → k → (RedBlackTree {n} {m} {t} {A} a k → (Maybe (Node a k)) → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	229 -- getRedBlackTree {_} {_} {t} {a} {k} tree k1 cs = checkNode (root tree)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	230 -- module GetRedBlackTree where -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	231 -- search : Node a k → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	232 -- checkNode : Maybe (Node a k) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	233 -- checkNode nothing = cs tree nothing
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	234 -- checkNode (just n) = search n
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	235 -- search n with compTri k1 (key n)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	236 -- search n \| tri< a ¬b ¬c = checkNode (left n)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	237 -- search n \| tri≈ ¬a b ¬c = cs tree (just n)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	238 -- search n \| tri> ¬a ¬b c = checkNode (right n)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	239
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	240
ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	241
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	242 -- compareT : {A B C : Set } → ℕ → ℕ → Tri A B C
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	243 -- compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder) x y
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	244 -- compareT x y \| tri< a ¬b ¬c = tri< {!!} {!!} {!!}
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	245 -- compareT x y \| tri≈ ¬a b ¬c = {!!}
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	246 -- compareT x y \| tri> ¬a ¬b c = {!!}
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	247 -- -- ... \| tri≈ a b c = {!!}
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	248 -- -- ... \| tri< a b c = {!!}
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	249 -- -- ... \| tri> a b c = {!!}
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	250
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	251 -- compare2 : (x y : ℕ ) → CompareResult {Level.zero}
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	252 -- compare2 zero zero = EQ
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	253 -- compare2 (suc _) zero = GT
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	254 -- compare2 zero (suc _) = LT
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	255 -- compare2 (suc x) (suc y) = compare2 x y
515 54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	256
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	257 -- -- putUnblanceTree : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} {A} a k → k → a → (RedBlackTree {n} {m} {t} {A} a k → t) → t
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	258 -- -- putUnblanceTree {n} {m} {A} {a} {k} {t} tree k1 value next with (root tree)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	259 -- -- ... \| nothing = next (record tree {root = just (leafNode k1 value) })
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	260 -- -- ... \| just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next))
533 2d6ccbf429ad add test Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 532 diff changeset	261
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	262 -- -- checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	263 -- -- checkT nothing _ = false
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	264 -- -- checkT (just n) x with compTri (value n) x
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	265 -- -- ... \| tri≈ _ _ _ = true
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	266 -- -- ... \| _ = false
545 b180dc78abcf add someTest ryokka parents: 543 diff changeset	267
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	268 -- -- checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (just n) x ≡ true
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	269 -- -- checkEQ x n refl with compTri (value n) x
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	270 -- -- ... \| tri≈ _ refl _ = refl
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	271 -- -- ... \| tri> _ neq gt = ⊥-elim (neq refl)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	272 -- -- ... \| tri< lt neq _ = ⊥-elim (neq refl)
564 40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 551 diff changeset	273
545 b180dc78abcf add someTest ryokka parents: 543 diff changeset	274
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	275 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	276 → RedBlackTree {n} {m} {t} a b
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	277 createEmptyRedBlackTreeℕ a b = record {
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	278 root = nothing
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	279 ; nodeStack = emptySingleLinkedStack
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	280 -- ; nodeComp = λ x x₁ → {!!}
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	281
545 b180dc78abcf add someTest ryokka parents: 543 diff changeset	282 }
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	283
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	284 -- ( x y : ℕ ) -> Tri ( x < y ) ( x ≡ y ) ( x > y )
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	285
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	286 -- test = (λ x → (createEmptyRedBlackTreeℕ x x)
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	287
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 575 diff changeset	288 -- ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0
575 73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	289
73fc32092b64 push local rbtree ryokka parents: 570 diff changeset	290 -- tes = putRedBlackTree {_} {_} {_} (createEmptyRedBlackTreeℕ {_} {_} {_} 3 3) 2 2 (λ t → t)

Mercurial > hg > Members > Moririn

annotate RedBlackTree.agda @ 589:37f5826ca7d2