Function lamcal::expand_inspected

pub fn expand_inspected(
    expr: &Term, 
    env: &Environment, 
    inspect: &mut impl Inspect
) -> 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.

Before each substitution of a variable with its bound term from the environment the given inspection is called. See the documentation of the inspect module for information on how to define an inspection and the implementations that are provided.

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 mut collected = Collect::new();
let result = expand_inspected(&expr, &env, &mut collected);

assert_eq!(
    collected.terms(),
    &vec![
        app![
            var("C"),
            lam("a", app(var("K"), var("I"))),
            var("e"),
            var("f")
        ],
        app![
            lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))),
            lam("a", app(var("K"), var("I"))),
            var("e"),
            var("f")
        ],
        app![
            lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))),
            lam("a", app(lam("a", lam("b", var("a"))), var("I"))),
            var("e"),
            var("f")
        ],
    ][..],
);
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")
    ]
);