(
&mut self,
rec_ty: &KExpr<M>,
prefix_skip: u64,
target_addr: &Address,
)
| 1425 | )?; |
| 1426 | // Wrap with `∀ block_params → body` to mirror compile-side |
| 1427 | // `mk_forall(j_type_block, &block_param_decls)`. The body's free Vars |
| 1428 | // for i < n_block_params already refer to the block params via the |
| 1429 | // recursor's outer context; the wrap binds them in place. |
| 1430 | typ = self.wrap_with_block_param_foralls(typ, &block_param_binders); |
| 1431 | |
| 1432 | // Synthetic aux ctor KIds and KConst::Ctor entries. |
| 1433 | let mut aux_ctor_kids: Vec<KId<M>> = Vec::with_capacity(ext_ctors.len()); |
| 1434 | for (ci, ext_ctor_id) in ext_ctors.iter().enumerate() { |
| 1435 | let (ext_ctor_ty, ext_ctor_fields) = |
| 1436 | match self.get_const(ext_ctor_id)? { |
| 1437 | KConst::Ctor { ty, fields, .. } => (ty.clone(), fields), |
| 1438 | _ => { |
| 1439 | return Err(TcError::Other( |
| 1440 | "canonical_aux_order: aux ext ctor is not a ctor".into(), |
| 1441 | )); |
| 1442 | }, |
| 1443 | }; |
| 1444 | let mut ctor_typ = |
| 1445 | self.instantiate_univ_params(&ext_ctor_ty, &member.occurrence_us)?; |
| 1446 | for j in 0..ext_n_params { |
| 1447 | let w = self.whnf(&ctor_typ)?; |
| 1448 | match w.data() { |
| 1449 | ExprData::All(_, _, _, body, _) => { |
| 1450 | let body = body.clone(); |
| 1451 | let p_idx = u64_to_usize::<M>(j)?; |
| 1452 | if p_idx >= member.spec_params.len() { |
| 1453 | break; |
| 1454 | } |
| 1455 | let p = member.spec_params[p_idx].clone(); |
| 1456 | ctor_typ = subst(&mut self.env.intern, &body, &p, 0); |
| 1457 | }, |
| 1458 | _ => break, |
| 1459 | } |
| 1460 | } |
| 1461 | |
| 1462 | // Rewrite nested occurrences inside aux ctor types to block-local |
| 1463 | // synthetic aux references before sorting. This mirrors the |
| 1464 | // compile-side `replace_all_nested` queue pass over the expanded |
| 1465 | // aux members. It covers both recursive fields such as |
no test coverage detected