summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--lexer.c8
-rw-r--r--operetta.c8
-rw-r--r--operetta.h1
-rw-r--r--parse.c34
-rw-r--r--parse.h3
-rw-r--r--proposition.c29
-rw-r--r--proposition.h19
-rw-r--r--testfile2
9 files changed, 101 insertions, 5 deletions
diff --git a/Makefile b/Makefile
index 0948a4e..83970cf 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
CFLAGS=-I. -Wall -Wextra -Wpedantic -O3 -lm -Wcast-align
CFLAGS+= -Wshadow -Wstrict-prototypes -Wundef -Wpointer-arith
-CFLAGS+= -Wunreachable-code -Wswitch-enum -Wformat=2 -g
+CFLAGS+= -Wunreachable-code -Wformat=2 -g
PREFIX ?= /usr
BINDIR ?= ${PREFIX}/bin
diff --git a/lexer.c b/lexer.c
index 5fe9e22..be35d85 100644
--- a/lexer.c
+++ b/lexer.c
@@ -120,6 +120,14 @@ token_t lex_first_token(char** content) {
free(s);
return init_token(ASSUMPTION, NULL);
}
+ else if (strcmp(s, "i") == 0) {
+ free(s);
+ return init_token(INTRODUCTION, NULL);
+ }
+ else if (strcmp(s, "e") == 0) {
+ free(s);
+ return init_token(ELIMINATION, NULL);
+ }
else if (strcmp(s, "^") == 0) {
free(s);
return init_token(CONJUNCTION, NULL);
diff --git a/operetta.c b/operetta.c
index 4c50434..4192ffb 100644
--- a/operetta.c
+++ b/operetta.c
@@ -13,6 +13,8 @@ int main(int argc, char** argv) {
lineSet_t lines = parse_lines(content, lineCount);
for (int i = 0; i < lines.count; i++) {
write_prop(lines.lines[i].proposition);
+ printf(" BECAUSE: ");
+ write_just(lines.lines[i].justification);
printf("\n");
}
free(content);
@@ -29,6 +31,12 @@ void write_prop(prop_t prop) {
printf(")");
}
}
+void write_just(just_t just) {
+ printf("%s", jrtos(just.rule));
+ for (int i = 0; i < just.referencesCount; i++) {
+ printf(" %d", just.references[i]);
+ }
+}
char* read_file(char* path) {
FILE* file = fopen(path, "r");
if (file == NULL) {
diff --git a/operetta.h b/operetta.h
index 17a0251..6d348ed 100644
--- a/operetta.h
+++ b/operetta.h
@@ -4,5 +4,6 @@
#include "proposition.h"
void write_line(line_t line);
void write_prop(prop_t prop);
+void write_just(just_t just);
char* read_file(char* path);
#endif
diff --git a/parse.c b/parse.c
index ad839fc..d7ec467 100644
--- a/parse.c
+++ b/parse.c
@@ -45,7 +45,7 @@ line_t parse_line(char* content) {
}
int* seek = calloc(sizeof(int), 1);
prop_t prop = parse_proposition(init_tokenset(ts.tokens, i), seek);
- just_t just;
+ just_t just = parse_justification(init_tokenset(ts.tokens + i + 1, ts.count - (i + 1)));
return init_line(prop, just);
}
prop_t parse_proposition(tokenSet_t tokenSet, int* seek) {
@@ -73,3 +73,35 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek) {
return metaProp;
}
}
+just_t parse_justification(tokenSet_t tokenSet) {
+ /* premise and assumption require no arguments */
+ if (tokenSet.tokens[0].type == PREMISE || tokenSet.tokens[0].type == ASSUMPTION) {
+ return init_just(tokenSet.tokens[0].type == PREMISE ? PREMISE_R : ASSUMPTION_R, NULL, 0);
+ }
+ justRule_t just;
+ int* references = malloc(sizeof(int) * (tokenSet.count - 2));
+ switch (tokenSet.tokens[0].type) {
+ case CONJUNCTION:
+ just = tokenSet.tokens[1].type == ELIMINATION ? CONJUNCT_ELIM : CONJUNCT_INTRO;
+ break;
+ case DISJUNCTION:
+ just = tokenSet.tokens[1].type == ELIMINATION ? DISJUNCT_ELIM : DISJUNCT_INTRO;
+ break;
+ case IMPLICATION:
+ just = tokenSet.tokens[1].type == ELIMINATION ? IMPLICATION_ELIM : IMPLICATION_INTRO;
+ break;
+ default:
+ return init_just(ERR_R, NULL, 0);
+ }
+ /* find the arguments */
+ int i;
+ for (i = 0; i < tokenSet.count - 2; i++) {
+ if (tokenSet.tokens[i + 2].type == INT) {
+ references[i] = *((int*)tokenSet.tokens[i + 2].value);
+ }
+ else {
+ return init_just(ERR_R, NULL, 0);
+ }
+ }
+ return init_just(just, references, i);
+}
diff --git a/parse.h b/parse.h
index 3fb0a3b..2bb49fa 100644
--- a/parse.h
+++ b/parse.h
@@ -14,5 +14,6 @@ lineSet_t init_lineset(line_t* lines, int count);
int count_lines(char* content);
lineSet_t parse_lines(char* content, int lineCount);
line_t parse_line(char* content);
-prop_t parse_proposition(tokenSet_t tokenSet, int* tokensRead);
+prop_t parse_proposition(tokenSet_t tokenSet, int* seek);
+just_t parse_justification(tokenSet_t tokenSet);
#endif
diff --git a/proposition.c b/proposition.c
index 0919aa8..76ae4cd 100644
--- a/proposition.c
+++ b/proposition.c
@@ -12,3 +12,32 @@ prop_t init_simple_prop(char* name) {
prop.isSimple = 1;
return prop;
}
+char* jrtos(justRule_t rule) {
+ switch (rule) {
+ case PREMISE_R:
+ return "PREMISE";
+ case ASSUMPTION_R:
+ return "ASSUMPTION";
+ case CONJUNCT_INTRO:
+ return "CONJUNCTION INTRODUCTION";
+ case DISJUNCT_INTRO:
+ return "DISJUNCTION INTRODUCTION";
+ case IMPLICATION_INTRO:
+ return "IMPLICATION INTRODUCTION";
+ case CONJUNCT_ELIM:
+ return "CONJUNCTION ELIMINATION";
+ case DISJUNCT_ELIM:
+ return "DISJUNCTION ELIMINATION";
+ case IMPLICATION_ELIM:
+ return "IMPLICATION ELIMINATION";
+ default:
+ return "ERR";
+ }
+}
+just_t init_just(justRule_t rule, int* references, int referencesCount) {
+ just_t just;
+ just.rule = rule;
+ just.references = references;
+ just.referencesCount = referencesCount;
+ return just;
+}
diff --git a/proposition.h b/proposition.h
index d2f5ac6..95f377c 100644
--- a/proposition.h
+++ b/proposition.h
@@ -10,7 +10,24 @@ typedef struct Proposition {
} prop_t;
prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation);
prop_t init_simple_prop(char* name);
+typedef enum JustificationRule {
+ ERR_R,
+ PREMISE_R,
+ ASSUMPTION_R,
+ CONJUNCT_INTRO,
+ DISJUNCT_INTRO,
+ IMPLICATION_INTRO,
+ BI_IMPLICATION_INTRO,
+ CONJUNCT_ELIM,
+ DISJUNCT_ELIM,
+ IMPLICATION_ELIM,
+ BI_IMPLICATION_ELIM
+} justRule_t;
+char* jrtos(justRule_t rule);
typedef struct Justification {
- tokenType_t rule;
+ justRule_t rule;
+ int* references;
+ int referencesCount;
} just_t;
+just_t init_just(justRule_t rule, int* references, int referencesCount);
#endif
diff --git a/testfile b/testfile
index 47019a4..b4fca7c 100644
--- a/testfile
+++ b/testfile
@@ -1,3 +1,3 @@
QvP | pr
KAI^PRESTON | as
-CATv(DOG^RABBIT) | pr
+CATv(DOG^RABBIT) | ^e 1 2
generated by cgit v1.3.1 (git 2.54.0) at 2026-10-22 00:53:39 +0000