Check definitional equality of two expressions.
(
&mut self,
a: &KExpr<M>,
b: &KExpr<M>,
)
| 56 | |
| 57 | /// Step journal (`IX_STEP_TRACE=1`): one `[deq] <fuel> <a8> ~ <b8>` line |
| 58 | /// per `is_def_eq` entry (plus `[whnf+]` lines in whnf.rs), mirroring the |
| 59 | /// Lean kernel's `IX_TC_STEP_TRACE` journal (`Ix.Tc` / `TcM.stepTrace`). |
| 60 | /// Diffing the two sequences localizes a behavioral divergence at the |
| 61 | /// first fork (workflow in `Ix/Tc/ParCheck.lean`). Unscoped by design — |
| 62 | /// pair with a seeded single-constant run (`--consts <name>`). |
| 63 | pub(crate) static IX_STEP_TRACE: crate::EnvFlag = |
| 64 | crate::EnvFlag::new(|| crate::env_var("IX_STEP_TRACE").is_ok()); |
| 65 | |
| 66 | impl<M: KernelMode> TypeChecker<'_, M> { |
| 67 | /// Check definitional equality of two expressions. |
| 68 | pub fn is_def_eq( |
| 69 | &mut self, |
| 70 | a: &KExpr<M>, |
| 71 | b: &KExpr<M>, |
| 72 | ) -> Result<bool, TcError<M>> { |
| 73 | if *IX_DEF_EQ_COUNT_LOG { |
| 74 | let n = DEF_EQ_COUNT.fetch_add(1, std::sync::atomic::Ordering::Relaxed); |
| 75 | if n.is_multiple_of(100_000) && n > 0 { |
| 76 | log::info!("[is_def_eq] count={n}"); |
| 77 | } |
| 78 | } |
| 79 | crate::profile::bump_def_eq(); |
| 80 | if *IX_STEP_TRACE { |
| 81 | eprintln!( |
| 82 | "[deq] {} {} ~ {}", |
| 83 | self.fuel_used(), |
| 84 | &a.hash_key(), |
| 85 | &b.hash_key(), |
| 86 | ); |
| 87 | } |
| 88 | if a.ptr_eq(b) { |
| 89 | return Ok(true); |
| 90 | } |
| 91 | if a.hash_key() == b.hash_key() { |
| 92 | // Hashes are alpha-invariant in both `Anon` and `Meta` modes — see |
| 93 | // `KExpr::lam_hash` etc., which deliberately omit binder `name`/ |
| 94 | // `bi`/`mdata` from the content hash. So hash equality is the only |
| 95 | // structural alpha-equivalence fast-path we need; an earlier |
| 96 | // additional `compare_kexpr` call here was redundant. |
| 97 | return Ok(true); |
| 98 | } |
| 99 | |
| 100 | // Diagnostic trace: emit a `[deq]` line when either side's head |
| 101 | // constant name contains the configured substring. Keeps output |
| 102 | // manageable — a naive unconditional trace blows out the log. |
| 103 | let trace_active = if let Some(prefix) = IX_DEF_EQ_TRACE.as_ref() { |
| 104 | let a_hit = head_const_name(a).is_some_and(|n| n.contains(prefix)); |
| 105 | let b_hit = head_const_name(b).is_some_and(|n| n.contains(prefix)); |
| 106 | if a_hit || b_hit { |
| 107 | log::info!( |
| 108 | "[deq] depth={} a={}", |
| 109 | self.def_eq_depth, |
| 110 | compact_def_eq_expr(a) |
| 111 | ); |
| 112 | log::info!( |
| 113 | "[deq] depth={} b={}", |
| 114 | self.def_eq_depth, |
| 115 | compact_def_eq_expr(b) |