From 8231fc0aee4eea2541a0f79637ad19ec31f043fa Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 17 May 2018 08:48:12 +0200 Subject: [PATCH] add alpha renaming --- Makefile | 2 +- lambda.h | 6 +++++- lambda.y | 11 ++++++----- mem.c | 6 ++++-- print.c | 14 +++++++++++++- reduce.c | 57 +++++++++++++++++++++++++++++++++++++++++++++++--------- 6 files changed, 77 insertions(+), 19 deletions(-) diff --git a/Makefile b/Makefile index 4799d18..c76d2ff 100644 --- 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 --- 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 --- 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 --- 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 --- a/print.c +++ b/print.c @@ -1,15 +1,27 @@ #include #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 --- a/reduce.c +++ b/reduce.c @@ -1,3 +1,4 @@ +#include #include #include #include @@ -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); } -- 2.20.1