1 files changed, 59 insertions, 0 deletions
diff --git a/src/eval.c b/src/eval.c
new file mode 100644
index 0000000..9132272
--- /dev/null
+++ b/src/eval.c
@@ -0,0 +1,59 @@
+#include <stdlib.h>
+#include "eval.h"
+#include "stdio.h"
+#include "parse.h"
+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;
+			w = lines.lines[just.references[0] - 1].proposition;
+			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:
+			w = lines.lines[just.references[0] - 1].proposition;
+			return peq(prop, *w.propA) || peq(prop, *w.propB);
+		default:
+			return 0;
+	}
+}