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 #define lhs(t) (*t)->data.application.expr1
  10 #define rhs(t) (*t)->data.application.expr2
  11 #define bdy(t) (*t)->data.abstraction.expr
  12
  13 void lambda_beta(struct lambda *binding, struct lambda **body, struct lambda *target, struct lambda *total)
  14 {
  15         switch((*body)->which){
  16         case lambda_ident:
  17                 if((*body)->data.identifier.binding == binding){
  18                         lambda_free(*body);
  19                         *body = copy(target);
  20                 }
  21                 break;
  22         case lambda_abs:
  23                 lambda_beta(binding, &bdy(body), target, total);
  24                 break;
  25         case lambda_app:
  26                 lambda_beta(binding, &lhs(body), target, total);
  27                 lambda_beta(binding, &rhs(body), target, total);
  28                 break;
  29         }
  30 }
  31
  32 bool lambda_reduce(struct lambda **t, struct lambda **total, bool applicative)
  33 {
  34         if((*t)->which == lambda_app){
  35                 if(applicative)
  36                         if(lambda_reduce(&rhs(t), total, applicative))
  37                                 return true;
  38                 if(lhs(t)->which != lambda_abs){
  39                         return lambda_reduce(&lhs(t), total, applicative);
  40                 } else {
  41                         if(lhs(t)->data.abstraction.strict)
  42                                 lambda_reduce(&rhs(t), total, true);
  43
  44                         //In this abstraction we substitute the result with the rhs
  45                         lambda_print(*total, *t);
  46                         lambda_beta(lhs(t), &lhs(t)->data.abstraction.expr, rhs(t), *total);
  47
  48                         struct lambda *newt = copy(lhs(t)->data.abstraction.expr);
  49                         lambda_free(*t);
  50                         *t = newt;
  51
  52                         printf("β -> ");
  53                         return true;
  54                 }
  55         } else if ((*t)->which == lambda_abs) {
  56                 return lambda_reduce(&bdy(t), total, applicative);
  57         }
  58         return false;
  59 }