From 1d3bbec4660dfe4e2117826ceef9b32758b40345 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Tue, 13 Jun 2023 14:50:00 -0700 Subject: restructured project --- .gitignore | 1 + Makefile | 2 +- eval.c | 59 -------------- eval.h | 6 -- examples/operetta_example | 14 ++++ lexer.c | 198 ---------------------------------------------- lexer.h | 40 ---------- operetta.c | 64 --------------- operetta.h | 9 --- parse.c | 184 ------------------------------------------ parse.h | 32 -------- proposition.c | 48 ----------- proposition.h | 34 -------- src/eval.c | 59 ++++++++++++++ src/eval.h | 6 ++ src/lexer.c | 198 ++++++++++++++++++++++++++++++++++++++++++++++ src/lexer.h | 40 ++++++++++ src/operetta.c | 64 +++++++++++++++ src/operetta.h | 9 +++ src/parse.c | 184 ++++++++++++++++++++++++++++++++++++++++++ src/parse.h | 32 ++++++++ src/proposition.c | 48 +++++++++++ src/proposition.h | 34 ++++++++ testfile | 4 - testfile2 | 5 -- 25 files changed, 690 insertions(+), 684 deletions(-) delete mode 100644 eval.c delete mode 100644 eval.h create mode 100644 examples/operetta_example delete mode 100644 lexer.c delete mode 100644 lexer.h delete mode 100644 operetta.c delete mode 100644 operetta.h delete mode 100644 parse.c delete mode 100644 parse.h delete mode 100644 proposition.c delete mode 100644 proposition.h create mode 100644 src/eval.c create mode 100644 src/eval.h create mode 100644 src/lexer.c create mode 100644 src/lexer.h create mode 100644 src/operetta.c create mode 100644 src/operetta.h create mode 100644 src/parse.c create mode 100644 src/parse.h create mode 100644 src/proposition.c create mode 100644 src/proposition.h delete mode 100644 testfile delete mode 100644 testfile2 diff --git a/.gitignore b/.gitignore index c7137bd..ce80e8f 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ operetta *.core vgcore.* *.dSYM/ +/testfiles/ diff --git a/Makefile b/Makefile index 94251dc..2eaf791 100644 --- a/Makefile +++ b/Makefile @@ -5,7 +5,7 @@ PREFIX ?= /usr BINDIR ?= ${PREFIX}/bin generate: - $(CC) -o operetta operetta.c proposition.c parse.c lexer.c eval.c $(CFLAGS) + $(CC) -o operetta src/operetta.c src/proposition.c src/parse.c src/lexer.c src/eval.c $(CFLAGS) install: operetta install operetta ${DESTDIR}${BINDIR} diff --git a/eval.c b/eval.c deleted file mode 100644 index 9132272..0000000 --- a/eval.c +++ /dev/null @@ -1,59 +0,0 @@ -#include -#include "eval.h" -#include "stdio.h" -#include "parse.h" -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; - 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)); - case DISJUNCT_INTRO: - a = *prop.propA; - b = *prop.propB; - w = lines.lines[just.references[0] - 1].proposition; - return peq(a, w) || peq(b, w); - 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; - case CONJUNCT_ELIM: - w = lines.lines[just.references[0] - 1].proposition; - return peq(prop, *w.propA) || peq(prop, *w.propB); - default: - return 0; - } -} diff --git a/eval.h b/eval.h deleted file mode 100644 index 74e7650..0000000 --- a/eval.h +++ /dev/null @@ -1,6 +0,0 @@ -#ifndef EVAL -#define EVAL -#include "proposition.h" -#include "parse.h" -char just_is_sound(line_t line, lineSet_t lines); -#endif diff --git a/examples/operetta_example b/examples/operetta_example new file mode 100644 index 0000000..c2cf2fc --- /dev/null +++ b/examples/operetta_example @@ -0,0 +1,14 @@ +INPUT: +A | pr +C | pr + B | as + C ^ B | ^i 2, 3 +B->C^B | ->i 3, 4 + +OUTPUT: +1. A BECAUSE: PREMISE [0] +2. C BECAUSE: PREMISE [0] +3. > B BECAUSE: ASSUMPTION [1] +4. > (C CONJUNCTION B) BECAUSE: CONJUNCTION INTRODUCTION 2 3 [1] +5. (B IMPLICATION (C CONJUNCTION B)) BECAUSE: IMPLICATION INTRODUCTION 3 4 [0] + diff --git a/lexer.c b/lexer.c deleted file mode 100644 index c6c4ffe..0000000 --- a/lexer.c +++ /dev/null @@ -1,198 +0,0 @@ -#include -#include -#include "lexer.h" - -token_t init_token(tokenType_t type, void* value) { - token_t t; - t.type = type; - t.value = value; - return t; -} -tokenSet_t init_tokenset(token_t* tokens, int count) { - tokenSet_t tokenSet; - tokenSet.tokens = tokens; - tokenSet.count = count; - return tokenSet; -} -char* tttos(tokenType_t tokenType) { - switch (tokenType) { - case ERR: - return "ERR"; - case EOL: - return "EOL"; - case INDENT: - return "INDENT"; - case STRING: - return "STRING"; - case INT: - return "INT"; - case OPEN_PAREN: - return "OPEN_PAREN"; - case CLOSE_PAREN: - return "CLOSE_PAREN"; - case START_COMMENT: - return "START_COMMENT"; - case JUSTIFICATION: - return "JUSTIFICATION"; - case PREMISE: - return "PREMISE"; - case NEGATION: - return "NEGATION"; - case ASSUMPTION: - return "ASSUMPTION"; - case CONJUNCTION: - return "CONJUNCTION"; - case DISJUNCTION: - return "DISJUNCTION"; - case IMPLICATION: - return "IMPLICATION"; - case BI_IMPLICATION: - return "BI_IMPLICATION"; - default: - return "???"; - } -} -int advance_whitespace(char** linePointer) { - int64_t a = (int64_t)linePointer; - while (**linePointer == ' ') { - (*linePointer)++; - } - return (int)((int64_t)linePointer - a); -} -tokenSet_t lex_line(char* line) { - char** p = malloc(sizeof(char*)); - *p = line; - int m = 50; - token_t* tokens = malloc(sizeof(token_t) * m); - int i = 0; - while (1) { - token_t t = lex_first_token(p); - if (t.type == EOL) { - break; - } - if (t.type == ERR) { - exit(1); - } - tokens[i] = t; - i++; - } - free(p); - return init_tokenset(tokens, i); -} -token_t lex_first_token(char** content) { - int m = 5; - char* s = malloc(sizeof(char) * m); - int c = 0; - advance_whitespace(content); - while (**content != '\n') { - s[c] = **content; - s[c+1] = '\0'; - (*content)++; - /* check if we need to parse a string or an int */ - if (s[c] >= 65 && s[c] <= 90) { - free(s); - (*content)--; - return lex_first_string(content); - } - else if (s[c] >= 48 && s[c] <= 57) { - free(s); - (*content)--; - return lex_first_int(content); - } - /* otherwise, check to see if a symbol has been matched */ - if (strcmp(s, "(") == 0) { - free(s); - return init_token(OPEN_PAREN, NULL); - } - else if (strcmp(s, ")") == 0) { - free(s); - return init_token(CLOSE_PAREN, NULL); - } - else if (strcmp(s, "#") == 0) { - free(s); - return init_token(START_COMMENT, NULL); - } - else if (strcmp(s, " ") == 0) { - free(s); - return init_token(INDENT, NULL); - } - else if (strcmp(s, "|") == 0) { - free(s); - return init_token(JUSTIFICATION, NULL); - } - else if (strcmp(s, "pr") == 0) { - free(s); - return init_token(PREMISE, NULL); - } - else if (strcmp(s, "as") == 0) { - 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(NEGATION, NULL); - } - else if (strcmp(s, "^") == 0) { - free(s); - return init_token(CONJUNCTION, NULL); - } - else if (strcmp(s, "v") == 0) { - free(s); - return init_token(DISJUNCTION, NULL); - } - else if (strcmp(s, "->") == 0) { - free(s); - return init_token(IMPLICATION, NULL); - } - else if (strcmp(s, "<-") == 0) { - free(s); - return init_token(BI_IMPLICATION, NULL); - } - else if (c <= m) { - c++; - continue; - } - else { - free(s); - return init_token(ERR, NULL); - } - } - return init_token(EOL, NULL); -} -token_t lex_first_string(char** content) { - int m = 50; - char* s = malloc(sizeof(char) * m); - int c = 0; - advance_whitespace(content); - while (**content >= 65 && **content <= 90) { - s[c] = **content; - (*content)++; - c++; - } - s[c] = '\0'; - return init_token(STRING, s); -} -token_t lex_first_int(char** content) { - int m = 10; - char* s = malloc(sizeof(char) * m); - int c = 0; - advance_whitespace(content); - while (**content >= 48 && **content <= 57) { - s[c] = **content; - (*content)++; - c++; - } - s[c] = '\0'; - int* ip = malloc(sizeof(int)); - *ip = atoi(s); - free(s); - return init_token(INT, (void*)ip); -} diff --git a/lexer.h b/lexer.h deleted file mode 100644 index e5d64dc..0000000 --- a/lexer.h +++ /dev/null @@ -1,40 +0,0 @@ -#ifndef LEXER -#define LEXER -typedef enum TokenType { - ERR, - EOL, - INDENT, - STRING, - INT, - OPEN_PAREN, - CLOSE_PAREN, - START_COMMENT, - JUSTIFICATION, - PREMISE, - ASSUMPTION, - NEGATION, - CONJUNCTION, - DISJUNCTION, - IMPLICATION, - BI_IMPLICATION, - EXPLOSION, - ELIMINATION, - INTRODUCTION -} tokenType_t; -typedef struct Token { - tokenType_t type; - void* value; -} token_t; -token_t init_token(tokenType_t type, void* value); -typedef struct TokenSet { - token_t* tokens; - int count; -} tokenSet_t; -tokenSet_t init_tokenset(token_t* tokens, int count); -char* tttos(tokenType_t tokenType); -int advance_whitespace(char** linePointer); -tokenSet_t lex_line(char* line); -token_t lex_first_token(char** content); -token_t lex_first_string(char** content); -token_t lex_first_int(char** content); -#endif diff --git a/operetta.c b/operetta.c deleted file mode 100644 index f754895..0000000 --- a/operetta.c +++ /dev/null @@ -1,64 +0,0 @@ -#include -#include -#include "operetta.h" -#include "lexer.h" -#include "parse.h" -#include "proposition.h" -#include "eval.h" - -int main(int argc, char** argv) { - /* read file */ - char* path = argv[1]; - char* content = read_file(path); - int lineCount = count_lines(content); - lineSet_t lines = parse_lines(content, lineCount); - for (int i = 0; i < lines.count; i++) { - line_t line = lines.lines[i]; - printf("%d. ", i + 1); - for (int j = 0; j < line.scope.depth; j++) { - printf(" > "); - } - write_prop(line.proposition); - printf(" BECAUSE: "); - write_just(line.justification); - printf(just_is_sound(line, lines) ? " " : " "); - printf(" [%d]", line.scope.id); - printf("\n"); - } - free(content); -} -void write_prop(prop_t prop) { - if (prop.isNegative) { - printf("%s", "!"); - } - if (prop.isSimple) { - printf("%s", prop.name); - } - else { - printf("("); - write_prop(*(prop.propA)); - printf(" %s ", tttos(prop.relation)); - write_prop(*(prop.propB)); - 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) { - printf("file %s does not exist\n", path); - } - fseek(file, 0, SEEK_END); - unsigned long int length = ftell(file); - fseek(file, 0, SEEK_SET); - char* out = malloc((length + 1) * sizeof(char)); - fread(out, length, 1, file); - fclose(file); - out[length] = '\0'; - return out; -} diff --git a/operetta.h b/operetta.h deleted file mode 100644 index 6d348ed..0000000 --- a/operetta.h +++ /dev/null @@ -1,9 +0,0 @@ -#ifndef OPERETTA -#define OPERETTA -#include "parse.h" -#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 deleted file mode 100644 index 830f9c5..0000000 --- a/parse.c +++ /dev/null @@ -1,184 +0,0 @@ -#include -#include -#include "parse.h" -#include "lexer.h" -#include "stdio.h" - -scope_t lastScope; -int scopes; - -scope_t init_scope(int id, int depth, scope_t* parent) { - scope_t scope; - scope.id = id; - scope.depth = depth; - scope.parent = parent; - return scope; -} -line_t init_line(scope_t scope, prop_t proposition, just_t justification) { - line_t line; - line.scope = scope; - line.proposition = proposition; - line.justification = justification; - return line; -} -lineSet_t init_lineset(line_t* lines, int count) { - lineSet_t lineSet; - lineSet.lines = lines; - lineSet.count = count; - return lineSet; -} -int count_lines(char* content) { - int i = 0; - while (*content != '\0') { - if (*content == '\n') { - i++; - } - content++; - } - return i; -} -lineSet_t parse_lines(char* content, int lineCount) { - line_t* lines = malloc(sizeof(line_t) * lineCount); - for (int i = 0; i < lineCount; i++) { - /* parse the line */ - lines[i] = parse_line(content); - /* advance to the next line */ - while (*content != '\n') { - content++; - } - content++; - } - return init_lineset(lines, lineCount); -} -line_t parse_line(char* content) { - tokenSet_t ts = lex_line(content); - int c = 0; - int indent = 0; - char isNewIndent = 0; - while (ts.tokens[c].type != JUSTIFICATION) { - if (ts.tokens[c].type == INDENT) { - indent++; - } - c++; - } - /* determine the ID of the scope we are working on */ - scope_t thisScope; - if (indent > lastScope.depth) { - scopes++; - scope_t* lsp = malloc(sizeof(scope_t)); - *lsp = lastScope; - thisScope = init_scope(scopes, indent, lsp); - isNewIndent = 1; - } - else if (indent < lastScope.depth) { - scope_t li = lastScope; - for (int i = 0; i < lastScope.depth - indent; i++) { - li = *li.parent; - } - thisScope = li; - } - else { - thisScope = lastScope; - } - lastScope = thisScope; - /* find the proposition and justification */ - int* seek = calloc(sizeof(int), 1); - prop_t prop = parse_proposition(init_tokenset(ts.tokens + indent, c - indent), seek, 0); - just_t just = parse_justification(init_tokenset(ts.tokens + c + 1, ts.count - (c + 1))); - free(seek); - if ((just.rule != ASSUMPTION_R && isNewIndent) || (just.rule == ASSUMPTION_R && !isNewIndent)) { - just.rule = ERR_R; - } - return init_line(thisScope, prop, just); -} -prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative) { - prop_t prop; - /* recurse to parse the parenthetical as its own proposition */ - if (tokenSet.tokens[*seek].type == OPEN_PAREN) { - (*seek)++; - prop = parse_proposition(tokenSet, seek, 0); - } - else if (tokenSet.tokens[*seek].type == NEGATION) { - (*seek)++; - prop = parse_proposition(tokenSet, seek, 1); - } - else { - prop = init_simple_prop(isNegative, tokenSet.tokens[*seek].value); - (*seek)++; - } - /* check if we were reading a simple prop, or if there is a relation */ - if (*seek >= tokenSet.count || tokenSet.tokens[*seek].type == CLOSE_PAREN) { - (*seek)++; - return prop; - } - else { - /* the proposition we just read had a relation, so find the related proposition */ - tokenType_t rel = tokenSet.tokens[*seek].type; - (*seek)++; - prop_t* prop1p = malloc(sizeof(prop_t)); - *prop1p = prop; - prop_t* prop2p = malloc(sizeof(prop_t)); - *prop2p = parse_proposition(tokenSet, seek, 0); - prop_t metaProp = init_prop(0, prop1p, prop2p, rel); - 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)); - /* check the relation, then use a ternary operator for elim/intro */ - 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); -} -char peq(prop_t prop1, prop_t prop2) { - if (prop1.isSimple && prop2.isSimple) { - /* both simple */ - return strcmp(prop1.name, prop2.name) == 0 && prop1.isNegative == prop2.isNegative; - } - else if (prop1.isSimple || prop2.isSimple) { - /* only one simple */ - return 0; - } - else { - /* neither simple */ - return prop1.isNegative == prop2.isNegative && prop1.relation == prop2.relation && peq(*prop1.propA, *prop2.propA) && peq(*prop1.propB, *prop2.propB); - } -} -char slt(scope_t scope1, scope_t scope2) { - while (scope1.parent != NULL) { - scope1 = *scope1.parent; - if (scope1.id == scope2.id) { - return 1; - } - } - return 0; -} -char seqlt(scope_t scope1, scope_t scope2) { - return scope1.id == scope2.id || slt(scope1, scope2); -} diff --git a/parse.h b/parse.h deleted file mode 100644 index c6e76ec..0000000 --- a/parse.h +++ /dev/null @@ -1,32 +0,0 @@ -#ifndef PARSE -#define PARSE -#include "proposition.h" -typedef struct Scope { - int id; - int depth; - struct Scope* parent; -} scope_t; -scope_t init_scope(int id, int depth, scope_t* parent); -typedef struct Line { - scope_t scope; - prop_t proposition; - just_t justification; -} line_t; -line_t init_line(scope_t scope, prop_t proposition, just_t justification); -typedef struct LineSet { - line_t* lines; - int count; -} lineSet_t; -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* seek, char isNegative); -just_t parse_justification(tokenSet_t tokenSet); -/* proposition equal */ -char peq(prop_t prop1, prop_t prop2); -/* scope is lesser than in depth and ID */ -char slt(scope_t scope1, scope_t scope2); -/* scope is equal to or lesser than in depth and ID */ -char seqlt(scope_t scope1, scope_t scope2); -#endif diff --git a/proposition.c b/proposition.c deleted file mode 100644 index 6f28fbe..0000000 --- a/proposition.c +++ /dev/null @@ -1,48 +0,0 @@ -#include "proposition.h" -/* a proposition defines a relation between two propositions */ -prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation) { - prop_t prop; - prop.isNegative = isNegative; - prop.propA = propA; - prop.propB = propB; - prop.relation = relation; - prop.isSimple = 0; - return prop; -} -/* a simple proposition is one with only a name */ -prop_t init_simple_prop(char isNegative, char* name) { - prop_t prop; - prop.isNegative = isNegative; - prop.name = 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 deleted file mode 100644 index 2d09688..0000000 --- a/proposition.h +++ /dev/null @@ -1,34 +0,0 @@ -#ifndef PROPOSITION -#define PROPOSITION -#include "lexer.h" -typedef struct Proposition { - char isSimple; - char isNegative; - struct Proposition* propA; - struct Proposition* propB; - tokenType_t relation; - char* name; -} prop_t; -prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation); -prop_t init_simple_prop(char isNegative, 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 { - justRule_t rule; - int* references; - int referencesCount; -} just_t; -just_t init_just(justRule_t rule, int* references, int referencesCount); -#endif diff --git a/src/eval.c b/src/eval.c new file mode 100644 index 0000000..9132272 --- /dev/null +++ b/src/eval.c @@ -0,0 +1,59 @@ +#include +#include "eval.h" +#include "stdio.h" +#include "parse.h" +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; + 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)); + case DISJUNCT_INTRO: + a = *prop.propA; + b = *prop.propB; + w = lines.lines[just.references[0] - 1].proposition; + return peq(a, w) || peq(b, w); + 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; + case CONJUNCT_ELIM: + w = lines.lines[just.references[0] - 1].proposition; + return peq(prop, *w.propA) || peq(prop, *w.propB); + default: + return 0; + } +} diff --git a/src/eval.h b/src/eval.h new file mode 100644 index 0000000..74e7650 --- /dev/null +++ b/src/eval.h @@ -0,0 +1,6 @@ +#ifndef EVAL +#define EVAL +#include "proposition.h" +#include "parse.h" +char just_is_sound(line_t line, lineSet_t lines); +#endif diff --git a/src/lexer.c b/src/lexer.c new file mode 100644 index 0000000..c6c4ffe --- /dev/null +++ b/src/lexer.c @@ -0,0 +1,198 @@ +#include +#include +#include "lexer.h" + +token_t init_token(tokenType_t type, void* value) { + token_t t; + t.type = type; + t.value = value; + return t; +} +tokenSet_t init_tokenset(token_t* tokens, int count) { + tokenSet_t tokenSet; + tokenSet.tokens = tokens; + tokenSet.count = count; + return tokenSet; +} +char* tttos(tokenType_t tokenType) { + switch (tokenType) { + case ERR: + return "ERR"; + case EOL: + return "EOL"; + case INDENT: + return "INDENT"; + case STRING: + return "STRING"; + case INT: + return "INT"; + case OPEN_PAREN: + return "OPEN_PAREN"; + case CLOSE_PAREN: + return "CLOSE_PAREN"; + case START_COMMENT: + return "START_COMMENT"; + case JUSTIFICATION: + return "JUSTIFICATION"; + case PREMISE: + return "PREMISE"; + case NEGATION: + return "NEGATION"; + case ASSUMPTION: + return "ASSUMPTION"; + case CONJUNCTION: + return "CONJUNCTION"; + case DISJUNCTION: + return "DISJUNCTION"; + case IMPLICATION: + return "IMPLICATION"; + case BI_IMPLICATION: + return "BI_IMPLICATION"; + default: + return "???"; + } +} +int advance_whitespace(char** linePointer) { + int64_t a = (int64_t)linePointer; + while (**linePointer == ' ') { + (*linePointer)++; + } + return (int)((int64_t)linePointer - a); +} +tokenSet_t lex_line(char* line) { + char** p = malloc(sizeof(char*)); + *p = line; + int m = 50; + token_t* tokens = malloc(sizeof(token_t) * m); + int i = 0; + while (1) { + token_t t = lex_first_token(p); + if (t.type == EOL) { + break; + } + if (t.type == ERR) { + exit(1); + } + tokens[i] = t; + i++; + } + free(p); + return init_tokenset(tokens, i); +} +token_t lex_first_token(char** content) { + int m = 5; + char* s = malloc(sizeof(char) * m); + int c = 0; + advance_whitespace(content); + while (**content != '\n') { + s[c] = **content; + s[c+1] = '\0'; + (*content)++; + /* check if we need to parse a string or an int */ + if (s[c] >= 65 && s[c] <= 90) { + free(s); + (*content)--; + return lex_first_string(content); + } + else if (s[c] >= 48 && s[c] <= 57) { + free(s); + (*content)--; + return lex_first_int(content); + } + /* otherwise, check to see if a symbol has been matched */ + if (strcmp(s, "(") == 0) { + free(s); + return init_token(OPEN_PAREN, NULL); + } + else if (strcmp(s, ")") == 0) { + free(s); + return init_token(CLOSE_PAREN, NULL); + } + else if (strcmp(s, "#") == 0) { + free(s); + return init_token(START_COMMENT, NULL); + } + else if (strcmp(s, " ") == 0) { + free(s); + return init_token(INDENT, NULL); + } + else if (strcmp(s, "|") == 0) { + free(s); + return init_token(JUSTIFICATION, NULL); + } + else if (strcmp(s, "pr") == 0) { + free(s); + return init_token(PREMISE, NULL); + } + else if (strcmp(s, "as") == 0) { + 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(NEGATION, NULL); + } + else if (strcmp(s, "^") == 0) { + free(s); + return init_token(CONJUNCTION, NULL); + } + else if (strcmp(s, "v") == 0) { + free(s); + return init_token(DISJUNCTION, NULL); + } + else if (strcmp(s, "->") == 0) { + free(s); + return init_token(IMPLICATION, NULL); + } + else if (strcmp(s, "<-") == 0) { + free(s); + return init_token(BI_IMPLICATION, NULL); + } + else if (c <= m) { + c++; + continue; + } + else { + free(s); + return init_token(ERR, NULL); + } + } + return init_token(EOL, NULL); +} +token_t lex_first_string(char** content) { + int m = 50; + char* s = malloc(sizeof(char) * m); + int c = 0; + advance_whitespace(content); + while (**content >= 65 && **content <= 90) { + s[c] = **content; + (*content)++; + c++; + } + s[c] = '\0'; + return init_token(STRING, s); +} +token_t lex_first_int(char** content) { + int m = 10; + char* s = malloc(sizeof(char) * m); + int c = 0; + advance_whitespace(content); + while (**content >= 48 && **content <= 57) { + s[c] = **content; + (*content)++; + c++; + } + s[c] = '\0'; + int* ip = malloc(sizeof(int)); + *ip = atoi(s); + free(s); + return init_token(INT, (void*)ip); +} diff --git a/src/lexer.h b/src/lexer.h new file mode 100644 index 0000000..e5d64dc --- /dev/null +++ b/src/lexer.h @@ -0,0 +1,40 @@ +#ifndef LEXER +#define LEXER +typedef enum TokenType { + ERR, + EOL, + INDENT, + STRING, + INT, + OPEN_PAREN, + CLOSE_PAREN, + START_COMMENT, + JUSTIFICATION, + PREMISE, + ASSUMPTION, + NEGATION, + CONJUNCTION, + DISJUNCTION, + IMPLICATION, + BI_IMPLICATION, + EXPLOSION, + ELIMINATION, + INTRODUCTION +} tokenType_t; +typedef struct Token { + tokenType_t type; + void* value; +} token_t; +token_t init_token(tokenType_t type, void* value); +typedef struct TokenSet { + token_t* tokens; + int count; +} tokenSet_t; +tokenSet_t init_tokenset(token_t* tokens, int count); +char* tttos(tokenType_t tokenType); +int advance_whitespace(char** linePointer); +tokenSet_t lex_line(char* line); +token_t lex_first_token(char** content); +token_t lex_first_string(char** content); +token_t lex_first_int(char** content); +#endif diff --git a/src/operetta.c b/src/operetta.c new file mode 100644 index 0000000..f754895 --- /dev/null +++ b/src/operetta.c @@ -0,0 +1,64 @@ +#include +#include +#include "operetta.h" +#include "lexer.h" +#include "parse.h" +#include "proposition.h" +#include "eval.h" + +int main(int argc, char** argv) { + /* read file */ + char* path = argv[1]; + char* content = read_file(path); + int lineCount = count_lines(content); + lineSet_t lines = parse_lines(content, lineCount); + for (int i = 0; i < lines.count; i++) { + line_t line = lines.lines[i]; + printf("%d. ", i + 1); + for (int j = 0; j < line.scope.depth; j++) { + printf(" > "); + } + write_prop(line.proposition); + printf(" BECAUSE: "); + write_just(line.justification); + printf(just_is_sound(line, lines) ? " " : " "); + printf(" [%d]", line.scope.id); + printf("\n"); + } + free(content); +} +void write_prop(prop_t prop) { + if (prop.isNegative) { + printf("%s", "!"); + } + if (prop.isSimple) { + printf("%s", prop.name); + } + else { + printf("("); + write_prop(*(prop.propA)); + printf(" %s ", tttos(prop.relation)); + write_prop(*(prop.propB)); + 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) { + printf("file %s does not exist\n", path); + } + fseek(file, 0, SEEK_END); + unsigned long int length = ftell(file); + fseek(file, 0, SEEK_SET); + char* out = malloc((length + 1) * sizeof(char)); + fread(out, length, 1, file); + fclose(file); + out[length] = '\0'; + return out; +} diff --git a/src/operetta.h b/src/operetta.h new file mode 100644 index 0000000..6d348ed --- /dev/null +++ b/src/operetta.h @@ -0,0 +1,9 @@ +#ifndef OPERETTA +#define OPERETTA +#include "parse.h" +#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/src/parse.c b/src/parse.c new file mode 100644 index 0000000..830f9c5 --- /dev/null +++ b/src/parse.c @@ -0,0 +1,184 @@ +#include +#include +#include "parse.h" +#include "lexer.h" +#include "stdio.h" + +scope_t lastScope; +int scopes; + +scope_t init_scope(int id, int depth, scope_t* parent) { + scope_t scope; + scope.id = id; + scope.depth = depth; + scope.parent = parent; + return scope; +} +line_t init_line(scope_t scope, prop_t proposition, just_t justification) { + line_t line; + line.scope = scope; + line.proposition = proposition; + line.justification = justification; + return line; +} +lineSet_t init_lineset(line_t* lines, int count) { + lineSet_t lineSet; + lineSet.lines = lines; + lineSet.count = count; + return lineSet; +} +int count_lines(char* content) { + int i = 0; + while (*content != '\0') { + if (*content == '\n') { + i++; + } + content++; + } + return i; +} +lineSet_t parse_lines(char* content, int lineCount) { + line_t* lines = malloc(sizeof(line_t) * lineCount); + for (int i = 0; i < lineCount; i++) { + /* parse the line */ + lines[i] = parse_line(content); + /* advance to the next line */ + while (*content != '\n') { + content++; + } + content++; + } + return init_lineset(lines, lineCount); +} +line_t parse_line(char* content) { + tokenSet_t ts = lex_line(content); + int c = 0; + int indent = 0; + char isNewIndent = 0; + while (ts.tokens[c].type != JUSTIFICATION) { + if (ts.tokens[c].type == INDENT) { + indent++; + } + c++; + } + /* determine the ID of the scope we are working on */ + scope_t thisScope; + if (indent > lastScope.depth) { + scopes++; + scope_t* lsp = malloc(sizeof(scope_t)); + *lsp = lastScope; + thisScope = init_scope(scopes, indent, lsp); + isNewIndent = 1; + } + else if (indent < lastScope.depth) { + scope_t li = lastScope; + for (int i = 0; i < lastScope.depth - indent; i++) { + li = *li.parent; + } + thisScope = li; + } + else { + thisScope = lastScope; + } + lastScope = thisScope; + /* find the proposition and justification */ + int* seek = calloc(sizeof(int), 1); + prop_t prop = parse_proposition(init_tokenset(ts.tokens + indent, c - indent), seek, 0); + just_t just = parse_justification(init_tokenset(ts.tokens + c + 1, ts.count - (c + 1))); + free(seek); + if ((just.rule != ASSUMPTION_R && isNewIndent) || (just.rule == ASSUMPTION_R && !isNewIndent)) { + just.rule = ERR_R; + } + return init_line(thisScope, prop, just); +} +prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative) { + prop_t prop; + /* recurse to parse the parenthetical as its own proposition */ + if (tokenSet.tokens[*seek].type == OPEN_PAREN) { + (*seek)++; + prop = parse_proposition(tokenSet, seek, 0); + } + else if (tokenSet.tokens[*seek].type == NEGATION) { + (*seek)++; + prop = parse_proposition(tokenSet, seek, 1); + } + else { + prop = init_simple_prop(isNegative, tokenSet.tokens[*seek].value); + (*seek)++; + } + /* check if we were reading a simple prop, or if there is a relation */ + if (*seek >= tokenSet.count || tokenSet.tokens[*seek].type == CLOSE_PAREN) { + (*seek)++; + return prop; + } + else { + /* the proposition we just read had a relation, so find the related proposition */ + tokenType_t rel = tokenSet.tokens[*seek].type; + (*seek)++; + prop_t* prop1p = malloc(sizeof(prop_t)); + *prop1p = prop; + prop_t* prop2p = malloc(sizeof(prop_t)); + *prop2p = parse_proposition(tokenSet, seek, 0); + prop_t metaProp = init_prop(0, prop1p, prop2p, rel); + 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)); + /* check the relation, then use a ternary operator for elim/intro */ + 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); +} +char peq(prop_t prop1, prop_t prop2) { + if (prop1.isSimple && prop2.isSimple) { + /* both simple */ + return strcmp(prop1.name, prop2.name) == 0 && prop1.isNegative == prop2.isNegative; + } + else if (prop1.isSimple || prop2.isSimple) { + /* only one simple */ + return 0; + } + else { + /* neither simple */ + return prop1.isNegative == prop2.isNegative && prop1.relation == prop2.relation && peq(*prop1.propA, *prop2.propA) && peq(*prop1.propB, *prop2.propB); + } +} +char slt(scope_t scope1, scope_t scope2) { + while (scope1.parent != NULL) { + scope1 = *scope1.parent; + if (scope1.id == scope2.id) { + return 1; + } + } + return 0; +} +char seqlt(scope_t scope1, scope_t scope2) { + return scope1.id == scope2.id || slt(scope1, scope2); +} diff --git a/src/parse.h b/src/parse.h new file mode 100644 index 0000000..c6e76ec --- /dev/null +++ b/src/parse.h @@ -0,0 +1,32 @@ +#ifndef PARSE +#define PARSE +#include "proposition.h" +typedef struct Scope { + int id; + int depth; + struct Scope* parent; +} scope_t; +scope_t init_scope(int id, int depth, scope_t* parent); +typedef struct Line { + scope_t scope; + prop_t proposition; + just_t justification; +} line_t; +line_t init_line(scope_t scope, prop_t proposition, just_t justification); +typedef struct LineSet { + line_t* lines; + int count; +} lineSet_t; +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* seek, char isNegative); +just_t parse_justification(tokenSet_t tokenSet); +/* proposition equal */ +char peq(prop_t prop1, prop_t prop2); +/* scope is lesser than in depth and ID */ +char slt(scope_t scope1, scope_t scope2); +/* scope is equal to or lesser than in depth and ID */ +char seqlt(scope_t scope1, scope_t scope2); +#endif diff --git a/src/proposition.c b/src/proposition.c new file mode 100644 index 0000000..6f28fbe --- /dev/null +++ b/src/proposition.c @@ -0,0 +1,48 @@ +#include "proposition.h" +/* a proposition defines a relation between two propositions */ +prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation) { + prop_t prop; + prop.isNegative = isNegative; + prop.propA = propA; + prop.propB = propB; + prop.relation = relation; + prop.isSimple = 0; + return prop; +} +/* a simple proposition is one with only a name */ +prop_t init_simple_prop(char isNegative, char* name) { + prop_t prop; + prop.isNegative = isNegative; + prop.name = 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/src/proposition.h b/src/proposition.h new file mode 100644 index 0000000..2d09688 --- /dev/null +++ b/src/proposition.h @@ -0,0 +1,34 @@ +#ifndef PROPOSITION +#define PROPOSITION +#include "lexer.h" +typedef struct Proposition { + char isSimple; + char isNegative; + struct Proposition* propA; + struct Proposition* propB; + tokenType_t relation; + char* name; +} prop_t; +prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation); +prop_t init_simple_prop(char isNegative, 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 { + 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 deleted file mode 100644 index 5f07502..0000000 --- a/testfile +++ /dev/null @@ -1,4 +0,0 @@ -Q | pr - KAI^PRESTON | as - ~CAT->(DOG^~RABBIT) | ^e 1 2 -V | pr diff --git a/testfile2 b/testfile2 deleted file mode 100644 index dbdaa34..0000000 --- a/testfile2 +++ /dev/null @@ -1,5 +0,0 @@ -A | pr -C | pr - B | as - C ^ B | ^i 2, 3 -B->C^B | ->i 3, 4 -- cgit v1.3.1