summaryrefslogtreecommitdiff
path: root/eval.c
diff options
context:
space:
mode:
Diffstat (limited to 'eval.c')
-rw-r--r--eval.c37
1 files changed, 37 insertions, 0 deletions
diff --git a/eval.c b/eval.c
new file mode 100644
index 0000000..02b85f1
--- /dev/null
+++ b/eval.c
@@ -0,0 +1,37 @@
+#include <stdlib.h>
+#include "eval.h"
+#include "parse.h"
+char just_is_sound(prop_t prop, just_t just, lineSet_t lines) {
+ prop_t a;
+ prop_t b;
+ if (!prop.isSimple) {
+ a = *prop.propA;
+ b = *prop.propB;
+ }
+ prop_t w;
+ prop_t x;
+ prop_t y;
+ prop_t z;
+ if (just.referencesCount > 0) {
+ w = lines.lines[just.references[0] - 1].proposition;
+ }
+ if (just.referencesCount > 1) {
+ x = lines.lines[just.references[1] - 1].proposition;
+ }
+ if (just.referencesCount > 2) {
+ y = lines.lines[just.references[2] - 1].proposition;
+ }
+ if (just.referencesCount > 3) {
+ z = lines.lines[just.references[3] - 1].proposition;
+ }
+ switch (just.rule) {
+ case PREMISE_R:
+ return 1;
+ case ASSUMPTION_R:
+ return 1;
+ case CONJUNCT_INTRO:
+ return (peq(a, w) && peq(b, x)) || (peq(a, x) && peq(b, w));
+ default:
+ return 0;
+ }
+}