diff options
Diffstat (limited to 'eval.c')
| -rw-r--r-- | eval.c | 38 |
1 files changed, 29 insertions, 9 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); |