reduce.c

   1 #include <stdlib.h>
   2 #include <stdio.h>
   3 #include <string.h>
   4 #include "lambda.h"
   5 #include "print.h"
   6 #include "mem.h"
   7
   8 void subst(char *ident, struct lambda *t1, struct lambda *t2, struct lambda *total)
   9 {
  10         struct lambda cpy;
  11         switch(t1->which){
  12         case lambda_ident:
  13                 if(strcmp(t1->data.identifier, ident) == 0){
  14                         cpy = *copy(t2);
  15                         free(t1->data.identifier);
  16                         if(total == t1)
  17                                 *total = cpy;
  18                         *t1 = cpy;
  19                 }
  20                 break;
  21         case lambda_abs:
  22                 if(strcmp(t1->data.abstraction.ident, ident) != 0)
  23                         subst(ident, t1->data.abstraction.expr, t2, total);
  24                 break;
  25         case lambda_app:
  26                 subst(ident, t1->data.application.expr1, t2, total);
  27                 subst(ident, t1->data.application.expr2, t2, total);
  28                 break;
  29         }
  30
  31 }
  32
  33 void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
  34 {
  35         if(*maxdepth == 0)
  36                 return;
  37         struct lambda *t1, *t2;
  38         switch(t->which){
  39         case lambda_ident:
  40                 break;
  41         case lambda_abs:
  42                 lambda_reduce(t->data.abstraction.expr, total, maxdepth);
  43                 break;
  44         case lambda_app:
  45                 //If the first argument is an abstraction, we apply
  46                 t1 = t->data.application.expr1;
  47                 t2 = t->data.application.expr2;
  48                 lambda_reduce(t1, total, maxdepth);
  49                 if(t1->which == lambda_abs){
  50                         subst(t1->data.abstraction.ident, t1->data.abstraction.expr, t2, total);
  51                         (*maxdepth)--;
  52                         if(total == t)
  53                                 *total = *t1->data.abstraction.expr;
  54                         *t = *t1->data.abstraction.expr;
  55                         printf("-> ");
  56                         lambda_print(total);
  57                         lambda_reduce(t, total, maxdepth);
  58                 } else {
  59                         lambda_reduce(t2, total, maxdepth);
  60                 }
  61                 break;
  62         }
  63 }