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
|
// Just for debugging purposes
// -> parses custom bruijn syntax
#include <stdio.h>
#include <parse.h>
#include <term.h>
static int name_generator(void)
{
static int current = 0x424242; // TODO: idk?
return current++;
}
static struct term *rec(const char **term)
{
struct term *res = 0;
if (!**term) {
fprintf(stderr, "invalid parsing state!\n");
} else if (**term == '[') {
(*term)++;
res = new_term(ABS);
res->u.abs.term = rec(term);
} else if (**term == '(') {
(*term)++;
res = new_term(APP);
res->u.app.lhs = rec(term);
res->u.app.rhs = rec(term);
} else if (**term >= '0' && **term <= '9') {
res = new_term(VAR);
res->u.var.name = **term - '0';
res->u.var.type = BRUIJN_INDEX;
(*term)++;
} else {
(*term)++;
res = rec(term); // this is quite tolerant..
}
return res;
}
// TODO: WARNING: This might not be 100% correct! Verify!
static void to_barendregt(struct term *term, int level, int replacement)
{
switch (term->type) {
case ABS:
term->u.abs.name = name_generator();
to_barendregt(term->u.abs.term, level + 1, term->u.abs.name);
break;
case APP:
to_barendregt(term->u.app.lhs, level, replacement);
to_barendregt(term->u.app.rhs, level, replacement);
break;
case VAR:
if (term->u.var.type == BRUIJN_INDEX) {
term->u.var.name = replacement - term->u.var.name;
term->u.var.type = BARENDREGT_VARIABLE;
}
break;
default:
fprintf(stderr, "Invalid type %d\n", term->type);
}
}
struct term *parse(const char *term)
{
struct term *parsed = rec(&term);
to_barendregt(parsed, -1, -name_generator());
return parsed;
}
|
