diff options
Diffstat (limited to 'src/reduce.c')
-rw-r--r-- | src/reduce.c | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/src/reduce.c b/src/reduce.c index 9e7520d..38baf06 100644 --- a/src/reduce.c +++ b/src/reduce.c @@ -4,6 +4,7 @@ #include <stdio.h> #include <term.h> +#include <map.h> #include <reduce.h> #include <log.h> #include <assert.h> @@ -13,26 +14,28 @@ static struct term *substitute(struct term *term, struct term *substitution, { if (term->type == VAR) { if (term->u.var.index == level) { - // TODO: deref index + term_deref_head(term); return substitution; } else { return term; } } else if (term->type == ABS) { + hash_t previous = term->u.abs.term->hash; struct term *new = substitute(term->u.abs.term, substitution, level + 1); - if (term->u.abs.term->hash == new->hash) + if (previous == new->hash) return term; // nothing changed struct term *rehashed = term_rehash_abs(term, new); term_rehash_parents(rehashed); return rehashed; } else if (term->type == APP) { + hash_t previous_lhs = term->u.app.lhs->hash; + hash_t previous_rhs = term->u.app.rhs->hash; struct term *lhs = substitute(term->u.app.lhs, substitution, level); struct term *rhs = substitute(term->u.app.rhs, substitution, level); - if (term->u.app.lhs->hash == lhs->hash && - term->u.app.rhs->hash == rhs->hash) + if (previous_lhs == lhs->hash && previous_rhs == rhs->hash) return term; // nothing changed struct term *rehashed = term_rehash_app(term, lhs, rhs); term_rehash_parents(rehashed); @@ -45,8 +48,12 @@ static struct term *substitute(struct term *term, struct term *substitution, // ([X] Y) -> X/Y struct term *reduce(struct term *term) { - assert(term->type == APP); - assert(term->u.app.lhs->type == ABS); + if (term->type != APP || term->u.app.lhs->type != ABS) + fatal("can't reduce non-beta-redex %d\n", term->type); - return substitute(term->u.app.lhs, term->u.app.rhs, -1); + map_delete(term->u.app.lhs->parents, term); + map_delete(term->u.app.rhs->parents, term); + struct term *reduced = substitute(term->u.app.lhs, term->u.app.rhs, -1); + term_deref_head(term); + return reduced; } |