( intern: &mut InternTable<M>, hash: blake3::Hash, build: impl FnOnce(Addr) -> KExpr<M>, stats: &mut ConvertStats, )
| 292 | } |
| 293 | |
| 294 | /// Universe counterpart of [`timed_intern_or_build`]. |
| 295 | #[inline] |
| 296 | fn timed_intern_univ<M: KernelMode>( |
| 297 | intern: &mut InternTable<M>, |
| 298 | u: KUniv<M>, |
| 299 | stats: &mut ConvertStats, |
| 300 | ) -> KUniv<M> { |
| 301 | if !stats.enabled { |
| 302 | return intern.intern_univ(u); |
| 303 | } |
| 304 | let t0 = Instant::now(); |
| 305 | let key = super::env::univ_key(&u); |
| 306 | let result = if let Some(existing) = intern.try_get_univ(&key) { |
| 307 | stats.intern_univ_get_hits += 1; |
| 308 | existing |
| 309 | } else { |
| 310 | intern.intern_univ(u) |
| 311 | }; |
| 312 | stats.intern_univ_calls += 1; |
| 313 | stats.intern_univ_ns += elapsed_ns(t0); |
| 314 | result |
| 315 | } |
| 316 | |
| 317 | /// Key-first interning. Builds the shallow structural key from already |
| 318 | /// canonical children, asks the intern table for an existing canonical |
| 319 | /// KExpr; only on a miss does it call `build()` to allocate a new KExpr |
| 320 | /// (which takes a fresh uid). |
| 321 | /// |
| 322 | /// Why this exists: profiling on Mathlib showed the construction + |
| 323 | /// interning pair dominates `convert` worker-sum, and most constructed |
| 324 | /// values are immediately discarded for an existing canonical Arc. By |
| 325 | /// probing with just the shallow key we skip construction entirely on a |
| 326 | /// hit. (Historically the probe key was a precomputed blake3 content |
| 327 | /// hash; the shallow key preserves the skip while removing the hash.) |
| 328 | #[inline] |
| 329 | fn timed_intern_or_build<M: KernelMode>( |
no test coverage detected