Build an IH type for a recursive field. For a direct recursive field (type = `I_bi params idx_args`): IH = `motive_bi(idx_args, field_var)` For a forall-wrapped recursive field (type = `∀ xs, I_bi params idx_args(xs)`): IH = `∀ xs, motive_bi(idx_args(xs), field xs)` Called when depth = minor_saved + n_fields + k (k IHs already pushed).
(
&mut self,
field_idx: usize,
block_ind_idx: usize,
n_params: usize,
n_fields: usize,
k: usize, // number of IHs already pushed before this one
minor_saved: usiz
| 2816 | sp.clone() |
| 2817 | }; |
| 2818 | ctor_app = self.intern(KExpr::app(ctor_app, lifted)); |
| 2819 | } |
| 2820 | } |
| 2821 | for i in 0..n_fields { |
| 2822 | let fvar = self.intern(KExpr::var((n_binders - 1 - i) as u64, anon())); |
| 2823 | ctor_app = self.intern(KExpr::app(ctor_app, fvar)); |
| 2824 | } |
| 2825 | conclusion = self.intern(KExpr::app(conclusion, ctor_app)); |
| 2826 | |
| 2827 | // Fold: ∀ (ihs...) (fields...), conclusion (from inside out) |
| 2828 | // Pop IHs first (innermost) |
| 2829 | for i in (0..n_ihs).rev() { |
| 2830 | self.lctx.truncate(self.lctx.len() - 1); |
| 2831 | conclusion = self.intern(KExpr::all( |
| 2832 | anon(), |
| 2833 | bi_default(), |
| 2834 | ih_domains[i].clone(), |
| 2835 | conclusion, |
| 2836 | )); |
| 2837 | } |
| 2838 | // Pop fields |
| 2839 | for i in (0..n_fields).rev() { |
| 2840 | self.lctx.truncate(self.lctx.len() - 1); |
| 2841 | conclusion = self.intern(KExpr::all( |
| 2842 | anon(), |
| 2843 | bi_default(), |
| 2844 | field_domains[i].clone(), |
| 2845 | conclusion, |
| 2846 | )); |
| 2847 | } |
| 2848 | |
| 2849 | self.lctx.truncate(saved); |
| 2850 | Ok(conclusion) |
| 2851 | } |
| 2852 | |
| 2853 | /// Build an IH type for a recursive field. |
| 2854 | /// |
| 2855 | /// For a direct recursive field (type = `I_bi params idx_args`): |
| 2856 | /// IH = `motive_bi(idx_args, field_var)` |
| 2857 | /// |
| 2858 | /// For a forall-wrapped recursive field (type = `∀ xs, I_bi params idx_args(xs)`): |
| 2859 | /// IH = `∀ xs, motive_bi(idx_args(xs), field xs)` |
| 2860 | /// |
| 2861 | /// Called when depth = minor_saved + n_fields + k (k IHs already pushed). |
| 2862 | fn build_direct_ih( |
| 2863 | &mut self, |
| 2864 | field_idx: usize, |
| 2865 | block_ind_idx: usize, |
| 2866 | n_params: usize, |
| 2867 | n_fields: usize, |
| 2868 | k: usize, // number of IHs already pushed before this one |
| 2869 | minor_saved: usize, // depth at entry of build_minor_at_depth |
| 2870 | motive_base: usize, |
| 2871 | field_domains: &[KExpr<M>], |
| 2872 | block_addrs: &[Address], |
| 2873 | ) -> Result<KExpr<M>, TcError<M>> { |
| 2874 | let anon = || M::meta_field(ix_common::env::Name::anon()); |
| 2875 | let bi_default = || M::meta_field(ix_common::env::BinderInfo::Default); |
no test coverage detected