A3: Strict positivity — block inductives must not appear in negative position.
(
&mut self,
ctor_ty: &KExpr<M>,
n_params: usize,
block_addrs: &[Address],
)
| 1701 | } |
| 1702 | self.dump_rule_rhs_first_diff(la, ra, &format!("{path}.arg"), depth + 1) |
| 1703 | }, |
| 1704 | _ => { |
| 1705 | log::info!("[rule rhs diff] first diff {path}"); |
| 1706 | log::info!(" gen: {lw}"); |
| 1707 | log::info!(" sto: {rw}"); |
| 1708 | Ok(true) |
| 1709 | }, |
| 1710 | } |
| 1711 | } |
| 1712 | |
| 1713 | /// A1: Check that the first `n_params` forall domains of ind_ty and ctor_ty agree. |
| 1714 | fn check_param_agreement( |
| 1715 | &mut self, |
| 1716 | ind_ty: &KExpr<M>, |
| 1717 | ctor_ty: &KExpr<M>, |
| 1718 | n_params: usize, |
| 1719 | ) -> Result<(), TcError<M>> { |
| 1720 | let saved = self.lctx.len(); |
| 1721 | let mut it = ind_ty.clone(); |
| 1722 | let mut ct = ctor_ty.clone(); |
| 1723 | |
| 1724 | for _ in 0..n_params { |
| 1725 | let wi = self.whnf(&it)?; |
| 1726 | let wc = self.whnf(&ct)?; |
| 1727 | match (wi.data(), wc.data()) { |
| 1728 | ( |
| 1729 | ExprData::All(_, _, i_dom, i_body, _), |
| 1730 | ExprData::All(_, _, c_dom, c_body, _), |
| 1731 | ) => { |
| 1732 | if !self.is_def_eq(i_dom, c_dom)? { |
| 1733 | self.lctx.truncate(saved); |
| 1734 | return Err(TcError::Other("param domain mismatch".into())); |
no test coverage detected