use debruijn indexing

[lambda.git] / reduce.c

diff --git a/reduce.c b/reduce.c
index b5e64e1..91299fc 100644 (file)
--- a/reduce.c
+++ b/reduce.c
@@ -6,95 +6,64 @@
 #include "print.h"
 #include "mem.h"
 
-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;
-       }
-}
+#define binder(t) (*t)->data.identifier.binding
+#define lhs(t) (*t)->data.application.expr1
+#define rhs(t) (*t)->data.application.expr2
+#define bdy(t) (*t)->data.abstraction.expr
 
-void lambda_alpha(struct lambda *expr, struct lambda *ident)
+void lambda_beta(struct lambda *binding, struct lambda **body, struct lambda *target, struct lambda *total)
 {
-       switch(expr->which){
+//     lambda_print(*body, NULL);
+//     printf(" [%s=", binding->data.abstraction.ident);
+//     lambda_print(target, NULL);
+//     printf("]\n");
+       switch((*body)->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 *body, struct lambda *target, struct lambda *total)
-{
-       struct lambda *cpy;
-       switch(body->which){
-       case lambda_ident:
-               if(lambda_ident_eq(body, ident)){
-                       lambda_print(total, NULL);
-                       printf("β -> ");
-                       cpy = copy(target);
-                       free(body->data.identifier.ident);
-                       if(total == body)
-                               *total = *cpy;
-                       *body = *cpy;
-                       free(cpy);
+               if(binder(body) == binding){
+                       lambda_free(*body);
+                       *body = target;
+                       target->refcount++;
                }
                break;
        case lambda_abs:
-               if(lambda_ident_eq(body, ident) == 0){
-                       lambda_print(total, body);
-                       lambda_alpha(body->data.abstraction.expr, body);
-                       body->data.abstraction.revision++;
-                       printf("α -> ");
-               }
-               lambda_beta(ident, body->data.abstraction.expr, target, total);
+               lambda_beta(binding, &bdy(body), target, total);
                break;
        case lambda_app:
-               lambda_beta(ident, body->data.application.expr1, target, total);
-               lambda_beta(ident, body->data.application.expr2, target, total);
+               lambda_beta(binding, &lhs(body), target, total);
+               lambda_beta(binding, &rhs(body), target, total);
                break;
        }
 }
 
-void lambda_reduce(struct lambda **t, struct lambda **total, int *maxdepth)
+bool lambda_reduce(struct lambda **t, struct lambda **total, bool applicative)
 {
-       if(*maxdepth == 0)
-               return;
-       struct lambda *t1, *t2;
        if((*t)->which == lambda_app){
-               t1 = (*t)->data.application.expr1;
-               t2 = (*t)->data.application.expr2;
-               lambda_reduce(&t1, total, maxdepth);
-               if(t1->which == lambda_abs){
-                       if(t1->data.abstraction.strict)
-                               lambda_reduce(&t2, total, maxdepth);
+               if(applicative)
+                       if(lambda_reduce(&rhs(t), total, applicative))
+                               return true;
+               if(lhs(t)->which != lambda_abs){
+                       return lambda_reduce(&lhs(t), total, applicative);
+               } else {
+                       if(lhs(t)->data.abstraction.strict)
+                               lambda_reduce(&rhs(t), total, true);
+
+                       if(lhs(t) == rhs(t))
+                               rhs(t) = copy(rhs(t));
+
+                       //In this abstraction we substitute the result with the rhs
                        lambda_print(*total, *t);
-                       printf("β -> ");
-                       lambda_beta(t1, t1->data.abstraction.expr, t2, *total);
-                       lambda_free(t2);
-                       t2 = copy(t1->data.abstraction.expr);
-                       if(total == t)
-                               **total = *t2;
-                       lambda_free(t1);
-                       **t = *t2;
-                       free(t2);
-                       (*maxdepth)--;
-                       lambda_reduce(t, total, maxdepth);
+                       lambda_beta(lhs(t), &lhs(t)->data.abstraction.expr, rhs(t), *total);
+
+                       struct lambda *newt = lhs(t)->data.abstraction.expr;
+                       lhs(t)->data.abstraction.expr->refcount++;
+                       lambda_free(*t);
+                       *t = newt;
+
+                       printf("\nβ -> ");
+                       return true;
                }
+       } else if ((*t)->which == lambda_abs) {
+               return lambda_reduce(&bdy(t), total, applicative);
        }
+       return false;
 }