refactor: tidy up

also remove `InteractiveGoals.deleted?` because it is not used yet.

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -171,7 +171,11 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
             let goals : Widget.InteractiveGoals := {goals}
             if useAfter then
               -- add a goal diff
-              Widget.diffInteractiveGoals ti.goalsBefore.toArray goals
+              try
+                Widget.diffInteractiveGoals ti.goalsBefore.toArray goals
+              catch e =>
+                let msg ← e.toMessageData.format
+                return {goals with message? := s!"internal error when diffing goals:\n{msg}"}
             else
               return goals
           )

src/Lean/Widget/Diff.lean

@@ -13,41 +13,40 @@ namespace Lean.Widget
 
 open Server Std Lean SubExpr
 
--- def getMvars (e : Expr) : Set (Expr) :=
-
 open Lean.Expr in
 /-- Define `m₁` to be the parent of `m₂` in a given mvar-context when `m₁` has been
 assigned with an expression containing `m₂`.
 
 Some technicalities:
 Suppose `m₁ : (n : Nat) → P`, and the new goal `n : Nat ⊢ m₂ : P` was got with an application of `intro`.
 Now, `m₁` is assigned the expression `fun (n : Nat) => m₃ n`.
-`m₃` is an auxilliary mvar with a delayed assignment.
+`m₃` is an auxilliary mvar with a delayed assignment, so we have to look a step further if there is a delayed mvar.
 
- -/
-partial def isParent (m₁ m₂ : MVarId) : MetaM Bool := do
-  let some assignment ← Lean.getExprMVarAssignment? m₁ | return false
-  let assignment ← instantiateMVars assignment
-  let r ← assignment.findExtM? (fun e => do
-    if !e.hasMVar then return FindStep.done else
-    match e with
-    | .mvar m =>
-      if m == m₂ then
-        return FindStep.found
-      let m' ← getDelayedMVarRoot m
-      if m' == m₂ then
-        return FindStep.found
-      if m' != m ∧ (← m'.isAssigned) then
-        if ← isParent m' m₂ then -- probably dodgy recursion
+-/
+partial def isParent (m₁ m₂ : MVarId): MetaM Bool := core m₁ 2
+  where core (m₁ : MVarId) (fuel : Nat) : MetaM Bool := do
+    let some assignment ← Lean.getExprMVarAssignment? m₁ | return false
+    let assignment ← instantiateMVars assignment
+    let r ← assignment.findExtM? (fun e => do
+      if !e.hasMVar then return FindStep.done else
+      match e with
+      | .mvar m =>
+        if m == m₂ then
           return FindStep.found
-      return FindStep.done
-    | _ => return FindStep.visit
-  )
-  return r.isSome
+        let m' ← getDelayedMVarRoot m
+        if m' == m₂ then
+          return FindStep.found
+        if m' != m ∧ (← m'.isAssigned) ∧ fuel > 0 then
+          if ← core m' (fuel - 1) then -- [todo] is this wf without fuel?
+            return FindStep.found
+        return FindStep.done
+      | _ => return FindStep.visit
+    )
+    return r.isSome
 
 /-- A marker for a point in the expression where a subexpression has been inserted.
 
-NOTE: in the future it may make sense to add `deleted` or `end_insert` tags too.
+NOTE: in the future we may add other tags such as `deleted` or `end_insert`.
   -/
 inductive ExprDiffPoint where
   | inserted
@@ -65,19 +64,27 @@ instance : FromJson ExprDiffPoint where
 instance : ToJson ExprDiffPoint where
   toJson x := x.toString |> Json.str
 
+/-- A description of the differences between a pair of expressions `e₀`, `e₁`.
+The information is only used to display a 'visual diff' for `e₁`. -/
 structure ExprDiff where
+  /-- A map from subexpr positions in `e₁` to 'diff points' which are tags
+  describing how the expression is changed at the given position.-/
   changes : PosMap ExprDiffPoint := ∅
 
 instance : EmptyCollection ExprDiff := ⟨{}⟩
 instance : Append ExprDiff where
   append a b := {changes := RBMap.mergeBy (fun _ _ b => b) a.changes b.changes}
 
