alpha

[lambda.git] / reduce.c

diff --git a/reduce.c b/reduce.c
index 1cad7a9..429b038 100644 (file)
--- 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;