diff options
| -rw-r--r-- | lexer.c | 10 | ||||
| -rw-r--r-- | lexer.h | 1 | ||||
| -rw-r--r-- | operetta.c | 3 | ||||
| -rw-r--r-- | parse.c | 16 | ||||
| -rw-r--r-- | parse.h | 2 | ||||
| -rw-r--r-- | proposition.c | 6 | ||||
| -rw-r--r-- | proposition.h | 7 | ||||
| -rw-r--r-- | testfile | 4 |
8 files changed, 35 insertions, 14 deletions
@@ -35,12 +35,18 @@ char* tttos(tokenType_t tokenType) { 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 "???"; } @@ -128,6 +134,10 @@ token_t lex_first_token(char** content) { 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); @@ -11,6 +11,7 @@ typedef enum TokenType { JUSTIFICATION, PREMISE, ASSUMPTION, + NEGATION, CONJUNCTION, DISJUNCTION, IMPLICATION, @@ -20,6 +20,9 @@ int main(int argc, char** argv) { free(content); } void write_prop(prop_t prop) { + if (prop.isNegative) { + printf("%s", "!"); + } if (prop.isSimple) { printf("%s", prop.name); } @@ -44,19 +44,23 @@ line_t parse_line(char* content) { i++; } int* seek = calloc(sizeof(int), 1); - prop_t prop = parse_proposition(init_tokenset(ts.tokens, i), seek); + prop_t prop = parse_proposition(init_tokenset(ts.tokens, i), seek, 0); 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) { +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); + 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(tokenSet.tokens[*seek].value); + prop = init_simple_prop(isNegative, tokenSet.tokens[*seek].value); (*seek)++; } /* check if we were reading a simple prop, or if there is a relation */ @@ -70,8 +74,8 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek) { prop_t* prop1p = malloc(sizeof(prop_t)); *prop1p = prop; prop_t* prop2p = malloc(sizeof(prop_t)); - *prop2p = parse_proposition(tokenSet, seek); - prop_t metaProp = init_prop(prop1p, prop2p, rel); + *prop2p = parse_proposition(tokenSet, seek, 0); + prop_t metaProp = init_prop(0, prop1p, prop2p, rel); return metaProp; } } @@ -14,6 +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* seek); +prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative); just_t parse_justification(tokenSet_t tokenSet); #endif diff --git a/proposition.c b/proposition.c index 2c1410c..c3fc897 100644 --- a/proposition.c +++ b/proposition.c @@ -1,15 +1,17 @@ #include "proposition.h" /* a proposition defines a relation between two propositions */ -prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation) { +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; return prop; } /* a simple proposition is one with only a name */ -prop_t init_simple_prop(char* name) { +prop_t init_simple_prop(char isNegative, char* name) { prop_t prop; + prop.isNegative = isNegative; prop.name = name; prop.isSimple = 1; return prop; diff --git a/proposition.h b/proposition.h index 95f377c..2d09688 100644 --- a/proposition.h +++ b/proposition.h @@ -2,14 +2,15 @@ #define PROPOSITION #include "lexer.h" typedef struct Proposition { + char isSimple; + char isNegative; struct Proposition* propA; struct Proposition* propB; tokenType_t relation; char* name; - char isSimple; } prop_t; -prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation); -prop_t init_simple_prop(char* name); +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, @@ -1,3 +1,3 @@ -QvP | pr +Q | pr KAI^PRESTON | as -CATv(DOG^RABBIT) | ^e 1 2 +~CAT->(DOG^~RABBIT) | ^e 1 2 |