Kernel-driven recursor coherence check (no syntactic compare). Catches the structural failure modes that `infer(rec.ty)` alone misses: - The major inductive is itself ill-formed (e.g. strict-positivity violation, bad ctor return shape, field universe too high). `check_inductive` runs A1–A4 and will reject the recursor-by- extension if those fail. - The declared `k` flag disagrees with what the ke
(
&mut self,
id: &KId<M>,
)
| 3973 | Some(rid) => match self.try_get_const(rid)? { |
| 3974 | Some(KConst::Recr { lvls, .. }) => { |
| 3975 | if lvls > ind_lvls { |
| 3976 | 1u64 |
| 3977 | } else { |
| 3978 | 0u64 |
| 3979 | } |
| 3980 | }, |
| 3981 | _ => 0, |
| 3982 | }, |
| 3983 | None => 0, |
| 3984 | }; |
| 3985 | let mut flat = |
| 3986 | self.build_flat_block(&block_inds, n_params_u64, univ_offset)?; |
| 3987 | let n_originals = block_inds.len(); |
| 3988 | if self.env.recursor_aux_order == RecursorAuxOrder::Canonical |
| 3989 | && flat.len() > n_originals + 1 |
| 3990 | { |
| 3991 | let block_us = flat[0].occurrence_us.to_vec(); |
| 3992 | let all0_name = block_inds.first().and_then(|id| M::meta_name(&id.name)); |
| 3993 | let block_first_id = block_inds.first().cloned(); |
| 3994 | let canonical_order = self.canonical_aux_order( |
| 3995 | &flat[n_originals..], |
| 3996 | n_params_u64, |
| 3997 | &block_us, |
| 3998 | all0_name.as_ref(), |
| 3999 | block_first_id.as_ref(), |
| 4000 | )?; |
| 4001 | let aux_part = flat[n_originals..].to_vec(); |
| 4002 | let mut new_aux: Vec<FlatBlockMember<M>> = |
| 4003 | Vec::with_capacity(canonical_order.len()); |
| 4004 | for &orig_idx in &canonical_order { |
| 4005 | new_aux.push(aux_part[orig_idx].clone()); |
| 4006 | } |
| 4007 | flat.truncate(n_originals); |
| 4008 | flat.extend(new_aux); |
| 4009 | } |
| 4010 | if flat.len() != generated_snapshot.len() { |
| 4011 | return Err(TcError::Other(format!( |
| 4012 | "populate_recursor_rules_from_block: flat/generated length mismatch: flat={} generated={}", |
| 4013 | flat.len(), |
no test coverage detected