added scoping; probably doesn't work

6 files changed, 70 insertions, 31 deletions

diff --git a/eval.c b/eval.c
index 02b85f1..225c45e 100644
--- a/eval.c
+++ b/eval.c
@@ -1,36 +1,38 @@
 #include <stdlib.h>
 #include "eval.h"
+#include "stdio.h"
 #include "parse.h"
 char just_is_sound(prop_t prop, just_t just, lineSet_t lines) {
-	prop_t a;
-	prop_t b;
-	if (!prop.isSimple) {
-		a = *prop.propA;
-		b = *prop.propB;
-	}
-	prop_t w;
-	prop_t x;
-	prop_t y;
-	prop_t z;
-	if (just.referencesCount > 0) {
-		w = lines.lines[just.references[0] - 1].proposition;
-	}
-	if (just.referencesCount > 1) {
-		x = lines.lines[just.references[1] - 1].proposition;
-	}
-	if (just.referencesCount > 2) {
-		y = lines.lines[just.references[2] - 1].proposition;
-	}
-	if (just.referencesCount > 3) {
-		z = lines.lines[just.references[3] - 1].proposition;
-	}
+	prop_t a, b, w, x, y, z;
 	switch (just.rule) {
 		case PREMISE_R:
 			return 1;
 		case ASSUMPTION_R:
 			return 1;
 		case CONJUNCT_INTRO:
+			a = *prop.propA;
+			b = *prop.propB;
+			w = lines.lines[just.references[0] - 1].proposition;
+			x = lines.lines[just.references[1] - 1].proposition;
 			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;
+			w = lines.lines[just.references[0] - 1].proposition;
+			x = lines.lines[just.references[1] - 1].proposition;
+			if ((peq(a, w) && peq(b, x)) || (peq(a, x) && peq(b, w))) {
+				return 1;
+			}
+			return 0;
+			
+		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/operetta.c b/operetta.c
index c72a979..f547f2f 100644
--- a/operetta.c
+++ b/operetta.c
@@ -15,7 +15,7 @@ int main(int argc, char** argv) {
 	for (int i = 0; i < lines.count; i++) {
 		line_t line = lines.lines[i];
 		printf("%d. ", i + 1);
-		for (int j = 0; j < line.aLevel; j++) {
+		for (int j = 0; j < line.scope.depth; j++) {
 			printf(" > ");
 		}
 		write_prop(line.proposition);
diff --git a/parse.c b/parse.c
index ca01fc0..f2cff36 100644
--- a/parse.c
+++ b/parse.c
@@ -4,9 +4,19 @@
 #include "lexer.h"
 #include "stdio.h"
 
-line_t init_line(int aLevel, prop_t proposition, just_t justification) {
+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.aLevel = aLevel;
+	line.scope = scope;
 	line.proposition = proposition;
 	line.justification = justification;
 	return line;
@@ -50,11 +60,31 @@ line_t parse_line(char* content) {
 		}
 		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);
+	}
+	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);
-	return init_line(indent, prop, just);
+	return init_line(thisScope, prop, just);
 }
 prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative) {
 	prop_t prop;
diff --git a/parse.h b/parse.h
index 67d7160..84b3613 100644
--- a/parse.h
+++ b/parse.h
@@ -1,16 +1,22 @@
 #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 {
-	int aLevel;
+	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;
-line_t init_line(int aLevel, prop_t proposition, just_t justification);
 lineSet_t init_lineset(line_t* lines, int count);
 int count_lines(char* content);
 lineSet_t parse_lines(char* content, int lineCount);
diff --git a/proposition.c b/proposition.c
index c3fc897..6f28fbe 100644
--- a/proposition.c
+++ b/proposition.c
@@ -6,6 +6,7 @@ prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t rela
 	prop.propA = propA;
 	prop.propB = propB;
 	prop.relation = relation;
+	prop.isSimple = 0;
 	return prop;
 }
 /* a simple proposition is one with only a name */
diff --git a/testfile2 b/testfile2
index c66aa88..7c3764f 100644
--- a/testfile2
+++ b/testfile2
@@ -1,3 +1,3 @@
-P^Q | pr
-L^V | pr
-(P^Q)^(L^V) | ^i 1, 2
+P | pr
+Q | pr
+P->Q | ->I 2, 1