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