| 1582 | &self, |
| 1583 | reason: &str, |
| 1584 | id: Option<&KId<M>>, |
| 1585 | idx: usize, |
| 1586 | a: &KExpr<M>, |
| 1587 | b: &KExpr<M>, |
| 1588 | ) { |
| 1589 | let Some(filter) = IX_ETA_TRACE.as_ref() else { |
| 1590 | return; |
| 1591 | }; |
| 1592 | if !self.debug_label_matches_env() { |
| 1593 | return; |
| 1594 | } |
| 1595 | let id_s = id.map_or_else(|| "<none>".into(), |id| id.to_string()); |
| 1596 | if !filter.is_empty() && !id_s.contains(filter) { |
| 1597 | return; |
| 1598 | } |
| 1599 | eprintln!( |
| 1600 | "[eta] const={} depth={} reason={} id={} idx={} a={} b={}", |
| 1601 | self.debug_label.as_deref().unwrap_or("<unknown>"), |
| 1602 | self.def_eq_depth, |
| 1603 | reason, |
| 1604 | id_s, |
| 1605 | idx, |
| 1606 | compact_def_eq_expr(a), |
| 1607 | compact_def_eq_expr(b) |
| 1608 | ); |
| 1609 | } |
| 1610 | } |
| 1611 | |
| 1612 | enum LazyDeltaStep { |
| 1613 | Equal, |
| 1614 | Unknown, |
| 1615 | Continue, |
| 1616 | } |