Merge branch 'master' of git.martlubbers.net:lambda

diff --combined reduce.c
index 2cef239,0c7d98c..1cad7a9
--- 1/reduce.c
--- 2/reduce.c
+++ b/reduce.c
@@@ -1,4 -1,3 +1,4 @@@
 +#include <stdbool.h>
  #include <stdlib.h>
  #include <stdio.h>
  #include <string.h>
@@@ -6,67 -5,28 +6,66 @@@
  #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;
        }
- 
  }
  
  void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
@@@ -85,12 -45,12 +84,12 @@@
                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);
                }