add alpha renaming

diff --git a/Makefile b/Makefile
index 4799d18..c76d2ff 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-CFLAGS:=-g -Wall -Werror -Wextra
+CFLAGS:=-g -Wall -Wextra
 lambda: lambda.tab.o lambda.yy.o main.o print.o mem.o reduce.o
        $(LINK.c) $(LDLIBS) $^ $(OUTPUT_OPTION)
 

diff --git a/lambda.h b/lambda.h
index a92a2bb..60bc284 100644 (file)
--- a/lambda.h
+++ b/lambda.h
@@ -9,9 +9,13 @@ enum lambda_which {lambda_ident, lambda_abs, lambda_app};
 struct lambda {
        enum lambda_which which;
        union {
-               char *identifier;
                struct {
                        char *ident;
+                       unsigned int revision;
+               } identifier;
+               struct {
+                       char *ident;
+                       unsigned int revision;
                        struct lambda *expr;
                } abstraction;
                struct {

diff --git a/lambda.y b/lambda.y
index f62de05..b49dbb2 100644 (file)
--- a/lambda.y
+++ b/lambda.y
@@ -28,7 +28,8 @@ struct lambda *make_ident(char *i)
 {
        struct lambda *r = make_lambda();
        r->which = lambda_ident;
-       r->data.identifier = strdup(i);
+       r->data.identifier.ident = strdup(i);
+       r->data.identifier.revision = 0;
        return r;
 }
 
@@ -84,7 +85,7 @@ lambda
                { result = $$; }
 decl
        : FUNC ASSIGN term SEMICOLON
-               { decls_prepend($1->data.identifier, $3); }
+               { decls_prepend($1->data.identifier.ident, $3); }
 term
        : term appterm
                { $$ = make_application($1, $2); }
@@ -93,12 +94,12 @@ term
 appterm
        : FUNC
                {
-                       $$ = decls_lookup($1->data.identifier);
+                       $$ = decls_lookup($1->data.identifier.ident);
                        lambda_free($1);
                }
        | IDENT
                {
-                       $$ = make_ident($1->data.identifier);
+                       $$ = make_ident($1->data.identifier.ident);
                        lambda_free($1);
                }
        | LAMBDA abstraction
@@ -108,7 +109,7 @@ appterm
 abstraction
        : IDENT abstraction
                {
-                       $$ = make_abstraction($1->data.identifier, $2);
+                       $$ = make_abstraction($1->data.identifier.ident, $2);
                        lambda_free($1);
                }
        | DOT term

diff --git a/mem.c b/mem.c
index 1e112a8..0792a97 100644 (file)
--- a/mem.c
+++ b/mem.c
@@ -6,7 +6,7 @@ void lambda_free(struct lambda *t)
        if(t != NULL){
                switch(t->which){
                case lambda_ident:
-                       free(t->data.identifier);
+                       free(t->data.identifier.ident);
                        break;
                case lambda_abs:
                        free(t->data.abstraction.ident);
@@ -27,11 +27,13 @@ struct lambda *copy(struct lambda *t)
        c->which = t->which;
        switch(t->which){
        case lambda_ident:
-               c->data.identifier = strdup(t->data.identifier);
+               c->data.identifier.ident = strdup(t->data.identifier.ident);
+               c->data.identifier.revision = t->data.identifier.revision;
                break;
        case lambda_abs:
                c->data.abstraction.ident = strdup(t->data.abstraction.ident);
                c->data.abstraction.expr = copy(t->data.abstraction.expr);
+               c->data.abstraction.revision = t->data.abstraction.revision;
                break;
        case lambda_app:
                c->data.application.expr1 = copy(t->data.application.expr1);

diff --git a/print.c b/print.c
index fb209f4..afaac01 100644 (file)
--- a/print.c
+++ b/print.c
@@ -1,15 +1,27 @@
 #include <stdio.h>
 #include "lambda.h"
 
+void print_apos(unsigned int revision)
+{
+       if(revision == 1)
+               printf("\'");
+       if(revision > 2){
+               printf("\"");
+               print_apos(revision - 2);
+       }
+}
+
 void term_print(struct lambda *t)
 {
        switch(t->which){
        case lambda_ident:
-               printf("%s", t->data.identifier);
+               printf("%s", t->data.identifier.ident);
+               print_apos(t->data.identifier.revision);
                break;
        case lambda_abs:
                printf("(λ");
                printf("%s", t->data.abstraction.ident);
+               print_apos(t->data.abstraction.revision);
                putchar('.');
                term_print(t->data.abstraction.expr);
                putchar(')');

diff --git a/reduce.c b/reduce.c
index 83ab536..2cef239 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;
        }
 
@@ -46,12 +85,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);
                }