checkpoint

6 files changed, 82 insertions, 25 deletions

diff --git a/inc/map.h b/inc/map.h
index 790d42f..53b0c98 100644
--- a/inc/map.h
+++ b/inc/map.h
@@ -9,8 +9,10 @@
 
 struct term *map_get(hash_t hash);
 void map_set(struct term *term, hash_t hash);
+void map_delete(struct term *term);
 void map_initialize(void);
 void map_destroy(void);
+void map_dump(void); // TODO: remove
 struct pqueue *map_to_pqueue(pqueue_cmp_pri_f cmppri, pqueue_get_pri_f getpri,
 			     pqueue_set_pos_f set_pos);
 
diff --git a/inc/term.h b/inc/term.h
index 5256b3c..c94894d 100644
--- a/inc/term.h
+++ b/inc/term.h
@@ -34,6 +34,7 @@ struct term *term_rehash_app(struct term *head, struct term *lhs,
 
 void term_refer_head(struct term *term, size_t depth);
 void term_refer(struct term *term, size_t depth);
+void term_deref_head(struct term *term);
 void term_deref(struct term *term);
 
 void term_print(struct term *term);
diff --git a/src/main.c b/src/main.c
index c60ebd2..47e88a9 100644
--- a/src/main.c
+++ b/src/main.c
@@ -59,9 +59,13 @@ int main(int argc, char *argv[])
 	free(orig_term);
 
 	term_print(handle.term);
+	fprintf(stderr, "\n");
 	struct term *new = reduce(handle.term);
-	fprintf(stderr, "\nafter\n");
+	fprintf(stderr, "after\n");
 	term_print(new);
+	fprintf(stderr, "\n");
+
+	map_dump();
 
 	/* schedule_init(); */
 	/* schedule(); */
diff --git a/src/map.c b/src/map.c
index 327af8d..c0a2f97 100644
--- a/src/map.c
+++ b/src/map.c
@@ -33,11 +33,30 @@ void map_initialize(void)
 	all_terms = hashmap_new(sizeof(struct term *), 0, hashmap_free_term);
 }
 
+void map_delete(struct term *term)
+{
+	hashmap_delete(all_terms, term->hash);
+}
+
 void map_destroy(void)
 {
 	hashmap_free(all_terms);
 }
 
