Function _make_expr_handler

examples/06_effectful_verifier/python/refine.py:123–146

Build an effectful handler that maps Term ops → Lean.Expr builders. *depth* is the number of forallE binders above the expression scope. Variable ``var_names[i]`` maps to ``bvar(depth - 1 - i)``.

(eb: ExprBuilder, var_names, var_ops, depth)

def _make_expr_handler(eb: ExprBuilder, var_names, var_ops, depth):
    """Build an effectful handler that maps Term ops → Lean.Expr builders.

    *depth* is the number of forallE binders above the expression scope.
    Variable ``var_names[i]`` maps to ``bvar(depth - 1 - i)``.
    """
    int_ops = defdata.dispatch(int)
    h = {}

    for i, name in enumerate(var_names):
        bv = eb.mk_bvar(depth - 1 - i)
        h[var_ops[name]] = (lambda bv=bv: lambda: bv)(bv)

    def coerce(x):
        return eb.mk_int(x) if isinstance(x, int) else x

    h[int_ops.__add__] = lambda a, b: eb.mk_int_add(coerce(a), coerce(b))
    h[int_ops.__sub__] = lambda a, b: eb.mk_int_sub(coerce(a), coerce(b))
    h[int_ops.__mul__] = lambda a, b: eb.mk_int_mul(coerce(a), coerce(b))
    h[int_ops.__gt__] = lambda a, b: eb.mk_int_gt(coerce(a), coerce(b))
    h[int_ops.__ge__] = lambda a, b: eb.mk_int_ge(coerce(a), coerce(b))
    h[int_ops.__lt__] = lambda a, b: eb.mk_int_lt(coerce(a), coerce(b))
    h[int_ops.__le__] = lambda a, b: eb.mk_int_le(coerce(a), coerce(b))
    return h


def _build_vc_expr(eb: ExprBuilder, vc_term, var_names, var_ops, precond_terms):