Merge branch 'master' of git.martlubbers.net:lambda

[lambda.git] / reduce.c

diff --git a/reduce.c b/reduce.c
index 0c7d98c..1cad7a9 100644 (file)
--- a/reduce.c
+++ b/reduce.c
@@ -1,3 +1,4 @@
+#include <stdbool.h>
 #include <stdlib.h>
 #include <stdio.h>
 #include <string.h>
@@ -5,26 +6,64 @@
 #include "print.h"
 #include "mem.h"
 
-void subst(char *ident, struct lambda *t1, struct lambda *t2, struct lambda *total)
+bool lambda_ident_eq(struct lambda *t1, struct lambda *t2)
+{
+       switch(t1->which){
+       case lambda_ident:
+               return strcmp(t1->data.identifier.ident, t2->data.identifier.ident) == 0
+                       && t1->data.identifier.revision == t2->data.identifier.revision;
+       case lambda_abs:
+               return strcmp(t1->data.abstraction.ident, t2->data.abstraction.ident) == 0
+                       && t1->data.abstraction.revision == t2->data.abstraction.revision;
+       default:
+               return false;
+       }
+}
+
+void lambda_alpha(struct lambda *expr, struct lambda *ident)
+{
+       switch(expr->which){
+       case lambda_ident:
+               if(lambda_ident_eq(expr, ident))
+                       expr->data.identifier.revision++;
+               break;
+       case lambda_abs:
+               if(!lambda_ident_eq(expr, ident))
+                       lambda_alpha(expr->data.abstraction.expr, ident);
+               break;
+       case lambda_app:
+               lambda_alpha(expr->data.application.expr1, ident);
+               lambda_alpha(expr->data.application.expr2, ident);
+               break;
+       }
+
+}
+
+void lambda_beta(struct lambda *ident, struct lambda *t1, struct lambda *t2, struct lambda *total)
 {
        struct lambda cpy;
        switch(t1->which){
        case lambda_ident:
-               if(strcmp(t1->data.identifier, ident) == 0){
+               if(lambda_ident_eq(t1, ident)){
                        cpy = *copy(t2);
-                       free(t1->data.identifier);
+                       free(t1->data.identifier.ident);
                        if(total == t1)
                                *total = cpy;
                        *t1 = cpy;
                }
                break;
        case lambda_abs:
-               if(strcmp(t1->data.abstraction.ident, ident) != 0)
-                       subst(ident, t1->data.abstraction.expr, t2, total);
+               if(lambda_ident_eq(t1, ident) == 0){
+                       lambda_alpha(t1->data.abstraction.expr, t1);
+                       t1->data.abstraction.revision++;
+                       printf("α -> ");
+                       lambda_print(total);
+               }
+               lambda_beta(ident, t1->data.abstraction.expr, t2, total);
                break;
        case lambda_app:
-               subst(ident, t1->data.application.expr1, t2, total);
-               subst(ident, t1->data.application.expr2, t2, total);
+               lambda_beta(ident, t1->data.application.expr1, t2, total);
+               lambda_beta(ident, t1->data.application.expr2, t2, total);
                break;
        }
 }
@@ -45,12 +84,12 @@ void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
                t1 = t->data.application.expr1;
                t2 = t->data.application.expr2;
                if(t1->which == lambda_abs){
-                       subst(t1->data.abstraction.ident, t1->data.abstraction.expr, t2, total);
+                       lambda_beta(t1, t1->data.abstraction.expr, t2, total);
                        (*maxdepth)--;
                        if(total == t)
                                *total = *t1->data.abstraction.expr;
                        *t = *t1->data.abstraction.expr;
-                       printf("-> ");
+                       printf("β -> ");
                        lambda_print(total);
                        lambda_reduce(t, total, maxdepth);
                }