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


/**
 * Recursively deallocate a `LIBNORMALFORM_SENTENCE *`
 * according to `libnormalform_free`
 *
 * @param  this  The object to deallocate
 */
NONNULL_INPUT static void
free_sentence(LIBNORMALFORM_SENTENCE *this)
{
	LIBNORMALFORM_SENTENCE *head = NULL, *a, *b;

	if (--this->refcount)
		return;

	do {
		if (this->atom && !--this->atom->refcount)
			free(this->atom);

		if (IS_BRANCH(this)) {
			a = LEFT(this);
			b = RIGHT(this);
			if (b && !--b->refcount)
				PUSH(&head, b);
		push_a:
			if (a && !--a->refcount)
				PUSH(&head, a);
		} else if (this->type == TYPE_TRANS) {
			a = this->data.trans.input;
			goto push_a;
		}

		free(this);
	} while (POP(&head, &this));
}


/**
 * Recursively deallocate a `LIBNORMALFORM_SENTENCE *`
 * according to `libnormalform_free`, but do not
 * deallocate the pointer itself
 *
 * @param  this  The object to deallocate
 */
NONNULL_INPUT static void
destroy_term(struct libnormalform_term *this)
{
	switch (this->type) {
	case LIBNORMALFORM_DISJUNCTION:
	case LIBNORMALFORM_CONJUNCTION:
	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
		while (this->term.clause.nterms)
			destroy_term(&this->term.clause.terms[--this->term.clause.nterms]);
		free(this->term.clause.terms);
		free(this);
		break;

	case LIBNORMALFORM_TRANSFORMATION:
		free(this->term.transformation.sentence);
		free(this);
		return;

	case LIBNORMALFORM_FOR_ALL:
	case LIBNORMALFORM_NEGATED_FOR_ALL:
	case LIBNORMALFORM_FOR_ANY:
	case LIBNORMALFORM_NEGATED_FOR_ANY:
	case LIBNORMALFORM_FOR_ONE:
	case LIBNORMALFORM_NEGATED_FOR_ONE:
		destroy_term(this->term.qualification.antecedent);
		destroy_term(this->term.qualification.predicate);
		free(this->term.qualification.antecedent);
		free(this->term.qualification.predicate);
		/* fall through */

	case LIBNORMALFORM_VARIABLE:
	case LIBNORMALFORM_NEGATED_VARIABLE:
	case LIBNORMALFORM_FUNCTION:
	case LIBNORMALFORM_NEGATED_FUNCTION:
		free(this);
		break;

	default:
		abort();
	}
}


void
(libnormalform_free)(void *this)
{
	if (!this)
		return;

	if (*(enum libnormalform_term_type *)this >= SENTENCE_TYPE_OFFSET) {
		free_sentence(this);
	} else {
		destroy_term(this);
		free(this);
	}
}


#else


int
main(void)
{
	TEST_BEGIN;

	libnormalform_free(NULL);

	/* Tested in other tests */

	TEST_END;
}


#endif