introduce DelabTermInfo

src/Init/Prelude.lean

@@ -648,15 +648,15 @@ set_option linter.unusedVariables.funArgs false in
 Auxiliary axiom used to implement the `sorry` term and tactic.
 
 The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`.
-It intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
+It is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
 Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
-but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
+but you can check if a declaration depends on `sorry` either directly or indirectly by looking for `sorryAx` in the output
 of the `#print axioms my_thm` command.
 
-The `synthetic` flag is false when written explicitly by the user, but it is
+The `synthetic` flag is false when a `sorry` is written explicitly by the user, but it is
 set to `true` when a tactic fails to prove a goal, or if there is a type error
 in the expression. A synthetic `sorry` acts like a regular one, except that it
-suppresses follow-up errors in order to prevent one error from causing a cascade
+suppresses follow-up errors in order to prevent an error from causing a cascade
 of other errors because the desired term was not constructed.
 -/
 @[extern "lean_sorry", never_extract]

src/Init/Tactics.lean

@@ -414,7 +414,7 @@ closing the main goal using `exact sorry`.
 This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton.
 Lean will give a warning whenever a proof uses `sorry`, so you aren't likely to miss it,
 but you can double check if a theorem depends on `sorry` by looking for `sorryAx` in the output
-of the `#print axioms my_thm` command, which is the axiom used by implementation of `sorry`.
+of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.
 -/
 macro "sorry" : tactic => `(tactic| exact sorry)
 

src/Lean/Elab/InfoTree/Main.lean

@@ -192,8 +192,12 @@ def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"
 
-def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
-  return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
+def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do
+  let loc := if let some (module, rng) := info.location? then f!"{module} {rng.start}-{rng.end}" else "none"
+  return f!"DelabTermInfo @ {← TermInfo.format ctx info.toTermInfo}\n\
+    Location: {loc}\n\
+    Docstring: {repr info.docString?}\n\
+    Explicit: {info.explicit}"
 
 def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
   f!"Choice @ {formatElabInfo ctx info.toElabInfo}"
@@ -211,7 +215,7 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofCustomInfo i         => pure <| Std.ToFormat.format i
   | ofFVarAliasInfo i      => pure <| i.format
   | ofFieldRedeclInfo i    => pure <| i.format ctx
-  | ofOmissionInfo i       => i.format ctx
+  | ofDelabTermInfo i      => i.format ctx
   | ofChoiceInfo i         => pure <| i.format ctx
 
 def Info.toElabInfo? : Info → Option ElabInfo
@@ -227,7 +231,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofCustomInfo _         => none
   | ofFVarAliasInfo _      => none
   | ofFieldRedeclInfo _    => none
-  | ofOmissionInfo i       => some i.toElabInfo
+  | ofDelabTermInfo i      => some i.toElabInfo
   | ofChoiceInfo i         => some i.toElabInfo
 
 /--

src/Lean/Elab/InfoTree/Types.lean

@@ -10,6 +10,7 @@ import Lean.Data.OpenDecl
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Data.Json
+import Lean.Data.Lsp.Basic
 import Lean.Server.Rpc.Basic
 import Lean.Widget.Types
 
@@ -168,14 +169,22 @@ structure FieldRedeclInfo where
   stx : Syntax
 
 /--
-Denotes information for the term `⋯` that is emitted by the delaborator when omitting a term
-due to `pp.deepTerms false` or `pp.proofs false`. Omission needs to be treated differently from regular terms because
+Denotes TermInfo with additional configurations to control interactions with delaborated terms.
+
+For example, the omission term `⋯` that is emitted by the delaborator when omitting a term
+due to `pp.deepTerms false` or `pp.proofs false` uses this.
+Omission needs to be treated differently from regular terms because
 it has to be delaborated differently in `Lean.Widget.InteractiveDiagnostics.infoToInteractive`:
 Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with
-regular delaboration settings.
+regular delaboration settings. Additionally, omissions come with a reason for omission.
 -/
-structure OmissionInfo extends TermInfo where
-  reason : String
+structure DelabTermInfo extends TermInfo where
+  /-- A module and source range to use for "go to definition", to override the default. -/
+  location? : Option (Name × Lsp.Range) := none
+  /-- Text to use to override the docstring. -/
+  docString? : Option String := none
+  /-- Whether to use explicit mode when pretty printing the term on hover. -/
+  explicit : Bool := true
 
 /--
 Indicates that all overloaded elaborators failed. The subtrees of a `ChoiceInfo` node are the
@@ -198,7 +207,7 @@ inductive Info where
   | ofCustomInfo (i : CustomInfo)
   | ofFVarAliasInfo (i : FVarAliasInfo)
   | ofFieldRedeclInfo (i : FieldRedeclInfo)
-  | ofOmissionInfo (i : OmissionInfo)
+  | ofDelabTermInfo (i : DelabTermInfo)
   | ofChoiceInfo (i : ChoiceInfo)
   deriving Inhabited
 

src/Lean/Meta.lean

@@ -17,6 +17,7 @@ import Lean.Meta.Instances
 import Lean.Meta.AbstractMVars
 import Lean.Meta.SynthInstance
 import Lean.Meta.AppBuilder
+import Lean.Meta.Sorry
 import Lean.Meta.Tactic
 import Lean.Meta.KAbstract
 import Lean.Meta.RecursorInfo

src/Lean/Meta/AppBuilder.lean

@@ -5,11 +5,9 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Structure
-import Lean.Util.Recognizers
 import Lean.Meta.SynthInstance
 import Lean.Meta.Check
 import Lean.Meta.DecLevel
-import Lean.Data.Lsp.Utf16
 
 namespace Lean.Meta
 
@@ -514,65 +512,6 @@ def mkSome (type value : Expr) : MetaM Expr := do
   let u ← getDecLevel type
   return mkApp2 (mkConst ``Option.some [u]) type value
 
-/--
-Returns `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error.
--/
-def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
-  let u ← getLevel type
-  return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)
-
-structure SorryLabelView where
-  module? : Option (Name × Lsp.Range) := none
-
-def SorryLabelView.encode (view : SorryLabelView) : CoreM Name :=
-  let name :=
-    if let some (mod, range) := view.module? then
-      mod |>.num range.start.line |>.num range.start.character |>.num range.end.line |>.num range.end.character
-    else
-      .anonymous
-  mkFreshUserName (name.str "_unique_sorry")
-
-def SorryLabelView.decode? (name : Name) : Option SorryLabelView := do
-  guard <| name.hasMacroScopes
-  let .str name "_unique_sorry" := name.eraseMacroScopes | failure
-  if let .num (.num (.num (.num name startLine) startChar) endLine) endChar := name then
-    return { module? := some (name, ⟨⟨startLine, startChar⟩, ⟨endLine, endChar⟩⟩) }
-  else
-    failure
-
-/--
-Makes a `sorryAx` that encodes the current ref into the term to support "go to definition" for the `sorry`.
-If `unique` is true, the `sorry` is unique, in the sense that it is not defeq to any other `sorry` created by `mkLabeledSorry`.
--/
-def mkLabeledSorry (type : Expr) (synthetic : Bool) (unique : Bool) : MetaM Expr := do
-  let tag ←
-    if let (some pos, some endPos) := ((← getRef).getPos?, (← getRef).getTailPos?) then
-      let range := (← getFileMap).utf8RangeToLspRange ⟨pos, endPos⟩
-      SorryLabelView.encode { module? := (← getMainModule, range) }
-    else
-      SorryLabelView.encode {}
-  if unique then
-    let e ← mkSorry (mkForall `tag .default (mkConst ``Lean.Name) type) synthetic
-    return .app e (toExpr tag)
-  else
-    let e ← mkSorry (mkForall `tag .default (mkConst ``Unit) type) synthetic
-    return .app e (mkApp4 (mkConst ``Function.const [levelOne, levelOne])
-      (mkConst ``Unit) (mkConst ``Lean.Name) (mkConst ``Unit.unit) (toExpr tag))
-
-/--
-Returns a `SorryLabelView` if `e` is an application of an expression returned by `mkLabeledSorry`.
--/
-def isLabeledSorry? (e : Expr) : Option SorryLabelView := do
-  guard <| e.isAppOf ``sorryAx && e.getAppNumArgs ≥ 3
-  let arg := e.getArg! 2
-  if let some tag := arg.name? then
-    SorryLabelView.decode? tag
-  else
-    guard <| arg.isAppOfArity ``Function.const 4
-    guard <| arg.appFn!.appArg!.isAppOfArity ``Unit.unit 0
-    let some tag := arg.appArg!.name? | failure
-    SorryLabelView.decode? tag
-
 /-- Return `Decidable.decide p` -/
 def mkDecide (p : Expr) : MetaM Expr :=
   mkAppOptM ``Decidable.decide #[p, none]

