From c427a114bf95620cb9f1b439a8a6e1db14a74fb0 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Tue, 13 Jun 2023 18:49:47 -0700 Subject: starting a new assumption on the same depth creates a new scope, added scoping detections for all rules --- src/eval.c | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'src/eval.c') diff --git a/src/eval.c b/src/eval.c index 9132272..4e978b6 100644 --- a/src/eval.c +++ b/src/eval.c @@ -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; -- cgit v1.3.1