+void map_dump(void)
+{
+	fprintf(stderr, "\n---\nMap dump:\n");
+	size_t iter = 0;
+	void *iter_val;
+	while (hashmap_iter(all_terms, &iter, &iter_val)) {
+		struct term *term = *(struct term **)iter_val;
+		fprintf(stderr, "%d ", term->type);
+		term_print(term);
+		fprintf(stderr, " %ld\n", term->refs);
+	}
+	fprintf(stderr, "---\n\n");
+}
+
 struct pqueue *map_to_pqueue(pqueue_cmp_pri_f cmppri, pqueue_get_pri_f getpri,
 			     pqueue_set_pos_f setpos)
 {
diff --git a/src/reduce.c b/src/reduce.c
index a927b12..f179ec4 100644
--- a/src/reduce.c
+++ b/src/reduce.c
@@ -10,27 +10,50 @@
 static struct term *substitute(struct term *term, struct term *substitution,
 			       size_t level)
 {
+	/* term_print(term); */
+	/* fprintf(stderr, " <- "); */
+	/* term_print(substitution); */
+	/* fprintf(stderr, " @ %ld\n", level); */
 	if (term->type == VAR && term->u.var.index == level) {
 		return substitution;
 	} else if (term->type == ABS) {
 		struct term *new =
 			substitute(term->u.abs.term, substitution, level + 1);
-		return term_rehash_abs(term, new);
+		if (term->u.abs.term->hash == substitution->hash)
+			return term;
+		term_deref(term->u.abs.term);
+		struct term *rehashed = term_rehash_abs(term, new);
+		term_deref_head(term);
+		return rehashed;
 	} else if (term->type == APP) {
 		struct term *lhs =
 			substitute(term->u.app.lhs, substitution, level);
 		struct term *rhs =
 			substitute(term->u.app.rhs, substitution, level);
-		return term_rehash_app(term, lhs, rhs);
+		if (term->u.app.lhs->hash == substitution->hash &&
+		    term->u.app.rhs->hash == substitution->hash)
+			return term;
+		if (term->u.app.lhs->hash != substitution->hash)
+			term_deref(term->u.app.lhs);
+		if (term->u.app.rhs->hash != substitution->hash)
+			term_deref(term->u.app.rhs);
+		struct term *rehashed = term_rehash_app(term, lhs, rhs);
+		term_deref_head(term);
+		return rehashed;
 	}
 	fatal("invalid type %d\n", term->type);
 }
 
+// APP: reduction of application
+// ([X],Y) -> X/Y
+//  (X,Y)  -> (RED(X),RED(Y))
 static struct term *reduce_app(struct term *term)
 {
 	if (term->u.app.lhs->type == ABS) {
-		return substitute(term->u.app.lhs->u.abs.term, term->u.app.rhs,
-				  0);
+		struct term *new = substitute(term->u.app.lhs->u.abs.term,
+					      term->u.app.rhs, -1);
+		term_deref_head(term);
+		return new;
 	} else {
 		struct term *lhs = reduce(term->u.app.lhs);
 		struct term *rhs = reduce(term->u.app.rhs);
@@ -38,11 +61,18 @@ static struct term *reduce_app(struct term *term)
 	}
 }
 
+// ABS: reduction of abstractions
+// [X] -> [RED(X)]
 static struct term *reduce_abs(struct term *term)
 {
-	return reduce(term->u.abs.term);
+	struct term *inner = reduce(term->u.abs.term);
+	return term_rehash_abs(term, inner);
 }
 
+// RED: main reduction
+// (X,Y) -> APP((X,Y))
+//  [X]  -> ABS([X])
+//   X   -> X
 struct term *reduce(struct term *term)
 {
 	if (term->type == APP) {
diff --git a/src/term.c b/src/term.c
index 64c58e8..1479134 100644
--- a/src/term.c
+++ b/src/term.c
@@ -46,8 +46,7 @@ void term_print(struct term *term)
 
 struct term *term_rehash_abs(struct term *head, struct term *term)
 {
-	if (head->u.abs.term->hash == term->hash)
-		return head;
+	/* assert(head->u.abs.term->hash != term->hash); */
 
 	hash_t res =
 		hash((uint8_t *)&head->type, sizeof(head->type), term->hash);
@@ -56,14 +55,10 @@ struct term *term_rehash_abs(struct term *head, struct term *term)
 
 	struct term *match = map_get(res);
 	if (match) { // already exists
-		term_refer(match, head->depth);
-		term_deref(head);
 		return match;
 	} else { // create new
 		struct term *new = term_new(ABS, res, head->depth);
 		new->u.abs.term = term;
-		term_refer(term, head->depth + 1);
-		term_deref(head);
 		map_set(new, res);
 		return new;
 	}
@@ -72,9 +67,8 @@ struct term *term_rehash_abs(struct term *head, struct term *term)
 struct term *term_rehash_app(struct term *head, struct term *lhs,
 			     struct term *rhs)
 {
-	if (head->u.app.lhs->hash == lhs->hash &&
-	    head->u.app.rhs->hash == rhs->hash)
-		return head;
+	/* assert(head->u.app.lhs->hash != lhs->hash || */
+	/*        head->u.app.rhs->hash != rhs->hash); */
 
 	hash_t res =
 		hash((uint8_t *)&head->type, sizeof(head->type), lhs->hash);
@@ -84,18 +78,18 @@ struct term *term_rehash_app(struct term *head, struct term *lhs,
 
 	struct term *match = map_get(res);
 	if (match) { // already exists
-		term_refer(match, head->depth);
-		term_deref(head);
+		/* term_refer(match, head->depth); */
+		/* term_deref(head); */
 		return match;
 	} else { // create new
 		struct term *new = term_new(APP, res, head->depth);
 		new->u.app.lhs = lhs;
 		new->u.app.rhs = rhs;
-		if (head->u.app.lhs->hash != lhs->hash)
-			term_refer(lhs, head->depth + 1);
-		if (head->u.app.rhs->hash != rhs->hash)
-			term_refer(rhs, head->depth + 1);
-		term_deref(head);
+		/* if (head->u.app.lhs->hash != lhs->hash) */
+		/* 	term_refer(lhs, head->depth + 1); */
+		/* if (head->u.app.rhs->hash != rhs->hash) */
+		/* 	term_refer(rhs, head->depth + 1); */
+		/* term_deref(head); */
 		map_set(new, res);
 		return new;
 	}
@@ -120,6 +114,15 @@ void term_refer(struct term *term, size_t depth)
 	term_refer_head(term, depth);
 }
 
+void term_deref_head(struct term *term)
+{
+	term->refs--;
+	if (term->refs == 0) {
+		map_delete(term);
+		free(term);
+	}
+}
+
 void term_deref(struct term *term)
 {
 	if (term->type == ABS) {
@@ -129,7 +132,5 @@ void term_deref(struct term *term)
 		term_deref(term->u.app.rhs);
 	}
 
-	// TODO: remove from hashmap?
-	if (--term->refs == 0)
-		free(term);
+	term_deref_head(term);
 }