From 3bd120957d570756d396db8a112113f2ffb8f33b Mon Sep 17 00:00:00 2001
From: Kai Stevenson <kai@kaistevenson.com>
Date: Tue, 13 Jun 2023 00:56:14 -0700
Subject: added negation

---
 lexer.c       | 10 ++++++++++
 lexer.h       |  1 +
 operetta.c    |  3 +++
 parse.c       | 16 ++++++++++------
 parse.h       |  2 +-
 proposition.c |  6 ++++--
 proposition.h |  7 ++++---
 testfile      |  4 ++--
 8 files changed, 35 insertions(+), 14 deletions(-)

diff --git a/lexer.c b/lexer.c
index be35d85..5df1103 100644
--- a/lexer.c
+++ b/lexer.c
@@ -35,12 +35,18 @@ char* tttos(tokenType_t tokenType) {
 			return "JUSTIFICATION";
 		case PREMISE:
 			return "PREMISE";
+		case NEGATION:
+			return "NEGATION";
 		case ASSUMPTION:
 			return "ASSUMPTION";
 		case CONJUNCTION:
 			return "CONJUNCTION";
 		case DISJUNCTION:
 			return "DISJUNCTION";
+		case IMPLICATION:
+			return "IMPLICATION";
+		case BI_IMPLICATION:
+			return "BI_IMPLICATION";
 		default:
 			return "???";
 	}
@@ -128,6 +134,10 @@ token_t lex_first_token(char** content) {
 			free(s);
 			return init_token(ELIMINATION, NULL);
 		}
+		else if (strcmp(s, "~") == 0) {
+			free(s);
+			return init_token(NEGATION, NULL);
+		}
 		else if (strcmp(s, "^") == 0) {
 			free(s);
 			return init_token(CONJUNCTION, NULL);
diff --git a/lexer.h b/lexer.h
index 7f4cfd0..ff7ab85 100644
--- a/lexer.h
+++ b/lexer.h
@@ -11,6 +11,7 @@ typedef enum TokenType {
 	JUSTIFICATION,
 	PREMISE,
 	ASSUMPTION,
+	NEGATION,
 	CONJUNCTION,
 	DISJUNCTION,
 	IMPLICATION,
diff --git a/operetta.c b/operetta.c
index 4192ffb..f399093 100644
--- a/operetta.c
+++ b/operetta.c
@@ -20,6 +20,9 @@ int main(int argc, char** argv) {
 	free(content);
 }
 void write_prop(prop_t prop) {
+	if (prop.isNegative) {
+		printf("%s", "!");
+	}
 	if (prop.isSimple) {
 		printf("%s", prop.name);
 	}
diff --git a/parse.c b/parse.c
index d26cfe8..6bea4af 100644
--- a/parse.c
+++ b/parse.c
@@ -44,19 +44,23 @@ line_t parse_line(char* content) {
 		i++;
 	}
 	int* seek = calloc(sizeof(int), 1);
-	prop_t prop = parse_proposition(init_tokenset(ts.tokens, i), seek);
+	prop_t prop = parse_proposition(init_tokenset(ts.tokens, i), seek, 0);
 	just_t just = parse_justification(init_tokenset(ts.tokens + i + 1, ts.count - (i + 1)));
 	return init_line(prop, just);
 }
-prop_t parse_proposition(tokenSet_t tokenSet, int* seek) {
+prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative) {
 	prop_t prop;
 	/* recurse to parse the parenthetical as its own proposition */
 	if (tokenSet.tokens[*seek].type == OPEN_PAREN) {
 		(*seek)++;
-		prop = parse_proposition(tokenSet, seek);
+		prop = parse_proposition(tokenSet, seek, 0);
+	}
+	else if (tokenSet.tokens[*seek].type == NEGATION) {
+		(*seek)++;
+		prop = parse_proposition(tokenSet, seek, 1);
 	}
 	else {
-		prop = init_simple_prop(tokenSet.tokens[*seek].value);
+		prop = init_simple_prop(isNegative, tokenSet.tokens[*seek].value);
 		(*seek)++;
 	}
 	/* check if we were reading a simple prop, or if there is a relation */
@@ -70,8 +74,8 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek) {
 		prop_t* prop1p = malloc(sizeof(prop_t));
 		*prop1p = prop;
 		prop_t* prop2p = malloc(sizeof(prop_t));
-		*prop2p = parse_proposition(tokenSet, seek);
-		prop_t metaProp = init_prop(prop1p, prop2p, rel);
+		*prop2p = parse_proposition(tokenSet, seek, 0);
+		prop_t metaProp = init_prop(0, prop1p, prop2p, rel);
 		return metaProp;
 	}
 }
diff --git a/parse.h b/parse.h
index 2bb49fa..80f92e2 100644
--- a/parse.h
+++ b/parse.h
@@ -14,6 +14,6 @@ lineSet_t init_lineset(line_t* lines, int count);
 int count_lines(char* content);
 lineSet_t parse_lines(char* content, int lineCount);
 line_t parse_line(char* content);
-prop_t parse_proposition(tokenSet_t tokenSet, int* seek);
+prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative);
 just_t parse_justification(tokenSet_t tokenSet);
 #endif
diff --git a/proposition.c b/proposition.c
index 2c1410c..c3fc897 100644
--- a/proposition.c
+++ b/proposition.c
@@ -1,15 +1,17 @@
 #include "proposition.h"
 /* a proposition defines a relation between two propositions */
-prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation) {
+prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation) {
 	prop_t prop;
+	prop.isNegative = isNegative;
 	prop.propA = propA;
 	prop.propB = propB;
 	prop.relation = relation;
 	return prop;
 }
 /* a simple proposition is one with only a name */
-prop_t init_simple_prop(char* name) {
+prop_t init_simple_prop(char isNegative, char* name) {
 	prop_t prop;
+	prop.isNegative = isNegative;
 	prop.name = name;
 	prop.isSimple = 1;
 	return prop;
diff --git a/proposition.h b/proposition.h
index 95f377c..2d09688 100644
--- a/proposition.h
+++ b/proposition.h
@@ -2,14 +2,15 @@
 #define PROPOSITION
 #include "lexer.h"
 typedef struct Proposition {
+	char isSimple;
+	char isNegative;
 	struct Proposition* propA;
 	struct Proposition* propB;
 	tokenType_t relation;
 	char* name;
-	char isSimple;
 } prop_t;
-prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation);
-prop_t init_simple_prop(char* name);
+prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation);
+prop_t init_simple_prop(char isNegative, char* name);
 typedef enum JustificationRule {
 	ERR_R,
 	PREMISE_R,
diff --git a/testfile b/testfile
index b4fca7c..af46bfb 100644
--- a/testfile
+++ b/testfile
@@ -1,3 +1,3 @@
-QvP | pr
+Q | pr
 KAI^PRESTON | as
-CATv(DOG^RABBIT) | ^e 1 2
+~CAT->(DOG^~RABBIT) | ^e 1 2
-- 
cgit v1.3.1