restructured project

1 files changed, 184 insertions, 0 deletions

diff --git a/src/parse.c b/src/parse.c
new file mode 100644
index 0000000..830f9c5
--- /dev/null
+++ b/src/parse.c
@@ -0,0 +1,184 @@
+#include <stdlib.h>
+#include <string.h>
+#include "parse.h"
+#include "lexer.h"
+#include "stdio.h"
+
+scope_t lastScope;
+int scopes;
+
+scope_t init_scope(int id, int depth, scope_t* parent) {
+	scope_t scope;
+	scope.id = id;
+	scope.depth = depth;
+	scope.parent = parent;
+	return scope;
+}
+line_t init_line(scope_t scope, prop_t proposition, just_t justification) {
+	line_t line;
+	line.scope = scope;
+	line.proposition = proposition;
+	line.justification = justification;
+	return line;
+}
+lineSet_t init_lineset(line_t* lines, int count) {
+	lineSet_t lineSet;
+	lineSet.lines = lines;
+	lineSet.count = count;
+	return lineSet;
+}
+int count_lines(char* content) {
+	int i = 0;
+	while (*content != '\0') {
+		if (*content == '\n') {
+			i++;
+		}
+		content++;
+	}
+	return i;
+}
+lineSet_t parse_lines(char* content, int lineCount) {
+	line_t* lines = malloc(sizeof(line_t) * lineCount);
+	for (int i = 0; i < lineCount; i++) {
+		/* parse the line */
+		lines[i] = parse_line(content);
+		/* advance to the next line */
+		while (*content != '\n') {
+			content++;
+		}
+		content++;
+	}
+	return init_lineset(lines, lineCount);
+}
+line_t parse_line(char* content) {
+	tokenSet_t ts = lex_line(content);
+	int c = 0;
+	int indent = 0;
+	char isNewIndent = 0;
+	while (ts.tokens[c].type != JUSTIFICATION) {
+		if (ts.tokens[c].type == INDENT) {
+			indent++;
+		}
+		c++;
+	}
+	/* determine the ID of the scope we are working on */
+	scope_t thisScope;
+	if (indent > lastScope.depth) {
+		scopes++;
+		scope_t* lsp = malloc(sizeof(scope_t));
+		*lsp = lastScope;
+		thisScope = init_scope(scopes, indent, lsp);
+		isNewIndent = 1;
+	}
+	else if (indent < lastScope.depth) {
+		scope_t li = lastScope;
+		for (int i = 0; i < lastScope.depth - indent; i++) {
+			li = *li.parent;
+		}
+		thisScope = li;
+	}
+	else {
+		thisScope = lastScope;
+	}
+	lastScope = thisScope;
+	/* find the proposition and justification */
+	int* seek = calloc(sizeof(int), 1);
+	prop_t prop = parse_proposition(init_tokenset(ts.tokens + indent, c - indent), seek, 0);
+	just_t just = parse_justification(init_tokenset(ts.tokens + c + 1, ts.count - (c + 1)));
+	free(seek);
+	if ((just.rule != ASSUMPTION_R && isNewIndent) || (just.rule == ASSUMPTION_R && !isNewIndent)) {
+			just.rule = ERR_R;
+	}
+	return init_line(thisScope, prop, just);
+}
+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, 0);
+	}
+	else if (tokenSet.tokens[*seek].type == NEGATION) {
+		(*seek)++;
+		prop = parse_proposition(tokenSet, seek, 1);
+	}
+	else {
+		prop = init_simple_prop(isNegative, tokenSet.tokens[*seek].value);
+		(*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) {
+		(*seek)++;
+		return prop;
+	}
+	else {
+		/* the proposition we just read had a relation, so find the related proposition */
+		tokenType_t rel = tokenSet.tokens[*seek].type;
+		(*seek)++;
+		prop_t* prop1p = malloc(sizeof(prop_t));
+		*prop1p = prop;
+		prop_t* prop2p = malloc(sizeof(prop_t));
+		*prop2p = parse_proposition(tokenSet, seek, 0);
+		prop_t metaProp = init_prop(0, prop1p, prop2p, rel);
+		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));
+	/* check the relation, then use a ternary operator for elim/intro */
+	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);
+}
+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);
+	}
+}
+char slt(scope_t scope1, scope_t scope2) {
+	while (scope1.parent != NULL) {
+		scope1 = *scope1.parent;
+		if (scope1.id == scope2.id) {
+			return 1;
+		}
+	}
+	return 0;
+}
+char seqlt(scope_t scope1, scope_t scope2) {
+	return scope1.id == scope2.id || slt(scope1, scope2);
+}