-def ExprDiff.tell (p : Pos) (d : ExprDiffPoint) : ExprDiff :=
+/-- Creates an ExprDiff with a single diff point. -/
+def ExprDiff.singleton (p : Pos) (d : ExprDiffPoint) : ExprDiff :=
   RBMap.empty |>.insert p d |> ExprDiff.mk
 
+/-- If true, the expression before and the expression after are identical. -/
 def ExprDiff.isEmpty (d : ExprDiff) : Bool :=
   RBMap.isEmpty <| d.changes
 
+/-- Determines whether the given expressions have the same function head and
+the same number of arguments. -/
 def sameHead (e₀ e₁ : Expr) : MetaM Bool := do
   if e₀ == e₁ then return true
   let f₀ := e₀.getAppFn
@@ -93,25 +100,43 @@ def ExprDiff.isRootReplacement (d : ExprDiff) : MetaM Bool := do
   | (some .inserted) => return true
   | _ => return false
 
+/-- Computes a diff between `before` and `after` expressions.
+
+This works by recursively comparing function arguments.
+
+TODO(ed):
+- diffs under binders, particularly if the binder count has changed as after `intro`.
+- experiment with a 'greatest common subexpression' design where
+  given `e₀`, `e₁`, find the greatest common subexpressions `Xs : Array Expr` and a congruence `F` such that
+  `e₀ = F[A₀[..Xs]]` and `e₀ = F[A₁[..Xs]]`. Then, we can have fancy diff highlighting where common subexpressions are not highlighted.
+ -/
 partial def exprDiff (before after : Expr) (p : Pos := Pos.root) : MetaM ExprDiff := do
   if before == after then
     return ∅
   if !(← sameHead before after) then
-    return ExprDiff.tell p ExprDiffPoint.inserted
+    return ExprDiff.singleton p ExprDiffPoint.inserted
   let afterArgs := after.getAppArgs
   let beforeArgs := before.getAppArgs
   if afterArgs.size == 0 then
-    return ExprDiff.tell p ExprDiffPoint.inserted
+    return ExprDiff.singleton p ExprDiffPoint.inserted
   let n := afterArgs.size
   let bas := Array.zip beforeArgs afterArgs
   let numDifferent := bas.filter (fun (a,b) => a != b) |>.size
   if numDifferent > 1 ∧ p != Pos.root then
-    return ExprDiff.tell p ExprDiffPoint.inserted
+    /- heuristic: if we are not at the root expression and more than one
+     argument is different, we say that the change has occurred at the head term.
+     eg if comm `x + y ↝ y + x`, we want to highlight all of `y + x`.
+     One common case is if `⊢ A = B` and a tactic rewrites both `A` and `B`.
+     in this case it looks a little better to recurse the diff to `A` and `B` separately.
+    -/
+    return ExprDiff.singleton p ExprDiffPoint.inserted
   let rs : Array ExprDiff ← bas.mapIdxM (fun i (x,y) => do
     exprDiff x y <| p.pushNaryArg n i
   )
   return rs.foldl (init := ∅) (· ++ ·)
 
+/-- Given a `diff` between `before` and `after : Expr`, and the rendered `infoAfter : CodeWithInfos` for `after`,
+this function decorates `infoAfter` with tags indicating where the expression has changed. -/
 def addDiffTags (diff : ExprDiff) (infoAfter : CodeWithInfos) : MetaM CodeWithInfos := do
   if diff.isEmpty then
     return infoAfter
@@ -126,23 +151,21 @@ def addDiffTags (diff : ExprDiff) (infoAfter : CodeWithInfos) : MetaM CodeWithIn
 open Meta
 
 def diffHypothesesBundle (ctx₀  : LocalContext) (h₁ : InteractiveHypothesisBundle) : MetaM InteractiveHypothesisBundle := do
-  let mut h₁ := h₁
+  /- Strategy: we say a hypothesis has mutated if the ppName is the same but the fvarid has changed.
+     this indicates that something like `rewrite at` has hit it. -/
   for (ppName, fvid) in Array.zip h₁.names h₁.fvarIds do
     if !(ctx₀.contains fvid) then
       if let some decl₀ := ctx₀.findFromUserName? ppName then
