(
&mut self,
a: &mut KExpr<M>,
b: &mut KExpr<M>,
)
| 1412 | /// previous `u32` encoding mapped `Abbrev` to `u32::MAX - 1` and saturated |
| 1413 | /// `Regular(h)` to `h.saturating_add(1)`, which collapsed at `h ≥ u32::MAX-2` |
| 1414 | /// — flipping delta direction in the rare case of an `Abbrev` paired with |
| 1415 | /// a maximally heavy regular definition. The structured tuple matches |
| 1416 | /// Lean's `compare(d_t->get_hints(), d_s->get_hints())` |
| 1417 | /// (`type_checker.cpp:910`): |
| 1418 | /// |
| 1419 | /// - `Opaque` / `Theorem` / unknown → `(0, 0)` |
| 1420 | /// - `Regular(h)` → `(1, h)` (ordered by height within the class) |
| 1421 | /// - `Abbrev` → `(2, 0)` (strictly greater than every `Regular(h)`) |
| 1422 | fn def_rank_id(&mut self, id: &KId<M>) -> Result<(u8, u32), TcError<M>> { |
| 1423 | use ix_common::env::ReducibilityHints; |
| 1424 | Ok(match self.try_get_const(id)? { |
| 1425 | Some(KConst::Defn { kind, hints, .. }) => match kind { |
| 1426 | DefKind::Opaque | DefKind::Theorem => (0, 0), |
| 1427 | DefKind::Definition => match hints { |
| 1428 | ReducibilityHints::Opaque => (0, 0), |
| 1429 | ReducibilityHints::Regular(h) => (1, h), |
| 1430 | ReducibilityHints::Abbrev => (2, 0), |
| 1431 | }, |
| 1432 | }, |
| 1433 | _ => (0, 0), |
| 1434 | }) |
| 1435 | } |
| 1436 | |
| 1437 | // ----------------------------------------------------------------------- |
| 1438 | // Post-delta congruence and projection unfolding (C5, C6) |
| 1439 | // ----------------------------------------------------------------------- |
| 1440 | |
| 1441 | /// Structural congruence after lazy delta exhaustion (lean4lean isDefEqConst/Proj). |
| 1442 | /// Checks Const-Const, Var-Var, Prj-Prj without further reduction. |
| 1443 | fn try_structural_congruence( |
| 1444 | &mut self, |
| 1445 | a: &KExpr<M>, |
| 1446 | b: &KExpr<M>, |
| 1447 | ) -> Result<bool, TcError<M>> { |
| 1448 | match (a.data(), b.data()) { |
| 1449 | (ExprData::Const(id1, us1, _), ExprData::Const(id2, us2, _)) => Ok( |
| 1450 | id1.addr == id2.addr |
| 1451 | && us1.len() == us2.len() |
| 1452 | && us1.iter().zip(us2.iter()).all(|(u, v)| univ_eq(u, v)), |
| 1453 | ), |
| 1454 | (ExprData::Var(i, _, _), ExprData::Var(j, _, _)) => Ok(i == j), |
| 1455 | (ExprData::Prj(id1, f1, v1, _), ExprData::Prj(id2, f2, v2, _)) => { |
| 1456 | if id1.addr != id2.addr || f1 != f2 { |
| 1457 | return Ok(false); |
| 1458 | } |
| 1459 | let mut v1 = v1.clone(); |
| 1460 | let mut v2 = v2.clone(); |
| 1461 | self.lazy_delta_proj_reduction(id1, *f1, &mut v1, &mut v2) |
| 1462 | }, |
| 1463 | _ => Ok(false), |
| 1464 | } |
| 1465 | } |
| 1466 | |
| 1467 | fn lazy_delta_proj_reduction( |
| 1468 | &mut self, |
| 1469 | struct_id: &KId<M>, |
| 1470 | field: u64, |
| 1471 | a: &mut KExpr<M>, |
no test coverage detected