diff options
Diffstat (limited to 'src/reduce.c')
| -rw-r--r-- | src/reduce.c | 68 |
1 files changed, 16 insertions, 52 deletions
diff --git a/src/reduce.c b/src/reduce.c index f693645..7cbc944 100644 --- a/src/reduce.c +++ b/src/reduce.c @@ -16,15 +16,15 @@ static struct term *shift(struct term *term, size_t level, size_t amount) if (term->type == VAR) { if (level > term->u.var.index) return term; - /* term->refs += 1; // TODO: Kinda hacky */ - return term_rehash_var(term, term->u.var.index + amount); + term->refs += 1; // TODO: Kinda hacky + return term_rehash_var(term, term->u.var.index + amount, 0); } else if (term->type == ABS) { struct term *previous = term->u.abs.term; struct term *new = shift(term->u.abs.term, level + 1, amount); if (previous->hash == new->hash) return term; // nothing changed - /* term->refs += 1; */ - return term_rehash_abs(term, new); + term->refs += 1; + return term_rehash_abs(term, new, 0); } else if (term->type == APP) { hash_t previous_lhs = term->u.app.lhs->hash; hash_t previous_rhs = term->u.app.rhs->hash; @@ -32,84 +32,50 @@ static struct term *shift(struct term *term, size_t level, size_t amount) struct term *rhs = shift(term->u.app.rhs, level, amount); if (previous_lhs == lhs->hash && previous_rhs == rhs->hash) return term; // nothing changed - /* term->refs += 1; */ - return term_rehash_app(term, lhs, rhs); + term->refs += 1; + return term_rehash_app(term, lhs, rhs, 0); } fatal("invalid type %d\n", term->type); } -// TODO: remove or to enum -struct substitution_state { - int a; -}; - // only substitutes (and therefore increments indices and rehashes) -// TODO: formalize (write all rules) -// TODO: fix inc.bruijn -// TODO: fix unbound.bruijn -// TODO: try [([[1 1]] [[1]])] -// TODO: fix reparenting static struct term *substitute(struct term *term, struct term *substitution, - size_t level, struct substitution_state *state) + size_t level) { debug("substituting %lx with %lx\n", term->hash & HASH_MASK, substitution->hash & HASH_MASK); if (term->type == VAR) { if (level == term->u.var.index) { // replace by shifted term - state->a = 1; struct term *shifted = shift(substitution, 0, level); - if (shifted->hash != substitution->hash) { - state->a = 4; - } return shifted; } else if (level > term->u.var.index) { // crush unbound - state->a = 2; - term_deref(substitution, 1); return term; } else { // shift idx by -1 - state->a = 3; struct term *shifted = shift(term, 0, -1); - term_deref(substitution, 1); return shifted; } } else if (term->type == ABS) { - /* struct term *previous = term->u.abs.term; */ + struct term *previous = term->u.abs.term; hash_t previous_hash = term->u.abs.term->hash; /* term->refs += 1; */ /* previous->refs += 1; */ - struct term *new = substitute(term->u.abs.term, substitution, - level + 1, state); + struct term *new = + substitute(term->u.abs.term, substitution, level + 1); if (previous_hash == new->hash) - return term; // nothing changed - struct term *rehashed = term_rehash_abs(term, new); + return new; // nothing changed + struct term *rehashed = term_rehash_abs(term, new, 1); term_rehash_parents(rehashed); - if (state->a == 3) { - /* term_deref_head(previous, 1); */ - /* term_deref_head(previous, 1); */ - /* term->refs -= 1; */ - state->a = 0; - } - if (state->a == 1) { - /* term_deref_head(previous, 1); */ - /* term_deref_head(previous, 1); */ - state->a = 0; - } - if (state->a == 4) { - /* term_deref_head(term, 0); */ - /* term_deref_head(previous, 0); */ - state->a = 0; - } return rehashed; } else if (term->type == APP) { // no beta reduction; just substitution 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, state); + substitute(term->u.app.lhs, substitution, level); struct term *rhs = - substitute(term->u.app.rhs, substitution, level, state); + substitute(term->u.app.rhs, substitution, level); if (previous_lhs == lhs->hash && previous_rhs == rhs->hash) return term; // nothing changed - struct term *rehashed = term_rehash_app(term, lhs, rhs); + struct term *rehashed = term_rehash_app(term, lhs, rhs, 1); term_rehash_parents(rehashed); return rehashed; } @@ -124,7 +90,5 @@ struct term *reduce(struct term *term) fatal("can't reduce non-beta-redex %d\n", term->type); debug("reducing %lx\n", term->hash & HASH_MASK); - - struct substitution_state state = { 0 }; - return substitute(term->u.app.lhs, term->u.app.rhs, -1, &state); + return substitute(term->u.app.lhs, term->u.app.rhs, -1); } |