Added parent hashmaps

1 files changed, 13 insertions, 47 deletions

diff --git a/src/reduce.c b/src/reduce.c
index f179ec4..1cfb520 100644
--- a/src/reduce.c
+++ b/src/reduce.c
@@ -6,14 +6,11 @@
 #include <term.h>
 #include <reduce.h>
 #include <log.h>
+#include <assert.h>
 
 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) {
@@ -21,9 +18,9 @@ static struct term *substitute(struct term *term, struct term *substitution,
 			substitute(term->u.abs.term, substitution, level + 1);
 		if (term->u.abs.term->hash == substitution->hash)
 			return term;
-		term_deref(term->u.abs.term);
+		/* term_deref(term->u.abs.term); */
 		struct term *rehashed = term_rehash_abs(term, new);
-		term_deref_head(term);
+		/* term_deref_head(term); */
 		return rehashed;
 	} else if (term->type == APP) {
 		struct term *lhs =
@@ -33,54 +30,23 @@ static struct term *substitute(struct term *term, struct term *substitution,
 		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 != 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);
+		/* term_deref_head(term); */
 		return rehashed;
 	}
 	fatal("invalid type %d\n", term->type);
 }
 
-// APP: reduction of application
+// reduction of application
 // ([X],Y) -> X/Y
-//  (X,Y)  -> (RED(X),RED(Y))
-static struct term *reduce_app(struct term *term)
+void reduce(struct term *term)
 {
-	if (term->u.app.lhs->type == ABS) {
-		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);
-		return term_rehash_app(term, lhs, rhs);
-	}
-}
-
-// ABS: reduction of abstractions
-// [X] -> [RED(X)]
-static struct term *reduce_abs(struct term *term)
-{
-	struct term *inner = reduce(term->u.abs.term);
-	return term_rehash_abs(term, inner);
-}
+	assert(term->type == APP);
+	assert(term->u.app.lhs->type == ABS);
 
-// RED: main reduction
-// (X,Y) -> APP((X,Y))
-//  [X]  -> ABS([X])
-//   X   -> X
-struct term *reduce(struct term *term)
-{
-	if (term->type == APP) {
-		return reduce_app(term);
-	} else if (term->type == ABS) {
-		return reduce_abs(term);
-	} else if (term->type == VAR) {
-		return term;
-	}
-	fatal("invalid type %d\n", term->type);
+	substitute(term->u.app.lhs->u.abs.term, term->u.app.rhs, 0);
 }