Check that two Lean expressions are alpha-equivalent (ignoring binder names, BinderInfo, and Mdata wrappers).
(a: &Expr, b: &Expr)
| 95 | /// Check that two Lean expressions are alpha-equivalent (ignoring binder |
| 96 | /// names, BinderInfo, and Mdata wrappers). |
| 97 | pub fn expr_alpha_eq(a: &Expr, b: &Expr) -> Result<(), String> { |
| 98 | // Strip Mdata from both sides. |
| 99 | let a = strip_mdata(a); |
| 100 | let b = strip_mdata(b); |
| 101 | |
| 102 | match (a.as_data(), b.as_data()) { |
| 103 | (ExprData::Bvar(n1, _), ExprData::Bvar(n2, _)) => { |
| 104 | if n1 == n2 { |
| 105 | Ok(()) |
| 106 | } else { |
| 107 | Err(format!( |
| 108 | "bvar mismatch: {n1} vs {n2}\n generated ctx: {}\n original ctx: {}", |
| 109 | a.pretty(), |
| 110 | b.pretty() |
| 111 | )) |
| 112 | } |
| 113 | }, |
| 114 | |
| 115 | (ExprData::Sort(l1, _), ExprData::Sort(l2, _)) => { |
| 116 | level_alpha_eq(l1, l2).map_err(|e| format!("sort: {e}")) |
| 117 | }, |
| 118 | |
| 119 | (ExprData::Const(n1, lvls1, _), ExprData::Const(n2, lvls2, _)) => { |
| 120 | if n1 != n2 { |
| 121 | return Err(format!( |
| 122 | "const name mismatch: {} vs {}", |
| 123 | n1.pretty(), |
| 124 | n2.pretty() |
| 125 | )); |
| 126 | } |
| 127 | if lvls1.len() != lvls2.len() { |
| 128 | return Err(format!( |
| 129 | "const {} level count: {} vs {}", |
| 130 | n1.pretty(), |
| 131 | lvls1.len(), |
| 132 | lvls2.len(), |
| 133 | )); |
| 134 | } |
| 135 | for (i, (l1, l2)) in lvls1.iter().zip(lvls2.iter()).enumerate() { |
| 136 | level_alpha_eq(l1, l2) |
| 137 | .map_err(|e| format!("const {}.lvl[{i}]: {e}", n1.pretty()))?; |
| 138 | } |
| 139 | Ok(()) |
| 140 | }, |
| 141 | |
| 142 | (ExprData::App(f1, a1, _), ExprData::App(f2, a2, _)) => { |
| 143 | expr_alpha_eq(f1, f2).map_err(|e| format!("app.fun: {e}"))?; |
| 144 | expr_alpha_eq(a1, a2).map_err(|e| format!("app.arg: {e}")) |
| 145 | }, |
| 146 | |
| 147 | // Lam: ignore binder name and BinderInfo |
| 148 | ( |
| 149 | ExprData::Lam(_, ty1, body1, _, _), |
| 150 | ExprData::Lam(_, ty2, body2, _, _), |
| 151 | ) => { |
| 152 | expr_alpha_eq(ty1, ty2).map_err(|e| format!("lam.ty: {e}"))?; |
| 153 | expr_alpha_eq(body1, body2).map_err(|e| format!("lam.body: {e}")) |
| 154 | }, |
no test coverage detected