Skip to main content

rewrite_native_guarded_calls_resolved_expr

aver::codegen::recursion

Function rewrite_native_guarded_calls_resolved_expr 

Source 
pub fn rewrite_native_guarded_calls_resolved_expr(
    expr: &Spanned<ResolvedExpr>,
    target_fn_id: FnId,
    aux_name: &str,
) -> Spanned<ResolvedExpr>
Expand description

ResolvedExpr mirror of rewrite_native_guarded_calls_expr. The proof-mode IntCountdownGuarded shape stores the rewritten arms on ProofIR (now resolved), so the rewriter that lifts fn(args) to aux_name(args, OMEGA_PROOF_SENTINEL) works in resolved space too.

Target detection: callers pass target_fn_id — the opaque crate::ir::FnId of the recursive fn the lowerer pinned. Every ResolvedCallee::Fn(callee_id) / TailCall { target, .. } site is compared by id, so two same-bare-name fns across modules can’t cross-rewrite by accident — same anti-collision rule as the rest of #147 phase E.

Synthesised aux call: emitted as ResolvedCallee::Unresolved { callee: Ident(aux_name) } rather than Builtin(...) because aux_name is a codegen-only helper (no entry in the program’s symbol table); Unresolved is exactly the variant the resolver uses for names it can’t classify, and the Lean expr emitter already renders the inner ident verbatim.