/*
 * relop.c - Relational operators
 *
 * Copyright 2012 by Werner Almesberger
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 */


#include <stdlib.h>
#include <stdio.h>

#include "relop.h"


/*
 * Operator to use for
 *
 * forall X: (A op B) == ((X opa A) -> (X opb B))
 *
 * For unlimited sets of values:
 *
 * opa ->  <   <=  ==  >=  >
 * opb 
 *  <      >=  >=  0   0   0
 *  <=     >   >=  0   0   0
 *  ==     >   >=  ==  <=  <
 *  >=     0   0   0   <=  <
 *  >      0   0   0   <=  <=
 *
 * For limited sets of values, we could decide also in some edge cases,
 * but let's save such sophistication for later.
 */


static const enum relop implies_op[idx_n][idx_n] = {
	[idx_lt][idx_lt] = rel_ge,
	[idx_lt][idx_le] = rel_ge,

	[idx_le][idx_lt] = rel_gt,
	[idx_le][idx_le] = rel_ge,

	[idx_eq][idx_lt] = rel_gt,
	[idx_eq][idx_le] = rel_ge,
	[idx_eq][idx_eq] = rel_eq,
};


static int relop2index(enum relop op)
{
	switch (op) {
	case rel_lt:
		return idx_lt;
	case rel_le:
		return idx_le;
	case rel_eq:
		return idx_eq;
	case rel_ge:
		return idx_ge;
	case rel_gt:
		return idx_gt;
	default:
		abort();
	}
}


static enum relop swap_op(enum relop op)
{
	return idx_n-1-relop2index(op);
}


int relop_implies(enum relop opa, enum relop opb, const void *a, const void *b,
    int (*cmp)(const void *a, enum relop op, const void *b, const void *user),
    const void *user)
{
	if (opa <= opb)
		return cmp(a,
		    implies_op[relop2index(opa)][relop2index(opb)], b, user);
	else
		return cmp(b,
		    swap_op(implies_op[relop2index(opb)][relop2index(opa)]),
		    a, user);
}


void dump_relop(FILE *file, enum relop op)
{
	switch (op) {
	case rel_lt:
		fprintf(file, "<");
		break;
	case rel_le:
		fprintf(file, "<=");
		break;
	case rel_eq:
		fprintf(file, "=");
		break;
	case rel_ge:
		fprintf(file, ">=");
		break;
	case rel_gt:
		fprintf(file, ">");
		break;
	default:
		abort();
	}
}