diff options
| -rw-r--r-- | src/eval.c | 12 | ||||
| -rw-r--r-- | src/parse.c | 14 |
2 files changed, 17 insertions, 9 deletions
@@ -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); |