From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 23 May 2018 08:23:49 +0000 (+0200)
Subject: use debruijn indexing
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=3b14b51dbda4af16b473da7e4db633f9a0e3326c;p=lambda.git

use debruijn indexing
---

diff --git a/lambda.h b/lambda.h
index 3eaa247..54c23e3 100644
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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