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


/**
 * String under construct
 */
struct string_construction {
	const char **strings; /**< Strings to right-concatenate one-by-one */
	char **dyn_strings;   /**< List of dynamically allocated strings that appear in `.strings` */
	size_t n;             /**< The number of elements in `.strings` */
	size_t size;          /**< The number of elements allocated to `.strings` */
	size_t dyn_n;         /**< The number of elements in `.dyn_strings` */
	size_t dyn_size;      /**< The number of elements allocated to `.dyn_strings` */
	size_t length;        /**< The total length of the string */
};


/**
 * Append a string (with its length already known)
 * 
 * @param   s    The string to append `str` to
 * @param   str  The string to append to `s`
 * @param   len  The length of `str`
 * @return       0 on sucess, -1 on failure
 */
USE_RESULT NONNULL_INPUT
static int
add_string_n(struct string_construction *s, const char *str, size_t len)
{
	if (s->n == s->size) {
		void *new = realloc(s->strings, (s->size += 128) * sizeof(*s->strings));
		if (!new)
			return -1;
		s->strings = new;
	}
	s->strings[s->n++] = str;
	s->length += len;
	return 0;
}


/**
 * Append a string
 * 
 * @param   s    The string to append `str` to
 * @param   str  The string to append to `s`
 * @return       0 on sucess, -1 on failure
 */
USE_RESULT NONNULL_INPUT
static int
add_string(struct string_construction *s, const char *str)
{
	return add_string_n(s, str, strlen(str));
}


/**
 * Append `size_t` encoded in decimal
 * 
 * @param   s    The string to append `num` to
 * @param   num  The number to append to `s`
 * @return       0 on sucess, -1 on failure
 */
USE_RESULT NONNULL_INPUT
static int
add_number(struct string_construction *s, size_t num)
{
	char buf[3 * sizeof(size_t)], *str;
	int len = sprintf(buf, "%zu", num);
	if (len < 0)
		abort();
	if (s->dyn_n == s->dyn_size) {
		void *new = realloc(s->dyn_strings, (s->dyn_size += 8) * sizeof(*s->dyn_strings));
		if (!new)
			return -1;
		s->dyn_strings = new;
	}
	s->dyn_strings[s->dyn_n++] = str = malloc((size_t)len + 1U);
	if (!str)
		return -1;
	memcpy(str, buf, (size_t)len + 1U);
	return add_string_n(s, str, (size_t)len);
}


/**
 * Append the serialisation of a sentence to a string
 *
 * @param   this         The sentence
 * @param   s            The string to append the serialisation to
 * @param   map          `.travel_index` to reference ID map, any sentence that has
 *                       not be been serialised will have its slot set to `SIZE_MAX`;
 *                       set to `NULL` (could also mean that there are not duplicates)
 *                       by `libnormalform__debug_print__` to allow printing during
 *                       indexing and restoration
 * @param   nextrefp     Reference to the next reference ID
 * @param   embed        Whether the sentence may be embed as additional terms
 *                       (1, 0 otherwise); -1 is used by `libnormalform__debug_print__`
 *                       to globally disable embedding
 * @param   depth_limit  Decreases by 1 for each level of recursion, when 0 is
 *                       reached "..." will be appended to `s`, instead of the
 *                       the serialisation of `this`; this is only used by
 *                       `libnormalform__debug_print__`, for
 *                       `libnormalform_to_string` it is initially set to `SIZE_MAX`
 *                       to nullify it's effect (you cannot possibility have more
 *                       levels of recursion than bytes in your stack memory)
 * @return               0 on success, -1 on failure
 */
