diff options
| -rw-r--r-- | eval.c | 46 | ||||
| -rw-r--r-- | operetta.c | 2 | ||||
| -rw-r--r-- | parse.c | 36 | ||||
| -rw-r--r-- | parse.h | 10 | ||||
| -rw-r--r-- | proposition.c | 1 | ||||
| -rw-r--r-- | testfile2 | 6 |
6 files changed, 70 insertions, 31 deletions
@@ -1,36 +1,38 @@ #include <stdlib.h> #include "eval.h" +#include "stdio.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; - } + prop_t a, b, w, x, y, z; switch (just.rule) { case PREMISE_R: return 1; case ASSUMPTION_R: return 1; case CONJUNCT_INTRO: + a = *prop.propA; + b = *prop.propB; + w = lines.lines[just.references[0] - 1].proposition; + x = lines.lines[just.references[1] - 1].proposition; 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; + w = lines.lines[just.references[0] - 1].proposition; + x = lines.lines[just.references[1] - 1].proposition; + if ((peq(a, w) && peq(b, x)) || (peq(a, x) && peq(b, w))) { + return 1; + } + return 0; + + case CONJUNCT_ELIM: + w = lines.lines[just.references[0] - 1].proposition; + return peq(prop, *w.propA) || peq(prop, *w.propB); default: return 0; } @@ -15,7 +15,7 @@ int main(int argc, char** argv) { for (int i = 0; i < lines.count; i++) { line_t line = lines.lines[i]; printf("%d. ", i + 1); - for (int j = 0; j < line.aLevel; j++) { + for (int j = 0; j < line.scope.depth; j++) { printf(" > "); } write_prop(line.proposition); @@ -4,9 +4,19 @@ #include "lexer.h" #include "stdio.h" -line_t init_line(int aLevel, prop_t proposition, just_t justification) { +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.aLevel = aLevel; + line.scope = scope; line.proposition = proposition; line.justification = justification; return line; @@ -50,11 +60,31 @@ line_t parse_line(char* content) { } 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); + } + 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); - return init_line(indent, prop, just); + return init_line(thisScope, prop, just); } prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative) { prop_t prop; @@ -1,16 +1,22 @@ #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 { - int aLevel; + 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; -line_t init_line(int aLevel, prop_t proposition, just_t justification); lineSet_t init_lineset(line_t* lines, int count); int count_lines(char* content); lineSet_t parse_lines(char* content, int lineCount); diff --git a/proposition.c b/proposition.c index c3fc897..6f28fbe 100644 --- a/proposition.c +++ b/proposition.c @@ -6,6 +6,7 @@ prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t rela prop.propA = propA; prop.propB = propB; prop.relation = relation; + prop.isSimple = 0; return prop; } /* a simple proposition is one with only a name */ @@ -1,3 +1,3 @@ -P^Q | pr -L^V | pr -(P^Q)^(L^V) | ^i 1, 2 +P | pr +Q | pr +P->Q | ->I 2, 1 |