diff options
| -rw-r--r-- | inc/term.h | 3 | ||||
| -rw-r--r-- | makefile | 6 | ||||
| -rw-r--r-- | src/main.c | 4 | ||||
| -rw-r--r-- | src/parse.c | 2 | ||||
| -rw-r--r-- | src/reducer.c | 169 |
5 files changed, 180 insertions, 4 deletions
@@ -1,7 +1,7 @@ #ifndef TERM_H #define TERM_H -typedef enum { INV, ABS, APP, VAR } term_type; +typedef enum { INV, ABS, APP, VAR, CLO, CACHE } term_type; struct term { term_type type; @@ -18,6 +18,7 @@ struct term { int name; enum { BRUIJN_INDEX, BARENDREGT_VARIABLE } type; } var; + void *other; } u; }; @@ -13,9 +13,9 @@ OBJS = $(patsubst $(SRC)/%.c, $(BUILD)/%.o, $(SRCS)) # I need the following on my machine. Look it up though before using it. # export ASAN_OPTIONS=verify_asan_link_order=0 -CFLAGS_DEBUG = -Wno-error -ggdb3 -Og -Wno-unused -fsanitize=address -fsanitize=undefined -fstack-protector-all +CFLAGS_DEBUG = -Wno-error -ggdb3 -Og -Wno-unused -fsanitize=address -fsanitize=undefined -fstack-protector-all $(CFLAGS_TEST) CFLAGS_WARNINGS = -Wall -Wextra -Werror -Wshadow -Wpointer-arith -Wwrite-strings -Wredundant-decls -Wnested-externs -Wformat=2 -Wmissing-declarations -Wstrict-prototypes -Wmissing-prototypes -Wcast-qual -Wswitch-default -Wswitch-enum -Wunreachable-code -Wundef -Wold-style-definition -Wvla -pedantic -Wno-switch-enum -CFLAGS = $(CFLAGS_WARNINGS) -std=c99 -fno-profile-generate -fno-omit-frame-pointer -fno-common -fno-asynchronous-unwind-tables -mno-red-zone -Ofast -D_DEFAULT_SOURCE -I$(INC) $(CFLAGS_DEBUG) +CFLAGS = $(CFLAGS_WARNINGS) -std=c99 -fno-profile-generate -fno-omit-frame-pointer -fno-common -fno-asynchronous-unwind-tables -mno-red-zone -Ofast -D_DEFAULT_SOURCE -I$(INC) #$(CFLAGS_DEBUG) all: compile sync @@ -25,6 +25,8 @@ compile: $(BUILD) $(OBJS) $(BUILD)/milcr clean: @rm -rf $(BUILD)/* +test: + sync: # Ugly hack @$(MAKE) $(BUILD)/milcr --always-make --dry-run | grep -wE 'gcc|g\+\+' | grep -w '\-c' | jq -nR '[inputs|{directory:".", command:., file: match(" [^ ]+$$").string[1:]}]' >compile_commands.json @$(TG) -R --exclude=.git --exclude=build . @@ -2,11 +2,15 @@ #include <parse.h> #include <term.h> +#include <reducer.h> int main(void) { struct term *term = parse("([[((0 1) [(1 0)])]] [0])"); print_term(term); + printf("\nReduced:\n"); + struct term *reduced = reduce(term); + print_term(reduced); printf("\n"); free_term(term); return 0; diff --git a/src/parse.c b/src/parse.c index 306bf4f..016b5e9 100644 --- a/src/parse.c +++ b/src/parse.c @@ -64,6 +64,6 @@ static void to_barendregt(struct term *term, int level, int replacement) struct term *parse(const char *term) { struct term *parsed = rec(&term); - to_barendregt(parsed, -1, -1); + to_barendregt(parsed, -1, -name_generator()); return parsed; } diff --git a/src/reducer.c b/src/reducer.c index e74946b..412dfb3 100644 --- a/src/reducer.c +++ b/src/reducer.c @@ -1,6 +1,175 @@ +// based on the RKNL abstract machine +#include <stdlib.h> +#include <assert.h> +#include <stdio.h> + #include <reducer.h> +#include <term.h> + +struct stack { + void *data; + struct stack *next; +}; + +#define STORE_SIZE 128 // hashmap +struct store { + struct stack *stack; +}; + +struct store_data { + int key; + void *data; +}; + +struct closure { + struct term *term; + struct store *store; +}; + +struct box { + enum { TODO, DONE } state; + void *data; +}; + +struct cache { + struct box *box; + struct term *term; +}; + +struct conf { + enum { CLOSURE, COMPUTED } type; + union { + struct { // closure + struct term *term; + struct store *store; + struct stack *stack; + } econf; // blue + + struct { // computed + struct stack *stack; + void *term; + } cconf; // green + } u; +}; + +static struct stack *stack_push(struct stack *stack, void *data) +{ + struct stack *new = malloc(sizeof(*new)); + new->data = data; + new->next = stack; + return new; +} + +static struct store *store_push(struct store *store, int key, void *data) +{ + struct store *elem = &store[key % STORE_SIZE]; + struct store_data *keyed = malloc(sizeof(*keyed)); + keyed->key = key; + keyed->data = data; + elem->stack = stack_push(elem->stack, keyed); + return store; +} + +static void *store_get(struct store *store, int key) +{ + struct store *elem = &store[key % STORE_SIZE]; + struct stack *iterator = elem->stack; + while (iterator) { + struct store_data *keyed = (struct store_data *)iterator->data; + if (keyed->key == key) + return keyed->data; + iterator = iterator->next; + } + return 0; +} + +static int trans(struct conf *conf) +{ + if (conf->type == CLOSURE) { + struct term *term = conf->u.econf.term; + struct store *store = conf->u.econf.store; + struct stack *stack = conf->u.econf.stack; + switch (term->type) { + case APP: // (1) + conf->type = CLOSURE; + conf->u.econf.term = term->u.app.lhs; + struct term *app = new_term(APP); + app->u.app.lhs = new_term(VAR); + app->u.app.rhs = new_term(CLO); + struct closure *closure = malloc(sizeof(*closure)); + closure->term = term->u.app.rhs; + closure->store = store; + app->u.app.rhs->u.other = closure; + conf->u.econf.stack = + stack_push(conf->u.econf.stack, app); + break; + case ABS: // (2) + conf->type = COMPUTED; + conf->u.cconf.stack = stack; + conf->u.cconf.term = new_term(CACHE); + struct cache *cache = malloc(sizeof(*cache)); + struct box *box = malloc(sizeof(*box)); + box->state = TODO; + box->data = 0; + cache->box = box; + closure = malloc(sizeof(*closure)); + closure->term = term; + closure->store = store; + cache->term = new_term(CLO); + cache->term->u.other = closure; + conf->u.cconf.term = cache; + break; + case VAR: + box = store_get(store, term->u.var.name); + if (!box) { + box = malloc(sizeof(*box)); + box->state = DONE; + box->data = term; + } + if (box->state != DONE) { // (3) + assert(box->state == TODO && + ((struct term *)box->data)->type == CLO); + closure = ((struct term *)box->data)->u.other; + conf->type = CLOSURE; + conf->u.econf.term = closure->term; + conf->u.econf.store = closure->store; + cache = malloc(sizeof(*cache)); + cache->box = box; + cache->term = new_term(VAR); + conf->u.econf.stack = + stack_push(conf->u.econf.stack, cache); + } else { // (4) + conf->type = COMPUTED; + conf->u.cconf.stack = stack; + conf->u.cconf.term = box->data; + } + break; + default: + fprintf(stderr, "Invalid type %d\n", term->type); + break; + } + } else if (conf->type == COMPUTED) { + // somewhere return 1 + } + return 0; +} + +static struct conf *for_each_state(struct conf *conf) +{ + int ret = trans(conf); + return ret ? conf : for_each_state(conf); +} struct term *reduce(struct term *term) { + struct stack stack = { 0 }; + struct stack store[STORE_SIZE] = { 0 }; + struct conf econf = { + .type = CLOSURE, + .u.econf.term = term, + .u.econf.store = (struct store *)store, + .u.econf.stack = &stack, + }; + for_each_state(&econf); return term; } |