#include <stdio.h>
#include "akashaLLRBContext.h"

/* C functions (TODO: convert to code segment) */

unsigned int min_height(struct Node* node, unsigned int height) {
    if ((node->left == NULL) && (node->right == NULL)) return height;
    if (node->left  == NULL) return min_height(node->right, height+1);
    if (node->right == NULL) return min_height(node->left, height+1);

    unsigned int left_min  = min_height(node->left, height+1);
    unsigned int right_min = min_height(node->right, height+1);

    if (left_min < right_min) {
        return left_min;
    } else {
        return right_min;
    }
}

unsigned int max_height(struct Node* node, unsigned int height) {
    if ((node->left == NULL) && (node->right == NULL)) return height;
    if (node->left  == NULL) return max_height(node->right, height+1);
    if (node->right == NULL) return max_height(node->left, height+1);

    unsigned int left_max  = max_height(node->left, height+1);
    unsigned int right_max = max_height(node->right, height+1);

    if (left_max > right_max) {
        return left_max;
    } else {
        return right_max;
    }
}
void printTree(struct Node* node, int n) {
    if (node != 0) {
        printTree(node->left, n+1);
        for (int i=0;i<n;i++)
            printf("  ");
        printf("key=%d value=%d color=%s\t%p\n", node->key, node->value,/* n, */node->color==0? "R":"B", node);
        printTree(node->right, n+1);
    }
}

/* Code Segments */

__code showTrace(struct Context* context, struct Iterator* iter) {
    printf("show trace(reversed):");

    for (; iter != NULL; iter = iter->previousDepth) {
        printf("%u ", iter->iteratedValue);
    }
    printf("\n");

    goto meta(context, context->next);
}

__code verifySpecification(struct Context* context, struct Tree* tree, struct Iterator* iter) {
    unsigned const int min_h = min_height(tree->root, 1);
    unsigned const int max_h = max_height(tree->root, 1);

    if (max_h > 2*min_h) {
        printf("llrb-condition violated.\n");
        printf("\tmin-height %u\n", min_h);
        printf("\tmax-height %u\n", max_h);

        context->next = Exit;
        goto meta(context, ShowTrace);
    }

    goto meta(context, DuplicateIterator);
}