// Copyright (c) 2023, Marvin Borner // SPDX-License-Identifier: MIT #include #include #include #include #include #include static struct term *substitute(struct term *term, struct term *substitution, size_t level) { if (term->type == VAR) { if (term->u.var.index == level) { 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 (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 (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); return rehashed; } fatal("invalid type %d\n", term->type); } // reduction of application // ([X] Y) -> X/Y struct term *reduce(struct term *term) { if (term->type != APP || term->u.app.lhs->type != ABS) fatal("can't reduce non-beta-redex %d\n", term->type); 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; }