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
*body
, struct lambda
*target
, struct lambda
*total
)
47 if(lambda_ident_eq(body
, ident
)){
48 lambda_print(total
, NULL
);
51 free(body
->data
.identifier
.ident
);
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
++;
65 lambda_beta(ident
, body
->data
.abstraction
.expr
, target
, total
);
68 lambda_beta(ident
, body
->data
.application
.expr1
, target
, total
);
69 lambda_beta(ident
, body
->data
.application
.expr2
, target
, total
);
74 void lambda_reduce(struct lambda
**t
, struct lambda
**total
, int *maxdepth
)
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 if(t1
->which
== lambda_abs
){
84 if(t1
->data
.abstraction
.strict
)
85 lambda_reduce(&t2
, total
, maxdepth
);
86 lambda_print(*total
, *t
);
88 lambda_beta(t1
, t1
->data
.abstraction
.expr
, t2
, *total
);
90 t2
= copy(t1
->data
.abstraction
.expr
);
97 lambda_reduce(t
, total
, maxdepth
);