9 bool lambda_ident_eq(struct lambda
*t1
, struct lambda
*t2
)
13 return strcmp(t1
->data
.identifier
.ident
, t2
->data
.identifier
.ident
) == 0
14 && t1
->data
.identifier
.revision
== t2
->data
.identifier
.revision
;
16 return strcmp(t1
->data
.abstraction
.ident
, t2
->data
.abstraction
.ident
) == 0
17 && t1
->data
.abstraction
.revision
== t2
->data
.abstraction
.revision
;
23 void lambda_alpha(struct lambda
*expr
, struct lambda
*ident
)
27 if(lambda_ident_eq(expr
, ident
))
28 expr
->data
.identifier
.revision
++;
31 if(!lambda_ident_eq(expr
, ident
))
32 lambda_alpha(expr
->data
.abstraction
.expr
, ident
);
35 lambda_alpha(expr
->data
.application
.expr1
, ident
);
36 lambda_alpha(expr
->data
.application
.expr2
, ident
);
42 void lambda_beta(struct lambda
*ident
, struct lambda
*t1
, struct lambda
*t2
, struct lambda
*total
)
47 if(lambda_ident_eq(t1
, ident
)){
49 free(t1
->data
.identifier
.ident
);
56 if(lambda_ident_eq(t1
, ident
) == 0){
57 lambda_alpha(t1
->data
.abstraction
.expr
, t1
);
58 t1
->data
.abstraction
.revision
++;
62 lambda_beta(ident
, t1
->data
.abstraction
.expr
, t2
, total
);
65 lambda_beta(ident
, t1
->data
.application
.expr1
, t2
, total
);
66 lambda_beta(ident
, t1
->data
.application
.expr2
, t2
, total
);
72 void lambda_reduce(struct lambda
*t
, struct lambda
*total
, int *maxdepth
)
76 struct lambda
*t1
, *t2
;
81 lambda_reduce(t
->data
.abstraction
.expr
, total
, maxdepth
);
84 //If the first argument is an abstraction, we apply
85 t1
= t
->data
.application
.expr1
;
86 t2
= t
->data
.application
.expr2
;
87 if(t1
->which
== lambda_abs
){
88 lambda_beta(t1
, t1
->data
.abstraction
.expr
, t2
, total
);
91 *total
= *t1
->data
.abstraction
.expr
;
92 *t
= *t1
->data
.abstraction
.expr
;
95 lambda_reduce(t
, total
, maxdepth
);