use debruijn indexing

diff --git a/lambda.h b/lambda.h
index 3eaa247..54c23e3 100644 (file)
--- a/lambda.h
+++ b/lambda.h
@@ -13,11 +13,10 @@ struct lambda {
        union {
                struct {
                        char *ident;
-                       unsigned int revision;
+                       struct lambda *binding;
                } identifier;
                struct {
                        char *ident;
-                       unsigned int revision;
                        bool strict;
                        struct lambda *expr;
                } abstraction;
@@ -34,6 +33,7 @@ struct decllist {
        struct lambda *value;
 };
 
+struct lambda *make_lambda();
 struct lambda *make_ident(char *);
 struct lambda *make_abstraction(char *, bool, struct lambda *);
 struct lambda *make_application(struct lambda *, struct lambda *);

diff --git a/lambda.y b/lambda.y
index 388693d..b0fe73a 100644 (file)
--- a/lambda.y
+++ b/lambda.y
@@ -41,18 +41,35 @@ struct lambda *make_ident(char *i)
        struct lambda *r = make_lambda();
        r->which = lambda_ident;
        r->data.identifier.ident = strdup(i);
-       r->data.identifier.revision = 0;
+       r->data.identifier.binding = NULL;
        return r;
 }
 
+void lambda_bind(struct lambda *tob, struct lambda *binding, char *ident)
+{
+       switch(tob->which){
+       case lambda_ident:
+               if(strcmp(ident, tob->data.identifier.ident) == 0 && tob->data.identifier.binding == NULL)
+                       tob->data.identifier.binding = binding;
+               break;
+       case lambda_abs:
+               lambda_bind(tob->data.abstraction.expr, binding, ident);
+               break;
+       case lambda_app:
+               lambda_bind(tob->data.application.expr1, binding, ident);
+               lambda_bind(tob->data.application.expr2, binding, ident);
+               break;
+       }
+}
+
 struct lambda *make_abstraction(char *i, bool strict, struct lambda *t)
 {
        struct lambda *r = make_lambda();
        r->which = lambda_abs;
        r->data.abstraction.ident = strdup(i);
-       r->data.abstraction.revision = 0;
        r->data.abstraction.strict = strict;
        r->data.abstraction.expr = t;
+       lambda_bind(t, r, i);
        return r;
 }
 
@@ -102,6 +119,7 @@ struct lambda *decls_lookup(char *ident)
 
 int main()
 {
+       setbuf(stdout, NULL);
        int r = yyparse();
        yylex_destroy();
        return r;
@@ -117,21 +135,25 @@ program
        :
        | lambda SEMICOLON program
 lambda
-       : term
-               {
-                       int maxdepth = 1000;
-                       printf("     ");
-                       lambda_reduce(&$1, &$1, &maxdepth);
-                       lambda_print($1, NULL);
-                       lambda_free($1);
-               }
-       | FUNC func
+       : FUNC func
                {
                        decls_prepend($1->data.identifier.ident, $2);
                        printf("%s = ", $1->data.identifier.ident);
                        lambda_print($2, NULL);
+                       putchar('\n');
                        lambda_free($1);
                }
+       | term
+               {
+                       struct lambda *t = $1;
+                       printf("     ");
+                       for(unsigned int i = 0; i<999; i++)
+                               if(!lambda_reduce(&t, &t, true))
+                                       break;
+                       lambda_print(t, NULL);
+                       putchar('\n');
+                       lambda_free(t);
+               }
 func
        : ASSIGN term
                { $$ = $2; }

diff --git a/mem.c b/mem.c
index a0b18da..4d73188 100644 (file)
--- a/mem.c
+++ b/mem.c
@@ -1,5 +1,6 @@
 #include <stdlib.h>
 #include "lambda.h"
+#include "print.h"
 
 void lambda_free(struct lambda *t)
 {
@@ -25,20 +26,37 @@ void lambda_free(struct lambda *t)
        }
 }
 
+void binding_replace(struct lambda *b, struct lambda *from, struct lambda *to)
+{
+       switch(b->which){
+       case lambda_ident:
+               if(b->data.identifier.binding == from)
+                       b->data.identifier.binding = to;
+               break;
+       case lambda_abs:
+               binding_replace(b->data.abstraction.expr, from, to);
+               break;
+       case lambda_app:
+               binding_replace(b->data.application.expr1, from, to);
+               binding_replace(b->data.application.expr2, from, to);
+               break;
+       }
+}
+
 struct lambda *copy(struct lambda *t)
 {
-       struct lambda *c = malloc(sizeof (struct lambda));
+       struct lambda *c = make_lambda();
        c->which = t->which;
        switch(t->which){
        case lambda_ident:
                c->data.identifier.ident = strdup(t->data.identifier.ident);
-               c->data.identifier.revision = t->data.identifier.revision;
+               c->data.identifier.binding = t->data.identifier.binding;
                break;
        case lambda_abs:
                c->data.abstraction.ident = strdup(t->data.abstraction.ident);
                c->data.abstraction.strict = t->data.abstraction.strict;
                c->data.abstraction.expr = copy(t->data.abstraction.expr);
-               c->data.abstraction.revision = t->data.abstraction.revision;
+               binding_replace(c->data.abstraction.expr, t, c);
                break;
        case lambda_app:
                c->data.application.expr1 = copy(t->data.application.expr1);
@@ -47,4 +65,3 @@ struct lambda *copy(struct lambda *t)
        }
        return c;
 }
-

diff --git a/mem.h b/mem.h
index 1964654..1b7fd29 100644 (file)
--- a/mem.h
+++ b/mem.h
@@ -5,4 +5,5 @@
 
 void lambda_free(struct lambda *);
 struct lambda *copy(struct lambda *);
+struct lambda *shallow_copy(struct lambda *);
 #endif

diff --git a/preamble b/preamble
index cdc65b0..0ce77eb 100644 (file)
--- a/preamble
+++ b/preamble
@@ -8,7 +8,7 @@ SOMEGA x = x x;
 OMEGA    = SOMEGA SOMEGA;
 Y g      = (\x.g (x x))(\x.g (x x));
 
-ZERO f !x  = x;
+ZERO f x  = x;
 SUCC n f x = f (n f x);
 PLUS m n   = m SUCC n;
 MULT m n   = m (PLUS n) 0;

diff --git a/print.c b/print.c
index c50d8dc..c7503b8 100644 (file)
--- a/print.c
+++ b/print.c
@@ -5,28 +5,17 @@
        if(t->data.abstraction.strict)\
                putchar('!');\
        printf("%s", t->data.abstraction.ident);\
-       print_apos(t->data.abstraction.revision);\
        }
 
 