USE_RESULT SOME_NONNULL_INPUT(1, 2, 4)
static int
to_string(LIBNORMALFORM_SENTENCE *this, struct string_construction *s,
          size_t *map, size_t *nextrefp, int embed, size_t depth_limit)
{
#define ADD_STRING(SC, STRING) add_string_n((SC), STRING, sizeof(STRING) - 1U)
#define IF_MAY_EMBED(X) (embed < 0 ? -1 : (X))

	LIBNORMALFORM_SENTENCE *term1 = NULL, *term2 = NULL;
	int inv = 0, associative = 0;
	const char *function, *identifier = NULL;

	if (!depth_limit)
		return ADD_STRING(s, "...");

	if (this->travel_count > 1 && map) {
		embed = -(embed < 0);
		if (map[this->travel_index] != SIZE_MAX) {
			if (ADD_STRING(s, "REF(") || add_number(s, map[this->travel_index]))
				return -1;
			return ADD_STRING(s, ")");
		}
	}

	switch (this->type) {
	case TYPE_TRUE:
		return ADD_STRING(s, "TRUE");

	case TYPE_FALSE:
		return ADD_STRING(s, "FALSE");

	case TYPE_AND:
		function = "AND";
		goto binary;

	case TYPE_OR:
		function = "OR";
		goto binary;

	case TYPE_XOR:
		function = "XOR";
	binary:
		term1 = this->data.binary.l;
		term2 = this->data.binary.r;
		associative = 1;
		break;

	case TYPE_ALL:
		function = "ALL";
		goto qualifier;

	case TYPE_ANY:
		function = "ANY";
		goto qualifier;

	case TYPE_NOT_ONE:
		inv = 1;
		/* fall through */

	case TYPE_ONE:
		function = "ONE";
	qualifier:
		identifier = this->data.qualifier.domain->identifier;
		term1 = this->data.qualifier.antecedent;
		term2 = this->data.qualifier.predicate;
		break;

	case TYPE_VARIABLE:
		inv = this->data.literal.inverted;
		function = "VARIABLE";
		identifier = this->data.literal.atom.variable->identifier;
		break;

	case TYPE_FUNCTION:
		inv = this->data.literal.inverted;
		function = "FUNCTION";
		identifier = this->data.literal.atom.function->identifier;
		break;

	case TYPE_TRANS:
		function = "TRANSFORMATION";
		identifier = this->data.trans.function->identifier;
		term1 = this->data.trans.input;
		break;

	default:
		abort();
	}

	if (embed == 1)
		goto add_terms;

	if (inv) {
		if (this->travel_count > 1 && map) {
			if (ADD_STRING(s, "NOT@") || add_number(s, *nextrefp) || ADD_STRING(s, "("))
				return -1;
			map[this->travel_index] = (*nextrefp)++;
		} else {
			if (ADD_STRING(s, "NOT("))
				return -1;
		}
	}
	if (add_string(s, function))
		return -1;
	if (!inv && this->travel_count > 1 && map) {
		if (ADD_STRING(s, "@") || add_number(s, *nextrefp))
			return -1;
		map[this->travel_index] = (*nextrefp)++;
	}
	if (ADD_STRING(s, "("))
		return -1;

	if (identifier) {
		if (add_string(s, identifier))
			return -1;
		if (term1 && ADD_STRING(s, ", "))
			return -1;
	}
add_terms:
	if (term1) {
		if (to_string(term1, s, map, nextrefp, IF_MAY_EMBED(associative && term1->type == this->type), depth_limit - 1))
			return -1;
		if (term2 && ADD_STRING(s, ", "))
			return -1;
	}
	if (term2) {
		if (to_string(term2, s, map, nextrefp, IF_MAY_EMBED(associative && term2->type == this->type), depth_limit - 1))
			return -1;
	}

	return embed == 1 ? 0 : inv ? ADD_STRING(s, "))") : ADD_STRING(s, ")");

#undef ADD_STRING
#undef IF_MAY_EMBED
}


#ifdef DEBUG

void
libnormalform__debug_print__(LIBNORMALFORM_SENTENCE *this, size_t depth_limit)
{
	struct string_construction s;
	char *res = NULL, *p;
	size_t i, nextref = 0;

	if (!this) {
		fprintf(stderr, "<debug error: libnormalform__debug_print__: %s>\n", "Null pointer input");
		return;
	}

	s.strings = NULL;
	s.dyn_strings = NULL;
	s.n = 0;
	s.size = 0;
	s.length = 0;
	s.dyn_n = 0;
	s.dyn_size = 0;

	if (to_string(this, &s, NULL, &nextref, -1, depth_limit ? depth_limit : SIZE_MAX))
		goto out;
	res = malloc(s.length + 1U);
	if (!res)
		goto out;

	p = res;
	for (i = 0; i < s.n; i++)
		p = stpcpy(p, s.strings[i]);
	*p = '\0';

out:
	while (s.dyn_n)
		free(s.dyn_strings[--s.dyn_n]);
	free(s.strings);
	free(s.dyn_strings);

	if (res) {
		fprintf(stderr, "%s\n", res);
		free(res);
	} else {
		fprintf(stderr, "<debug error: libnormalform__debug_print__: %s>\n", strerror(errno));
	}
	fflush(stderr);
}

