Gears/GearsAgda: RedBlackTree.agda annotate

annotate RedBlackTree.agda @ 529:c9be3631cc41

fix insertCase4

author	ryokka
date	Tue, 09 Jan 2018 15:43:35 +0900
parents	7719f40e1367
children	63f3df7f5448

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
24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	3 open import stack
511 044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	4 open import Level
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	5
511 044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	6 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	7 field
044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	8 putImpl : treeImpl -> a -> (treeImpl -> t) -> t
044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	9 getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t
044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	10 open TreeMethods
044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	11
044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	12 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	13 field
24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	14 tree : treeImpl
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	15 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	16 putTree : a -> (Tree treeImpl -> t) -> t
511 044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	17 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	18 getTree : (Tree treeImpl -> Maybe a -> t) -> t
511 044c25475ed4 fix stack.agda mir3636 parents: 478 diff changeset	19 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	20
478 0223c07c3946 fix stack.agda ryokka parents: 428 diff changeset	21 open Tree
0223c07c3946 fix stack.agda ryokka parents: 428 diff changeset	22
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	23 data Color {n : Level } : Set n where
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	24 Red : Color
ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	25 Black : Color
ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	26
512 95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	27 data CompareResult {n : Level } : Set n where
95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	28 LT : CompareResult
95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	29 GT : CompareResult
95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	30 EQ : CompareResult
95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	31
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	32 record Node {n : Level } (a k : Set n) : Set n where
f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	33 inductive
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	34 field
512 95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	35 key : k
95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	36 value : a
513 f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	37 right : Maybe (Node a k)
f2a3acc766b5 fix RedBlackTree.agda ryokka parents: 512 diff changeset	38 left : Maybe (Node a k)
514 f86da73d611e fix RedBlackTree.agda ryokka parents: 513 diff changeset	39 color : Color {n}
512 95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	40 open Node
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	41
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	42 record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	43 field
514 f86da73d611e fix RedBlackTree.agda ryokka parents: 513 diff changeset	44 root : Maybe (Node a k)
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	45 nodeStack : Stack {n} {m} (Node a k) {t} si
514 f86da73d611e fix RedBlackTree.agda ryokka parents: 513 diff changeset	46 compare : k -> k -> CompareResult {n}
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	47
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	48 open RedBlackTree
24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	49
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	50 open Stack
512 95865cab040a fix RedBlackTree.agda mir3636 parents: 511 diff changeset	51
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	52 --
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	53 -- 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	54 --
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	55 {-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	56 replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	57 replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	58 \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	59 where
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	60 replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	61 replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )
c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	62 replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )
c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	63 replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	64 replaceNode1 s (Just grandParent) result with result
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	65 ... \| LT = replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	66 ... \| GT = replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	67 ... \| EQ = next tree
478 0223c07c3946 fix stack.agda ryokka parents: 428 diff changeset	68
525 0696b9846415 write rotateRithg. but not working now ryokka parents: 523 diff changeset	69
526 c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	70 rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Maybe (Node a k) -> Node a k ->
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	71 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Maybe (Node a k) -> Node a k -> t) -> t
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	72 rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext with parent
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	73 ... \| Nothing = rotateNext tree s n0 Nothing grandParent
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	74 ... \| Just parent1 with left parent1
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	75 ... \| Nothing = rotateNext tree s n0 Nothing grandParent
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	76 ... \| Just leftParent with compare tree (key n0) (key leftParent)
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	77 ... \| EQ = rotateNext tree s n0 parent grandParent
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	78 ... \| _ = rotateNext tree s n0 parent grandParent
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	79
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	80 rotateLeft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Maybe (Node a k) -> Node a k ->
526 c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	81 (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Maybe (Node a k) -> Node a k -> t) -> t
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	82 rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent rotateNext with parent
526 c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	83 ... \| Nothing = rotateNext tree s n0 Nothing grandParent
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	84 ... \| Just parent1 with right parent1
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	85 ... \| Nothing = rotateNext tree s n0 Nothing grandParent
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	86 ... \| Just rightParent with compare tree (key n0) (key rightParent)
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	87 ... \| EQ = rotateNext tree s n0 parent grandParent
c2d236418459 add rotateRight, rotateLeft ryokka parents: 525 diff changeset	88 ... \| _ = rotateNext tree s n0 parent grandParent
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	89
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	90 insertCase5 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	91 insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	92
528 7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	93 insertCase4 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
527 a829a367cf7d add insertCase4 ryokka parents: 526 diff changeset	94 insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next
528 7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	95 with (right parent) \| (left grandParent)
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	96 ... \| Nothing \| _ = insertCase5 tree s n0 parent grandParent next
c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	97 ... \| _ \| Nothing = insertCase5 tree s n0 parent grandParent next
528 7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	98 ... \| Just rightParent \| Just leftGrandParent with compare tree (key n0) (key rightParent) \| compare tree (key parent) (key leftGrandParent)
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	99 ... \| EQ \| EQ = rotateLeft tree s n0 (Just parent) grandParent {!!}
c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	100 ... \| _ \| _ = insertCase5 tree s n0 parent grandParent next
527 a829a367cf7d add insertCase4 ryokka parents: 526 diff changeset	101
a829a367cf7d add insertCase4 ryokka parents: 526 diff changeset	102
519 0a723e418b2a add some more directives in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 518 diff changeset	103 {-# TERMINATING #-}
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	104 insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	105 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	106 where
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	107 insertCase1 : Stack (Node a k) si -> 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	108 -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	109 insertCase3 : Stack (Node a k) si -> 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	110 insertCase3 s n0 parent grandParent with left grandParent \| right grandParent
528 7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	111 ... \| Nothing \| Nothing = insertCase4 tree s n0 parent grandParent next
7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	112 ... \| Nothing \| Just uncle = insertCase4 tree s n0 parent grandParent next
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	113 ... \| Just uncle \| _ with compare tree ( key uncle ) ( key parent )
528 7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	114 ... \| EQ = insertCase4 tree s n0 parent grandParent next
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	115 ... \| _ with color uncle
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	116 ... \| Red = pop2Stack s ( \s p0 p1 -> insertCase1 s (
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	117 record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } ) ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
528 7719f40e1367 fix insertCase4 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 527 diff changeset	118 ... \| Black = insertCase4 tree s n0 parent grandParent next
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	119 insertCase2 : Stack (Node a k) si -> 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	120 insertCase2 s n0 parent grandParent with color parent
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	121 ... \| Black = replaceNode tree s grandParent n0 next
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	122 ... \| Red = insertCase3 s n0 parent grandParent
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	123 insertCase1 s n0 Nothing Nothing = next tree
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	124 insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	125 insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	126 insertCase1 s n0 (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	127
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	128
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	129 findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	130 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	131 where
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	132 findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
515 54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	133 findNode2 s Nothing = next tree s n0
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	134 findNode2 s (Just n) = findNode tree s n0 n next
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	135 findNode1 : Stack (Node a k) si -> (Node a k) -> t
515 54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	136 findNode1 s n1 with (compare tree (key n0) (key n1))
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	137 ... \| EQ = next tree s n0
515 54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	138 ... \| GT = findNode2 s (right n1)
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	139 ... \| LT = findNode2 s (left n1)
425 ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	140
ea6353b6c4ef Add findNode to RedBlackTree.agda innparusu parents: 417 diff changeset	141
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	142 leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k
515 54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	143 leafNode k1 value = record {
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	144 key = k1 ;
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	145 value = value ;
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	146 right = Nothing ;
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	147 left = Nothing ;
529 c9be3631cc41 fix insertCase4 ryokka parents: 528 diff changeset	148 color = Black
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	149 }
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	150
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	151 putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	152 putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
515 54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	153 ... \| Nothing = next (record tree {root = Just (leafNode k1 value) })
518 c9f90f573efe add more reblack tree in agda Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 515 diff changeset	154 ... \| Just n2 = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
515 54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	155
522 f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	156 getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
f63a9a081b61 remove implementation from RedBlackTree.aga Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 521 diff changeset	157 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
417 24c98ca207f4 add RedBlackTree.agda mir3636 parents: diff changeset	158 where
515 54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	159 checkNode : Maybe (Node a k) -> t
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	160 checkNode Nothing = cs tree Nothing
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	161 checkNode (Just n) = search n
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	162 where
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	163 search : Node a k -> t
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	164 search n with compare tree k1 (key n)
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	165 search n \| LT = checkNode (left n)
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	166 search n \| GT = checkNode (right n)
54ff7a97aec1 fix findNode in Agda ryokka parents: 514 diff changeset	167 search n \| EQ = cs tree (Just n)

Mercurial > hg > Gears > GearsAgda

annotate RedBlackTree.agda @ 529:c9be3631cc41