Function decompile_env

crates/compile/src/decompile.rs:4263–4520

Decompile an Ixon environment back to Lean format. Single-pass parallel work-stealing scheduler. Computes SCCs over the name-level reference graph, then processes SCC blocks in topological order. For each block: - Phase A: decompile all non-aux_gen constants (`decompile_named_const`) - Phase B: regenerate aux_gen constants if the block has any (`decompile_block_aux_gen`) - Phase C: resolve deps t

(
  stt: &CompileState,
)

          .iter()
          .zip(original_all.iter())
          .any(|(class, orig)| class[0] != *orig));
    let aux_layout_changed = block.aux_layout.as_ref().is_some_and(|layout| {
      // Keep identical to the compile-side predicate in `compile_mutual`
      // — evaporated positions need their head-rewrite plans even when
      // no canonical slot moved.
      layout.evaporated.iter().any(|&b| b)
        || layout.perm.iter().enumerate().any(|(source_j, &canonical_i)| {
          canonical_i != aux_gen::nested::PERM_OUT_OF_SCC
            && canonical_i != source_j
        })
    });

    if !user_layout_changed && !aux_layout_changed {
      continue;
    }

    let plans = surgery::compute_call_site_plans(
      &block.class_names,
      &original_all,
      env,
      block.aux_layout.as_ref(),
    )
    .map_err(|e| DecompileError::BadConstantFormat {
      msg: format!("decompile aux plan compute_call_site_plans: {e}"),
    })?;

    for (name, plan) in plans {
      // First-wins per name, but a DIFFERING later plan means two stored
      // blocks claim one source-indexed aux name — the same collision
      // class the compile side now rejects; surface it rather than
      // decompiling with whichever block's plan happened to install
      // first (plans/aux-recursor-alias-collision.md §2.4).
      if let Some(brecon_name) = surgery::rec_name_to_brecon_name(&name)
        && (aux_member_names.contains(&brecon_name)
          || env.contains_key(&brecon_name))
      {
        let new_plan = surgery::BRecOnCallSitePlan::from_rec_plan(&plan);
        // Mirror the compile side: Type-level `.brecOn.go` / `.brecOn.eq`
        // share `.brecOn`'s telescope and are referenced directly by
        // equation-lemma proofs, so they carry the same plan keys.
        let mut plan_keys = vec![brecon_name.clone()];
        for sub in ["go", "eq"] {
          let sub_name = Name::str(brecon_name.clone(), sub.to_string());
          if aux_member_names.contains(&sub_name) || env.contains_key(&sub_name)
          {
            plan_keys.push(sub_name);
          }
        }
        for key in plan_keys {
          // Probe-then-act: the DashMap read guard must drop before
          // insert.
          let existing_differs =
            stt.brec_on_call_site_plans.get(&key).map(|e| *e != new_plan);
          match existing_differs {
            Some(true) => {
              return Err(DecompileError::BadConstantFormat {
                msg: format!(
                  "conflicting brecOn call-site plans for '{}' across \