feat: goal-diffs

src/Init/Data/List/Basic.lean

@@ -456,11 +456,22 @@ def isPrefixOf [BEq α] : List α → List α → Bool
   | _,     []    => false
   | a::as, b::bs => a == b && isPrefixOf as bs
 
+/-- `isPrefixOf? l₁ l₂` returns `some t` when `l₂ == l₁ ++ t`. -/
+def isPrefixOf? [BEq α] : List α → List α → Option (List α)
+  | [], l₂ => some l₂
+  | _, [] => none
+  | (x₁ :: l₁), (x₂ :: l₂) =>
+    if x₁ == x₂ then isPrefixOf? l₁ l₂ else none
+
 /--  `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`.
 That is, there exists a `t` such that `l₂ == t ++ l₁`. -/
 def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
   isPrefixOf l₁.reverse l₂.reverse
 
+/-- `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.-/
+def isSuffixOf? [BEq α] (l₁ l₂ : List α) : Option (List α) :=
+  Option.map List.reverse <| isPrefixOf? l₁.reverse l₂.reverse
+
 @[specialize] def isEqv : List α → List α → (α → α → Bool) → Bool
   | [],    [],    _   => true
   | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv

src/Init/Data/Option/Basic.lean

@@ -76,6 +76,14 @@ instance (r : α → α → Prop) [s : DecidableRel r] : DecidableRel (Option.lt
   | some _, none   => isFalse not_false
   | none,   none   => isFalse not_false
 
+/-- Take a pair of options and if they are both `some`, apply the given fn to produce an output.
+Otherwise act like `orElse`. -/
+def merge (fn : α → α → α) : Option α → Option α → Option α
+  | none  , none   => none
+  | some x, none   => some x
+  | none  , some y => some y
+  | some x, some y => some <| fn x y
+
 end Option
 
 deriving instance DecidableEq for Option

src/Lean/Data/RBMap.lean

@@ -346,6 +346,9 @@ instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
 @[inline] def fromList (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
   l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β cmp)
 
+@[inline] def fromArray (l : Array (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
+  l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β cmp)
+
 /-- Returns true if the given predicate is true for all items in the RBMap. -/
 @[inline] def all : RBMap α β cmp → (α → β → Bool) → Bool
   | ⟨t, _⟩, p => t.all p

src/Lean/Data/RBTree.lean

@@ -89,6 +89,9 @@ instance [Repr α] : Repr (RBTree α cmp) where
 def fromList (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=
   l.foldl insert (mkRBTree α cmp)
 
+def fromArray (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp :=
+  l.foldl insert (mkRBTree α cmp)
+
 @[inline] def all (t : RBTree α cmp) (p : α → Bool) : Bool :=
   RBMap.all t (fun a _ => p a)
 

src/Lean/Expr.lean

@@ -852,6 +852,17 @@ def getForallBody : Expr → Expr
   | forallE _ _ b .. => getForallBody b
   | e                => e
 
+def getForallBodyMaxDepth : (maxDepth : Nat) → Expr → Expr
+  | (n+1), forallE _ _ b _ => getForallBodyMaxDepth n b
+  | 0, e => e
+  | _, e => e
+
+/-- Given a sequence of nested foralls `(a₁ : α₁) → ... → (aₙ : αₙ) → _`,
+returns the names `[a₁, ... aₙ]`. -/
+def getForallBinderNames : Expr → List Name
+  | forallE n _ b _ => n :: getForallBinderNames b
+  | _ => []
+
 /--
 If the given expression is a sequence of
 function applications `f a₁ .. aₙ`, return `f`.

src/Lean/Meta/Basic.lean

@@ -704,6 +704,11 @@ def getLocalDeclFromUserName (userName : Name) : MetaM LocalDecl := do
   | some d => pure d
   | none   => throwError "unknown local declaration '{userName}'"
 
+/-- Given a user-facing name for a free variable, return the free variable or throw if not declared. -/
+def getFVarFromUserName (userName : Name) : MetaM Expr := do
+  let d ← getLocalDeclFromUserName userName
+  return Expr.fvar d.fvarId
+
 /--
 Lift a `MkBindingM` monadic action `x` to `MetaM`.
 -/

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -47,7 +47,7 @@ structure State where
   /-- We attach `Elab.Info` at various locations in the `Syntax` output in order to convey
   its semantics. While the elaborator emits `InfoTree`s, here we have no real text location tree
   to traverse, so we use a flattened map. -/
-  infos    : Std.RBMap Pos Info compare := {}
+  infos    : PosMap Info := {}
   /-- See `SubExpr.nextExtraPos`. -/
   holeIter : SubExpr.HoleIterator := {}
 
@@ -268,10 +268,10 @@ to true or `pp.notation` is set to false, it will not be called at all.",
 
 end Delaborator
 
-open SubExpr (Pos)
+open SubExpr (Pos PosMap)
 open Delaborator (OptionsPerPos topDownAnalyze)
 
-def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × Std.RBMap Pos Elab.Info compare) := do
+def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × PosMap Elab.Info) := do
   /- Using `erasePatternAnnotations` here is a bit hackish, but we do it
      `Expr.mdata` affects the delaborator. TODO: should we fix that? -/
   let e ← Meta.erasePatternRefAnnotations e

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -16,6 +16,7 @@ import Lean.Server.References
 import Lean.Server.GoTo
 
 import Lean.Widget.InteractiveGoal
+import Lean.Widget.Diff
 
 namespace Lean.Server.FileWorker
 open Lsp
@@ -162,19 +163,33 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
   withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
     (notFoundX := return none) fun snap => do
       if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } =>
-          let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
-          let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
-          ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPForTacticGoal (Widget.goalToInteractive g))
-        return some { goals := goals.toArray }
+        let goals : List Widget.InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+          let ciAfter := { ci with mctx := ti.mctxAfter }
+          let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
+          -- compute the interactive goals
+          let goals ← ci.runMetaM {} (do
+            let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
+            let goals ← goals.mapM (fun g => Meta.withPPForTacticGoal (Widget.goalToInteractive g))
+            return {goals}
+          )
+          -- compute the goal diff
+          let goals ← ciAfter.runMetaM {} (do
+              try
+                Widget.diffInteractiveGoals useAfter ti goals
+              catch _ =>
+                -- fail silently, since this is just a bonus feature
+                return goals
+          )
+          return goals
+        return some <| goals.foldl (· ++ ·) ∅
       else
         return none
 
 open Elab in
 def handlePlainGoal (p : PlainGoalParams)
     : RequestM (RequestTask (Option PlainGoal)) := do
   let t ← getInteractiveGoals p
-  return t.map <| Except.map <| Option.map <| fun ⟨goals⟩ =>
+  return t.map <| Except.map <| Option.map <| fun {goals, ..} =>
     if goals.isEmpty then
       { goals := #[], rendered := "no goals" }
     else

src/Lean/SubExpr.lean

@@ -98,6 +98,14 @@ def pushNaryFn (numArgs : Nat) (p : Pos) : Pos :=
 def pushNaryArg (numArgs argIdx : Nat) (p : Pos) : Pos :=
   show Nat from p.asNat * (maxChildren ^ (numArgs - argIdx)) + 1
 
+def pushNthBindingDomain : (binderIdx : Nat) → Pos → Pos
+  | 0, p => p.pushBindingDomain
+  | (n+1), p => pushNthBindingDomain n p.pushBindingBody
+
+def pushNthBindingBody : (numBinders : Nat) → Pos → Pos
+  | 0, p => p
+  | (n+1), p => pushNthBindingBody n p.pushBindingBody
+
 protected def toString (p : Pos) : String :=
   p.toArray.toList
   |>.map toString
@@ -117,9 +125,18 @@ protected def fromString? : String → Except String Pos
     | "" :: tail => Pos.ofArray <$> tail.toArray.mapM ofStringCoord
     | ss => error s!"malformed {ss}"
 
+protected def fromString! (s : String) : Pos :=
+  match Pos.fromString? s with
+  | Except.ok a => a
+  | Except.error e => panic! e
+
 instance : Ord Pos := show Ord Nat by infer_instance
 instance : DecidableEq Pos := show DecidableEq Nat by infer_instance
 instance : ToString Pos := ⟨Pos.toString⟩
+instance : EmptyCollection Pos := ⟨root⟩
+instance : Repr Pos where
+  reprPrec p _ := f!"Pos.fromString! {repr p.toString}"
+
 
 -- Note: we can't send the bare Nat over the wire because Json will convert to float
 -- if the nat is too big and least significant bits will be lost.
@@ -150,6 +167,19 @@ def mkRoot (e : Expr) : SubExpr := ⟨e, Pos.root⟩
 /-- Returns true if the selected subexpression is the topmost one.-/
 def isRoot (s : SubExpr) : Bool := s.pos.isRoot
 
+/-- Map from subexpr positions to values. -/
+abbrev PosMap (α : Type u) := Std.RBMap Pos α compare
+
+def bindingBody! : SubExpr → SubExpr
+  | ⟨.forallE _ _ b _, p⟩ => ⟨b, p.pushBindingBody⟩
+  | ⟨.lam _ _ b _, p⟩ => ⟨b, p.pushBindingBody⟩
+  | _ => panic! "subexpr is not a binder"
+
+def bindingDomain! : SubExpr → SubExpr
+  | ⟨.forallE _ t _ _, p⟩ => ⟨t, p.pushBindingDomain⟩
+  | ⟨.lam _ t _ _, p⟩ => ⟨t, p.pushBindingDomain⟩
+  | _ => panic! "subexpr is not a binder"
+
 end SubExpr
 
 open SubExpr in