More parenting

1 files changed, 23 insertions, 17 deletions

diff --git a/src/reduce.c b/src/reduce.c
index 1cfb520..aa17655 100644
--- a/src/reduce.c
+++ b/src/reduce.c
@@ -11,42 +11,48 @@
 static struct term *substitute(struct term *term, struct term *substitution,
 			       size_t level)
 {
-	if (term->type == VAR && term->u.var.index == level) {
-		return substitution;
+	/* 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
+			return substitution;
+		} else {
+			return term;
+		}
 	} else if (term->type == ABS) {
 		struct term *new =
 			substitute(term->u.abs.term, substitution, level + 1);
-		if (term->u.abs.term->hash == substitution->hash)
-			return term;
-		/* term_deref(term->u.abs.term); */
+		if (term->u.abs.term->hash == new->hash)
+			return term; // nothing changed
 		struct term *rehashed = term_rehash_abs(term, new);
-		/* term_deref_head(term); */
+		term_rehash_parents(rehashed);
 		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);
-		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); */
+		if (term->u.app.lhs->hash == lhs->hash &&
+		    term->u.app.rhs->hash == rhs->hash)
+			return term; // nothing changed
 		struct term *rehashed = term_rehash_app(term, lhs, rhs);
-		/* term_deref_head(term); */
+		term_rehash_parents(rehashed);
 		return rehashed;
 	}
 	fatal("invalid type %d\n", term->type);
 }
 
 // reduction of application
-// ([X],Y) -> X/Y
-void reduce(struct term *term)
+// ([X] Y) -> X/Y
+struct term *reduce(struct term *term)
 {
 	assert(term->type == APP);
 	assert(term->u.app.lhs->type == ABS);
 
-	substitute(term->u.app.lhs->u.abs.term, term->u.app.rhs, 0);
+	return substitute(term->u.app.lhs, term->u.app.rhs, -1);
 }