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                         free(cpy);
  56                 }
  57                 break;
  58         case lambda_abs:
  59                 if(lambda_ident_eq(body, ident) == 0){
  60                         lambda_print(total, body);
  61                         lambda_alpha(body->data.abstraction.expr, body);
  62                         body->data.abstraction.revision++;
  63                         printf("α -> ");
  64                 }
  65                 lambda_beta(ident, body->data.abstraction.expr, target, total);
  66                 break;
  67         case lambda_app:
  68                 lambda_beta(ident, body->data.application.expr1, target, total);
  69                 lambda_beta(ident, body->data.application.expr2, target, total);
  70                 break;
  71         }
  72 }
  73
  74 void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
  75 {
  76         if(*maxdepth == 0)
  77                 return;
  78         struct lambda *t1, *t2;
  79         if(t->which == lambda_app){
  80                 t1 = t->data.application.expr1;
  81                 t2 = t->data.application.expr2;
  82                 lambda_reduce(t1, total, maxdepth);
  83                 //For applicative order
  84                 lambda_reduce(t2, total, maxdepth);
  85                 if(t1->which == lambda_abs){
  86                         lambda_print(total, t);
  87                         printf("β -> ");
  88                         lambda_beta(t1, t1->data.abstraction.expr, t2, total);
  89                         lambda_free(t2);
  90                         t2 = copy(t1->data.abstraction.expr);
  91                         if(total == t)
  92                                 *total = *t2;
  93                         lambda_free(t1);
  94                         *t = *t2;
  95                         free(t2);
  96                         (*maxdepth)--;
  97                         lambda_reduce(t, total, maxdepth);
  98                 }
  99                 //For applicative order
 100         } else if(t->which == lambda_abs) {
 101                 lambda_reduce(t->data.abstraction.expr, total, maxdepth);
 102         }
 103 }