starting a new assumption on the same depth creates a new scope, added scoping detections for all rules

2 files changed, 17 insertions, 9 deletions

diff --git a/src/eval.c b/src/eval.c
index 9132272..4e978b6 100644
--- a/src/eval.c
+++ b/src/eval.c
@@ -27,7 +27,11 @@ char just_is_sound(line_t line, lineSet_t lines) {
 		case DISJUNCT_INTRO:
 			a = *prop.propA;
 			b = *prop.propB;
-			w = lines.lines[just.references[0] - 1].proposition;
+			wl = lines.lines[just.references[0] - 1];
+			w = wl.proposition;
+			if (!seqlt(line.scope, wl.scope)) {
+				return 0;
+			}
 			return peq(a, w) || peq(b, w);
 		case IMPLICATION_INTRO:
 			a = *prop.propA;
@@ -51,7 +55,11 @@ char just_is_sound(line_t line, lineSet_t lines) {
 			/* 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;
+			wl = lines.lines[just.references[0] - 1];
+			w = wl.proposition;
+			if (!seqlt(line.scope, wl.scope)) {
+				return 0;
+			}
 			return peq(prop, *w.propA) || peq(prop, *w.propB);
 		default:
 			return 0;
diff --git a/src/parse.c b/src/parse.c
index 830f9c5..cae66a0 100644
--- a/src/parse.c
+++ b/src/parse.c
@@ -61,9 +61,14 @@ line_t parse_line(char* content) {
 		}
 		c++;
 	}
+	/* 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);
 	/* determine the ID of the scope we are working on */
 	scope_t thisScope;
-	if (indent > lastScope.depth) {
+	if (indent > lastScope.depth || just.rule == ASSUMPTION_R) {
 		scopes++;
 		scope_t* lsp = malloc(sizeof(scope_t));
 		*lsp = lastScope;
@@ -81,12 +86,7 @@ line_t parse_line(char* content) {
 		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)) {
+	if ((just.rule != ASSUMPTION_R && isNewIndent) || (just.rule == ASSUMPTION_R && !isNewIndent) || (just.rule == PREMISE_R && indent != 0)) {
 			just.rule = ERR_R;
 	}
 	return init_line(thisScope, prop, just);