diff options
Diffstat (limited to 'inc')
| -rw-r--r-- | inc/lib/pqueue.h | 10 | ||||
| -rw-r--r-- | inc/schedule.h | 1 | ||||
| -rw-r--r-- | inc/term.h | 1 |
3 files changed, 11 insertions, 1 deletions
diff --git a/inc/lib/pqueue.h b/inc/lib/pqueue.h index 732002e..02988ce 100644 --- a/inc/lib/pqueue.h +++ b/inc/lib/pqueue.h @@ -105,7 +105,7 @@ size_t pqueue_size(struct pqueue *q); int pqueue_insert(struct pqueue *q, void *d); /** - * move an existing entry to a different priority + * move an existing entry to a different priority. * @param q the queue * @param new_pri the new priority * @param d the entry @@ -113,6 +113,14 @@ int pqueue_insert(struct pqueue *q, void *d); void pqueue_change_priority(struct pqueue *q, pqueue_pri_t new_pri, void *d); /** + * remove an item from the queue. + * @param q the queue + * @param d the item + * @return 0 on success + */ +int pqueue_remove(struct pqueue *q, void *d); + +/** * pop the highest-ranking item from the queue. * @param q the queue * @return NULL on error, otherwise the entry diff --git a/inc/schedule.h b/inc/schedule.h index eaf1e0c..9151d49 100644 --- a/inc/schedule.h +++ b/inc/schedule.h @@ -9,6 +9,7 @@ void schedule_initialize(void); void schedule_sync_priorities(void); void schedule_add(struct term *term); +void schedule_remove(struct term *term); void schedule(void); void schedule_destroy(void); @@ -35,6 +35,7 @@ struct term { }; struct term *term_new(term_type_t type, hash_t hash, size_t depth); +char term_is_beta_redex(struct term *term); void term_rehash_parents(struct term *term); struct term *term_rehash(struct term *term); struct term *term_rehash_abs(struct term *head, struct term *term); |