#include <stdlib.h>
#include "eval.h"
#include "stdio.h"
#include "parse.h"
/* TODO: separate cases into functions */
char just_is_sound(line_t line, lineSet_t lines) {
	prop_t prop = line.proposition;
	just_t just = line.justification;
	prop_t a, b, w, x, y, z;
	line_t wl, xl, yl, zl;
	switch (just.rule) {
		case PREMISE_R:
			return 1;
		case ASSUMPTION_R:
			return 1;
		case CONJUNCT_INTRO:
			a = *prop.propA;
			b = *prop.propB;
			wl = lines.lines[just.references[0] - 1];
			xl = lines.lines[just.references[1] - 1];
			w = wl.proposition;
			x = xl.proposition;
			/* the references are in a deeper scope than the justification */
			if (!seqlt(line.scope, wl.scope) || !seqlt(line.scope, xl.scope)) {
				return 0;
			}
			return (peq(a, w) && peq(b, x)) || (peq(a, x) && peq(b, w));
		case DISJUNCT_INTRO:
			a = *prop.propA;
			b = *prop.propB;
			wl = lines.lines[just.references[0] - 1];
			w = wl.proposition;
			if (!seqlt(line.scope, wl.scope)) {
				return 0;
			}
			return peq(a, w) || peq(b, w);
		case IMPLICATION_INTRO:
			a = *prop.propA;
			b = *prop.propB;
			wl = lines.lines[just.references[0] - 1];
			xl = lines.lines[just.references[1] - 1];
			line_t as;
			line_t res;
			/* find the positions of the arguments */
			if (peq(a, wl.proposition) && peq(b, xl.proposition)) {
				as = wl;
				res = xl;
			}
			else if (peq(a, xl.proposition) && peq(b, wl.proposition)) {
				as = xl;
				res = wl;
			}
			else {
				return 0;
			}
			/* ensure that the arguments are in the correct scope */
			return as.scope.id == res.scope.id && as.scope.depth == line.scope.depth + 1;
		case CONJUNCT_ELIM:
			wl = lines.lines[just.references[0] - 1];
			w = wl.proposition;
			if (!seqlt(line.scope, wl.scope)) {
				return 0;
			}
			return peq(prop, *w.propA) || peq(prop, *w.propB);
		case IMPLICATION_ELIM:
			wl = lines.lines[just.references[0] - 1];
			xl = lines.lines[just.references[1] - 1];
			w = wl.proposition;
			x = xl.proposition;
			if (!seqlt(line.scope, wl.scope) || !seqlt(line.scope, xl.scope)) {
				return 0;
			}
			/* find the positions of the arguments */
			if (!w.isSimple && peq(prop, *w.propB) && w.relation == IMPLICATION && peq(x, *w.propA)) {
				return 1;
			}
			else if (!x.isSimple && peq(prop, *x.propB) && x.relation == IMPLICATION && peq(w, *x.propA)) {
				return 1;
			}
			else {
				return 0;
			}
		default:
			return 0;
	}
}