+        -- on the old context there was an fvar with the same name as this one.
         let t₀ := decl₀.type
         try
-          h₁ ← withTypeDiff t₀ h₁
-          return h₁
+          return ← withTypeDiff t₀ h₁
         catch e =>
           let f ← e.toMessageData.format
           return {h₁ with message? := s!"{f}"}
       else
         return {h₁ with isInserted? := true}
-  -- all fvids are present on original
-  -- [todo], not completly sure how tactics work but I think
-  -- we can assume that fvarids are refreshed if eg `rw [...] at h` is used
-  -- so on this branch we can assume no change.
+  -- all fvids are present on original so we can assume no change.
   return h₁
   where withTypeDiff (t₀ : Expr) (h₁ : InteractiveHypothesisBundle) : MetaM InteractiveHypothesisBundle := do
       let some x₁ := h₁.fvarIds[0]?
@@ -173,29 +196,29 @@ def diffInteractiveGoal (g₀ : MVarId) (i₁ : InteractiveGoal) : MetaM Interac
     | throwError "Unknown goal {g₁}"
   let t₁ ← instantiateMVars md₁.type
   let tδ ← exprDiff t₀ t₁
-  if !(← tδ.isRootReplacement) then
-    let c₁ ← addDiffTags tδ i₁.type
-    i₁ := {i₁ with type := c₁, isInserted? := false}
+  let c₁ ← addDiffTags tδ i₁.type
+  i₁ := {i₁ with type := c₁, isInserted? := false}
   return i₁
 
 def ppMvar (m : MVarId) : MetaM Format := Meta.ppExpr <| .mvar m
 
-def diffInteractiveGoals (gs₀ : Array MVarId) (igs₁ : InteractiveGoals) : MetaM InteractiveGoals := do
-  let goals ← igs₁.goals.mapM (fun ig₁ => do
+/-- Modifies `goalsAfter` with additional information about how it is different to `goalsBefore`.  -/
+def diffInteractiveGoals (goalsBefore : Array MVarId) (goalsAfter : InteractiveGoals) : MetaM InteractiveGoals := do
+  let goals ← goalsAfter.goals.mapM (fun ig₁ => do
     let some g₁ := ig₁.mvarId?
       | return {ig₁ with message? := "error: goal not found"}
     withGoalCtx (g₁ : MVarId) (fun _lctx₁ _md₁ => do
       -- if the goal is present on the previous version then continue
-      if gs₀.any (fun g₀ => g₀ == g₁) then
+      if goalsBefore.any (fun g₀ => g₀ == g₁) then
         return {ig₁ with isInserted? := none}
-      let some g₀ ← gs₀.findM? (fun g₀ => isParent g₀ g₁)
+      let some g₀ ← goalsBefore.findM? (fun g₀ => isParent g₀ g₁)
         | return {ig₁ with
           isInserted? := true
         }
       let ig₁ ← diffInteractiveGoal g₀ ig₁
       return ig₁
     )
   )
-  return {igs₁ with goals := goals}
+  return {goalsAfter with goals := goals}
 
 end Lean.Widget

src/Lean/Widget/InteractiveGoal.lean

@@ -96,23 +96,12 @@ end InteractiveTermGoal
 
 structure InteractiveGoals where
   goals : Array InteractiveGoal
-  /-- Positions between items in the array where there used to be an item that has now been deleted.
-
-  E.g., deleting the first item would give `[0]`.
-  If there are `n` items, deleting the last item would give `[n]`.
-
-  We can render little red triangles in the margin indicating that an item was deleted at a particular position. -/
-  deleted? : Option (Array Nat) := none
   /-- An optional string to show the user after all of the goals. This is useful for debugging.-/
   message? : Option (String) := none
   deriving RpcEncodable
 
-def InteractiveGoals.deleted (g : InteractiveGoals) : Array Nat :=
-  g.deleted?.getD ∅
-
 def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
   goals := l.goals ++ r.goals
-  deleted? := Option.merge (fun ld rd => ld ++ rd.map (· + l.goals.size)) l.deleted? r.deleted?
   message? := Option.merge (fun ld rd => s!"{ld}\n{rd}") l.message? r.message?
 
 instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