diff options
| -rw-r--r-- | inc/reducer.h | 8 | ||||
| -rw-r--r-- | inc/term.h | 7 | ||||
| -rw-r--r-- | readme.md | 2 | ||||
| -rw-r--r-- | src/main.c | 1 | ||||
| -rw-r--r-- | src/parse.c | 36 | ||||
| -rw-r--r-- | src/reducer.c | 6 | ||||
| -rw-r--r-- | src/term.c | 4 |
7 files changed, 57 insertions, 7 deletions
diff --git a/inc/reducer.h b/inc/reducer.h new file mode 100644 index 0000000..28fe8b1 --- /dev/null +++ b/inc/reducer.h @@ -0,0 +1,8 @@ +#ifndef REDUCER_H +#define REDUCER_H + +#include <term.h> + +struct term *reduce(struct term *term); + +#endif @@ -1,20 +1,23 @@ #ifndef TERM_H #define TERM_H -typedef int bruijn; typedef enum { INV, ABS, APP, VAR } term_type; struct term { term_type type; union { struct { + int name; struct term *term; } abs; struct { struct term *lhs; struct term *rhs; } app; - bruijn var; + struct { + int name; + enum { BRUIJN_INDEX, BARENDREGT_VARIABLE } type; + } var; } u; }; @@ -12,7 +12,7 @@ ## Research -In no particular order: +Interesting/relevant research in no particular order: 0. Biernacka, M., Charatonik, W., & Drab, T. (2022). A simple and efficient implementation of strong call by need by an abstract @@ -7,6 +7,7 @@ int main(void) { struct term *term = parse("([[((0 1) [(1 0)])]] [0])"); print_term(term); + printf("\n"); free_term(term); return 0; } diff --git a/src/parse.c b/src/parse.c index 495f55f..306bf4f 100644 --- a/src/parse.c +++ b/src/parse.c @@ -6,6 +6,12 @@ #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; @@ -22,7 +28,8 @@ static struct term *rec(const char **term) res->u.app.rhs = rec(term); } else if (**term >= '0' && **term <= '9') { res = new_term(VAR); - res->u.var = **term - '0'; + res->u.var.name = **term - '0'; + res->u.var.type = BRUIJN_INDEX; (*term)++; } else { (*term)++; @@ -31,7 +38,32 @@ static struct term *rec(const char **term) 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) { - return rec(&term); + struct term *parsed = rec(&term); + to_barendregt(parsed, -1, -1); + return parsed; } diff --git a/src/reducer.c b/src/reducer.c new file mode 100644 index 0000000..e74946b --- /dev/null +++ b/src/reducer.c @@ -0,0 +1,6 @@ +#include <reducer.h> + +struct term *reduce(struct term *term) +{ + return term; +} @@ -38,7 +38,7 @@ void print_term(struct term *term) { switch (term->type) { case ABS: - printf("["); + printf("[{%d} ", term->u.abs.name); print_term(term->u.abs.term); printf("]"); break; @@ -50,7 +50,7 @@ void print_term(struct term *term) printf(")"); break; case VAR: - printf("%d", term->u.var); + printf("%d", term->u.var.name); break; default: fprintf(stderr, "Invalid type %d\n", term->type); |