#include <stdlib.h>
#include "parse.h"
#include "lexer.h"

line_t init_line(prop_t proposition, just_t justification) {
	line_t line;
	line.proposition = proposition;
	line.justification = justification;
	return line;
}
lineSet_t init_lineset(line_t* lines, int count) {
	lineSet_t lineSet;
	lineSet.lines = lines;
	lineSet.count = count;
	return lineSet;
}
int count_lines(char* content) {
	int i = 0;
	while (*content != '\0') {
		if (*content == '\n') {
			i++;
		}
		content++;
	}
	return i;
}
lineSet_t parse_lines(char* content, int lineCount) {
	line_t* lines = malloc(sizeof(line_t) * lineCount);
	for (int i = 0; i < lineCount; i++) {
		/* parse the line */
		lines[i] = parse_line(content);
		/* advance to the next line */
		while (*content != '\n') {
			content++;
		}
		content++;
	}
	return init_lineset(lines, lineCount);
}
line_t parse_line(char* content) {
	tokenSet_t ts = lex_line(content);
	int i = 0;
	while (ts.tokens[i].type != JUSTIFICATION) {
		i++;
	}
	int* seek = calloc(sizeof(int), 1);
	prop_t prop = parse_proposition(init_tokenset(ts.tokens, i), seek);
	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 prop;
	/* recurse to parse the parenthetical as its own proposition */
	if (tokenSet.tokens[*seek].type == OPEN_PAREN) {
		(*seek)++;
		prop = parse_proposition(tokenSet, seek);
	}
	else {
		prop = init_simple_prop(tokenSet.tokens[*seek].value);
		(*seek)++;
	}
	/* check if we were reading a simple prop, or if there is a relation */
	if (*seek == tokenSet.count || tokenSet.tokens[*seek].type == CLOSE_PAREN) {
		return prop;
	}
	else {
		/* the proposition we just read had a relation, so find the related proposition */
		tokenType_t rel = tokenSet.tokens[*seek].type;
		(*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);
		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));
	/* check the relation, then use a ternary operator for elim/intro */
	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);
}