Gather the set of major inductive KIds from all peer recursors in a recursor block. Used to look up the rec_majors_cache.
(
&mut self,
rec_block: &KId<M>,
)
| 4408 | checked_metadata_sum::<M>( |
| 4409 | "generated recursor universe arity", |
| 4410 | &[flat[target_bi].lvls, 1], |
| 4411 | )? |
| 4412 | } else { |
| 4413 | flat[target_bi].lvls |
| 4414 | } |
| 4415 | }, |
| 4416 | }; |
| 4417 | let rec_lvls: Box<[KUniv<M>]> = (0..peer_rec_lvls) |
| 4418 | .map(|i| KUniv::param(i, M::meta_field(ix_common::env::Name::anon()))) |
| 4419 | .collect(); |
| 4420 | |
| 4421 | // Peel foralls from the domain to detect wrapping. |
| 4422 | // After peeling, the head should be `I_target params idx_args`. |
| 4423 | let wdom = if Self::has_flat_member_head(dom, flat) { |
| 4424 | dom.clone() |
| 4425 | } else { |
| 4426 | self.whnf(dom)? |
| 4427 | }; |
| 4428 | let mut inner = wdom.clone(); |
| 4429 | let mut forall_doms: Vec<KExpr<M>> = Vec::new(); |
| 4430 | |
| 4431 | while let ExprData::All(_, _, fd, fb, _) = inner.data() { |
| 4432 | // Check if this forall's result type (after peeling) has a block |
| 4433 | // inductive as head. If inner itself IS a block inductive app, stop. |
| 4434 | let (h, _) = collect_app_spine(&inner); |
| 4435 | if matches!(h.data(), ExprData::Const(id, _, _) |
| 4436 | if flat.iter().any(|m| m.id.addr == id.addr)) |
| 4437 | { |
| 4438 | break; |
| 4439 | } |
| 4440 | forall_doms.push(fd.clone()); |
| 4441 | inner = fb.clone(); |
| 4442 | } |
| 4443 | let n_xs = checked_usize_to_u64::<M>( |
| 4444 | "generated recursor wrapped-field binder count", |
| 4445 | forall_doms.len(), |
| 4446 | )?; |
| 4447 | |
| 4448 | // Extract index args from the inner application: `I_target params idx_args` |
| 4449 | let inner_w = if Self::has_flat_member_head(&inner, flat) { |
| 4450 | inner.clone() |
| 4451 | } else { |
| 4452 | self.whnf(&inner)? |
no test coverage detected