diff options
Diffstat (limited to 'src/parse.c')
| -rw-r--r-- | src/parse.c | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/src/parse.c b/src/parse.c index cae66a0..fedd3ab 100644 --- a/src/parse.c +++ b/src/parse.c @@ -102,6 +102,9 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek, char isNegative) { (*seek)++; prop = parse_proposition(tokenSet, seek, 1); } + else if (tokenSet.tokens[*seek].type == CONTRADICTION) { + return init_contradiction_prop(); + } else { prop = init_simple_prop(isNegative, tokenSet.tokens[*seek].value); (*seek)++; @@ -141,6 +144,12 @@ just_t parse_justification(tokenSet_t tokenSet) { case IMPLICATION: just = tokenSet.tokens[1].type == ELIMINATION ? IMPLICATION_ELIM : IMPLICATION_INTRO; break; + case NEGATION: + just = tokenSet.tokens[1].type == ELIMINATION ? NEGATION_ELIM : NEGATION_INTRO; + break; + case CONTRADICTION: + just = tokenSet.tokens[1].type == ELIMINATION ? ERR_R : CONTRADICTION_INTRO; + break; default: return init_just(ERR_R, NULL, 0); } @@ -157,6 +166,15 @@ just_t parse_justification(tokenSet_t tokenSet) { return init_just(just, references, i); } char peq(prop_t prop1, prop_t prop2) { + if (prop1.isContradiction && prop2.isContradiction) { + /* both are contradictions */ + return 1; + } + if (prop1.isContradiction || prop1.isContradiction) { + /* only one is a contradiction */ + return 0; + } + /* neither are contradictions */ if (prop1.isSimple && prop2.isSimple) { /* both simple */ return strcmp(prop1.name, prop2.name) == 0 && prop1.isNegative == prop2.isNegative; @@ -170,6 +188,29 @@ char peq(prop_t prop1, prop_t prop2) { return prop1.isNegative == prop2.isNegative && prop1.relation == prop2.relation && peq(*prop1.propA, *prop2.propA) && peq(*prop1.propB, *prop2.propB); } } +char pbeq(prop_t prop1, prop_t prop2) { + if (prop1.isContradiction && prop2.isContradiction) { + /* both are contradictions */ + return 1; + } + if (prop1.isContradiction || prop1.isContradiction) { + /* only one is a contradiction */ + return 0; + } + /* neither are contradictions */ + if (prop1.isSimple && prop2.isSimple) { + /* both simple */ + return strcmp(prop1.name, prop2.name) == 0; + } + else if (prop1.isSimple || prop2.isSimple) { + /* only one simple */ + return 0; + } + else { + /* neither simple */ + return 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; |