src/Lean/Meta/Check.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.InferType
+import Lean.Meta.Sorry
 
 /-!
 This is not the Kernel type checker, but an auxiliary method for checking
@@ -133,6 +134,12 @@ where
           if fn? == ``OfNat.ofNat && as.size ≥ 3 && firstImplicitDiff? == some 0 then
             -- Even if there is an explicit diff, it is better to see that the type is different.
             return (a.setPPNumericTypes true, b.setPPNumericTypes true)
+          if fn? == ``sorryAx then
+            -- If these are `sorry`s with differing source positions, make sure the delaborator shows the positions.
+            if let some { module? := moda? } := isLabeledSorry? a then
+              if let some { module? := modb? } := isLabeledSorry? b then
+                if moda? != modb? then
+                  return (a.setOption `pp.sorrySource true, b.setOption `pp.sorrySource true)
           -- General case
           if let some i := firstExplicitDiff? <|> firstImplicitDiff? then
             let (ai, bi) ← visit as[i]! bs[i]!

src/Lean/Meta/Sorry.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Data.Lsp.Utf16
+import Lean.Meta.InferType
+import Lean.Util.Recognizers
+
+/-!
+# Utilities for creating and recognizing `sorry`
+
+This module
+-/
+
+namespace Lean.Meta
+
+/--
+Returns `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error.
+
+See also `Lean.Meta.mkLabeledSorry`, for creating a `sorry` that encodes the origin position of the `sorry`,
+and which has facilities for making a `sorry` that is not defeq to any other `sorry`.
+-/
+def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
+  let u ← getLevel type
+  return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)
+
+structure SorryLabelView where
+  /--
+  Records the origin module name, logical source position, and LSP range for the `sorry`.
+  The logical source position is used when displaying the sorry when the `pp.sorrySource` option is true,
+  and the LSP range is used for "go to definition".
+  -/
+  module? : Option (Name × Position × Lsp.Range) := none
+
+def SorryLabelView.encode (view : SorryLabelView) : CoreM Name :=
+  let name :=
+    if let some (mod, pos, range) := view.module? then
+      mod |>.num pos.line |>.num pos.column |>.num range.start.line |>.num range.start.character |>.num range.end.line |>.num range.end.character
+    else
+      .anonymous
+  mkFreshUserName (name.str "_sorry")
+
+def SorryLabelView.decode? (name : Name) : Option SorryLabelView := do
+  guard <| name.hasMacroScopes
+  let .str name "_sorry" := name.eraseMacroScopes | failure
+  if let .num (.num (.num (.num (.num (.num name posLine) posCol) startLine) startChar) endLine) endChar := name then
+    return { module? := some (name, ⟨posLine, posCol⟩, ⟨⟨startLine, startChar⟩, ⟨endLine, endChar⟩⟩) }
+  else
+    failure
+
+/--
+Makes a `sorryAx` that encodes the current ref into the term to support "go to definition" for the `sorry`.
+If `unique` is true, the `sorry` is unique, in the sense that it is not defeq to any other `sorry` created by `mkLabeledSorry`.
+-/
+def mkLabeledSorry (type : Expr) (synthetic : Bool) (unique : Bool) : MetaM Expr := do
+  let tag ←
+    if let (some startPos, some endPos) := ((← getRef).getPos?, (← getRef).getTailPos?) then
+      let fileMap ← getFileMap
+      let pos := fileMap.toPosition startPos
+      let range := fileMap.utf8RangeToLspRange ⟨startPos, endPos⟩
+      SorryLabelView.encode { module? := (← getMainModule, pos, range) }
+    else
+      SorryLabelView.encode {}
+  if unique then
+    let e ← mkSorry (mkForall `tag .default (mkConst ``Lean.Name) type) synthetic
+    return .app e (toExpr tag)
+  else
+    let e ← mkSorry (mkForall `tag .default (mkConst ``Unit) type) synthetic
+    let tag' := mkApp4 (mkConst ``Function.const [levelOne, levelOne]) (mkConst ``Unit) (mkConst ``Lean.Name) (mkConst ``Unit.unit) (toExpr tag)
+    return .app e tag'
+
+/--
+Returns a `SorryLabelView` if `e` is an application of an expression returned by `mkLabeledSorry`.
+If it is, then the `sorry` takes the first three arguments, and the tag is at argument 3.
+-/
+def isLabeledSorry? (e : Expr) : Option SorryLabelView := do
+  guard <| e.isAppOf ``sorryAx
+  let numArgs := e.getAppNumArgs
+  guard <| numArgs ≥ 3
+  let arg := e.getArg! 2
+  if let some tag := arg.name? then
+    SorryLabelView.decode? tag
+  else
+    guard <| arg.isAppOfArity ``Function.const 4
+    guard <| arg.appFn!.appArg!.isAppOfArity ``Unit.unit 0
+    let tag ← arg.appArg!.name?
+    SorryLabelView.decode? tag

src/Lean/Parser/Term.lean

@@ -221,7 +221,7 @@ The `sorry` term is a temporary placeholder for a missing proof or value.
 The syntax is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
 Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
 but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
-of the `#print axioms my_thm` command, which is the axiom used by implementation of `sorry`.
+of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.
 
 "Go to definition" on `sorry` will go to the source position where it was introduced.
 

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -211,6 +211,16 @@ where
     stx := stx
   }
 
