diff options
Diffstat (limited to 'parse.c')
| -rw-r--r-- | parse.c | 34 |
1 files changed, 33 insertions, 1 deletions
@@ -45,7 +45,7 @@ line_t parse_line(char* content) { } int* seek = calloc(sizeof(int), 1); prop_t prop = parse_proposition(init_tokenset(ts.tokens, i), seek); - just_t just; + 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) { @@ -73,3 +73,35 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek) { 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)); + 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); +} |