added contradiction introduction rule

7 files changed, 94 insertions, 5 deletions

diff --git a/src/console.c b/src/console.c
index 8d0cebb..221dfcd 100644
--- a/src/console.c
+++ b/src/console.c
@@ -89,6 +89,5 @@ void interact_selected() {
 	else {
 		lineCache.lines[selected].onInteract();
 	}
-	clear_screen();
 	draw_screen();
 }
diff --git a/src/eval.c b/src/eval.c
index 0c5d1db..26d1629 100644
--- a/src/eval.c
+++ b/src/eval.c
@@ -55,6 +55,24 @@ char just_is_sound(line_t line, lineSet_t lines) {
 			}
 			/* ensure that the arguments are in the correct scope */
 			return as.scope.id == res.scope.id && as.scope.depth == line.scope.depth + 1;
+		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;
 		case CONJUNCT_ELIM:
 			wl = lines.lines[just.references[0] - 1];
 			w = wl.proposition;
diff --git a/src/operetta.c b/src/operetta.c
index 7e257f0..9b7fea3 100644
--- a/src/operetta.c
+++ b/src/operetta.c
@@ -28,7 +28,8 @@ int main(int argc, char** argv) {
 		s[0] = '\0';
 		char* propString = write_prop(line.proposition);
 		char* justString = write_just(line.justification);
-		snprintf(s, 100, "%d. %s BECAUSE: %s", i + 1, propString, justString);
+		char isValid = just_is_sound(line, lines);
+		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);
@@ -48,6 +49,12 @@ int main(int argc, char** argv) {
 	free(content);
 }
 char* write_prop(prop_t prop) {
+	if (prop.isContradiction) {
+		char* s = tttos(CONTRADICTION);
+		char* sp = malloc(sizeof(char) * strlen(s) + 1);
+		strcpy(sp, s);
+		return sp;
+	}
 	char* out = calloc(sizeof(char), 100);
 	out[0] = '\0';
 	if (prop.isNegative) {
@@ -69,7 +76,7 @@ char* write_prop(prop_t prop) {
 		free(c2);
 		strcat(out, ")");
 	}
-	return out;
+	return realloc(out, sizeof(char) * strlen(out) + 1);
 }
 char* write_just(just_t just) {
 	char* out = calloc(sizeof(char), 50);
@@ -81,7 +88,7 @@ char* write_just(just_t just) {
 		strcat(out, n);
 		free(n);
 	}
-	return out;
+	return realloc(out, sizeof(char) * strlen(out) + 1);
 }
 char* read_file(char* path) {
 	FILE* file = fopen(path, "r");
diff --git a/src/parse.c b/src/parse.c
index cae66a0..fedd3ab 100644
--- a/src/parse.c
+++ b/src/parse.c
@@ -102,6 +102,9 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative) {
 		(*seek)++;
 		prop = parse_proposition(tokenSet, seek, 1);
 	}
+	else if (tokenSet.tokens[*seek].type == CONTRADICTION) {
+		return init_contradiction_prop();
+	}
 	else {
 		prop = init_simple_prop(isNegative, tokenSet.tokens[*seek].value);
 		(*seek)++;
@@ -141,6 +144,12 @@ just_t parse_justification(tokenSet_t tokenSet) {
 		case IMPLICATION:
 			just = tokenSet.tokens[1].type == ELIMINATION ? IMPLICATION_ELIM : IMPLICATION_INTRO;
 			break;
+		case NEGATION:
+			just = tokenSet.tokens[1].type == ELIMINATION ? NEGATION_ELIM : NEGATION_INTRO;
+			break;
+		case CONTRADICTION:
+			just = tokenSet.tokens[1].type == ELIMINATION ? ERR_R : CONTRADICTION_INTRO;
+			break;
 		default:
 			return init_just(ERR_R, NULL, 0); 
 	}
@@ -157,6 +166,15 @@ just_t parse_justification(tokenSet_t tokenSet) {
 	return init_just(just, references, i);
 }
 char peq(prop_t prop1, prop_t prop2) {
+	if (prop1.isContradiction && prop2.isContradiction) {
+		/* both are contradictions */
+		return 1;
+	}
+	if (prop1.isContradiction || prop1.isContradiction) {
+		/* only one is a contradiction */
+		return 0;
+	}
+	/* neither are contradictions */
 	if (prop1.isSimple && prop2.isSimple) {
 		/* both simple */
 		return strcmp(prop1.name, prop2.name) == 0 && prop1.isNegative == prop2.isNegative;
@@ -170,6 +188,29 @@ char peq(prop_t prop1, prop_t prop2) {
 		return prop1.isNegative == prop2.isNegative && prop1.relation == prop2.relation && peq(*prop1.propA, *prop2.propA) && peq(*prop1.propB, *prop2.propB);
 	}
 }
+char pbeq(prop_t prop1, prop_t prop2) {
+	if (prop1.isContradiction && prop2.isContradiction) {
+		/* both are contradictions */
+		return 1;
+	}
+	if (prop1.isContradiction || prop1.isContradiction) {
+		/* only one is a contradiction */
+		return 0;
+	}
+	/* neither are contradictions */
+	if (prop1.isSimple && prop2.isSimple) {
+		/* both simple */
+		return strcmp(prop1.name, prop2.name) == 0;
+	}
+	else if (prop1.isSimple || prop2.isSimple) {
+		/* only one simple */
+		return 0;
+	}
+	else {
+		/* neither simple */
+		return prop1.relation == prop2.relation && peq(*prop1.propA, *prop2.propA) && peq(*prop1.propB, *prop2.propB);
+	}
+}
 char slt(scope_t scope1, scope_t scope2) {
 	while (scope1.parent != NULL) {
 		scope1 = *scope1.parent;
diff --git a/src/parse.h b/src/parse.h
index c6e76ec..4282ead 100644
--- a/src/parse.h
+++ b/src/parse.h
@@ -25,6 +25,8 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative);
 just_t parse_justification(tokenSet_t tokenSet);
 /* proposition equal */
 char peq(prop_t prop1, prop_t prop2);
+/* proposition equal, disregarding negation */
+char pbeq(prop_t prop1, prop_t prop2);
 /* scope is lesser than in depth and ID */
 char slt(scope_t scope1, scope_t scope2);
 /* scope is equal to or lesser than in depth and ID */
diff --git a/src/proposition.c b/src/proposition.c
index 6f28fbe..4d4b473 100644
--- a/src/proposition.c
+++ b/src/proposition.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 #include "proposition.h"
 /* a proposition defines a relation between two propositions */
 prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation) {
@@ -7,6 +8,7 @@ prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t rela
 	prop.propB = propB;
 	prop.relation = relation;
 	prop.isSimple = 0;
+	prop.isContradiction = 0;
 	return prop;
 }
 /* a simple proposition is one with only a name */
@@ -15,6 +17,15 @@ prop_t init_simple_prop(char isNegative, char* name) {
 	prop.isNegative = isNegative;
 	prop.name = name;
 	prop.isSimple = 1;
+	prop.isContradiction = 0;
+	return prop;
+}
+prop_t init_contradiction_prop() {
+	prop_t prop;
+	prop.isNegative = 0;
+	prop.name = NULL;
+	prop.isSimple = 1;
+	prop.isContradiction = 1;
 	return prop;
 }
 char* jrtos(justRule_t rule) {
@@ -29,12 +40,18 @@ char* jrtos(justRule_t rule) {
 			return "DISJUNCTION INTRODUCTION";
 		case IMPLICATION_INTRO:
 			return "IMPLICATION INTRODUCTION";
+		case NEGATION_INTRO:
+			return "NEGATION INTRODUCTION";
+		case CONTRADICTION_INTRO:
+			return "CONTRADICTION INTRODUCTION";
 		case CONJUNCT_ELIM:
 			return "CONJUNCTION ELIMINATION";
 		case DISJUNCT_ELIM:
 			return "DISJUNCTION ELIMINATION";
 		case IMPLICATION_ELIM:
 			return "IMPLICATION ELIMINATION";
+		case NEGATION_ELIM:
+			return "NEGATION ELIMINATION";
 		default:
 			return "ERR";
 	}
diff --git a/src/proposition.h b/src/proposition.h
index 2d09688..09509ea 100644
--- a/src/proposition.h
+++ b/src/proposition.h
@@ -4,6 +4,7 @@
 typedef struct Proposition {
 	char isSimple;
 	char isNegative;
+	char isContradiction;
 	struct Proposition* propA;
 	struct Proposition* propB;
 	tokenType_t relation;
@@ -11,6 +12,7 @@ typedef struct Proposition {
 } prop_t;
 prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation);
 prop_t init_simple_prop(char isNegative, char* name);
+prop_t init_contradiction_prop(void);
 typedef enum JustificationRule {
 	ERR_R,
 	PREMISE_R,
@@ -19,10 +21,13 @@ typedef enum JustificationRule {
 	DISJUNCT_INTRO,
 	IMPLICATION_INTRO,
 	BI_IMPLICATION_INTRO,
+	NEGATION_INTRO,
+	CONTRADICTION_INTRO,
 	CONJUNCT_ELIM,
 	DISJUNCT_ELIM,
 	IMPLICATION_ELIM,
-	BI_IMPLICATION_ELIM
+	BI_IMPLICATION_ELIM,
+	NEGATION_ELIM
 } justRule_t;
 char* jrtos(justRule_t rule);
 typedef struct Justification {