Check if a field domain is a recursive occurrence of a flat block member. Returns `Some(block_index)` if, after peeling foralls, the result is `I_k params args` where `I_k` matches a flat member: - **Original** members (`is_aux = false`): head address match is sufficient. - **Auxiliary** members (`is_aux = true`): head address must match AND the first `own_params` args must be definitionally equa
(
&mut self,
dom: &KExpr<M>,
flat: &[FlatBlockMember<M>],
spec_params_lift_by: u64,
)
| 2967 | let motive_var = (depth - 1 - (motive_base + block_ind_idx)) as u64; |
| 2968 | let mut ih_body = KExpr::var(motive_var, anon()); |
| 2969 | |
| 2970 | for idx in &idx_args { |
| 2971 | ih_body = self.intern(KExpr::app(ih_body, idx.clone())); |
| 2972 | } |
| 2973 | |
| 2974 | // field is at context level minor_saved + field_idx |
| 2975 | let field_var = (depth - 1 - (minor_saved + field_idx)) as u64; |
| 2976 | ih_body = |
| 2977 | self.intern(KExpr::app(ih_body, KExpr::var(field_var, anon()))); |
| 2978 | |
| 2979 | Ok(ih_body) |
| 2980 | }, |
| 2981 | } |
| 2982 | } |
| 2983 | |
| 2984 | /// Check if a field domain is a recursive occurrence of a flat block member. |
| 2985 | /// Returns `Some(block_index)` if, after peeling foralls, the result is |
| 2986 | /// `I_k params args` where `I_k` matches a flat member: |
| 2987 | /// |
| 2988 | /// - **Original** members (`is_aux = false`): head address match is |
| 2989 | /// sufficient. |
| 2990 | /// - **Auxiliary** members (`is_aux = true`): head address must match |
| 2991 | /// AND the first `own_params` args must be definitionally equal to |
| 2992 | /// the member's stored `spec_params` (after lifting spec_params to |
| 2993 | /// the caller's param-reference frame). The addr check alone can't |
| 2994 | /// distinguish two auxiliaries sharing an external inductive (e.g. |
| 2995 | /// `List A` vs `List B`). |
| 2996 | /// |
| 2997 | /// # Depth handling |
| 2998 | /// |
| 2999 | /// `spec_params` are stored at the param context (depth = |
| 3000 | /// `flat[0].own_params`). Callers reference block params via Var |
| 3001 | /// indices that may live at different effective depths: |
| 3002 | /// |
| 3003 | /// - `build_minor_at_depth` pushes field locals as it scans; at the |
| 3004 | /// `is_rec_field` call `self.depth() - n_rec_params` gives the |
| 3005 | /// offset needed. |
| 3006 | /// - `build_rule_rhs` does NOT push locals — it substitutes params |
| 3007 | /// with `Var(total_lams - 1 - j)` (virtual positions for the final |
| 3008 | /// lambda chain), leaving `self.depth() = 0` regardless of how |
| 3009 | /// many virtual binders are open. The correct offset is |
| 3010 | /// `total_lams - n_rec_params`. |
| 3011 | /// |
| 3012 | /// Rather than have the function guess, the caller passes |
| 3013 | /// `spec_params_lift_by` explicitly. Comparison uses `is_def_eq` |
| 3014 | /// after lifting, which handles alpha equivalence, whnf, and beta — |
| 3015 | /// anything a raw `addr()` hash comparison would miss on `Var` |
| 3016 | /// parameter references. |
| 3017 | /// |
| 3018 | /// Historical note: the original implementation used raw `addr()` |
| 3019 | /// comparison after spine decomposition, which returned false |
| 3020 | /// whenever a spec_param was a bare `Var` (block param). That |
| 3021 | /// dropped the IH for any recursive field whose nested type used the |
| 3022 | /// block's params directly — e.g. `head : Entry α β (Node α β)` in |
| 3023 | /// a nested `List (Entry α β (Node α β))` scan. An interim fix |