From 1d3bbec4660dfe4e2117826ceef9b32758b40345 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Tue, 13 Jun 2023 14:50:00 -0700 Subject: restructured project --- parse.c | 184 ---------------------------------------------------------------- 1 file changed, 184 deletions(-) delete mode 100644 parse.c (limited to 'parse.c') 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); -} -- cgit v1.3.1