From d22916fdcd96fc7d56b007c5426bd99ce7026f8a Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 7 Oct 2022 10:01:35 +0100 Subject: [PATCH] feat: improve expression diff Added recursion cases to the diff algorithm for projections and mdata. Previously, these would be rendered as the entire expression being different but we can do better by checking if the recursion args are the same. With mdata, these are entirely ignored by the diff algorithm. --- src/Lean/Widget/Diff.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Lean/Widget/Diff.lean b/src/Lean/Widget/Diff.lean index f6f7c452e1..15ff3d74c3 100644 --- a/src/Lean/Widget/Diff.lean +++ b/src/Lean/Widget/Diff.lean @@ -107,6 +107,8 @@ partial def exprDiffCore (before after : SubExpr) : MetaM ExprDiff := do if before.expr == after.expr then return ∅ match before.expr, after.expr with + | .mdata _ e₀, _ => exprDiffCore {before with expr := e₀} after + | _, .mdata _ e₁ => exprDiffCore before {after with expr := e₁} | .app .., .app .. => let (fn₀, args₀) := after.expr.withApp Prod.mk let (fn₁, args₁) := before.expr.withApp Prod.mk @@ -128,6 +130,11 @@ partial def exprDiffCore (before after : SubExpr) : MetaM ExprDiff := do return ← exprDiffCore ⟨b₀, before.pos.pushBindingBody⟩ ⟨b₁, after.pos.pushBindingBody⟩ else return δd ++ ExprDiff.withChangePos before.pos.pushBindingBody after.pos.pushBindingBody + | .proj n₀ i₀ e₀, .proj n₁ i₁ e₁ => + if n₀ != n₁ || i₀ != i₁ then + return ExprDiff.withChange before after + else + exprDiffCore ⟨e₀, before.pos.pushProj⟩ ⟨e₁, after.pos.pushProj⟩ | _, _ => return ExprDiff.withChange before after where piDiff (before after : SubExpr) : MetaM ExprDiff := do