reduce.c

   1 #include <stdbool.h>
   2 #include <stdlib.h>
   3 #include <stdio.h>
   4 #include <string.h>
   5 #include "lambda.h"
   6 #include "print.h"
   7 #include "mem.h"
   8
   9 bool lambda_ident_eq(struct lambda *t1, struct lambda *t2)
  10 {
  11         switch(t1->which){
  12         case lambda_ident:
  13                 return strcmp(t1->data.identifier.ident, t2->data.identifier.ident) == 0
  14                         && t1->data.identifier.revision == t2->data.identifier.revision;
  15         case lambda_abs:
  16                 return strcmp(t1->data.abstraction.ident, t2->data.abstraction.ident) == 0
  17                         && t1->data.abstraction.revision == t2->data.abstraction.revision;
  18         default:
  19                 return false;
  20         }
  21 }
  22
  23 void lambda_alpha(struct lambda *expr, struct lambda *ident)
  24 {
  25         switch(expr->which){
  26         case lambda_ident:
  27                 if(lambda_ident_eq(expr, ident))
  28                         expr->data.identifier.revision++;
  29                 break;
  30         case lambda_abs:
  31                 if(!lambda_ident_eq(expr, ident))
  32                         lambda_alpha(expr->data.abstraction.expr, ident);
  33                 break;
  34         case lambda_app:
  35                 lambda_alpha(expr->data.application.expr1, ident);
  36                 lambda_alpha(expr->data.application.expr2, ident);
  37                 break;
  38         }
  39
  40 }
  41
  42 void lambda_beta(struct lambda *ident, struct lambda *t1, struct lambda *t2, struct lambda *total)
  43 {
  44         struct lambda cpy;
  45         switch(t1->which){
  46         case lambda_ident:
  47                 if(lambda_ident_eq(t1, ident)){
  48                         cpy = *copy(t2);
  49                         free(t1->data.identifier.ident);
  50                         if(total == t1)
  51                                 *total = cpy;
  52                         *t1 = cpy;
  53                 }
  54                 break;
  55         case lambda_abs:
  56                 if(lambda_ident_eq(t1, ident) == 0){
  57                         lambda_alpha(t1->data.abstraction.expr, t1);
  58                         t1->data.abstraction.revision++;
  59                         printf("α -> ");
  60                         lambda_print(total);
  61                 }
  62                 lambda_beta(ident, t1->data.abstraction.expr, t2, total);
  63                 break;
  64         case lambda_app:
  65                 lambda_beta(ident, t1->data.application.expr1, t2, total);
  66                 lambda_beta(ident, t1->data.application.expr2, t2, total);
  67                 break;
  68         }
  69 }
  70
  71 void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
  72 {
  73         if(*maxdepth == 0)
  74                 return;
  75         struct lambda *t1, *t2;
  76         switch(t->which){
  77         case lambda_ident:
  78                 break;
  79         case lambda_abs:
  80                 lambda_reduce(t->data.abstraction.expr, total, maxdepth);
  81                 break;
  82         case lambda_app:
  83                 //If the first argument is an abstraction, we apply
  84                 t1 = t->data.application.expr1;
  85                 t2 = t->data.application.expr2;
  86                 if(t1->which == lambda_abs){
  87                         lambda_beta(t1, t1->data.abstraction.expr, t2, total);
  88                         (*maxdepth)--;
  89                         if(total == t)
  90                                 *total = *t1->data.abstraction.expr;
  91                         *t = *t1->data.abstraction.expr;
  92                         printf("β -> ");
  93                         lambda_print(total);
  94                         lambda_reduce(t, total, maxdepth);
  95                 }
  96                 break;
  97         }
  98 }