separated switch case into functions, added negation intro rule

3 files changed, 147 insertions, 85 deletions

diff --git a/src/eval.c b/src/eval.c
index 26d1629..4af7153 100644
--- a/src/eval.c
+++ b/src/eval.c
@@ -2,102 +2,152 @@
 #include "eval.h"
 #include "stdio.h"
 #include "parse.h"
-/* TODO: separate cases into functions */
-char just_is_sound(line_t line, lineSet_t lines) {
+/* 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;
-	prop_t a, b, w, x, y, z;
-	line_t wl, xl, yl, zl;
+	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:
-			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));
+			return conjunct_intro_is_sound(line, ref1, ref2);
 		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);
+			return disjunct_intro_is_sound(line, ref1);
 		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;
+			return implication_intro_is_sound(line, ref1, ref2);
 		case CONTRADICTION_INTRO:
-			if (!prop.isContradiction) {
-				return 0;
-			}
-			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;
-			}
-			if (!pbeq(w, x) ) {
-				return 0;
-			}
-			if (w.isNegative == x.isNegative) {
-				return 0;
-			}
-			return 1;
+			return contradiction_intro_is_sound(line, ref1, ref2);
+		case NEGATION_INTRO:
+			return negation_intro_is_sound(line, ref1, ref2);
 		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);
+			return conjunct_elim_is_sound(line, ref1);
 		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;
-			}
+			return implication_elim_is_sound(line, ref1, ref2);
 		default:
 			return 0;
 	}
diff --git a/src/lexer.c b/src/lexer.c
index 45a6f79..906af85 100644
--- a/src/lexer.c
+++ b/src/lexer.c
@@ -142,7 +142,7 @@ token_t lex_first_token(char** content) {
 			free(s);
 			return init_token(ELIMINATION, NULL);
 		}
-		else if (strcmp(s, "~") == 0) {
+		else if (strcmp(s, "~") == 0 || strcmp(s, "!") == 0) {
 			free(s);
 			return init_token(NEGATION, NULL);
 		}
diff --git a/src/operetta.c b/src/operetta.c
index 9b7fea3..ae9a418 100644
--- a/src/operetta.c
+++ b/src/operetta.c
@@ -32,7 +32,19 @@ int main(int argc, char** argv) {
 		snprintf(s, 100, "%d. %s BECAUSE: %s <%s>", i + 1, propString, justString, isValid ? "SOUND" : "UNSOUND");
 		free(propString);
 		free(justString);
-		consoleLines[i] = init_simple_consoleline(CWHITE, s);
+		int indent = lines.lines[i].scope.depth;
+		if (indent > 0) {
+			char* si = malloc(sizeof(char) * (indent + strlen(s) + 1));
+			for (int j = 0; j < indent; j++) {
+				si[j] = '	';
+			}
+			si[indent] = '\0';
+			strcat(si, s);
+			consoleLines[i] = init_simple_consoleline(CWHITE, si);
+		}
+		else {
+			consoleLines[i] = init_simple_consoleline(CWHITE, s);
+		}
 	}
 	set_cache(init_consolelineset(consoleLines, lines.count));
 	/* enter main loop */