Decompile a single named constant (non-aux_gen) into the decompile state. Dispatches on the constant kind (definition, recursor, axiom, quotient, projection). Constants with `named.original.is_some()` and a recognized aux_gen suffix are skipped — they'll be regenerated by `decompile_block_aux_gen`.
( name: &Name, named: &Named, stt: &CompileState, dstt: &DecompileState, )
| 3090 | // REGEN input must differ at byte level — diff this probe |
| 3091 | // summary against the regen summary above. |
| 3092 | // addr != orig ⇒ `Named.original.0` is not reproducible from |
| 3093 | // the constant alone: the original-track compile context |
| 3094 | // (cache/ref-table/surgery state) differed, and the |
| 3095 | // divergence is contextual, not a regen defect. |
| 3096 | if singleton && let Some(oenv) = orig_env { |
| 3097 | let nm = consts[0].name(); |
| 3098 | let omc: Option<LeanMutConst> = match oenv.get(&nm).as_deref() { |
| 3099 | Some(LeanConstantInfo::RecInfo(rv)) => { |
| 3100 | Some(LeanMutConst::Recr(rv.clone())) |
| 3101 | }, |
| 3102 | Some(LeanConstantInfo::DefnInfo(dv)) => { |
| 3103 | Some(LeanMutConst::Defn(Def::mk_defn(dv))) |
| 3104 | }, |
| 3105 | Some(LeanConstantInfo::ThmInfo(tv)) => { |
| 3106 | Some(LeanMutConst::Defn(Def::mk_theo(tv))) |
| 3107 | }, |
| 3108 | Some(LeanConstantInfo::OpaqueInfo(ov)) => { |
| 3109 | Some(LeanMutConst::Defn(Def::mk_opaq(ov))) |
| 3110 | }, |
| 3111 | _ => None, |
| 3112 | }; |
| 3113 | if let Some(omc) = omc { |
| 3114 | let mut pcache = CompileBlockCache::default(); |
| 3115 | let mut pexprs: Vec<(&LeanExpr, &[Name])> = Vec::new(); |
| 3116 | collect_mut_const_exprs(&omc, &mut pexprs); |
| 3117 | let preseeded = preseed_expr_tables( |
| 3118 | &pexprs, |
| 3119 | &mut_ctx, |
| 3120 | &mut pcache, |
| 3121 | stt, |
| 3122 | "roundtrip_probe", |
| 3123 | ); |
| 3124 | let compiled = preseeded.and_then(|()| match &omc { |
| 3125 | LeanMutConst::Defn(d) => { |
| 3126 | compile_definition(d, &mut_ctx, &mut pcache, stt) |
| 3127 | .map(|(data, _)| MutConst::Defn(data)) |
| 3128 | }, |
| 3129 | LeanMutConst::Recr(r) => { |
| 3130 | compile_recursor(r, &mut_ctx, &mut pcache, stt) |
| 3131 | .map(|(data, _)| MutConst::Recr(data)) |
| 3132 | }, |
| 3133 | LeanMutConst::Indc(_) => unreachable!("probe is Defn/Recr only"), |
| 3134 | }); |
| 3135 | match compiled { |
| 3136 | Ok(data) => { |
| 3137 | let prefs: Vec<Address> = pcache.refs.iter().cloned().collect(); |
| 3138 | let punivs: Vec<Arc<Univ>> = |
| 3139 | pcache.univs.iter().cloned().collect(); |
| 3140 | let result = match &data { |
| 3141 | MutConst::Defn(def) => { |
| 3142 | crate::compile::apply_sharing_to_definition_with_stats( |
| 3143 | def.clone(), |
| 3144 | prefs, |
| 3145 | punivs, |
| 3146 | Some(&name_str), |
| 3147 | ) |
| 3148 | }, |
| 3149 | MutConst::Recr(rec) => { |
no test coverage detected