From 43bfe5935b3f1d38775c3bc65262aca5683c0fb5 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Sun, 11 Jun 2023 23:33:40 -0700 Subject: added parsing of justifications --- parse.c | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) (limited to 'parse.c') diff --git a/parse.c b/parse.c index ad839fc..d7ec467 100644 --- a/parse.c +++ b/parse.c @@ -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); +} -- cgit v1.3.1