-void print_apos(unsigned int revision)
-{
-       if(revision == 1)
-               printf("\'");
-       if(revision > 2){
-               printf("\"");
-               print_apos(revision - 2);
-       }
-}
-
 void term_print(struct lambda *t, struct lambda *mark)
 {
        if(t == mark)
                putchar('|');
        switch(t->which){
        case lambda_ident:
+//             printf("%s(%p)", t->data.identifier.ident, (void *)t->data.identifier.binding);
                printf("%s", t->data.identifier.ident);
-               print_apos(t->data.identifier.revision);
                break;
        case lambda_abs:
                printf("λ");
@@ -61,5 +50,5 @@ void term_print(struct lambda *t, struct lambda *mark)
 void lambda_print(struct lambda *t, struct lambda *mark)
 {
        term_print(t, mark);
-       printf(";\n");
+       printf(";");
 }

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;
 }

diff --git a/reduce.h b/reduce.h
index 833c7a9..f90a051 100644 (file)
--- a/reduce.h
+++ b/reduce.h
@@ -3,5 +3,5 @@
 
 #include "lambda.h"
 
-void lambda_reduce(struct lambda **t, struct lambda **total, int *maxdepth);
+bool lambda_reduce(struct lambda **t, struct lambda **total, bool applicative);
 #endif