Mercurial > hg > Members > Moririn
view src/parallel_execution/RedBlackTree.agda @ 425:ea6353b6c4ef
Add findNode to RedBlackTree.agda
author | innparusu |
---|---|
date | Fri, 06 Oct 2017 19:00:26 +0900 |
parents | 24c98ca207f4 |
children | 07ccd411ad70 |
line wrap: on
line source
module RedBlackTree where open import stack record Tree {a t : Set} (treeImpl : Set) : Set where field tree : treeImpl put : treeImpl -> a -> (treeImpl -> t) -> t get : treeImpl -> (treeImpl -> Maybe a -> t) -> t data Color : Set where Red : Color Black : Color record Node (a : Set) : Set where field node : Element a right : Maybe (Node a) left : Maybe (Node a) color : Color record RedBlackTree (a : Set) : Set where field root : Maybe (Node a) stack : Stack open RedBlackTree putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t putRedBlackTree tree datum next with (root tree) ... | Nothing = insertNode tree datum next ... | Just n = findNode tree datum n (\ tree1 -> insertNode tree1 datum next) findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t findNode tree datum n next = push (stack tree) n (\ s -> findNode1 (record { root = root tree; stack = s }) datum n next) findNode1 : {Data t : Set} -> RedBlackTree Data -> Data -> Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t findNode1 tree datum n next with (compare datum n) ... | EQ = next (record { root = root tree; stack = createSingleLinkedStack }) ... | GT = findNode2 tree datum (right n) next ... | LT = findNode2 tree datum (left n) next where findNode2 tree datum nothing next = insertNode tree datum next findNode2 tree datum (just n) next = findNode tree datum n next insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next) insertCase1 tree datum nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack }) insertCase1 tree datum (just parent) grandparent next = insertCase2 tree datum parent grandparent next insertCase2 tree datum parent grandparent next with (color parent) ... | Red = insertCase3 tree datum parent grandparent next ... | Black = next (record { root = ?; stack = createSingleLinkedStack }) insertCase3 tree datum parent grandparent next getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t getRedBlackTree tree cs with (root tree) ... | Nothing = cs tree Nothing ... | Just d = cs stack1 (Just data1) where data1 = datum d stack1 = record { root = (next d) } __code insertCase3(struct RedBlackTree* tree) { struct Stack* nodeStack = tree->nodeStack; struct Node* uncle; if (tree->grandparent->left == tree->parent) uncle = tree->grandparent->right; else uncle = tree->grandparent->left; if (uncle && (uncle->color == Red)) { // do insertcase1 on grandparent, stack must be pop by two tree->parent->color = Black; uncle->color = Black; tree->grandparent->color = Red; tree->current = tree->grandparent; goto nodeStack->pop2(insertCase1); } goto insertCase4(); } __code insertCase4(struct RedBlackTree* tree, struct RotateTree* rotateTree) { struct Stack* nodeStack = tree->nodeStack; if ((tree->current == tree->parent->right) && (tree->parent == tree->grandparent->left)) { tree->current = tree->current->left; tree->parent = tree->grandparent; rotateTree->traverse = tree; rotateTree->next = C_insertCase5; goto nodeStack->pop(rotateLeft); } else if ((tree->current == tree->parent->left) && (tree->parent == tree->grandparent->right)) { tree->parent = tree->grandparent; tree->current = tree->current->right; rotateTree->traverse = tree; rotateTree->next = C_insertCase5; goto nodeStack->pop(rotateRight); } goto insertCase5(); } __code insertCase5(struct RedBlackTree* tree) { struct Stack* nodeStack = tree->nodeStack; goto nodeStack->pop2(insertCase51); } __code insertCase51(struct RedBlackTree* tree, struct RotateTree* rotateTree, struct Node* parent, struct Node* grandparent) { struct Node* current = tree->current; tree->parent = parent; tree->grandparent = grandparent; parent->color = Black; grandparent->color = Red; tree->current = grandparent; rotateTree->traverse = tree; rotateTree->next = C_stackClear; if ((current == parent->left) && (parent == grandparent->left)) goto rotateRight(); else goto rotateLeft(); } __code insertCase51_stub(struct Context* context) { struct Node* parent = &context->data[D_Stack]->Stack.data->Node; struct Node* grandparent = &context->data[D_Stack]->Stack.data1->Node; goto insertCase51(context, &Gearef(context, Tree)->tree->Tree.tree->RedBlackTree, Gearef(context, RotateTree), parent, grandparent); } __code rotateLeft(struct RedBlackTree* tree, struct Stack* nodeStack) { nodeStack->stack = (union Data*)tree->nodeStack; nodeStack->next = C_rotateLeft1; goto meta(context, tree->nodeStack->get); } __code rotateLeft_stub(struct Context* context) { struct RedBlackTree* traverse = context->data[D_RotateTree]->RotateTree.traverse; goto rotateLeft(context, traverse, Gearef(context, Stack)); } __code rotateLeft1(struct Node* node, struct RedBlackTree* tree, struct Node* parent, struct RotateTree* rotateTree) { struct Node* tmp = node->right; if (parent) { if (node == parent->left) parent->left = tmp; else parent->right = tmp; } else { tree->root = tmp; } node->right = tmp->left; tmp->left = node; tree->current = tmp; goto meta(context, rotateTree->next); } __code rotateLeft1_stub(struct Context* context) { struct RedBlackTree* traverse = context->data[D_RotateTree]->RotateTree.traverse; struct Node* parent = &context->data[D_Stack]->Stack.data->Node; goto rotateLeft1(context, traverse->current, traverse, parent, Gearef(context, RotateTree)); } __code rotateRight(struct RedBlackTree* tree, struct Stack* nodeStack) { nodeStack->stack = (union Data*)tree->nodeStack; nodeStack->next = C_rotateRight1; goto meta(context, tree->nodeStack->get); } __code rotateRight_stub(struct Context* context) { struct RedBlackTree* traverse = context->data[D_RotateTree]->RotateTree.traverse; goto rotateLeft(context, traverse, Gearef(context, Stack)); } __code rotateRight1(struct Node* node, struct RedBlackTree* traverse,struct Node *parent,struct RotateTree *rotateTree) { struct Node* tmp = node->left; if (parent) { if (node == parent->left) parent->left = tmp; else parent->right = tmp; } else { traverse->root = tmp; } node->left = tmp->right; tmp->right = node; traverse->current = tmp; goto meta(context, rotateTree->next); } __code rotateRight1_stub(struct Context* context) { struct RedBlackTree* traverse = context->data[D_RotateTree]->RotateTree.traverse; struct Node* parent = &context->data[D_Stack]->Stack.data->Node; goto rotateRight1(context, traverse->current, traverse, parent, Gearef(context, RotateTree)); } __code stackClear(struct RedBlackTree* tree, struct Stack* nodeStack, __code next(...)) { tree->current = 0; nodeStack->stack = (union Data*)tree->nodeStack; nodeStack->next = next; goto meta(context, tree->nodeStack->clear); } __code getRedBlackTree(struct RedBlackTree* tree, __code next(...)) { if (tree->root) { tree->current = tree->root; goto search(); } goto next(...); } __code search(struct RedBlackTree* tree, struct Node* node, __code next(...)) { // compare(context, traverse, traverse->current->key, node->key); tree->result = compare(tree->current, node); if (tree->result == EQ) { *node = *tree->current; goto meta(context, next); } else if (tree->result == GT) { tree->current = tree->current->right; } else { tree->current = tree->current->left; } if (tree->current) goto meta(context, C_search); goto next(...); } /* /\* __code delete(struct Context* context, struct Tree* tree) { *\/ */ /* /\* if (tree->root) { *\/ */ /* /\* stack_push(context->code_stack, &context->next); *\/ */ /* /\* context->next = Delete1; *\/ */ /* /\* goto meta(context, Get); *\/ */ /* /\* } *\/ */ /* /\* goto meta(context, context->next); *\/ */ /* /\* } *\/ */ /* /\* __code delete_stub(struct Context* context) { *\/ */ /* /\* goto delete(context, &context->data[Tree]->tree); *\/ */ /* /\* } *\/ */ /* /\* __code delete1(struct Context* context, struct Tree* tree, struct Allocate* allocate) { *\/ */ /* /\* allocate->size = sizeof(struct Node); *\/ */ /* /\* allocator(context); *\/ */ /* /\* struct Node* root = tree->root; *\/ */ /* /\* tree->root = &context->data[context->dataNum]->node; *\/ */ /* /\* tree->current = root; *\/ */ /* /\* compare(context, tree, tree->current->key, context->data[Node]->node.key); *\/ */ /* /\* goto meta(context, Replace_d1); *\/ */ /* /\* } *\/ */ /* /\* __code delete1_stub(struct Context* context) { *\/ */ /* /\* goto delete1(context, &context->data[Tree]->tree, &context->data[Allocate]->allocate); *\/ */ /* /\* } *\/ */ /* /\* __code delete2(struct Context* context, struct Node* current) { *\/ */ /* /\* if (current->color == Black) { *\/ */ /* /\* struct Node* child = current->right == NULL ? current->left : current->right; *\/ */ /* /\* current->color = child == NULL ? Black : child->color; *\/ */ /* /\* goto meta(context, DeleteCase1); *\/ */ /* /\* } *\/ */ /* /\* goto meta(context, Delete3); *\/ */ /* /\* } *\/ */ /* /\* __code delete2_stub(struct Context* context) { *\/ */ /* /\* goto delete2(context, context->data[Tree]->tree.current); *\/ */ /* /\* } *\/ */ /* /\* __code delete3(struct Context* context, struct Tree* tree, struct Node* current) { *\/ */ /* /\* struct Node* tmp = current->right == NULL ? current->left : current->right; *\/ */ /* /\* if (current->parent) { *\/ */ /* /\* if (current == current->parent->left) *\/ */ /* /\* current->parent->left = tmp; *\/ */ /* /\* else *\/ */ /* /\* current->parent->right = tmp; *\/ */ /* /\* } else { *\/ */ /* /\* tree->root = tmp; *\/ */ /* /\* } *\/ */ /* /\* if (tmp) *\/ */ /* /\* tmp->parent = current->parent; *\/ */ /* /\* if (current->parent == NULL && tmp) *\/ */ /* /\* tmp->color = Black; *\/ */ /* /\* current == current->parent->left ? (current->parent->left = NULL) : (current->parent->right = NULL); *\/ */ /* /\* stack_pop(context->code_stack, &context->next); *\/ */ /* /\* goto meta(context, context->next); *\/ */ /* /\* } *\/ */ /* /\* __code delete3_stub(struct Context* context) { *\/ */ /* /\* goto delete3(context, &context->data[Tree]->tree, context->data[Tree]->tree.current); *\/ */ /* /\* } *\/ */ /* /\* __code replaceNodeForDelete1(struct Context* context, struct Tree* tree, struct Node* oldNode, struct Node* newNode, int result) { *\/ */ /* /\* *newNode = *oldNode; *\/ */ /* /\* if (result == EQ) *\/ */ /* /\* goto meta(context, Replace_d2); *\/ */ /* /\* else if (result == GT) *\/ */ /* /\* tree->current = newNode->right; *\/ */ /* /\* else *\/ */ /* /\* tree->current = newNode->left; *\/ */ /* /\* tree->current->parent = newNode; *\/ */ /* /\* if (tree->current->left == NULL && tree->current->right == NULL) *\/ */ /* /\* goto meta(context, Delete2); *\/ */ /* /\* if (result == GT) *\/ */ /* /\* newNode->right = context->heap; *\/ */ /* /\* else if (result == LT) *\/ */ /* /\* newNode->left = context->heap; *\/ */ /* /\* allocator(context); *\/ */ /* /\* compare(context, tree, tree->current->key, context->data[Node]->node.key); *\/ */ /* /\* goto meta(context, Replace_d1); *\/ */ /* /\* } *\/ */ /* /\* __code replaceNodeForDelete1_stub(struct Context* context) { *\/ */ /* /\* goto replaceNodeForDelete1(context, &context->data[Tree]->tree, context->data[Tree]->tree.current, &context->data[context->dataNum]->node, context->data[Tree]->tree.result); *\/ */ /* /\* } *\/ */ /* /\* __code replaceNodeForDelete2(struct Context* context, struct Tree* tree, struct Node* newNode) { *\/ */ /* /\* if (tree->current->left && tree->current->right) { *\/ */ /* /\* newNode->left->parent = newNode; *\/ */ /* /\* tree->current = newNode->left; *\/ */ /* /\* newNode->left = context->heap; *\/ */ /* /\* tree->deleted = newNode; *\/ */ /* /\* allocator(context); *\/ */ /* /\* tree->current->parent = newNode; *\/ */ /* /\* goto meta(context, FindMax1); *\/ */ /* /\* } *\/ */ /* /\* goto meta(context, Delete2); *\/ */ /* /\* } *\/ */ /* /\* __code replaceNodeForDelete2_stub(struct Context* context) { *\/ */ /* /\* goto replaceNodeForDelete2(context, &context->data[Tree]->tree, &context->data[context->dataNum]->node); *\/ */ /* /\* } *\/ */ /* /\* __code findMax1(struct Context* context, struct Tree* tree, struct Node* oldNode, struct Node* newNode) { *\/ */ /* /\* *newNode = *oldNode; *\/ */ /* /\* if (newNode->right) *\/ */ /* /\* goto meta(context, FindMax2); *\/ */ /* /\* tree->deleted->key = newNode->key; *\/ */ /* /\* tree->deleted->value = newNode->value; *\/ */ /* /\* tree->current = newNode; *\/ */ /* /\* goto meta(context, Delete2); *\/ */ /* /\* } *\/ */ /* /\* __code findMax1_stub(struct Context* context) { *\/ */ /* /\* goto findMax1(context, &context->data[Tree]->tree, context->data[Tree]->tree.current, &context->data[context->dataNum]->node); *\/ */ /* /\* } *\/ */ /* /\* __code findMax2(struct Context* context, struct Tree* tree, struct Node* oldNode, struct Node* newNode) { *\/ */ /* /\* *newNode = *oldNode; *\/ */ /* /\* if (newNode->right->right) { *\/ */ /* /\* tree->current = newNode->right; *\/ */ /* /\* newNode->right = context->heap; *\/ */ /* /\* allocator(context); *\/ */ /* /\* tree->current->parent = newNode; *\/ */ /* /\* goto meta(context, FindMax2); *\/ */ /* /\* } *\/ */ /* /\* tree->deleted->key = newNode->right->key; *\/ */ /* /\* tree->deleted->value = newNode->right->value; *\/ */ /* /\* tree->current = newNode; *\/ */ /* /\* goto meta(context, Delete2); *\/ */ /* /\* } *\/ */ /* /\* __code findMax2_stub(struct Context* context) { *\/ */ /* /\* goto findMax2(context, &context->data[Tree]->tree, context->data[Tree]->tree.current, &context->data[context->dataNum]->node); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase1(struct Context* context, struct Node* current) { *\/ */ /* /\* if (current->parent) *\/ */ /* /\* goto meta(context, DeleteCase2); *\/ */ /* /\* goto meta(context, Delete3); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase1_stub(struct Context* context) { *\/ */ /* /\* goto deleteCase1(context, context->data[Tree]->tree.current); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase2(struct Context* context, struct Tree* tree, struct Node* current) { *\/ */ /* /\* struct Node* sibling = current == current->parent->left ? current->parent->right : current->parent->left; *\/ */ /* /\* if ((sibling == NULL ? Black : sibling->color) == Red) { *\/ */ /* /\* current->parent->color = Red; *\/ */ /* /\* sibling->color = Black; *\/ */ /* /\* current == current->parent->left ? (current->parent->left = context->heap) : (current->parent->right = context->heap); *\/ */ /* /\* allocator(context); *\/ */ /* /\* context->data[context->dataNum]->node = *sibling; *\/ */ /* /\* tree->current = current->parent; *\/ */ /* /\* context->next = DeleteCase3; *\/ */ /* /\* stack_push(context->code_stack, &context->next); *\/ */ /* /\* if (current == current->parent->left) *\/ */ /* /\* goto meta(context, RotateL); *\/ */ /* /\* else *\/ */ /* /\* goto meta(context, RotateR); *\/ */ /* /\* } *\/ */ /* /\* goto meta(context, DeleteCase3); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase2_stub(struct Context* context) { *\/ */ /* /\* goto deleteCase2(context, &context->data[Tree]->tree, context->data[Tree]->tree.current); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase3(struct Context* context, struct Tree* tree, struct Node* current) { *\/ */ /* /\* struct Node* sibling = current == current->parent->left ? current->parent->right : current->parent->left; *\/ */ /* /\* if (current->parent->color == Black && *\/ */ /* /\* (sibling == NULL ? Black : sibling->color) == Black && *\/ */ /* /\* (sibling->left == NULL ? Black : sibling->left->color) == Black && *\/ */ /* /\* (sibling->right == NULL ? Black : sibling->right->color) == Black) { *\/ */ /* /\* sibling->color = Red; *\/ */ /* /\* tree->current = current->parent; *\/ */ /* /\* goto meta(context, DeleteCase1); *\/ */ /* /\* } *\/ */ /* /\* goto meta(context, DeleteCase4); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase3_stub(struct Context* context) { *\/ */ /* /\* goto deleteCase3(context, &context->data[Tree]->tree, context->data[Tree]->tree.current); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase4(struct Context* context, struct Node* current) { *\/ */ /* /\* struct Node* sibling = current == current->parent->left ? current->parent->right : current->parent->left; *\/ */ /* /\* if (current->parent->color == Red && *\/ */ /* /\* (sibling == NULL ? Black : sibling->color) == Black && *\/ */ /* /\* (sibling->left == NULL ? Black : sibling->left->color) == Black && *\/ */ /* /\* (sibling->right == NULL ? Black : sibling->right->color) == Black) { *\/ */ /* /\* sibling->color = Red; *\/ */ /* /\* current->parent->color = Black; *\/ */ /* /\* goto meta(context, Delete3); *\/ */ /* /\* } *\/ */ /* /\* goto meta(context, DeleteCase5); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase4_stub(struct Context* context) { *\/ */ /* /\* goto deleteCase4(context, context->data[Tree]->tree.current); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase5(struct Context* context, struct Tree* tree, struct Node* current) { *\/ */ /* /\* struct Node* sibling = current == current->parent->left ? current->parent->right : current->parent->left; *\/ */ /* /\* sibling->parent = current->parent; *\/ */ /* /\* if (current == current->parent->left && *\/ */ /* /\* (sibling == NULL ? Black : sibling->color) == Black && *\/ */ /* /\* (sibling->left == NULL ? Black : sibling->left->color) == Red && *\/ */ /* /\* (sibling->right == NULL ? Black : sibling->right->color) == Black) { *\/ */ /* /\* sibling->color = Red; *\/ */ /* /\* sibling->left->color = Black; *\/ */ /* /\* sibling == sibling->parent->left ? (sibling->parent->left = context->heap) : (sibling->parent->right = context->heap); *\/ */ /* /\* allocator(context); *\/ */ /* /\* struct Node* tmp = &context->data[context->dataNum]->node; *\/ */ /* /\* *tmp = *sibling; *\/ */ /* /\* tmp->parent = current; *\/ */ /* /\* tmp->left = context->heap; *\/ */ /* /\* allocator(context); *\/ */ /* /\* context->data[context->dataNum]->node = *sibling->left; *\/ */ /* /\* context->data[context->dataNum]->node.parent = tmp; *\/ */ /* /\* tree->current = tmp; *\/ */ /* /\* context->next = DeleteCase6; *\/ */ /* /\* stack_push(context->code_stack, &context->next); *\/ */ /* /\* goto meta(context, RotateR); *\/ */ /* /\* } else if (current == current->parent->right && *\/ */ /* /\* (sibling == NULL ? Black : sibling->color) == Black && *\/ */ /* /\* (sibling->left == NULL ? Black : sibling->left->color) == Black && *\/ */ /* /\* (sibling->right == NULL ? Black : sibling->right->color) == Red) { *\/ */ /* /\* sibling->color = Red; *\/ */ /* /\* sibling->right->color = Black; *\/ */ /* /\* sibling == sibling->parent->left ? (sibling->parent->left = context->heap) : (sibling->parent->right = context->heap); *\/ */ /* /\* allocator(context); *\/ */ /* /\* struct Node* tmp = &context->data[context->dataNum]->node; *\/ */ /* /\* *tmp = *sibling; *\/ */ /* /\* tmp->parent = current; *\/ */ /* /\* tmp->right = context->heap; *\/ */ /* /\* allocator(context); *\/ */ /* /\* context->data[context->dataNum]->node = *sibling->right; *\/ */ /* /\* context->data[context->dataNum]->node.parent = tmp; *\/ */ /* /\* tree->current = tmp; *\/ */ /* /\* context->next = DeleteCase6; *\/ */ /* /\* stack_push(context->code_stack, &context->next); *\/ */ /* /\* goto meta(context, RotateL); *\/ */ /* /\* } *\/ */ /* /\* goto meta(context, DeleteCase6); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase5_stub(struct Context* context) { *\/ */ /* /\* goto deleteCase5(context, &context->data[Tree]->tree, context->data[Tree]->tree.current); *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase6(struct Context* context, struct Tree* tree, struct Node* current) { *\/ */ /* /\* struct Node* sibling = current == current->parent->left ? current->parent->right : current->parent->left; *\/ */ /* /\* sibling == sibling->parent->left ? (sibling->parent->left = context->heap) : (sibling->parent->right = context->heap); *\/ */ /* /\* allocator(context); *\/ */ /* /\* struct Node* tmp = &context->data[context->dataNum]->node; *\/ */ /* /\* *tmp = *sibling; *\/ */ /* /\* tmp->parent = current; *\/ */ /* /\* tmp->color = current->parent->color; *\/ */ /* /\* current->parent->color = Black; *\/ */ /* /\* context->next = Delete3; *\/ */ /* /\* stack_push(context->code_stack, &context->next); *\/ */ /* /\* if (current == current->parent->left) { *\/ */ /* /\* tmp->right->color = Black; *\/ */ /* /\* tree->current = current->parent; *\/ */ /* /\* goto meta(context, RotateL); *\/ */ /* /\* } else { *\/ */ /* /\* tmp->left->color = Black; *\/ */ /* /\* tree->current = current->parent; *\/ */ /* /\* goto meta(context, RotateR); *\/ */ /* /\* } *\/ */ /* /\* } *\/ */ /* /\* __code deleteCase6_stub(struct Context* context) { *\/ */ /* /\* goto deleteCase6(context, &context->data[Tree]->tree, context->data[Tree]->tree.current); *\/ */ /* /\* } *\/ */