#include <stdlib.h>
#include "eval.h"
#include "stdio.h"
#include "parse.h"
char just_is_sound(prop_t prop, just_t just, lineSet_t lines) {
	prop_t a, b, w, x, y, z;
	switch (just.rule) {
		case PREMISE_R:
			return 1;
		case ASSUMPTION_R:
			return 1;
		case CONJUNCT_INTRO:
			a = *prop.propA;
			b = *prop.propB;
			w = lines.lines[just.references[0] - 1].proposition;
			x = lines.lines[just.references[1] - 1].proposition;
			return (peq(a, w) && peq(b, x)) || (peq(a, x) && peq(b, w));
		case DISJUNCT_INTRO:
			a = *prop.propA;
			b = *prop.propB;
			w = lines.lines[just.references[0] - 1].proposition;
			return peq(a, w) || peq(b, w);
		case IMPLICATION_INTRO:
			a = *prop.propA;
			b = *prop.propB;
			w = lines.lines[just.references[0] - 1].proposition;
			x = lines.lines[just.references[1] - 1].proposition;
			if ((peq(a, w) && peq(b, x)) || (peq(a, x) && peq(b, w))) {
				return 1;
			}
			return 0;
			
		case CONJUNCT_ELIM:
			w = lines.lines[just.references[0] - 1].proposition;
			return peq(prop, *w.propA) || peq(prop, *w.propB);
		default:
			return 0;
	}
}