restructured project

10 files changed, 674 insertions, 0 deletions

diff --git a/src/eval.c b/src/eval.c
new file mode 100644
index 0000000..9132272
--- /dev/null
+++ b/src/eval.c
@@ -0,0 +1,59 @@
+#include <stdlib.h>
+#include "eval.h"
+#include "stdio.h"
+#include "parse.h"
+char just_is_sound(line_t line, lineSet_t lines) {
+	prop_t prop = line.proposition;
+	just_t just = line.justification;
+	prop_t a, b, w, x, y, z;
+	line_t wl, xl, yl, zl;
+	switch (just.rule) {
+		case PREMISE_R:
+			return 1;
+		case ASSUMPTION_R:
+			return 1;
+		case CONJUNCT_INTRO:
+			a = *prop.propA;
+			b = *prop.propB;
+			wl = lines.lines[just.references[0] - 1];
+			xl = lines.lines[just.references[1] - 1];
+			w = wl.proposition;
+			x = xl.proposition;
+			/* the references are in a deeper scope than the justification */
+			if (!seqlt(line.scope, wl.scope) || !seqlt(line.scope, xl.scope)) {
+				return 0;
+			}
+			return (peq(a, w) && peq(b, x)) || (peq(a, x) && peq(b, w));
+		case DISJUNCT_INTRO:
+			a = *prop.propA;
+			b = *prop.propB;
+			w = lines.lines[just.references[0] - 1].proposition;
+			return peq(a, w) || peq(b, w);
+		case IMPLICATION_INTRO:
+			a = *prop.propA;
+			b = *prop.propB;
+			wl = lines.lines[just.references[0] - 1];
+			xl = lines.lines[just.references[1] - 1];
+			line_t as;
+			line_t res;
+			/* find the positions of the arguments */
+			if (peq(a, wl.proposition) && peq(b, xl.proposition)) {
+				as = wl;
+				res = xl;
+			}
+			else if (peq(a, xl.proposition) && peq(b, wl.proposition)) {
+				as = xl;
+				res = wl;
+			}
+			else {
+				return 0;
+			}
+			/* ensure that the arguments are in the correct scope */
+			return as.scope.id == res.scope.id && as.scope.depth == line.scope.depth + 1;
+		case CONJUNCT_ELIM:
+			w = lines.lines[just.references[0] - 1].proposition;
+			return peq(prop, *w.propA) || peq(prop, *w.propB);
+		default:
+			return 0;
+	}
+}
diff --git a/src/eval.h b/src/eval.h
new file mode 100644
index 0000000..74e7650
--- /dev/null
+++ b/src/eval.h
@@ -0,0 +1,6 @@
+#ifndef EVAL
+#define EVAL
+#include "proposition.h"
+#include "parse.h"
+char just_is_sound(line_t line, lineSet_t lines);
+#endif
diff --git a/src/lexer.c b/src/lexer.c
new file mode 100644
index 0000000..c6c4ffe
--- /dev/null
+++ b/src/lexer.c
@@ -0,0 +1,198 @@
+#include <stdlib.h>
+#include <string.h>
+#include "lexer.h"
+
+token_t init_token(tokenType_t type, void* value) {
+	token_t t;
+	t.type = type;
+	t.value = value;
+	return t;
+}
+tokenSet_t init_tokenset(token_t* tokens, int count) {
+	tokenSet_t tokenSet;
+	tokenSet.tokens = tokens;
+	tokenSet.count = count;
+	return tokenSet;
+}
+char* tttos(tokenType_t tokenType) {
+	switch (tokenType) {
+		case ERR:
+			return "ERR";
+		case EOL:
+			return "EOL";
+		case INDENT:
+			return "INDENT";
+		case STRING:
+			return "STRING";
+		case INT:
+			return "INT";
+		case OPEN_PAREN:
+			return "OPEN_PAREN";
+		case CLOSE_PAREN:
+			return "CLOSE_PAREN";
+		case START_COMMENT:
+			return "START_COMMENT";
+		case JUSTIFICATION:
+			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 "???";
+	}
+}
+int advance_whitespace(char** linePointer) {
+	int64_t a = (int64_t)linePointer;
+	while (**linePointer == ' ') {
+		(*linePointer)++;
+	}
+	return (int)((int64_t)linePointer - a);
+}
+tokenSet_t lex_line(char* line) {
+	char** p = malloc(sizeof(char*));
+	*p = line;
+	int m = 50;
+	token_t* tokens = malloc(sizeof(token_t) * m);
+	int i = 0;
+	while (1) {
+		token_t t = lex_first_token(p);
+		if (t.type == EOL) {
+			break;
+		}
+		if (t.type == ERR) {
+			exit(1);
+		}
+		tokens[i] = t;
+		i++;
+	}
+	free(p);
+	return init_tokenset(tokens, i);
+}
+token_t lex_first_token(char** content) {
+	int m = 5;
+	char* s = malloc(sizeof(char) * m);
+	int c = 0;
+	advance_whitespace(content);
+	while (**content != '\n') {
+		s[c] = **content;
+		s[c+1] = '\0';
+		(*content)++;
+		/* check if we need to parse a string or an int */
+		if (s[c] >= 65 && s[c] <= 90) {
+			free(s);
+			(*content)--;
+			return lex_first_string(content);
+		}
+		else if (s[c] >= 48 && s[c] <= 57) {
+			free(s);
+			(*content)--;
+			return lex_first_int(content);
+		}
+		/* otherwise, check to see if a symbol has been matched */
+		if (strcmp(s, "(") == 0) {
+			free(s);
+			return init_token(OPEN_PAREN, NULL);
+		}
+		else if (strcmp(s, ")") == 0) {
+			free(s);
+			return init_token(CLOSE_PAREN, NULL);
+		}
+		else if (strcmp(s, "#") == 0) {
+			free(s);
+			return init_token(START_COMMENT, NULL);
+		}
+		else if (strcmp(s, "	") == 0) {
+			free(s);
+			return init_token(INDENT, NULL);
+		}
+		else if (strcmp(s, "|") == 0) {
+			free(s);
+			return init_token(JUSTIFICATION, NULL);
+		}
+		else if (strcmp(s, "pr") == 0) {
+			free(s);
+			return init_token(PREMISE, NULL);
+		}
+		else if (strcmp(s, "as") == 0) {
+			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(NEGATION, NULL);
+		}
+		else if (strcmp(s, "^") == 0) {
+			free(s);
+			return init_token(CONJUNCTION, NULL);
+		}
+		else if (strcmp(s, "v") == 0) {
+			free(s);
+			return init_token(DISJUNCTION, NULL);
+		}
+		else if (strcmp(s, "->") == 0) {
+			free(s);
+			return init_token(IMPLICATION, NULL);
+		}
+		else if (strcmp(s, "<-") == 0) {
+			free(s);
+			return init_token(BI_IMPLICATION, NULL);
+		}
+		else if (c <= m) {
+			c++;
+			continue;
+		}
+		else {
+			free(s);
+			return init_token(ERR, NULL);
+		}
+	}
+	return init_token(EOL, NULL);
+}
+token_t lex_first_string(char** content) {
+	int m = 50;
+	char* s = malloc(sizeof(char) * m);
+	int c = 0;
+	advance_whitespace(content);
+	while (**content >= 65 && **content <= 90) {
+		s[c] = **content;
+		(*content)++;
+		c++;
+	}
+	s[c] = '\0';
+	return init_token(STRING, s);
+}
+token_t lex_first_int(char** content) {
+	int m = 10;
+	char* s = malloc(sizeof(char) * m);
+	int c = 0;
+	advance_whitespace(content);
+	while (**content >= 48 && **content <= 57) {
+		s[c] = **content;
+		(*content)++;
+		c++;
+	}
+	s[c] = '\0';
+	int* ip = malloc(sizeof(int));
+	*ip = atoi(s);
+	free(s);
+	return init_token(INT, (void*)ip);
+}
diff --git a/src/lexer.h b/src/lexer.h
new file mode 100644
index 0000000..e5d64dc
--- /dev/null
+++ b/src/lexer.h
@@ -0,0 +1,40 @@
+#ifndef LEXER
+#define LEXER
+typedef enum TokenType {
+	ERR,
+	EOL,
+	INDENT,
+	STRING,
+	INT,
+	OPEN_PAREN,
+	CLOSE_PAREN,
+	START_COMMENT,
+	JUSTIFICATION,
+	PREMISE,
+	ASSUMPTION,
+	NEGATION,
+	CONJUNCTION,
+	DISJUNCTION,
+	IMPLICATION,
+	BI_IMPLICATION,
+	EXPLOSION,
+	ELIMINATION,
+	INTRODUCTION
+} tokenType_t;
+typedef struct Token {
+	tokenType_t type;
+	void* value;
+} token_t;
+token_t init_token(tokenType_t type, void* value);
+typedef struct TokenSet {
+	token_t* tokens;
+	int count;
+} tokenSet_t;
+tokenSet_t init_tokenset(token_t* tokens, int count);
+char* tttos(tokenType_t tokenType);
+int advance_whitespace(char** linePointer);
+tokenSet_t lex_line(char* line);
+token_t lex_first_token(char** content);
+token_t lex_first_string(char** content);
+token_t lex_first_int(char** content);
+#endif
diff --git a/src/operetta.c b/src/operetta.c
new file mode 100644
index 0000000..f754895
--- /dev/null
+++ b/src/operetta.c
@@ -0,0 +1,64 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "operetta.h"
+#include "lexer.h"
+#include "parse.h"
+#include "proposition.h"
+#include "eval.h"
+
+int main(int argc, char** argv) {
+	/* read file */
+	char* path = argv[1];
+	char* content = read_file(path);
+	int lineCount = count_lines(content);
+	lineSet_t lines = parse_lines(content, lineCount);
+	for (int i = 0; i < lines.count; i++) {
+		line_t line = lines.lines[i];
+		printf("%d. ", i + 1);
+		for (int j = 0; j < line.scope.depth; j++) {
+			printf(" > ");
+		}
+		write_prop(line.proposition);
+		printf(" BECAUSE: ");
+		write_just(line.justification);
+		printf(just_is_sound(line, lines) ? " <SOUND>" : " <UNSOUND>");
+		printf(" [%d]", line.scope.id);
+		printf("\n");
+	}
+	free(content);
+}
+void write_prop(prop_t prop) {
+	if (prop.isNegative) {
+		printf("%s", "!");
+	}
+	if (prop.isSimple) {
+		printf("%s", prop.name);
+	}
+	else {
+		printf("(");
+		write_prop(*(prop.propA));
+		printf(" %s ", tttos(prop.relation));
+		write_prop(*(prop.propB));
+		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) {
+		printf("file %s does not exist\n", path);
+	}
+	fseek(file, 0, SEEK_END);
+	unsigned long int length = ftell(file);
+	fseek(file, 0, SEEK_SET);
+	char* out = malloc((length + 1) * sizeof(char));
+	fread(out, length, 1, file);
+	fclose(file);
+	out[length] = '\0';
+	return out;
+}
diff --git a/src/operetta.h b/src/operetta.h
new file mode 100644
index 0000000..6d348ed
--- /dev/null
+++ b/src/operetta.h
@@ -0,0 +1,9 @@
+#ifndef OPERETTA
+#define OPERETTA
+#include "parse.h"
+#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/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);
+}
diff --git a/src/parse.h b/src/parse.h
new file mode 100644
index 0000000..c6e76ec
--- /dev/null
+++ b/src/parse.h
@@ -0,0 +1,32 @@
+#ifndef PARSE
+#define PARSE
+#include "proposition.h"
+typedef struct Scope {
+	int id;
+	int depth;
+	struct Scope* parent;
+} scope_t;
+scope_t init_scope(int id, int depth, scope_t* parent);
+typedef struct Line {
+	scope_t scope;
+	prop_t proposition;
+	just_t justification;
+} line_t;
+line_t init_line(scope_t scope, prop_t proposition, just_t justification);
+typedef struct LineSet {
+	line_t* lines;
+	int count;
+} lineSet_t;
+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, char isNegative);
+just_t parse_justification(tokenSet_t tokenSet);
+/* proposition equal */
+char peq(prop_t prop1, prop_t prop2);
+/* scope is lesser than in depth and ID */
+char slt(scope_t scope1, scope_t scope2);
+/* scope is equal to or lesser than in depth and ID */
+char seqlt(scope_t scope1, scope_t scope2);
+#endif
diff --git a/src/proposition.c b/src/proposition.c
new file mode 100644
index 0000000..6f28fbe
--- /dev/null
+++ b/src/proposition.c
@@ -0,0 +1,48 @@
+#include "proposition.h"
+/* a proposition defines a relation between two propositions */
+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;
+	prop.isSimple = 0;
+	return prop;
+}
+/* a simple proposition is one with only a name */
+prop_t init_simple_prop(char isNegative, char* name) {
+	prop_t prop;
+	prop.isNegative = isNegative;
+	prop.name = 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/src/proposition.h b/src/proposition.h
new file mode 100644
index 0000000..2d09688
--- /dev/null
+++ b/src/proposition.h
@@ -0,0 +1,34 @@
+#ifndef PROPOSITION
+#define PROPOSITION
+#include "lexer.h"
+typedef struct Proposition {
+	char isSimple;
+	char isNegative;
+	struct Proposition* propA;
+	struct Proposition* propB;
+	tokenType_t relation;
+	char* name;
+} prop_t;
+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,
+	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 {
+	justRule_t rule;
+	int* references;
+	int referencesCount;
+} just_t;
+just_t init_just(justRule_t rule, int* references, int referencesCount);
+#endif