diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lib/pqueue.c | 18 | ||||
| -rw-r--r-- | src/main.c | 19 | ||||
| -rw-r--r-- | src/map.c | 21 | ||||
| -rw-r--r-- | src/reduce.c | 6 | ||||
| -rw-r--r-- | src/schedule.c | 50 | ||||
| -rw-r--r-- | src/term.c | 2 |
6 files changed, 73 insertions, 43 deletions
diff --git a/src/lib/pqueue.c b/src/lib/pqueue.c index c080bb2..cf0611f 100644 --- a/src/lib/pqueue.c +++ b/src/lib/pqueue.c @@ -35,7 +35,8 @@ #define parent(i) ((i) >> 1) struct pqueue *pqueue_init(size_t n, pqueue_cmp_pri_f cmppri, - pqueue_get_pri_f getpri, pqueue_set_pos_f setpos) + pqueue_get_pri_f getpri, pqueue_set_pri_f setpri, + pqueue_get_pos_f getpos, pqueue_set_pos_f setpos) { struct pqueue *q; @@ -51,7 +52,9 @@ struct pqueue *pqueue_init(size_t n, pqueue_cmp_pri_f cmppri, q->size = 1; q->avail = q->step = (n + 1); /* see comment above about n+1 */ q->cmppri = cmppri; + q->setpri = setpri; q->getpri = getpri; + q->getpos = getpos; q->setpos = setpos; return q; @@ -144,6 +147,19 @@ int pqueue_insert(struct pqueue *q, void *d) return 0; } +void pqueue_change_priority(struct pqueue *q, pqueue_pri_t new_pri, void *d) +{ + size_t posn; + pqueue_pri_t old_pri = q->getpri(d); + + q->setpri(d, new_pri); + posn = q->getpos(d); + if (q->cmppri(old_pri, new_pri)) + bubble_up(q, posn); + else + percolate_down(q, posn); +} + void *pqueue_pop(struct pqueue *q) { void *head; @@ -53,24 +53,21 @@ int main(int argc, char *argv[]) char *term = read_path(argv[1]); map_initialize(); + schedule_initialize(); char *orig_term = term; - struct term_handle handle = parse_blc(&term, 1); + parse_blc(&term, 1); free(orig_term); - term_print(handle.term); - fprintf(stderr, "\n"); - struct term *reduced = reduce(handle.term->u.abs.term); - fprintf(stderr, "after\n"); - term_print(reduced); - fprintf(stderr, "\n"); + schedule_sync_priorities(); - map_dump(map_all_terms()); + /* map_dump(map_all_terms()); */ + debug("reducing...\n"); - /* schedule_init(); */ - /* schedule(); */ - /* schedule_destroy(); */ + schedule(); + map_dump(map_all_terms()); map_destroy(map_all_terms()); + schedule_destroy(); return 0; } @@ -6,6 +6,7 @@ #include <lib/hashmap.h> #include <map.h> #include <parse.h> +#include <schedule.h> static struct hashmap *all_terms; @@ -30,6 +31,8 @@ struct term *map_get(struct hashmap *map, hash_t hash) void map_set(struct hashmap *map, struct term *term) { + if (!hashmap_get(map, term->hash)) + schedule_add(term); // also add to schedule hashmap_set(map, &term, term->hash); } @@ -70,21 +73,3 @@ void map_dump(struct hashmap *map) } fprintf(stderr, "---\n\n"); } - -struct pqueue *map_to_pqueue(struct hashmap *map, pqueue_cmp_pri_f cmppri, - pqueue_get_pri_f getpri, pqueue_set_pos_f setpos) -{ - size_t size = hashmap_count(map) + 42; - struct pqueue *queue = pqueue_init(size, cmppri, getpri, setpos); - - size_t iter = 0; - void *iter_val; - while (hashmap_iter(map, &iter, &iter_val)) { - struct term *term = *(struct term **)iter_val; - if (term->type == APP && term->u.app.lhs->type == ABS) { - pqueue_insert(queue, term); - } - } - - return queue; -} diff --git a/src/reduce.c b/src/reduce.c index aa17655..9e7520d 100644 --- a/src/reduce.c +++ b/src/reduce.c @@ -11,12 +11,6 @@ static struct term *substitute(struct term *term, struct term *substitution, size_t level) { - /* fprintf(stderr, "substitute: "); */ - /* term_print(term); */ - /* fprintf(stderr, " with "); */ - /* term_print(substitution); */ - /* fprintf(stderr, " at level %ld\n", level); */ - if (term->type == VAR) { if (term->u.var.index == level) { // TODO: deref index diff --git a/src/schedule.c b/src/schedule.c index 3465752..93cd700 100644 --- a/src/schedule.c +++ b/src/schedule.c @@ -18,7 +18,13 @@ static struct pqueue *queue; static pqueue_pri_t get_pri(void *a) { struct term *term = a; - return (parse_get_max_depth() - term->depth + 1) * term->refs; + return term->priority; +} + +static void set_pri(void *a, pqueue_pri_t pri) +{ + struct term *term = a; + term->priority = pri; } static int cmp_pri(pqueue_pri_t next, pqueue_pri_t curr) @@ -26,10 +32,16 @@ static int cmp_pri(pqueue_pri_t next, pqueue_pri_t curr) return next < curr; } +static size_t get_pos(void *a) +{ + struct term *term = a; + return term->position; +} + static void set_pos(void *a, size_t position) { - (void)a; - (void)position; + struct term *term = a; + term->position = position; } // skewed random number generator @@ -40,6 +52,20 @@ static size_t choose_position(void) return size - (size_t)sqrt(((size_t)rand() % (size_t)pow(size, 2))); } +static pqueue_pri_t calculate_priority(struct term *term) +{ + return (parse_get_max_depth() - term->depth + 1) * term->refs; +} + +void schedule_add(struct term *term) +{ + if (!(term->type == APP && term->u.app.lhs->type == ABS)) + return; // no beta redex + + set_pri(term, calculate_priority(term)); + pqueue_insert(queue, term); +} + void schedule(void) { while (pqueue_size(queue) > 0) { @@ -51,10 +77,24 @@ void schedule(void) debug("no more redexes!\n"); } -void schedule_init(void) +void schedule_sync_priorities(void) +{ + size_t iter = 0; + void *iter_val; + while (hashmap_iter(map_all_terms(), &iter, &iter_val)) { + struct term *term = *(struct term **)iter_val; + if (term->type == APP && term->u.app.lhs->type == ABS) { + pqueue_change_priority(queue, calculate_priority(term), + term); + } + } +} + +void schedule_initialize(void) { srand(time(0)); - queue = map_to_pqueue(map_all_terms(), cmp_pri, get_pri, set_pos); + size_t size = hashmap_count(map_all_terms()) + 42; + queue = pqueue_init(size, cmp_pri, get_pri, set_pri, get_pos, set_pos); } void schedule_destroy(void) @@ -143,10 +143,8 @@ void term_rehash_parents(struct term *term) parents = new; } - fprintf(stderr, "NEW\n"); struct parent_list *iterator = parents; while (iterator && iterator->term) { - fprintf(stderr, "rehashing parent\n"); struct term *parent = iterator->term; hash_t previous = parent->hash; struct term *new = term_rehash(parent); |