From 2f7ac38cca2ebab41b8adb76b69e0949eeae488d Mon Sep 17 00:00:00 2001
From: Kai Stevenson <kai@kaistevenson.com>
Date: Tue, 13 Jun 2023 01:59:43 -0700
Subject: fixed bugs, just_is_sound works for conjunct intro

---
 Makefile   |  2 +-
 eval.c     | 37 +++++++++++++++++++++++++++++++++++++
 eval.h     |  6 ++++++
 operetta.c | 10 +++++++---
 parse.c    | 18 +++++++++++++++++-
 parse.h    |  1 +
 testfile2  |  3 +++
 7 files changed, 72 insertions(+), 5 deletions(-)
 create mode 100644 eval.c
 create mode 100644 eval.h
 create mode 100644 testfile2

diff --git a/Makefile b/Makefile
index 83970cf..94251dc 100644
--- a/Makefile
+++ b/Makefile
@@ -5,7 +5,7 @@ PREFIX ?= /usr
 BINDIR ?= ${PREFIX}/bin
 
 generate:
-	$(CC) -o operetta operetta.c proposition.c parse.c lexer.c $(CFLAGS)
+	$(CC) -o operetta operetta.c proposition.c parse.c lexer.c eval.c $(CFLAGS)
 
 install: operetta
 	install operetta ${DESTDIR}${BINDIR}
diff --git a/eval.c b/eval.c
new file mode 100644
index 0000000..02b85f1
--- /dev/null
+++ b/eval.c
@@ -0,0 +1,37 @@
+#include <stdlib.h>
+#include "eval.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;
+	}
+	switch (just.rule) {
+		case PREMISE_R:
+			return 1;
+		case ASSUMPTION_R:
+			return 1;
+		case CONJUNCT_INTRO:
+			return (peq(a, w) && peq(b, x)) || (peq(a, x) && peq(b, w));
+		default:
+			return 0;
+	}
+}
diff --git a/eval.h b/eval.h
new file mode 100644
index 0000000..bb994f3
--- /dev/null
+++ b/eval.h
@@ -0,0 +1,6 @@
+#ifndef EVAL
+#define EVAL
+#include "proposition.h"
+#include "parse.h"
+char just_is_sound(prop_t prop, just_t just, lineSet_t lines);
+#endif
diff --git a/operetta.c b/operetta.c
index 2c4f555..c72a979 100644
--- a/operetta.c
+++ b/operetta.c
@@ -4,6 +4,7 @@
 #include "lexer.h"
 #include "parse.h"
 #include "proposition.h"
+#include "eval.h"
 
 int main(int argc, char** argv) {
 	/* read file */
@@ -12,12 +13,15 @@ int main(int argc, char** argv) {
 	int lineCount = count_lines(content);
 	lineSet_t lines = parse_lines(content, lineCount);
 	for (int i = 0; i < lines.count; i++) {
-		for (int j = 0; j < lines.lines[i].aLevel; j++) {
+		line_t line = lines.lines[i];
+		printf("%d. ", i + 1);
+		for (int j = 0; j < line.aLevel; j++) {
 			printf(" > ");
 		}
-		write_prop(lines.lines[i].proposition);
+		write_prop(line.proposition);
 		printf(" BECAUSE: ");
-		write_just(lines.lines[i].justification);
+		write_just(line.justification);
+		printf(just_is_sound(line.proposition, line.justification, lines) ? " <SOUND>" : " <UNSOUND>");
 		printf("\n");
 	}
 	free(content);
diff --git a/parse.c b/parse.c
index 75be330..ca01fc0 100644
--- a/parse.c
+++ b/parse.c
@@ -1,4 +1,5 @@
 #include <stdlib.h>
+#include <string.h>
 #include "parse.h"
 #include "lexer.h"
 #include "stdio.h"
@@ -71,7 +72,8 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative) {
 		(*seek)++;
 	}
 	/* check if we were reading a simple prop, or if there is a relation */
-	if (*seek == tokenSet.count || tokenSet.tokens[*seek].type == CLOSE_PAREN) {
+	if (*seek >= tokenSet.count || tokenSet.tokens[*seek].type == CLOSE_PAREN) {
+		(*seek)++;
 		return prop;
 	}
 	else {
@@ -119,3 +121,17 @@ just_t parse_justification(tokenSet_t tokenSet) {
 	}
 	return init_just(just, references, i);
 }
+char peq(prop_t prop1, prop_t prop2) {
+	if (prop1.isSimple && prop2.isSimple) {
+		/* both simple */
+		return strcmp(prop1.name, prop2.name) == 0 && prop1.isNegative == prop2.isNegative;
+	}
+	else if (prop1.isSimple || prop2.isSimple) {
+		/* only one simple */
+		return 0;
+	}
+	else {
+		/* neither simple */
+		return prop1.isNegative == prop2.isNegative && prop1.relation == prop2.relation && peq(*prop1.propA, *prop2.propA) && peq(*prop1.propB, *prop2.propB);
+	}
+}
diff --git a/parse.h b/parse.h
index 320ca45..67d7160 100644
--- a/parse.h
+++ b/parse.h
@@ -17,4 +17,5 @@ lineSet_t parse_lines(char* content, int lineCount);
 line_t parse_line(char* content);
 prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative);
 just_t parse_justification(tokenSet_t tokenSet);
+char peq(prop_t prop1, prop_t prop2);
 #endif
diff --git a/testfile2 b/testfile2
new file mode 100644
index 0000000..c66aa88
--- /dev/null
+++ b/testfile2
@@ -0,0 +1,3 @@
+P^Q | pr
+L^V | pr
+(P^Q)^(L^V) | ^i 1, 2
-- 
cgit v1.3.1