added scoping; probably doesn't work

1 files changed, 24 insertions, 22 deletions

diff --git a/eval.c b/eval.c
index 02b85f1..225c45e 100644
--- a/eval.c
+++ b/eval.c
@@ -1,36 +1,38 @@
 #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;
-	prop_t b;
-	if (!prop.isSimple) {
-		a = *prop.propA;
-		b = *prop.propB;
-	}
-	prop_t w;
-	prop_t x;
-	prop_t y;
-	prop_t z;
-	if (just.referencesCount > 0) {
-		w = lines.lines[just.references[0] - 1].proposition;
-	}
-	if (just.referencesCount > 1) {
-		x = lines.lines[just.references[1] - 1].proposition;
-	}
-	if (just.referencesCount > 2) {
-		y = lines.lines[just.references[2] - 1].proposition;
-	}
-	if (just.referencesCount > 3) {
-		z = lines.lines[just.references[3] - 1].proposition;
-	}
+	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;
 	}