#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 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){
+ 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((*body)->data.identifier.binding == binding){
+ lambda_free(*body);
+ *body = copy(target);
}
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;
- switch(t->which){
- case lambda_ident:
- break;
- case lambda_abs:
-// lambda_reduce(t->data.abstraction.expr, total, maxdepth);
- break;
- case lambda_app:
- t1 = t->data.application.expr1;
- t2 = t->data.application.expr2;
- lambda_reduce(t1, total, maxdepth);
- if(t1->which == lambda_abs){
- lambda_print(total, t);
+ if((*t)->which == lambda_app){
+ 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);
+
+ //In this abstraction we substitute the result with the rhs
+ lambda_print(*total, *t);
+ lambda_beta(lhs(t), &lhs(t)->data.abstraction.expr, rhs(t), *total);
+
+ struct lambda *newt = copy(lhs(t)->data.abstraction.expr);
+ lambda_free(*t);
+ *t = newt;
+
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);
+ return true;
}
- break;
+ } else if ((*t)->which == lambda_abs) {
+ return lambda_reduce(&bdy(t), total, applicative);
}
+ return false;
}