blob: 0b9fd82712cc930f12a43d299c2d655ced917b0d (
plain) (
blame)
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
|
// Copyright (c) 2023, Marvin Borner <dev@marvinborner.de>
#include <stdio.h>
#include <parse.h>
#include <term.h>
static struct term *rec_bruijn(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_bruijn(term);
} else if (**term == '(') {
(*term)++;
res = new_term(APP);
res->u.app.lhs = rec_bruijn(term);
res->u.app.rhs = rec_bruijn(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_bruijn(term); // this is quite tolerant..
}
return res;
}
static struct term *rec_blc(const char **term)
{
struct term *res = 0;
if (!**term) {
fprintf(stderr, "invalid parsing state!\n");
} else if (**term == '0' && *(*term + 1) == '0') {
(*term) += 2;
res = new_term(ABS);
res->u.abs.term = rec_blc(term);
} else if (**term == '0' && *(*term + 1) == '1') {
(*term) += 2;
res = new_term(APP);
res->u.app.lhs = rec_blc(term);
res->u.app.rhs = rec_blc(term);
} else if (**term == '1') {
const char *cur = *term;
while (**term == '1')
(*term)++;
res = new_term(VAR);
res->u.var.name = *term - cur - 1;
res->u.var.type = BRUIJN_INDEX;
(*term)++;
} else {
(*term)++;
res = rec_blc(term); // this is quite tolerant..
}
return res;
}
struct term *parse_bruijn(const char *term)
{
struct term *parsed = rec_bruijn(&term);
to_barendregt(parsed);
return parsed;
}
struct term *parse_blc(const char *term)
{
struct term *parsed = rec_blc(&term);
to_barendregt(parsed);
return parsed;
}
|
