summaryrefslogtreecommitdiff
path: root/src/eval.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/eval.c')
-rw-r--r--src/eval.c216
1 files changed, 133 insertions, 83 deletions
diff --git a/src/eval.c b/src/eval.c
index 26d1629..4af7153 100644
--- a/src/eval.c
+++ b/src/eval.c
@@ -2,102 +2,152 @@
#include "eval.h"
#include "stdio.h"
#include "parse.h"
-/* TODO: separate cases into functions */
-char just_is_sound(line_t line, lineSet_t lines) {
+/* TODO: error reporting */
+char conjunct_intro_is_sound(line_t line, line_t ref1, line_t ref2) {
+ prop_t prop = line.proposition;
+ prop_t a = *prop.propA;
+ prop_t b = *prop.propB;
+ prop_t r1p = ref1.proposition;
+ prop_t r2p = ref2.proposition;
+ /* the references are in a deeper scope than the justification */
+ if (!seqlt(line.scope, ref1.scope) || !seqlt(line.scope, ref2.scope)) {
+ return 0;
+ }
+ return (peq(a, r1p) && peq(b, r2p)) || (peq(a, r2p) && peq(b, r1p));
+}
+char disjunct_intro_is_sound(line_t line, line_t ref1) {
+ prop_t prop = line.proposition;
+ prop_t a = *prop.propA;
+ prop_t b = *prop.propB;
+ prop_t r1p = ref1.proposition;
+ if (!seqlt(line.scope, ref1.scope)) {
+ return 0;
+ }
+ return peq(a, r1p) || peq(b, r1p);
+}
+char implication_intro_is_sound(line_t line, line_t ref1, line_t ref2) {
+ prop_t prop = line.proposition;
+ prop_t a = *prop.propA;
+ prop_t b = *prop.propB;
+ prop_t r1p = ref1.proposition;
+ prop_t r2p = ref2.proposition;
+ line_t as;
+ line_t res;
+ /* find the positions of the arguments */
+ if (peq(a, r1p) && peq(b, r2p)) {
+ as = ref1;
+ res = ref2;
+ }
+ else if (peq(a, r2p) && peq(b, r1p)) {
+ as = ref2;
+ res = ref1;
+ }
+ else {
+ return 0;
+ }
+ /* ensure that the arguments are in the correct scope */
+ if (as.scope.id != res.scope.id || as.scope.depth != line.scope.depth + 1) {
+ return 0;
+ }
+ return 1;
+}
+char contradiction_intro_is_sound(line_t line, line_t ref1, line_t ref2) {
+ prop_t prop = line.proposition;
+ if (!prop.isContradiction) {
+ return 0;
+ }
+ prop_t r1p = ref1.proposition;
+ prop_t r2p = ref2.proposition;
+ if (r1p.isNegative == r2p.isNegative) {
+ return 0;
+ }
+ if (!seqlt(line.scope, ref1.scope) || !seqlt(line.scope, ref2.scope)) {
+ return 0;
+ }
+ if (!pbeq(r1p, r2p) ) {
+ return 0;
+ }
+ return 1;
+}
+char negation_intro_is_sound(line_t line, line_t ref1, line_t ref2) {
+ prop_t prop = line.proposition;
+ if (!prop.isNegative) {
+ return 0;
+ }
+ prop_t r1p = ref1.proposition;
+ prop_t r2p = ref2.proposition;
+ prop_t as;
+ /* TODO: scoping */
+ if (r1p.isContradiction) {
+ as = r2p;
+ }
+ else if (r2p.isContradiction) {
+ as = r1p;
+ }
+ else {
+ return 0;
+ }
+ if (!pbeq(as, prop) || as.isNegative == prop.isNegative) {
+ return 0;
+ }
+ return 1;
+}
+char conjunct_elim_is_sound(line_t line, line_t ref1) {
prop_t prop = line.proposition;
+ prop_t r1p = ref1.proposition;
+ if (!seqlt(line.scope, ref1.scope)) {
+ return 0;
+ }
+ return peq(prop, *r1p.propA) || peq(prop, *r1p.propB);
+}
+char implication_elim_is_sound(line_t line, line_t ref1, line_t ref2) {
+ prop_t prop = line.proposition;
+ prop_t r1p = ref1.proposition;
+ prop_t r2p = ref2.proposition;
+ if (!seqlt(line.scope, ref1.scope) || !seqlt(line.scope, ref2.scope)) {
+ return 0;
+ }
+ if (!r1p.isSimple && peq(prop, *r1p.propB) && r1p.relation == IMPLICATION && peq(r2p, *r1p.propA)) {
+ return 1;
+ }
+ else if (!r2p.isSimple && peq(prop, *r2p.propB) && r2p.relation == IMPLICATION && peq(r1p, *r2p.propA)) {
+ return 1;
+ }
+ else {
+ return 0;
+ }
+}
+char just_is_sound(line_t line, lineSet_t lines) {
just_t just = line.justification;
- prop_t a, b, w, x, y, z;
- line_t wl, xl, yl, zl;
+ line_t ref1, ref2, ref3;
+ if (just.referencesCount > 0) {
+ ref1 = lines.lines[just.references[0] - 1];
+ if (just.referencesCount > 1) {
+ ref2 = lines.lines[just.references[1] - 1];
+ if (just.referencesCount > 2) {
+ ref3 = lines.lines[just.references[2] - 1];
+ }
+ }
+ }
switch (just.rule) {
case PREMISE_R:
return 1;
case ASSUMPTION_R:
return 1;
case CONJUNCT_INTRO:
- a = *prop.propA;
- b = *prop.propB;
- 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));
+ return conjunct_intro_is_sound(line, ref1, ref2);
case DISJUNCT_INTRO:
- a = *prop.propA;
- b = *prop.propB;
- 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);
+ return disjunct_intro_is_sound(line, ref1);
case IMPLICATION_INTRO:
- a = *prop.propA;
- b = *prop.propB;
- 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;
- }
- 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;
+ return implication_intro_is_sound(line, ref1, ref2);
case CONTRADICTION_INTRO:
- if (!prop.isContradiction) {
- return 0;
- }
- wl = lines.lines[just.references[0] - 1];
- xl = lines.lines[just.references[1] - 1];
- w = wl.proposition;
- x = xl.proposition;
- if (!seqlt(line.scope, wl.scope) || !seqlt(line.scope, xl.scope)) {
- return 0;
- }
- if (!pbeq(w, x) ) {
- return 0;
- }
- if (w.isNegative == x.isNegative) {
- return 0;
- }
- return 1;
+ return contradiction_intro_is_sound(line, ref1, ref2);
+ case NEGATION_INTRO:
+ return negation_intro_is_sound(line, ref1, ref2);
case CONJUNCT_ELIM:
- 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);
+ return conjunct_elim_is_sound(line, ref1);
case IMPLICATION_ELIM:
- wl = lines.lines[just.references[0] - 1];
- xl = lines.lines[just.references[1] - 1];
- w = wl.proposition;
- x = xl.proposition;
- if (!seqlt(line.scope, wl.scope) || !seqlt(line.scope, xl.scope)) {
- return 0;
- }
- /* find the positions of the arguments */
- if (!w.isSimple && peq(prop, *w.propB) && w.relation == IMPLICATION && peq(x, *w.propA)) {
- return 1;
- }
- else if (!x.isSimple && peq(prop, *x.propB) && x.relation == IMPLICATION && peq(w, *x.propA)) {
- return 1;
- }
- else {
- return 0;
- }
+ return implication_elim_is_sound(line, ref1, ref2);
default:
return 0;
}
generated by cgit v1.3.1 (git 2.54.0) at 2026-10-21 23:53:03 +0000