Find peer recursor KIds for each flat block member. Returns None if peer recursors can't be found (block not in env).
(
&mut self,
block_id: &KId<M>,
flat: &[FlatBlockMember<M>],
)
| 3221 | |
| 3222 | // Collect fields and push them as locals |
| 3223 | let mut field_domains: Vec<KExpr<M>> = Vec::new(); |
| 3224 | let mut rec_field_indices: Vec<(usize, usize)> = Vec::new(); // (field_idx, block_ind_idx) |
| 3225 | |
| 3226 | let mut fidx = 0; |
| 3227 | loop { |
| 3228 | let w = self.whnf(&ty)?; |
| 3229 | match w.data() { |
| 3230 | ExprData::All(_, _, dom, body, _) => { |
| 3231 | field_domains.push(dom.clone()); |
| 3232 | // Field args reference block params at current pushed-local |
| 3233 | // depth; spec_params live at depth = n_rec_params (shared |
| 3234 | // block params = flat[0].own_params). Lift by the difference. |
| 3235 | let n_rec_params = flat.first().map_or(0, |m| m.own_params); |
| 3236 | let lift_by = self.depth().saturating_sub(n_rec_params); |
| 3237 | if let Some(bi) = self.is_rec_field(dom, flat, lift_by)? { |
| 3238 | rec_field_indices.push((fidx, bi)); |
| 3239 | } |
| 3240 | let _ = self.push_fvar_decl_anon(dom.clone()); |
| 3241 | ty = body.clone(); |
| 3242 | fidx += 1; |
| 3243 | }, |
| 3244 | _ => break, |
| 3245 | } |
| 3246 | } |
| 3247 | let n_fields = field_domains.len(); |
| 3248 | |
| 3249 | // Build IH types for recursive fields and push them as locals. |
| 3250 | // At this point depth = saved + n_fields. |
| 3251 | let mut ih_domains: Vec<KExpr<M>> = Vec::new(); |
| 3252 | for (k, &(field_idx, block_ind_idx)) in rec_field_indices.iter().enumerate() |
| 3253 | { |
| 3254 | // depth = saved + n_fields + k (k IHs already pushed) |
| 3255 | // For IH building, n_params should be the TARGET member's own_params |
| 3256 | // (the member that the recursive field targets). |
| 3257 | let target_n_params = if block_ind_idx < flat.len() { |
| 3258 | u64_to_usize::<M>(flat[block_ind_idx].own_params)? |
| 3259 | } else { |
| 3260 | n_rec_params |
| 3261 | }; |
| 3262 | let ih_ty = self.build_direct_ih( |
| 3263 | field_idx, |
| 3264 | block_ind_idx, |
| 3265 | target_n_params, |
| 3266 | n_fields, |
| 3267 | k, |
| 3268 | saved, |
| 3269 | motive_base, |
| 3270 | &field_domains, |
| 3271 | block_addrs, |
| 3272 | )?; |
| 3273 | ih_domains.push(ih_ty.clone()); |
| 3274 | let _ = self.push_fvar_decl_anon(ih_ty); |
| 3275 | } |
| 3276 | let n_ihs = ih_domains.len(); |
| 3277 | let n_binders = checked_binder_sum::<M>( |
| 3278 | "generated minor fields + induction hypotheses", |
| 3279 | n_fields, |
| 3280 | n_ihs, |
no test coverage detected