From 78f77f113d37f73ab0d04aca022b562e9a5a412e Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 17 May 2018 09:28:36 +0200
Subject: [PATCH] alpha

---
 lambda.y |  2 +-
 main.c   |  4 ++--
 print.c  | 17 +++++++++++------
 print.h  |  2 +-
 reduce.c | 36 +++++++++++++++++++-----------------
 5 files changed, 34 insertions(+), 27 deletions(-)

diff --git a/lambda.y b/lambda.y
index b49dbb2..eda3c59 100644
--- a/lambda.y
+++ b/lambda.y
@@ -58,7 +58,7 @@ void decls_prepend(char *ident, struct lambda *value)
 	head->ident = ident;
 	head->value = value;
 	printf("Declared %s as ", ident);
-	lambda_print(value);
+	lambda_print(value, NULL);
 	decls = head;
 }
 
diff --git a/main.c b/main.c
index f4a2296..907336b 100644
--- a/main.c
+++ b/main.c
@@ -14,9 +14,9 @@ int main()
 	int r = yyparse();
 	int maxdepth = 100;
 	if(r == 0){
-		printf("   ");
-		lambda_print(result);
+		printf("     ");
 		lambda_reduce(result, result, &maxdepth);
+		lambda_print(result, NULL);
 		lambda_free(result);
 	}
 	yylex_destroy();
diff --git a/print.c b/print.c
index afaac01..33e7104 100644
--- a/print.c
+++ b/print.c
@@ -11,8 +11,10 @@ void print_apos(unsigned int revision)
 	}
 }
 
-void term_print(struct lambda *t)
+void term_print(struct lambda *t, struct lambda *mark)
 {
+	if(t == mark)
+		putchar('|');
 	switch(t->which){
 	case lambda_ident:
 		printf("%s", t->data.identifier.ident);
@@ -23,20 +25,23 @@ void term_print(struct lambda *t)
 		printf("%s", t->data.abstraction.ident);
 		print_apos(t->data.abstraction.revision);
 		putchar('.');
-		term_print(t->data.abstraction.expr);
+		term_print(t->data.abstraction.expr, mark);
 		putchar(')');
 		break;
 	case lambda_app:
 		putchar('(');
-		term_print(t->data.application.expr1);
-		term_print(t->data.application.expr2);
+		term_print(t->data.application.expr1, mark);
+		putchar(' ');
+		term_print(t->data.application.expr2, mark);
 		putchar(')');
 		break;
 	}
+	if(t == mark)
+		putchar('|');
 }
 
-void lambda_print(struct lambda *t)
+void lambda_print(struct lambda *t, struct lambda *mark)
 {
-	term_print(t);
+	term_print(t, mark);
 	putchar('\n');
 }
diff --git a/print.h b/print.h
index 2f40e36..af3a008 100644
--- a/print.h
+++ b/print.h
@@ -3,5 +3,5 @@
 
 #include "lambda.h"
 
-void lambda_print(struct lambda *);
+void lambda_print(struct lambda *, struct lambda *);
 #endif
diff --git a/reduce.c b/reduce.c
index 1cad7a9..429b038 100644
--- a/reduce.c
+++ b/reduce.c
@@ -39,31 +39,33 @@ void lambda_alpha(struct lambda *expr, struct lambda *ident)
 
 }
 
-void lambda_beta(struct lambda *ident, struct lambda *t1, struct lambda *t2, struct lambda *total)
+void lambda_beta(struct lambda *ident, struct lambda *body, struct lambda *target, struct lambda *total)
 {
 	struct lambda cpy;
-	switch(t1->which){
+	switch(body->which){
 	case lambda_ident:
-		if(lambda_ident_eq(t1, ident)){
-			cpy = *copy(t2);
-			free(t1->data.identifier.ident);
-			if(total == t1)
+		if(lambda_ident_eq(body, ident)){
+			lambda_print(total, NULL);
+			printf("β -> ");
+			cpy = *copy(target);
+			free(body->data.identifier.ident);
+			if(total == body)
 				*total = cpy;
-			*t1 = cpy;
+			*body = cpy;
 		}
 		break;
 	case lambda_abs:
-		if(lambda_ident_eq(t1, ident) == 0){
-			lambda_alpha(t1->data.abstraction.expr, t1);
-			t1->data.abstraction.revision++;
+		if(lambda_ident_eq(body, ident) == 0){
+			lambda_print(total, body);
+			lambda_alpha(body->data.abstraction.expr, body);
+			body->data.abstraction.revision++;
 			printf("α -> ");
-			lambda_print(total);
 		}
-		lambda_beta(ident, t1->data.abstraction.expr, t2, total);
+		lambda_beta(ident, body->data.abstraction.expr, target, total);
 		break;
 	case lambda_app:
-		lambda_beta(ident, t1->data.application.expr1, t2, total);
-		lambda_beta(ident, t1->data.application.expr2, t2, total);
+		lambda_beta(ident, body->data.application.expr1, target, total);
+		lambda_beta(ident, body->data.application.expr2, target, total);
 		break;
 	}
 }
@@ -80,17 +82,17 @@ void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
 		lambda_reduce(t->data.abstraction.expr, total, maxdepth);
 		break;
 	case lambda_app:
-		//If the first argument is an abstraction, we apply
 		t1 = t->data.application.expr1;
 		t2 = t->data.application.expr2;
+		lambda_reduce(t1, total, maxdepth);
 		if(t1->which == lambda_abs){
+			lambda_print(total, t);
+			printf("β -> ");
 			lambda_beta(t1, t1->data.abstraction.expr, t2, total);
 			(*maxdepth)--;
 			if(total == t)
 				*total = *t1->data.abstraction.expr;
 			*t = *t1->data.abstraction.expr;
-			printf("β -> ");
-			lambda_print(total);
 			lambda_reduce(t, total, maxdepth);
 		}
 		break;
-- 
2.20.1