Function lamcal::expand

pub fn expand(expr: &Term, env: &Environment) -> Term

Replaces free variables in a term with the term that is bound to the variable's name in the given environment.

This function walks through the whole term and replaces any free variable with the term bound to the variable's name in the given environment. Bound variables are not replaced.

The result is returned as a new Term. The given term remains unchanged. If you want to expand named constants in a term in place use the associated function Term::expand instead.

Examples

let env = Environment::default();

let expr = app![
    var("C"),
    lam("a", app(var("K"), var("I"))),
    var("e"),
    var("f")
];

let result = expand(&expr, &env);

assert_eq!(
    result,
    app![
        lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))),
        lam("a", app(lam("a", lam("b", var("a"))), lam("a", var("a")))),
        var("e"),
        var("f")
    ]
);

Bound variables are not replaced even though there is a bound term for the identifier K defined in the environment:

let env = Environment::default();

let expr = lam("K", app(var("K"), var("I")));

let result = expand(&expr, &env);

assert_eq!(result, lam("K", app(var("K"), lam("a", var("a")))));