+#include <stdbool.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#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;
}
}
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);
}