Function expr_congruent

crates/kernel/src/congruence.rs:62–165

Check that a Lean-side Expr matches a zero Expr structurally.

(
  lean_expr: &lean::Expr,
  zero_expr: &KExpr<Anon>,
  nr: &NameResolver,
)

/// Check that a Lean-side Expr matches a zero Expr<Anon> structurally.
pub fn expr_congruent(
  lean_expr: &lean::Expr,
  zero_expr: &KExpr<Anon>,
  nr: &NameResolver,
) -> Result<(), String> {
  use lean::ExprData as LE;
  match (lean_expr.as_data(), zero_expr.data()) {
    (LE::Bvar(n, _), ExprData::Var(m, _, _)) => {
      let n = n.to_u64().unwrap_or(u64::MAX);
      if n == *m {
        Ok(())
      } else {
        Err(format!("var mismatch: lean={n} vs zero={m}"))
      }
    },

    (LE::Sort(l, _), ExprData::Sort(u, _)) => level_congruent(l, u, nr),

    (LE::Const(name, levels, _), ExprData::Const(id, univs, _)) => {
      match nr.resolve(name) {
        Some(expected) if expected == &id.addr => {},
        Some(expected) => {
          return Err(format!(
            "const address mismatch for {name}: expected {}, got {}",
            expected.hex(),
            id.addr.hex()
          ));
        },
        None => {
          return Err(format!("const name not found in resolver: {name}"));
        },
      }
      if levels.len() != univs.len() {
        return Err(format!(
          "const {name}: level count mismatch: {} vs {}",
          levels.len(),
          univs.len()
        ));
      }
      for (l, u) in levels.iter().zip(univs.iter()) {
        level_congruent(l, u, nr)?;
      }
      Ok(())
    },

    (LE::App(f1, a1, _), ExprData::App(f2, a2, _)) => {
      expr_congruent(f1, f2, nr)?;
      expr_congruent(a1, a2, nr)
    },

    (LE::Lam(_, ty1, body1, _, _), ExprData::Lam(_, _, ty2, body2, _))
    | (LE::ForallE(_, ty1, body1, _, _), ExprData::All(_, _, ty2, body2, _)) =>
    {
      expr_congruent(ty1, ty2, nr)?;
      expr_congruent(body1, body2, nr)
    },

    (