added parsing of justifications

9 files changed, 101 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 0948a4e..83970cf 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 CFLAGS=-I. -Wall -Wextra -Wpedantic -O3 -lm -Wcast-align 
 CFLAGS+= -Wshadow -Wstrict-prototypes -Wundef -Wpointer-arith 
-CFLAGS+= -Wunreachable-code -Wswitch-enum -Wformat=2 -g
+CFLAGS+= -Wunreachable-code -Wformat=2 -g
 PREFIX ?= /usr
 BINDIR ?= ${PREFIX}/bin
 
diff --git a/lexer.c b/lexer.c
index 5fe9e22..be35d85 100644
--- a/lexer.c
+++ b/lexer.c
@@ -120,6 +120,14 @@ token_t lex_first_token(char** content) {
 			free(s);
 			return init_token(ASSUMPTION, NULL);
 		}
+		else if (strcmp(s, "i") == 0) {
+			free(s);
+			return init_token(INTRODUCTION, NULL);
+		}
+		else if (strcmp(s, "e") == 0) {
+			free(s);
+			return init_token(ELIMINATION, NULL);
+		}
 		else if (strcmp(s, "^") == 0) {
 			free(s);
 			return init_token(CONJUNCTION, NULL);
diff --git a/operetta.c b/operetta.c
index 4c50434..4192ffb 100644
--- a/operetta.c
+++ b/operetta.c
@@ -13,6 +13,8 @@ int main(int argc, char** argv) {
 	lineSet_t lines = parse_lines(content, lineCount);
 	for (int i = 0; i < lines.count; i++) {
 		write_prop(lines.lines[i].proposition);
+		printf(" BECAUSE: ");
+		write_just(lines.lines[i].justification);
 		printf("\n");
 	}
 	free(content);
@@ -29,6 +31,12 @@ void write_prop(prop_t prop) {
 		printf(")");
 	}
 }
+void write_just(just_t just) {
+	printf("%s", jrtos(just.rule));
+	for (int i = 0; i < just.referencesCount; i++) {
+		printf(" %d", just.references[i]);
+	}
+}
 char* read_file(char* path) {
 	FILE* file = fopen(path, "r");
 	if (file == NULL) {
diff --git a/operetta.h b/operetta.h
index 17a0251..6d348ed 100644
--- a/operetta.h
+++ b/operetta.h
@@ -4,5 +4,6 @@
 #include "proposition.h"
 void write_line(line_t line);
 void write_prop(prop_t prop);
+void write_just(just_t just);
 char* read_file(char* path);
 #endif
diff --git a/parse.c b/parse.c
index ad839fc..d7ec467 100644
--- a/parse.c
+++ b/parse.c
@@ -45,7 +45,7 @@ line_t parse_line(char* content) {
 	}
 	int* seek = calloc(sizeof(int), 1);
 	prop_t prop = parse_proposition(init_tokenset(ts.tokens, i), seek);
-	just_t just;
+	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) {
@@ -73,3 +73,35 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek) {
 		return metaProp;
 	}
 }
+just_t parse_justification(tokenSet_t tokenSet) {
+	/* premise and assumption require no arguments */
+	if (tokenSet.tokens[0].type == PREMISE || tokenSet.tokens[0].type == ASSUMPTION) {
+		return init_just(tokenSet.tokens[0].type == PREMISE ? PREMISE_R : ASSUMPTION_R, NULL, 0);
+	}
+	justRule_t just;
+	int* references = malloc(sizeof(int) * (tokenSet.count - 2));
+	switch (tokenSet.tokens[0].type) {
+		case CONJUNCTION:
+			just = tokenSet.tokens[1].type == ELIMINATION ? CONJUNCT_ELIM : CONJUNCT_INTRO;
+			break;
+		case DISJUNCTION:
+			just = tokenSet.tokens[1].type == ELIMINATION ? DISJUNCT_ELIM : DISJUNCT_INTRO;
+			break;
+		case IMPLICATION:
+			just = tokenSet.tokens[1].type == ELIMINATION ? IMPLICATION_ELIM : IMPLICATION_INTRO;
+			break;
+		default:
+			return init_just(ERR_R, NULL, 0); 
+	}
+	/* find the arguments */
+	int i;
+	for (i = 0; i < tokenSet.count - 2; i++) {
+		if (tokenSet.tokens[i + 2].type == INT) {
+			references[i] = *((int*)tokenSet.tokens[i + 2].value);
+		}
+		else {
+			return init_just(ERR_R, NULL, 0);
+		}
+	}
+	return init_just(just, references, i);
+}
diff --git a/parse.h b/parse.h
index 3fb0a3b..2bb49fa 100644
--- a/parse.h
+++ b/parse.h
@@ -14,5 +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* tokensRead);
+prop_t parse_proposition(tokenSet_t tokenSet, int* seek);
+just_t parse_justification(tokenSet_t tokenSet);
 #endif
diff --git a/proposition.c b/proposition.c
index 0919aa8..76ae4cd 100644
--- a/proposition.c
+++ b/proposition.c
@@ -12,3 +12,32 @@ prop_t init_simple_prop(char* name) {
 	prop.isSimple = 1;
 	return prop;
 }
+char* jrtos(justRule_t rule) {
+	switch (rule) {
+		case PREMISE_R:
+			return "PREMISE";
+		case ASSUMPTION_R:
+			return "ASSUMPTION";
+		case CONJUNCT_INTRO:
+			return "CONJUNCTION INTRODUCTION";
+		case DISJUNCT_INTRO:
+			return "DISJUNCTION INTRODUCTION";
+		case IMPLICATION_INTRO:
+			return "IMPLICATION INTRODUCTION";
+		case CONJUNCT_ELIM:
+			return "CONJUNCTION ELIMINATION";
+		case DISJUNCT_ELIM:
+			return "DISJUNCTION ELIMINATION";
+		case IMPLICATION_ELIM:
+			return "IMPLICATION ELIMINATION";
+		default:
+			return "ERR";
+	}
+}
+just_t init_just(justRule_t rule, int* references, int referencesCount) {
+	just_t just;
+	just.rule = rule;
+	just.references = references;
+	just.referencesCount = referencesCount;
+	return just;
+}
diff --git a/proposition.h b/proposition.h
index d2f5ac6..95f377c 100644
--- a/proposition.h
+++ b/proposition.h
@@ -10,7 +10,24 @@ typedef struct Proposition {
 } prop_t;
 prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation);
 prop_t init_simple_prop(char* name);
+typedef enum JustificationRule {
+	ERR_R,
+	PREMISE_R,
+	ASSUMPTION_R,
+	CONJUNCT_INTRO,
+	DISJUNCT_INTRO,
+	IMPLICATION_INTRO,
+	BI_IMPLICATION_INTRO,
+	CONJUNCT_ELIM,
+	DISJUNCT_ELIM,
+	IMPLICATION_ELIM,
+	BI_IMPLICATION_ELIM
+} justRule_t;
+char* jrtos(justRule_t rule);
 typedef struct Justification {
-	tokenType_t rule;
+	justRule_t rule;
+	int* references;
+	int referencesCount;
 } just_t;
+just_t init_just(justRule_t rule, int* references, int referencesCount);
 #endif
diff --git a/testfile b/testfile
index 47019a4..b4fca7c 100644
--- a/testfile
+++ b/testfile
@@ -1,3 +1,3 @@
 QvP | pr
 KAI^PRESTON | as
-CATv(DOG^RABBIT) | pr
+CATv(DOG^RABBIT) | ^e 1 2