added parsing of justifications

1 files changed, 33 insertions, 1 deletions

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);
+}