From caa9d17ea794a0b4823170551545498d458e1fc2 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Tue, 13 Jun 2023 14:21:07 -0700 Subject: implemented scoping for some justifications, added helper functions --- eval.c | 38 +++++++++++++++++++++++++++++--------- eval.h | 2 +- operetta.c | 3 ++- parse.c | 17 +++++++++++++++++ parse.h | 5 +++++ testfile2 | 8 +++++--- 6 files changed, 59 insertions(+), 14 deletions(-) diff --git a/eval.c b/eval.c index 225c45e..9132272 100644 --- a/eval.c +++ b/eval.c @@ -2,8 +2,11 @@ #include "eval.h" #include "stdio.h" #include "parse.h" -char just_is_sound(prop_t prop, just_t just, lineSet_t lines) { +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; @@ -12,8 +15,14 @@ char just_is_sound(prop_t prop, just_t just, lineSet_t lines) { 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; + 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; @@ -23,13 +32,24 @@ char just_is_sound(prop_t prop, just_t just, lineSet_t lines) { 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; + 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; } - return 0; - + 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); diff --git a/eval.h b/eval.h index bb994f3..74e7650 100644 --- a/eval.h +++ b/eval.h @@ -2,5 +2,5 @@ #define EVAL #include "proposition.h" #include "parse.h" -char just_is_sound(prop_t prop, just_t just, lineSet_t lines); +char just_is_sound(line_t line, lineSet_t lines); #endif diff --git a/operetta.c b/operetta.c index f547f2f..f754895 100644 --- a/operetta.c +++ b/operetta.c @@ -21,7 +21,8 @@ int main(int argc, char** argv) { write_prop(line.proposition); printf(" BECAUSE: "); write_just(line.justification); - printf(just_is_sound(line.proposition, line.justification, lines) ? " " : " "); + printf(just_is_sound(line, lines) ? " " : " "); + printf(" [%d]", line.scope.id); printf("\n"); } free(content); diff --git a/parse.c b/parse.c index f2cff36..830f9c5 100644 --- a/parse.c +++ b/parse.c @@ -54,6 +54,7 @@ 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++; @@ -67,6 +68,7 @@ line_t parse_line(char* content) { 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; @@ -84,6 +86,9 @@ line_t parse_line(char* content) { 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) { @@ -165,3 +170,15 @@ char peq(prop_t prop1, prop_t prop2) { 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/parse.h b/parse.h index 84b3613..c6e76ec 100644 --- a/parse.h +++ b/parse.h @@ -23,5 +23,10 @@ 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/testfile2 b/testfile2 index 7c3764f..dbdaa34 100644 --- a/testfile2 +++ b/testfile2 @@ -1,3 +1,5 @@ -P | pr -Q | pr -P->Q | ->I 2, 1 +A | pr +C | pr + B | as + C ^ B | ^i 2, 3 +B->C^B | ->i 3, 4 -- cgit v1.3.1