From c427a114bf95620cb9f1b439a8a6e1db14a74fb0 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Tue, 13 Jun 2023 18:49:47 -0700 Subject: starting a new assumption on the same depth creates a new scope, added scoping detections for all rules --- src/parse.c | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src/parse.c') 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); -- cgit v1.3.1