1 files changed, 35 insertions, 5 deletions

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) {