Function lamcal::evaluate_inspected

pub fn evaluate_inspected<B, I>(
    expr: &Term, 
    env: &Environment, 
    inspect: &mut I
) -> Term where
    B: BetaReduce,
    I: Inspect, 

Evaluates a lambda expression with inspection in the given environment.

This function takes the given expression by reference and returns a new Term with the evaluation applied. The given Term remains unchanged.

For the β-reduction step a reduction strategy is required. Therefore the reduction strategy must be specified as the type parameter B.

The given inspection is called before each substitution of a free variable with its bound term from the environment and before each contraction (reduction step). See the documentation of the inspect for information on how to define an inspection and the implementations that are provided.

Examples

let env = Environment::default();

let expr = app![
    var("C"),
    lam("x", lam("y", app(var("x"), var("y")))),
    var("e"),
    var("f")
];

let mut collected = Collect::new();

let result = evaluate_inspected::<NormalOrder<Enumerate>, _>(&expr, &env, &mut collected);

assert_eq!(
    collected.terms(),
    &vec![
        app![
            var("C"),
            lam("x", lam("y", app(var("x"), var("y")))),
            var("e"),
            var("f")
        ],
        app![
            lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))),
            lam("x", lam("y", app(var("x"), var("y")))),
            var("e"),
            var("f")
        ],
        app![
            lam(
                "b",
                lam(
                    "c",
                    app![
                        lam("x", lam("y", app(var("x"), var("y")))),
                        var("c"),
                        var("b")
                    ]
                )
            ),
            var("e"),
            var("f")
        ],
        app![
            lam(
                "b",
                lam("c", app![lam("y", app(var("c"), var("y"))), var("b")])
            ),
            var("e"),
            var("f")
        ],
        app![
            lam("b", lam("c", app(var("c"), var("b")),)),
            var("e"),
            var("f")
        ],
        app![lam("c", app(var("c"), var("e"))), var("f")],
    ][..],
);
assert_eq!(result, app(var("f"), var("e")));