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 *body, struct lambda *target, struct lambda *total)
  43 {
  44         struct lambda cpy;
  45         switch(body->which){
  46         case lambda_ident:
  47                 if(lambda_ident_eq(body, ident)){
  48                         lambda_print(total, NULL);
  49                         printf("β -> ");
  50                         cpy = *copy(target);
  51                         free(body->data.identifier.ident);
  52                         if(total == body)
  53                                 *total = cpy;
  54                         *body = cpy;
  55                 }
  56                 break;
  57         case lambda_abs:
  58                 if(lambda_ident_eq(body, ident) == 0){
  59                         lambda_print(total, body);
  60                         lambda_alpha(body->data.abstraction.expr, body);
  61                         body->data.abstraction.revision++;
  62                         printf("α -> ");
  63                 }
  64                 lambda_beta(ident, body->data.abstraction.expr, target, total);
  65                 break;
  66         case lambda_app:
  67                 lambda_beta(ident, body->data.application.expr1, target, total);
  68                 lambda_beta(ident, body->data.application.expr2, target, total);
  69                 break;
  70         }
  71 }
  72
  73 void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
  74 {
  75         if(*maxdepth == 0)
  76                 return;
  77         struct lambda *t1, *t2;
  78         switch(t->which){
  79         case lambda_ident:
  80                 break;
  81         case lambda_abs:
  82                 lambda_reduce(t->data.abstraction.expr, total, maxdepth);
  83                 break;
  84         case lambda_app:
  85                 t1 = t->data.application.expr1;
  86                 t2 = t->data.application.expr2;
  87                 lambda_reduce(t1, total, maxdepth);
  88                 if(t1->which == lambda_abs){
  89                         lambda_print(total, t);
  90                         printf("β -> ");
  91                         lambda_beta(t1, t1->data.abstraction.expr, t2, total);
  92                         (*maxdepth)--;
  93                         if(total == t)
  94                                 *total = *t1->data.abstraction.expr;
  95                         *t = *t1->data.abstraction.expr;
  96                         lambda_reduce(t, total, maxdepth);
  97                 }
  98                 break;
  99         }
 100 }