Check that a field domain doesn't have block inductives in negative position. Follows lean4lean's `checkPositivity`: recurse through foralls, reject if inductive in domain (negative), accept if result is a valid inductive app (direct or nested). For nested inductives `J Ds is` where `J` is external and `Ds` mention block inductives, we recursively verify that `J`'s constructors (with `Ds` substit
(
&mut self,
dom: &KExpr<M>,
block_addrs: &[Address],
)
| 1740 | Ok(None) |
| 1741 | } |
| 1742 | |
| 1743 | fn major_domain_signature_eq( |
| 1744 | &mut self, |
| 1745 | a: &KExpr<M>, |
| 1746 | b: &KExpr<M>, |
| 1747 | ) -> Result<bool, TcError<M>> { |
| 1748 | let (a_head, a_args) = collect_app_spine(a); |
| 1749 | let (b_head, b_args) = collect_app_spine(b); |
| 1750 | let (a_id, a_us) = match a_head.data() { |
| 1751 | ExprData::Const(id, us, _) => (id, us), |
| 1752 | _ => return Ok(false), |
| 1753 | }; |
| 1754 | let (b_id, b_us) = match b_head.data() { |
| 1755 | ExprData::Const(id, us, _) => (id, us), |
| 1756 | _ => return Ok(false), |
| 1757 | }; |
| 1758 | if a_id.addr != b_id.addr |
| 1759 | || a_us.len() != b_us.len() |
| 1760 | || a_args.len() != b_args.len() |
| 1761 | { |
| 1762 | return Ok(false); |
| 1763 | } |
| 1764 | if !a_us.iter().zip(b_us.iter()).all(|(u, v)| univ_eq(u, v)) { |
| 1765 | return Ok(false); |
| 1766 | } |
| 1767 | for (a_arg, b_arg) in a_args.iter().zip(b_args.iter()) { |
| 1768 | if !self.is_def_eq(a_arg, b_arg)? { |
| 1769 | return Ok(false); |
| 1770 | } |
| 1771 | } |
| 1772 | Ok(true) |
| 1773 | } |
| 1774 | |
| 1775 | fn major_domain_signature_text(domain: Option<&KExpr<M>>) -> String { |
| 1776 | match domain { |
| 1777 | Some(d) => { |
| 1778 | let (head, args) = collect_app_spine(d); |
| 1779 | match head.data() { |
| 1780 | ExprData::Const(id, _, _) => { |
| 1781 | format!("head={id} args={} dom={d}", args.len()) |
| 1782 | }, |
| 1783 | _ => format!("head=<non-const> args={} dom={d}", args.len()), |
| 1784 | } |
| 1785 | }, |
| 1786 | None => "<none>".to_string(), |
| 1787 | } |
| 1788 | } |
| 1789 | |
| 1790 | /// Dump the full per-peer alignment table when |
| 1791 | /// `populate_recursor_rules_from_block` detects canonical-order divergence. |
| 1792 | /// Prints both the kernel's reconstructed flat layout and the stored |
| 1793 | /// recursor block side-by-side, with the extracted major-domain signature |
| 1794 | /// for each peer, so the divergence can be pinpointed. |
| 1795 | /// |
| 1796 | /// Always emits to stderr (this is a real bug, not opt-in tracing). Output |
| 1797 | /// is bounded by the block's recursor count, so even a worst-case mutual |
| 1798 | /// block with many auxiliaries produces a few dozen lines, not thousands. |
| 1799 | #[allow(clippy::too_many_arguments)] |
no test coverage detected