reduce rules arithmetics in preamble

diff --git a/preamble b/preamble
index 8eda655..2861a88 100644 (file)
--- a/preamble
+++ b/preamble
@@ -7,3 +7,7 @@ W=\x y.x y y;
 SOMEGA=\x.x x;
 OMEGA=SOMEGA SOMEGA;
 Y=\g.(\x.g (x x))(\x.g (x x));
+ZERO=\f x.x;
+SUCC=\n f x.f(n f x);
+PLUS=\m n.m SUCC n;
+MULT=\m n f x.m(n f)x;

diff --git a/reduce.c b/reduce.c
index 7335bfd..9dbf678 100644 (file)
--- a/reduce.c
+++ b/reduce.c
@@ -45,6 +45,7 @@ void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
                //If the first argument is an abstraction, we apply
                t1 = t->data.application.expr1;
                t2 = t->data.application.expr2;
+               lambda_reduce(t1, total, maxdepth);
                if(t1->which == lambda_abs){
                        subst(t1->data.abstraction.ident, t1->data.abstraction.expr, t2, total);
                        (*maxdepth)--;
@@ -54,9 +55,9 @@ void lambda_reduce(struct lambda *t, struct lambda *total, int *maxdepth)
                        printf("-> ");
                        lambda_print(total);
                        lambda_reduce(t, total, maxdepth);
+               } else {
+                       lambda_reduce(t2, total, maxdepth);
                }
-               lambda_reduce(t1, total, maxdepth);
-               lambda_reduce(t, total, maxdepth);
                break;
        }
 }