1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
#include <stdlib.h>
#include "parse.h"
#include "lexer.h"
#include "stdio.h"
line_t init_line(int aLevel, prop_t proposition, just_t justification) {
line_t line;
line.aLevel = aLevel;
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 c = 0;
int indent = 0;
while (ts.tokens[c].type != JUSTIFICATION) {
if (ts.tokens[c].type == INDENT) {
indent++;
}
c++;
}
int* seek = calloc(sizeof(int), 1);
prop_t prop = parse_proposition(init_tokenset(ts.tokens + indent, c - indent), seek, 0);
just_t just = parse_justification(init_tokenset(ts.tokens + c + 1, ts.count - (c + 1)));
free(seek);
return init_line(indent, prop, just);
}
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, 0);
}
else if (tokenSet.tokens[*seek].type == NEGATION) {
(*seek)++;
prop = parse_proposition(tokenSet, seek, 1);
}
else {
prop = init_simple_prop(isNegative, 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, 0);
prop_t metaProp = init_prop(0, 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);
}
|
