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 +++++++++++++++++++++++++++++--------- 1 file changed, 29 insertions(+), 9 deletions(-) (limited to 'eval.c') 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); -- cgit v1.3.1