#include <stdlib.h>
#include "eval.h"
#include "stdio.h"
#include "parse.h"
/* TODO: error reporting */
char conjunct_intro_is_sound(line_t line, line_t ref1, line_t ref2) {
	prop_t prop = line.proposition;
	prop_t a = *prop.propA;
	prop_t b = *prop.propB;
	prop_t r1p = ref1.proposition;
	prop_t r2p = ref2.proposition;
	/* the references are in a deeper scope than the justification */
	if (!seqlt(line.scope, ref1.scope) || !seqlt(line.scope, ref2.scope)) {
		return 0;
	}
	return (peq(a, r1p) && peq(b, r2p)) || (peq(a, r2p) && peq(b, r1p));
}
char disjunct_intro_is_sound(line_t line, line_t ref1) {
	prop_t prop = line.proposition;
	prop_t a = *prop.propA;
	prop_t b = *prop.propB;
	prop_t r1p = ref1.proposition;
	if (!seqlt(line.scope, ref1.scope)) {
		return 0;
	}
	return peq(a, r1p) || peq(b, r1p);
}
char implication_intro_is_sound(line_t line, line_t ref1, line_t ref2) {
	prop_t prop = line.proposition;
	prop_t a = *prop.propA;
	prop_t b = *prop.propB;
	prop_t r1p = ref1.proposition;
	prop_t r2p = ref2.proposition;
	line_t as;
	line_t res;
	/* find the positions of the arguments */
	if (peq(a, r1p) && peq(b, r2p)) {
		as = ref1;
		res = ref2;
	}
	else if (peq(a, r2p) && peq(b, r1p)) {
		as = ref2;
		res = ref1;
	}
	else {
		return 0;
	}
	/* ensure that the arguments are in the correct scope */
	if (as.scope.id != res.scope.id || as.scope.depth != line.scope.depth + 1) {
		return 0;
	}
	return 1;
}
char contradiction_intro_is_sound(line_t line, line_t ref1, line_t ref2) {
	prop_t prop = line.proposition;
	if (!prop.isContradiction) {
		return 0;
	}
	prop_t r1p = ref1.proposition;
	prop_t r2p = ref2.proposition;
	if (r1p.isNegative == r2p.isNegative) {
		return 0;
	}
	if (!seqlt(line.scope, ref1.scope) || !seqlt(line.scope, ref2.scope)) {
		return 0;
	}
	if (!pbeq(r1p, r2p) ) {
		return 0;
	}
	return 1;
}
char negation_intro_is_sound(line_t line, line_t ref1, line_t ref2) {
	prop_t prop = line.proposition;
	if (!prop.isNegative) {
		return 0;
	}
	prop_t r1p = ref1.proposition;
	prop_t r2p = ref2.proposition;
	prop_t as;
	/* TODO: scoping */
	if (r1p.isContradiction) {
		as = r2p;
	}
	else if (r2p.isContradiction) {
		as = r1p;
	}
	else {
		return 0;
	}
	if (!pbeq(as, prop) || as.isNegative == prop.isNegative) {
		return 0;
	}
	return 1;
}
char conjunct_elim_is_sound(line_t line, line_t ref1) {
	prop_t prop = line.proposition;
	prop_t r1p = ref1.proposition;
	if (!seqlt(line.scope, ref1.scope)) {
		return 0;
	}
	return peq(prop, *r1p.propA) || peq(prop, *r1p.propB);
}
char implication_elim_is_sound(line_t line, line_t ref1, line_t ref2) {
	prop_t prop = line.proposition;
	prop_t r1p = ref1.proposition;
	prop_t r2p = ref2.proposition;
	if (!seqlt(line.scope, ref1.scope) || !seqlt(line.scope, ref2.scope)) {
		return 0;
	}
	if (!r1p.isSimple && peq(prop, *r1p.propB) && r1p.relation == IMPLICATION && peq(r2p, *r1p.propA)) {
		return 1;
	}
	else if (!r2p.isSimple && peq(prop, *r2p.propB) && r2p.relation == IMPLICATION && peq(r1p, *r2p.propA)) {
		return 1;
	}
	else {
		return 0;
	}
}
char just_is_sound(line_t line, lineSet_t lines) {
	just_t just = line.justification;
	line_t ref1, ref2, ref3;
	if (just.referencesCount > 0) {
		ref1 = lines.lines[just.references[0] - 1];
		if (just.referencesCount > 1) {
			ref2 = lines.lines[just.references[1] - 1];
			if (just.referencesCount > 2) {
				ref3 = lines.lines[just.references[2] - 1];
			}
		}
	}
	switch (just.rule) {
		case PREMISE_R:
			return 1;
		case ASSUMPTION_R:
			return 1;
		case CONJUNCT_INTRO:
			return conjunct_intro_is_sound(line, ref1, ref2);
		case DISJUNCT_INTRO:
			return disjunct_intro_is_sound(line, ref1);
		case IMPLICATION_INTRO:
			return implication_intro_is_sound(line, ref1, ref2);
		case CONTRADICTION_INTRO:
			return contradiction_intro_is_sound(line, ref1, ref2);
		case NEGATION_INTRO:
			return negation_intro_is_sound(line, ref1, ref2);
		case CONJUNCT_ELIM:
			return conjunct_elim_is_sound(line, ref1);
		case IMPLICATION_ELIM:
			return implication_elim_is_sound(line, ref1, ref2);
		default:
			return 0;
	}
}