65610e56a0422ee19e1b18a00f2a4d7655842561
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 lambda_print(total
, t
);
86 lambda_beta(t1
, t1
->data
.abstraction
.expr
, t2
, total
);
88 t2
= copy(t1
->data
.abstraction
.expr
);
95 lambda_reduce(t
, total
, maxdepth
);