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 = target;
  20                         target->refcount++;
  21                 }
  22                 break;
  23         case lambda_abs:
  24                 lambda_beta(binding, &bdy(body), target, total);
  25                 break;
  26         case lambda_app:
  27                 lambda_beta(binding, &lhs(body), target, total);
  28                 lambda_beta(binding, &rhs(body), target, total);
  29                 break;
  30         }
  31 }
  32
  33 bool lambda_reduce(struct lambda **t, struct lambda **total, bool applicative)
  34 {
  35         if((*t)->which == lambda_app){
  36                 if(applicative)
  37                         if(lambda_reduce(&rhs(t), total, applicative))
  38                                 return true;
  39                 if(lhs(t)->which != lambda_abs){
  40                         return lambda_reduce(&lhs(t), total, applicative);
  41                 } else {
  42                         if(lhs(t)->data.abstraction.strict)
  43                                 lambda_reduce(&rhs(t), total, true);
  44
  45                         if(lhs(t) == rhs(t)){
  46                                 lhs(t)->refcount--;
  47                                 rhs(t) = copy(rhs(t));
  48                         }
  49
  50                         //In this abstraction we substitute the result with the rhs
  51                         lambda_print(*total, *t);
  52                         lambda_beta(lhs(t), &lhs(t)->data.abstraction.expr, rhs(t), *total);
  53
  54                         struct lambda *newt = lhs(t)->data.abstraction.expr;
  55                         lhs(t)->data.abstraction.expr->refcount++;
  56                         lambda_free(*t);
  57                         *t = newt;
  58
  59                         printf("\nβ -> ");
  60                         return true;
  61                 }
  62         } else if ((*t)->which == lambda_abs) {
  63                 return lambda_reduce(&bdy(t), total, applicative);
  64         }
  65         return false;
  66 }