Function rs_debug_sharing_analysis

crates/ffi/src/lean_ixon/sharing.rs:14–53

(
  exprs_obj: LeanArray<LeanBorrowed<'_>>,
)

/// This helps diagnose why Lean and Rust make different sharing decisions.
#[unsafe(no_mangle)]
pub extern "C" fn rs_debug_sharing_analysis(
  exprs_obj: LeanArray<LeanBorrowed<'_>>,
) {
  let exprs: Vec<Arc<IxonExpr>> =
    exprs_obj.map(|x| Arc::new(LeanIxonExpr(x).decode()));

  println!("[Rust] Analyzing {} input expressions", exprs.len());

  let (info_map, _ptr_to_hash, topo_order) = analyze_block(&exprs, false);
  let effective_sizes =
    ixon::sharing::compute_effective_sizes(&info_map, &topo_order);

  println!("[Rust] Found {} unique subterms", info_map.len());

  // Collect subterms with usage >= 2
  let mut candidates: Vec<_> = info_map
    .iter()
    .filter(|(_, info)| info.usage_count >= 2)
    .filter_map(|(hash, info)| {
      let eff_size = *effective_sizes.get(hash)?;
      Some((hash, info, eff_size))
    })
    .collect();

  // Sort by usage count descending
  candidates.sort_by(|a, b| b.1.usage_count.cmp(&a.1.usage_count));

  println!("[Rust] Subterms with usage >= 2:");
  for (hash, info, eff_size) in candidates {
    let n = info.usage_count;
    let n_i = n.cast_signed();
    let eff_size_i = eff_size.cast_signed();
    let potential = (n_i - 1) * eff_size_i - (n_i + eff_size_i);
    println!(
      "  usage={} eff_size={} potential={} hash={:.8}",
      n, eff_size, potential, hash
    );
    println!("    expr={:?}", info.expr);
  }
}

/// FFI: Run Rust's sharing analysis on Lean-provided Ixon.Expr array.
/// Returns the number of shared items Rust would produce.