java/LCEvaluator.java


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59

package org.lambdanantes.lcgoji;

import org.lambdanantes.lcgoji.ast.Abs;
import org.lambdanantes.lcgoji.ast.App;
import org.lambdanantes.lcgoji.ast.Term;
import org.lambdanantes.lcgoji.ast.Var;

import static org.lambdanantes.lcgoji.ast.Abs.λ;
import static org.lambdanantes.lcgoji.ast.App.apply;

public class LCEvaluator {

    public static Term evaluate(Term term) {
        switch (term) {
            case Var var -> {
                return var;
            }
            case Abs abs -> {
                return abs;
            }
            case App app -> {
                switch (app.left) {
                    case Abs abs -> {
                        return substitute(abs.body, abs.arg, app.right);
                    }
                    case App _app -> {
                        return app;
                    }
                    case Var _var -> {
                        return app;
                    }
                }
            }
        }
    }

    private static Term substitute(Term body, String arg, Term val) {
        switch (body) {
            case Var var -> {
                if (var.name.equals(arg)) {
                    return val;
                } else {
                    return body;
                }
            }
            case App app -> {
                return apply(substitute(app.left, arg, val), substitute(app.right, arg, val));
            }
            case Abs abs -> {
                if (abs.arg.equals(arg)) {
                    // Pas de substitution des variables redéfinies
                    return abs;
                } else {
                    return λ(abs.arg, substitute(abs.body, arg, val));
                }
            }
        }
    }
}