/* See LICENSE file for copyright and license details. */
#include "common.h"
#ifndef TEST


/** 
 * See `.inverse` in `struct libnormalform_sentence` (Transformation function implementation)
 */
static LIBNORMALFORM_SENTENCE *
trans_inverse(LIBNORMALFORM_SENTENCE *this)
{
	return libnormalform_transformation(this->data.trans.function, this->data.trans.input->inverse(this->data.trans.input));
}


/** 
 * See `.equals` in `struct libnormalform_sentence` (Transformation function implementation)
 */
static int
trans_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out)
{
	if (other->type != TYPE_TRANS || this->data.trans.function != other->data.trans.function)
		return 0;
	return this->data.trans.input->equals(this->data.trans.input, other->data.trans.input, inv_out);
}


/** 
 * See `.evaluate` in `struct libnormalform_sentence` (Transformation function implementation)
 */
static int
trans_evaluate(LIBNORMALFORM_SENTENCE *this, void *input)
{
	int r;
	input = this->data.trans.function->transform(this->data.trans.function->user_data, input);
	if (!input)
		return -1;
	r = this->data.trans.input->evaluate(this->data.trans.input, input);
	if (this->data.trans.function->deallocate)
		this->data.trans.function->deallocate(this->data.trans.function->user_data, input);
	return r;
}


LIBNORMALFORM_SENTENCE *
(libnormalform_transformation)(struct libnormalform_transformer *function, LIBNORMALFORM_SENTENCE *sentence)
{
	static const struct libnormalform_sentence prototype = {
		PROTOTYPE_COMMON,
		.type = TYPE_TRANS,
		.inverse = &trans_inverse,
		.equals = &trans_equals,
		.evaluate = &trans_evaluate
	};

	LIBNORMALFORM_SENTENCE *ret, *left, *right;
	LIBNORMALFORM_SENTENCE *(*connective)(LIBNORMALFORM_SENTENCE *, LIBNORMALFORM_SENTENCE *);

	if (!sentence)
		return NULL;

	function->builtin = LIBNORMALFORM_NOT_BUILT_IN;

	switch (sentence->type) {
	case TYPE_ALL:
	case TYPE_ANY:
	case TYPE_ONE:
	case TYPE_NOT_ONE:
		libnormalform_free(sentence);
		errno = EDOM;
		return NULL;

	case TYPE_TRUE:
	case TYPE_FALSE:
	case TYPE_VARIABLE:
		return sentence;

	case TYPE_FUNCTION:
	case TYPE_TRANS:
		ret = malloc(sizeof(*ret));
		if (!ret) {
			libnormalform_free(sentence);
			return NULL;
		}
		*ret = prototype;
		ret->hash = TRANS_HASH(function, sentence);
		ret->data.trans.function = function;
		ret->data.trans.input = sentence;
		return ret;

	case TYPE_AND:
		connective = &libnormalform_and2__;
		break;
	case TYPE_OR:
		connective = &libnormalform_or2__;
		break;
	case TYPE_XOR:
		connective = &libnormalform_xor2__;
		break;

	default:
		abort();
	}

	left = LEFT(sentence), LEFT(sentence) = NULL;
	right = RIGHT(sentence), RIGHT(sentence) = NULL;
	libnormalform_free(sentence);
	left = libnormalform_transformation(function, left);
	if (!left) {
		libnormalform_free(right);
		return NULL;
	}
	right = libnormalform_transformation(function, right);
	if (!right) {
		libnormalform_free(left);
		return NULL;
	}

	return (*connective)(left, right);
}


#else


static void *
uppercase(void *user_data, void *input)
{
	char *s = strdup(input), *p;
	(void) user_data;
	if (s)
		for (p = s; *p; p++)
			*p = (char)toupper(*p);
	return s;
}


static void *
constuppercase(void *user_data, void *input)
{
	static char ret[] = "HELLO WORLD";
	(void) user_data;
	(void) input;
	return ret;
}