#endif


char *
(libnormalform_to_string)(LIBNORMALFORM_SENTENCE *this)
{
	struct string_construction s;
	char *ret = NULL, *p;
	size_t i, dupcount, *map = NULL, nextref = 0;

	dupcount = libnormalform_set_indices_and_counts__(this);
	if (dupcount) {
		map = malloc(dupcount * sizeof(*map));
		if (!map)
			goto out;
		while (dupcount--)
			map[dupcount] = SIZE_MAX;
	}

	s.strings = NULL;
	s.dyn_strings = NULL;
	s.n = 0;
	s.size = 0;
	s.length = 0;
	s.dyn_n = 0;
	s.dyn_size = 0;

	if (to_string(this, &s, map, &nextref, 0, SIZE_MAX))
		goto out;
	ret = malloc(s.length + 1U);
	if (!ret)
		goto out;

	p = ret;
	for (i = 0; i < s.n; i++)
		p = stpcpy(p, s.strings[i]);
	*p = '\0';

out:
	while (s.dyn_n)
		free(s.dyn_strings[--s.dyn_n]);
	free(s.strings);
	free(s.dyn_strings);
	free(map);
	libnormalform_reset_indices_and_counts__(this);
	return ret;
}


#else


NONNULL_INPUT static LIBNORMALFORM_SENTENCE *
set_order(size_t order, LIBNORMALFORM_SENTENCE *x)
{
	x->hash = order;
	return x;
}


