Check positivity of a nested inductive's constructor fields. Strips `n_params` forall binders from `ctor_ty`, substitutes the actual `param_args` (with universe instantiation via `us`), then checks each remaining field domain for positivity against `augmented_addrs`.
(
&mut self,
ctor_ty: &KExpr<M>,
n_params: usize,
param_args: &[KExpr<M>],
us: &[KUniv<M>],
augmented_addrs: &[Address],
)
| 1857 | .iter() |
| 1858 | .take(n_params) |
| 1859 | .any(|a| expr_mentions_any_addr(a, block_addrs)); |
| 1860 | if !has_nested_ref { |
| 1861 | return Err(TcError::Other( |
| 1862 | "positivity: not a valid inductive app".into(), |
| 1863 | )); |
| 1864 | } |
| 1865 | |
| 1866 | // Index args (after params) must not mention block inductives |
| 1867 | for arg in args.iter().skip(n_params) { |
| 1868 | if expr_mentions_any_addr(arg, block_addrs) { |
| 1869 | return Err(TcError::Other( |
| 1870 | "positivity: index mentions block inductive".into(), |
| 1871 | )); |
| 1872 | } |
| 1873 | } |
| 1874 | |
| 1875 | // Build augmented address set: original block + external inductive's block |
| 1876 | let mut augmented: Vec<Address> = block_addrs.to_vec(); |
| 1877 | let ext_block_inductives = |
| 1878 | self.discover_block_inductives(&block)?; |
| 1879 | for ext_id in &ext_block_inductives { |
| 1880 | if !augmented.contains(&ext_id.addr) { |
| 1881 | augmented.push(ext_id.addr.clone()); |
| 1882 | } |
| 1883 | } |
| 1884 | |
| 1885 | // Collect param args and universe args for substitution |
| 1886 | let param_args: Vec<KExpr<M>> = |
| 1887 | args.iter().take(n_params).cloned().collect(); |
| 1888 | let us = us.clone(); |
| 1889 | |
| 1890 | // For each constructor, strip params, substitute actual param args, |
| 1891 | // and recursively check positivity of each field domain |
| 1892 | for ctor_id in &ctors { |
| 1893 | let ctor_ty = match self.get_const(ctor_id)? { |
| 1894 | KConst::Ctor { ty, .. } => ty.clone(), |
| 1895 | _ => { |
| 1896 | return Err(TcError::Other( |
| 1897 | "positivity: nested ctor not found".into(), |
no test coverage detected