static void *
einval(void *user_data, void *input)
{
	(void) user_data;
	(void) input;
	errno = EINVAL;
	return NULL;
}


static void
deallocate(void *user_data, void *input)
{
	(void) user_data;
	free(input);
}


static int
validate(void *expected, void *input)
{
	return input ? !strcmp(input, expected) : (errno = EDOM, -1);
}


int
main(void)
{
	TEST_BEGIN;

	struct libnormalform_transformer trans1, trans2;
	struct libnormalform_function fun1, fun2;
	struct libnormalform_variable var1;
	struct libnormalform_map dom1;
	LIBNORMALFORM_SENTENCE *a, *b, *f1, *f2;

	errno = 0;
	ASSERT(!libnormalform_transformation(&trans1, NULL) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_transformation(&trans1, NULL) && errno == 1);

	/* F(⊤) = ⊤ */
	ASSUME(a = libnormalform_true());
	ASSUME(b = libnormalform_transformation(&trans1, REF(a)));
	ASSERT(b->refcount == 2);
	ASSERT(b->type == TYPE_TRUE);
	ASSERT(b == a);
	libnormalform_free(a);
	libnormalform_free(b);

	/* F(⊥) = ⊥ */
	ASSUME(a = libnormalform_false());
	ASSUME(b = libnormalform_transformation(&trans1, REF(a)));
	ASSERT(b->refcount == 2);
	ASSERT(b->type == TYPE_FALSE);
	ASSERT(b == a);
	libnormalform_free(a);
	libnormalform_free(b);

	/* F(a) = a */
	ASSUME(a = libnormalform_variable(&var1));
	ASSUME(b = libnormalform_transformation(&trans1, REF(a)));
	ASSERT(b->refcount == 2);
	ASSERT(b->type == TYPE_VARIABLE);
	ASSERT(b == a);
	libnormalform_free(a);
	libnormalform_free(b);

	/* F(f(x)) irreducible */
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_transformation(&trans1, REF(a)));
	ASSERT(b->refcount == 1);
	ASSERT(a->refcount == 2);
	ASSERT(b->type == TYPE_TRANS);
	ASSERT(b->data.trans.function == &trans1);
	ASSERT(b->data.trans.input == a);
	libnormalform_free(a);
	libnormalform_free(b);

	/* F(f(x) ∧ g(x)) = F(f(x)) ∧ F(g(x)) */
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_and2(a, b));
	ASSUME(b = libnormalform_transformation(&trans1, a));
	ASSERT(b->refcount == 1);
	ASSERT(b->type == TYPE_AND);
	ASSERT(LEFT(b)->type == TYPE_TRANS);
	ASSERT(RIGHT(b)->type == TYPE_TRANS);
	ASSERT(LEFT(b)->refcount == 1);
	ASSERT(RIGHT(b)->refcount == 1);
	ASSERT(LEFT(b)->data.trans.function == &trans1);
	ASSERT(RIGHT(b)->data.trans.function == &trans1);
	ASSERT(LEFT(b)->data.trans.input);
	ASSERT(RIGHT(b)->data.trans.input);
	ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION);
	ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION);
	ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input);
	libnormalform_free(b);

	/* F(f(x) ∨ g(x)) = F(f(x)) ∨ F(g(x)) */
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_or2(a, b));
	ASSUME(b = libnormalform_transformation(&trans1, a));
	ASSERT(b->refcount == 1);
	ASSERT(b->type == TYPE_OR);
	ASSERT(LEFT(b)->type == TYPE_TRANS);
	ASSERT(RIGHT(b)->type == TYPE_TRANS);
	ASSERT(LEFT(b)->refcount == 1);
	ASSERT(RIGHT(b)->refcount == 1);
	ASSERT(LEFT(b)->data.trans.function == &trans1);
	ASSERT(RIGHT(b)->data.trans.function == &trans1);
	ASSERT(LEFT(b)->data.trans.input);
	ASSERT(RIGHT(b)->data.trans.input);
	ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION);
	ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION);
	ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input);
	libnormalform_free(b);

	/* F(f(x) ⊕ g(x)) = F(f(x)) ⊕ F(g(x)) */
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_xor2(a, b));
	ASSUME(b = libnormalform_transformation(&trans1, a));
	ASSERT(b->refcount == 1);
	ASSERT(b->type == TYPE_XOR);
	ASSERT(LEFT(b)->type == TYPE_TRANS);
	ASSERT(RIGHT(b)->type == TYPE_TRANS);
	ASSERT(LEFT(b)->refcount == 1);
	ASSERT(RIGHT(b)->refcount == 1);
	ASSERT(LEFT(b)->data.trans.function == &trans1);
	ASSERT(RIGHT(b)->data.trans.function == &trans1);
	ASSERT(LEFT(b)->data.trans.input);
	ASSERT(RIGHT(b)->data.trans.input);
	ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION);
	ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION);
	ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input);
	libnormalform_free(b);

	/* F(Q(q)∀{p,q}:P(p)) illegal construct */
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_all(&dom1, a, b));
	errno = 0;
	ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM);

	/* F(Q(q)∃{p,q}:P(p)) illegal construct */
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_any(&dom1, a, b));
	errno = 0;
	ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM);

	/* F(Q(q)∃!{p,q}:P(p)) illegal construct */
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_one(&dom1, a, b));
	errno = 0;
	ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM);

	/* F(¬(Q(q)∃!{p,q}:P(p))) illegal construct */
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_one(&dom1, a, b));
	ASSUME(a = libnormalform_not(a));
	errno = 0;
	ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM);

	ASSUME(a = libnormalform_function(&fun1));
	trans1.transform = &uppercase;
	trans1.deallocate = &deallocate;

	fun1.evaluate = validate;
	ASSUME(fun1.user_data = strdup("hello world"));
	ASSERT(a->evaluate(a, (char []){"hello world"}) == 1);
	ASSERT(a->evaluate(a, (char []){"HELLO WORLD"}) == 0);
	ASSERT(a->evaluate(a, (char []){"x"}) == 0);
	errno = 0;
	ASSERT(a->evaluate(a, NULL) == -1 && errno == EDOM);
	free(fun1.user_data);

	fun1.evaluate = validate;
	ASSUME(fun1.user_data = strdup("HELLO WORLD"));
	ASSUME(a = libnormalform_transformation(&trans1, a));
	ASSERT(a->evaluate(a, (char []){"hello world"}) == 1);
	ASSERT(a->evaluate(a, (char []){"HELLO WORLD"}) == 1);
	ASSERT(a->evaluate(a, (char []){"x"}) == 0);
	trans1.transform = constuppercase;
	trans1.deallocate = NULL;
	ASSERT(a->evaluate(a, (char []){"hello world"}) == 1);
	free(fun1.user_data);

	libnormalform_free(a);

	ASSUME(f1 = libnormalform_function(&fun1));
	ASSUME(f2 = libnormalform_function(&fun2));

	ASSUME(a = libnormalform_transformation(&trans1, REF(f1)));
	trans1.transform = einval;
	trans1.deallocate = NULL;
	errno = 0;
	ASSERT(a->evaluate(a, (char []){"hello world"}) == -1 && errno == EINVAL);

	ASSERT_NOTEQUAL(a, f1);

	ASSUME(b = libnormalform_true());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_true());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_variable(&var1));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_transformation(&trans1, REF(f1)));
	ASSERT_EQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_transformation(&trans1, libnormalform_not(REF(f1))));
	ASSERT_INVEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_transformation(&trans1, REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_transformation(&trans2, REF(f1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_and2(REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_or2(REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_xor2(REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_all(&dom1, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_any(&dom1, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_one(&dom1, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	ASSUME(b = libnormalform_not(b));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_not(libnormalform_transformation(&trans1, REF(f1))));
	ASSERT_INVEQUAL(a, b);
	libnormalform_free(b);

	libnormalform_free(a);
	libnormalform_free(f1);
	libnormalform_free(f2);

	TEST_END;
}


#endif