From 1d3bbec4660dfe4e2117826ceef9b32758b40345 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Tue, 13 Jun 2023 14:50:00 -0700 Subject: restructured project --- 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 ++++++++++ 10 files changed, 674 insertions(+) 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 (limited to 'src') 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 -- cgit v1.3.1