diff options
| -rw-r--r-- | eval.c | 38 | ||||
| -rw-r--r-- | eval.h | 2 | ||||
| -rw-r--r-- | operetta.c | 3 | ||||
| -rw-r--r-- | parse.c | 17 | ||||
| -rw-r--r-- | parse.h | 5 | ||||
| -rw-r--r-- | testfile2 | 8 |
6 files changed, 59 insertions, 14 deletions
@@ -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); @@ -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 @@ -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) ? " <SOUND>" : " <UNSOUND>"); + printf(just_is_sound(line, lines) ? " <SOUND>" : " <UNSOUND>"); + printf(" [%d]", line.scope.id); printf("\n"); } free(content); @@ -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); +} @@ -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 @@ -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 |