int
main(void)
{
	TEST_BEGIN;

	struct libnormalform_variable var1, var2, var3;
	struct libnormalform_function fun1, fun2;
	struct libnormalform_map dom1, dom2;
	struct libnormalform_transformer trans1;
	LIBNORMALFORM_SENTENCE *ref0, *ref1, *ref2, *ref3, *ref4, *a, *b, *t, *f;
	LIBNORMALFORM_SENTENCE *pref0, *pref1, *ref0a, *ref0b;
	char *s;

	var1.identifier = "var1";
	var2.identifier = "var2";
	var3.identifier = "var3";
	fun1.identifier = "fun1";
	fun2.identifier = "fun2";
	dom1.identifier = "dom1";
	dom2.identifier = "dom2";
	trans1.identifier = "trans1";

	ASSUME(t = libnormalform_true());
	ASSUME(f = libnormalform_false());

#define REF1P "VARIABLE(var1)"
	ASSUME(ref1 = libnormalform_variable(&var1));
	ASSUME(s = libnormalform_to_string(ref1));
	ASSERT(!strcmp(s, REF1P));
	free(s);

#define REF0 "AND@0(VARIABLE@1(var1), VARIABLE(var2), VARIABLE(var3))"
#define REF0P "AND(VARIABLE(var1), VARIABLE(var2), VARIABLE(var3))"
	ASSUME(ref0 =
		libnormalform_and2(
			set_order(1, REF(ref1)),
			set_order(2, libnormalform_and2(
				set_order(3, libnormalform_variable(&var2)),
				set_order(4, libnormalform_variable(&var3))
			))
		)
	);
	ASSUME(s = libnormalform_to_string(ref0));
	ASSERT(!strcmp(s, REF0P));
	free(s);

	ref0a = libnormalform_ref(ref0);

#define REF2 "NOT@2(FUNCTION(fun1))"
#define REF2P "NOT(FUNCTION(fun1))"
	ASSUME(ref2 = libnormalform_not(libnormalform_function(&fun1)));
	ASSUME(s = libnormalform_to_string(ref2));
	ASSERT(!strcmp(s, REF2P));
	free(s);

#define A1 "AND("REF2", REF(1), TRANSFORMATION(trans1, FUNCTION(fun2)))"
#define A1P "AND("REF2P", "REF1P", TRANSFORMATION(trans1, FUNCTION(fun2)))"
#define A1Q "AND("REF2P", REF(1), TRANSFORMATION(trans1, FUNCTION(fun2)))"
	ASSUME(a =
		libnormalform_and2__(
			set_order(1, libnormalform_and2__(
				set_order(2, REF(ref2)),
				set_order(3, REF(ref1))
			)),
			set_order(4, (pref0 = libnormalform_transformation(&trans1, libnormalform_function(&fun2))))
		)
	);
	ASSUME(s = libnormalform_to_string(a));
	ASSERT(!strcmp(s, A1P));
	free(s);

	ref0b = libnormalform_ref(ref0);

#define A2 "XOR("REF0", ALL(dom1, REF(0), "A1"))"
#define A2P "XOR("REF0", ALL(dom1, REF(0), "A1Q"))"
	ASSUME(a =
		libnormalform_xor2(
			REF(ref0),
			libnormalform_all(&dom1, REF(ref0), a)
		)
	);
	ASSUME(s = libnormalform_to_string(a));
	ASSERT(!strcmp(s, A2P));
	free(s);

	libnormalform_free(ref1);

#define REF3 "ONE@3(dom2, TRUE, TRUE)"
#define REF3P "ONE(dom2, TRUE, TRUE)"
	ASSUME(ref3 = libnormalform_one(&dom2, REF(t), REF(t)));
	ASSUME(s = libnormalform_to_string(ref3));
	ASSERT(!strcmp(s, REF3P));
	free(s);

#define REF4 "NOT@4(ONE(dom2, TRUE, TRUE))"
#define REF4P "NOT(ONE(dom2, TRUE, TRUE))"
	ASSUME(ref4 = libnormalform_not(REF(ref3)));
	ASSUME(s = libnormalform_to_string(ref4));
	ASSERT(!strcmp(s, REF4P));
	free(s);

#define B1P "XOR("REF3P", "REF4P")"
#define B1R "XOR(REF(3), REF(4))"
	ASSUME(b = libnormalform_xor2__(set_order(1, REF(ref3)), set_order(2, REF(ref4))));
	ASSUME(s = libnormalform_to_string(b));
	ASSERT(!strcmp(s, B1P));
	free(s);

#define A3P "OR("A2", REF(2), ANY(dom1, TRUE, TRUE), "REF3P", "REF4P")"
#define A3 A2", REF(2), ANY(dom1, TRUE, TRUE), "REF3", "REF4
	ASSUME(a =
		set_order(9, libnormalform_or2(
		set_order(7, libnormalform_or2(
		set_order(5, libnormalform_or2(
		set_order(3, libnormalform_or2(
			set_order(1, a),
			set_order(2, REF(ref2))
		)),
			set_order(4, (pref1 = libnormalform_any(&dom1, REF(t), REF(t))))
		)),
			set_order(6, REF(ref3))
		)),
			set_order(8, REF(ref4))
		))
	);
	ASSUME(s = libnormalform_to_string(a));
	ASSERT(!strcmp(s, A3P));
	free(s);

#define EXPECTED "OR("A3", "B1R")"
	ASSUME(a = libnormalform_or2(set_order(1, a), set_order(2, b)));

	pref0 = libnormalform_ref(pref0);
	pref1 = libnormalform_ref(pref1);

	ASSUME(s = libnormalform_to_string(a));
	ASSERT(!strcmp(s, EXPECTED));
	free(s);

	libnormalform_free(pref0);
	libnormalform_free(pref1);

	libnormalform_free(a);
	libnormalform_free(ref0);
	libnormalform_free(ref0a);
	libnormalform_free(ref0b);
	libnormalform_free(ref2);
	libnormalform_free(ref3);
	libnormalform_free(ref4);

	ASSUME(a = libnormalform_all(&dom1, REF(t), REF(f)));
	ASSUME(s = libnormalform_to_string(a));
	ASSERT(!strcmp(s, "ALL(dom1, TRUE, FALSE)"));
	free(s);
	libnormalform_free(a);

	libnormalform_free(t);
	libnormalform_free(f);

	TEST_END;
}


#endif