alpha

diff --git a/lambda.y b/lambda.y
index b49dbb2..eda3c59 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (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;