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); *\/ */
/* /\* } *\/ */