+def addDelabTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false)
+    (location? : Option (Name × Lsp.Range) := none) (docString? : Option String := none) (explicit : Bool := true) : DelabM Unit := do
+  let info := Info.ofDelabTermInfo {
+    toTermInfo := ← addTermInfo.mkTermInfo stx e (isBinder := isBinder)
+    location?  := location?
+    docString? := docString?
+    explicit   := explicit
+  }
+  modify fun s => { s with infos := s.infos.insert pos info }
+
 /--
 Annotates the term with the current expression position and registers `TermInfo`
 to associate the term to the current expression.
@@ -238,6 +248,13 @@ def withAnnotateTermInfo (d : Delab) : Delab := do
   let stx ← d
   annotateTermInfo stx
 
+/--
+Modifies the delaborator so that it ensures resulting term is annotated using `annotateTermInfoUnlessAnnotated`.
+-/
+def withAnnotateTermInfoUnlessAnnotated (d : Delab) : Delab := do
+  let stx ← d
+  annotateTermInfoUnlessAnnotated stx
+
 /--
 Gets an name based on `suggestion` that is unused in the local context.
 Erases macro scopes.
@@ -297,22 +314,14 @@ inductive OmissionReason
   | deep
   | proof
   | maxSteps
-  | uniqueSorry
 
 def OmissionReason.toString : OmissionReason → String
   | deep => "Term omitted due to its depth (see option `pp.deepTerms`)."
   | proof => "Proof omitted (see option `pp.proofs`)."
   | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
-  | uniqueSorry => "This is a `sorry` term associated to a source position. Use 'Go to definition' to go there."
 
 def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
-  let info := Info.ofOmissionInfo <| ← mkOmissionInfo stx e
-  modify fun s => { s with infos := s.infos.insert pos info }
-where
-  mkOmissionInfo stx e := return {
-    toTermInfo := ← addTermInfo.mkTermInfo stx e (isBinder := false)
-    reason := reason.toString
-  }
+  addDelabTermInfo pos stx e (docString? := reason.toString) (explicit := true)
 
 /--
 Runs the delaborator `act` with increased depth.