diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main.c | 4 | ||||
| -rw-r--r-- | src/parse.c | 2 | ||||
| -rw-r--r-- | src/reduce.c | 68 | ||||
| -rw-r--r-- | src/schedule.c | 1 | ||||
| -rw-r--r-- | src/term.c | 1 |
5 files changed, 20 insertions, 56 deletions
@@ -47,7 +47,7 @@ static char *read_path(const char *path) int main(int argc, char *argv[]) { -#if DEBUG +#ifdef DEBUG debug_enable(1); #endif @@ -64,9 +64,7 @@ int main(int argc, char *argv[]) schedule_sync_priorities(); - /* map_dump(map_all_terms()); */ debug("reducing...\n"); - schedule(); map_dump(map_all_terms(), 0); diff --git a/src/parse.c b/src/parse.c index b3840d3..e2d2498 100644 --- a/src/parse.c +++ b/src/parse.c @@ -22,7 +22,7 @@ static struct term_handle abs_blc(char **term, size_t depth) } else { res_term = term_new(res_type, res, depth); res_term->u.abs.term = inner.term; - // TODO: remove hash from map_set (already in term anyway)? + // TODO: remove hash from map_set (already in term anyway) map_set(map_all_terms(), res_term); } 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); } diff --git a/src/schedule.c b/src/schedule.c index 458d8a2..081acfe 100644 --- a/src/schedule.c +++ b/src/schedule.c @@ -55,6 +55,7 @@ static size_t choose_position(void) static pqueue_pri_t calculate_priority(struct term *term) { + // TODO: Try different formulas (hyperfine) return (parse_get_max_depth() - term->depth + 1) * term->refs; } @@ -111,6 +111,7 @@ struct term *term_rehash_abs(struct term *head, struct term *term, } // TODO: main problem is reparenting substitution tickle-up +// TODO: investigate reparenting using gen.blc? ?!!?! struct term *term_rehash_app(struct term *head, struct term *lhs, struct term *rhs, int including_parents) { |