feat: elidible subterms (#3201)

This PR adds two new delaboration settings: `pp.deepTerms : Bool`
(default: `true`) and `pp.deepTerms.threshold : Nat` (default: `20`).

Setting `pp.deepTerms` to `false` will make the delaborator terminate
early after `pp.deepTerms.threshold` layers of recursion and replace the
omitted subterm with the symbol `⋯` if the subterm is deeper than
`pp.deepTerms.threshold / 4` (i.e. it is not shallow). To display the
omitted subterm in the InfoView, `⋯` can be clicked to open a popup with
the delaborated subterm.

<details>
<summary>InfoView with pp.deepTerms set to false (click to show
image)</summary>


![image](https://github.com/leanprover/lean4/assets/10852073/f6df8b2c-d769-41c8-821e-efd0af23ccfa)
</details>

### Implementation

- The delaborator is adjusted to use the new configuration settings and
terminate early if the threshold is exceeded and the corresponding term
to omit is shallow.
- To be able to distinguish `⋯` from regular terms, a new constructor
`Lean.Elab.Info.ofOmissionInfo` is added to `Lean.Elab.Info` that takes
a value of a new type `Lean.Elab.OmissionInfo`.
- `ofOmissionInfo` is needed in `Lean.Widget.makePopup` for the
`Lean.Widget.InteractiveDiagnostics.infoToInteractive` RPC procedure
that is used to display popups when clicking on terms in the InfoView.
It ensures that the expansion of an omitted subterm is delaborated using
`explicit := false`, which is typically set to `true` in popups for
regular terms.
- Several `Info` widget utility functions are adjusted to support
`ofOmissionInfo`.
- The list delaborator is adjusted with special support for `⋯` so that
long lists `[x₁, ..., xₖ, ..., xₙ]` are shortened to `[x₁, ..., xₖ, ⋯]`.

Author: mhuisi

RELEASES.md

@@ -196,6 +196,8 @@ example : x + foo 2 = 12 + x := by
 
 * Add language server support for [call hierarchy requests](https://www.youtube.com/watch?v=r5LA7ivUb2c) ([PR #3082](https://github.com/leanprover/lean4/pull/3082)). The change to the .ilean format in this PR means that projects must be fully rebuilt once in order to generate .ilean files with the new format before features like "find references" work correctly again.
 
+* Add pretty printer settings to omit deeply nested terms (`pp.deepTerms false` and `pp.deepTerms.threshold`) ([PR #3201](https://github.com/leanprover/lean4/pull/3201))
+
 
 v4.5.0
 ---------

src/Init/NotationExtra.lean

@@ -170,16 +170,34 @@ See [Theorem Proving in Lean 4][tpil4] for more information.
 -/
 syntax (name := calcTactic) "calc" calcSteps : tactic
 
+/--
+Denotes a term that was omitted by the pretty printer.
+This is only used for pretty printing, and it cannot be elaborated.
+The presence of `⋯` is controlled by the `pp.deepTerms` and `pp.deepTerms.threshold`
+options.
+-/
+syntax "⋯" : term
+
+macro_rules | `(⋯) => Macro.throwError "\
+  Error: The '⋯' token is used by the pretty printer to indicate omitted terms, \
+  and it cannot be elaborated. \
+  Its presence in pretty printing output is controlled by the 'pp.deepTerms' and \
+  `pp.deepTerms.threshold` options."
+
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
 
 @[app_unexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `([])
 
 @[app_unexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander
-  | `($(_) $x [])      => `([$x])
-  | `($(_) $x [$xs,*]) => `([$x, $xs,*])
-  | _                  => throw ()
+  | `($(_) $x $tail) =>
+    match tail with
+    | `([])      => `([$x])
+    | `([$xs,*]) => `([$x, $xs,*])
+    | `(⋯)       => `([$x, $tail]) -- Unexpands to `[x, y, z, ⋯]` for `⋯ : List α`
+    | _          => throw ()
+  | _ => throw ()
 
 @[app_unexpander List.toArray] def unexpandListToArray : Lean.PrettyPrinter.Unexpander
   | `($(_) [$xs,*]) => `(#[$xs,*])

src/Lean/Elab/InfoTree/Main.lean

@@ -171,6 +171,9 @@ 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}"
+
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
@@ -183,6 +186,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
 
 def Info.toElabInfo? : Info → Option ElabInfo
   | ofTacticInfo i         => some i.toElabInfo
@@ -196,6 +200,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofCustomInfo _         => none
   | ofFVarAliasInfo _      => none
   | ofFieldRedeclInfo _    => none
+  | ofOmissionInfo i       => some i.toElabInfo
 
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.

src/Lean/Elab/InfoTree/Types.lean

@@ -154,6 +154,15 @@ structure Bar extends Foo :=
 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`. 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.
+-/
+structure OmissionInfo extends TermInfo
+
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where
   | ofTacticInfo (i : TacticInfo)
@@ -167,6 +176,7 @@ inductive Info where
   | ofCustomInfo (i : CustomInfo)
   | ofFVarAliasInfo (i : FVarAliasInfo)
   | ofFieldRedeclInfo (i : FieldRedeclInfo)
+  | ofOmissionInfo (i : OmissionInfo)
   deriving Inhabited
 
 /-- The InfoTree is a structure that is generated during elaboration and used

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -40,6 +40,8 @@ structure Context where
   openDecls      : List OpenDecl
   inPattern      : Bool := false -- true when delaborating `match` patterns
   subExpr        : SubExpr
+  /-- Current recursion depth during delaboration. Used by the `pp.deepTerms false` option. -/
+  depth          : Nat := 0
 
 structure State where
   /-- We attach `Elab.Info` at various locations in the `Syntax` output in order to convey
@@ -81,8 +83,10 @@ instance (priority := low) : MonadWithReaderOf SubExpr DelabM where
 
 instance (priority := low) : MonadStateOf SubExpr.HoleIterator DelabM where
   get         := State.holeIter <$> get
-  set iter    := modify fun ⟨infos, _⟩ => ⟨infos, iter⟩
-  modifyGet f := modifyGet fun ⟨infos, iter⟩ => let (ret, iter') := f iter; (ret, ⟨infos, iter'⟩)
+  set iter    := modify fun s => { s with holeIter := iter }
+  modifyGet f := modifyGet fun s =>
+    let (ret, holeIter') := f s.holeIter
+    (ret, { s with holeIter := holeIter' })
 
 -- Macro scopes in the delaborator output are ultimately ignored by the pretty printer,
 -- so give a trivial implementation.
@@ -147,7 +151,7 @@ def getOptionsAtCurrPos : DelabM Options := do
   return opts
 
 /-- Evaluate option accessor, using subterm-specific options if set. -/
-def getPPOption (opt : Options → Bool) : DelabM Bool := do
+def getPPOption (opt : Options → α) : DelabM α := do
   return opt (← getOptionsAtCurrPos)
 
 def whenPPOption (opt : Options → Bool) (d : Delab) : Delab := do
@@ -203,10 +207,10 @@ def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
   liftM x
 
 def addTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false) : DelabM Unit := do
-  let info ← mkTermInfo stx e isBinder
+  let info := Info.ofTermInfo <| ← mkTermInfo stx e isBinder
   modify fun s => { s with infos := s.infos.insert pos info }
 where
-  mkTermInfo stx e isBinder := return Info.ofTermInfo {
+  mkTermInfo stx e isBinder := return {
     elaborator := `Delab,
     stx := stx,
     lctx := (← getLCtx),
@@ -216,22 +220,71 @@ where
  }
 
 def addFieldInfo (pos : Pos) (projName fieldName : Name) (stx : Syntax) (val : Expr) : DelabM Unit := do
-  let info ← mkFieldInfo projName fieldName stx val
+  let info := Info.ofFieldInfo <| ← mkFieldInfo projName fieldName stx val
   modify fun s => { s with infos := s.infos.insert pos info }
 where
-  mkFieldInfo projName fieldName stx val := return Info.ofFieldInfo {
+  mkFieldInfo projName fieldName stx val := return {
     projName := projName,
     fieldName := fieldName,
     lctx := (← getLCtx),
     val := val,
     stx := stx
   }
 
+def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) : 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)
+  }
+
+/--
+Runs the delaborator `act` with increased depth.
+The depth is used when `pp.deepTerms` is `false` to determine what is a deep term.
+See also `Lean.PrettyPrinter.Delaborator.Context.depth`.
+-/
+def withIncDepth (act : DelabM α) : DelabM α := fun ctx =>
+  act { ctx with depth := ctx.depth + 1 }
+
+/--
+Returns `true` if, at the current depth, we should omit the term and use `⋯` rather than
+delaborating it. This function can only return `true` if `pp.deepTerms` is set to `false`.
+It also contains a heuristic to allow "shallow terms" to be delaborated, even if they appear deep in
+an expression, which prevents terms such as atomic expressions or `OfNat.ofNat` literals from being
+delaborated as `⋯`.
+-/
+def shouldOmitExpr (e : Expr) : DelabM Bool := do
+  if ← getPPOption getPPDeepTerms then
+    return false
+
+  let depth := (← read).depth
+  let depthThreshold ← getPPOption getPPDeepTermsThreshold
+  let approxDepth := e.approxDepth.toNat
+  let depthExcess := depth - depthThreshold
+
+  let isMaxedOutApproxDepth := approxDepth >= 255
+  let isShallowExpression :=
+    !isMaxedOutApproxDepth && approxDepth <= depthThreshold/4 - depthExcess
+
+  return depthExcess > 0 && !isShallowExpression
+
 def annotateTermInfo (stx : Term) : Delab := do
   let stx ← annotateCurPos stx
   addTermInfo (← getPos) stx (← getExpr)
   pure stx
 
+
+/--
+Delaborates the current expression as `⋯` and attaches `Elab.OmissionInfo`, which influences how the
+subterm omitted by `⋯` is delaborated when hovered over.
+-/
+def omission : Delab := do
+  let stx ← `(⋯)
+  let stx ← annotateCurPos stx
+  addOmissionInfo (← getPos) stx (← getExpr)
+  pure stx
+
 partial def delabFor : Name → Delab
   | Name.anonymous => failure
   | k              =>
@@ -243,6 +296,9 @@ partial def delab : Delab := do
   checkSystem "delab"
   let e ← getExpr
 
+  if ← shouldOmitExpr e then
+    return ← omission
+
   -- no need to hide atomic proofs
   if ← pure !e.isAtomic <&&> pure !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch _ => pure false) then
     if ← getPPOption getPPProofsWithType then
@@ -251,7 +307,7 @@ partial def delab : Delab := do
     else
       return ← annotateTermInfo (← ``(_))
   let k ← getExprKind
-  let stx ← delabFor k <|> (liftM $ show MetaM _ from throwError "don't know how to delaborate '{k}'")
+  let stx ← withIncDepth <| delabFor k <|> (liftM $ show MetaM _ from throwError "don't know how to delaborate '{k}'")
   if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> pure !e.isMData then
     let typeStx ← withType delab
     `(($stx : $typeStx)) >>= annotateCurPos

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -125,6 +125,16 @@ register_builtin_option pp.instanceTypes : Bool := {
   group    := "pp"
   descr    := "(pretty printer) when printing explicit applications, show the types of inst-implicit arguments"
 }
+register_builtin_option pp.deepTerms : Bool := {
+  defValue := true
+  group    := "pp"
+  descr    := "(pretty printer) display deeply nested terms, replacing them with `⋯` if set to false"
+}
+register_builtin_option pp.deepTerms.threshold : Nat := {
+  defValue := 20
+  group    := "pp"
+  descr    := "(pretty printer) when `pp.deepTerms` is false, the depth at which terms start being replaced with `⋯`"
+}
 register_builtin_option pp.motives.pi : Bool := {
   defValue := true
   group    := "pp"
@@ -205,5 +215,7 @@ def getPPMotivesNonConst (o : Options) : Bool := o.get pp.motives.nonConst.name
 def getPPMotivesAll (o : Options) : Bool := o.get pp.motives.all.name pp.motives.all.defValue
 def getPPInstances (o : Options) : Bool := o.get pp.instances.name pp.instances.defValue
 def getPPInstanceTypes (o : Options) : Bool := o.get pp.instanceTypes.name pp.instanceTypes.defValue
+def getPPDeepTerms (o : Options) : Bool := o.get pp.deepTerms.name pp.deepTerms.defValue
+def getPPDeepTermsThreshold (o : Options) : Nat := o.get pp.deepTerms.threshold.name pp.deepTerms.threshold.defValue
 
 end Lean

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -53,18 +53,25 @@ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
         | none => pure none
       let exprExplicit? ← match i.info with
         | Elab.Info.ofTermInfo ti =>
-          let ti ← ppExprTagged ti.expr (explicit := true)
-          -- remove top-level expression highlight
-          pure <| some <| match ti with
-            | .tag _ tt => tt
-            | tt => tt
+          pure <| some <| ← ppExprTaggedWithoutTopLevelHighlight ti.expr (explicit := true)
+        | Elab.Info.ofOmissionInfo { toTermInfo := ti } =>
+          -- Omitted terms are simply to be expanded, not printed explicitly.
+          -- Keep the top-level tag so that users can also see the explicit version
+          -- of the omitted term.
+          pure <| some <| ← ppExprTagged ti.expr (explicit := false)
         | Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString
         | _ => pure none
       return {
         type := type?
         exprExplicit := exprExplicit?
         doc := ← i.info.docString? : InfoPopup
       }
+where
+  ppExprTaggedWithoutTopLevelHighlight (e : Expr) (explicit : Bool) : MetaM CodeWithInfos := do
+    let pp ← ppExprTagged e (explicit := explicit)
+    return match pp with
+      | .tag _ tt => tt
+      | tt => tt
 
 builtin_initialize
   registerBuiltinRpcProcedure

src/Lean/Server/InfoUtils.lean

@@ -112,11 +112,13 @@ def Info.stx : Info → Syntax
   | ofUserWidgetInfo i     => i.stx
   | ofFVarAliasInfo _      => .missing
   | ofFieldRedeclInfo i    => i.stx
+  | ofOmissionInfo i       => i.stx
 
 def Info.lctx : Info → LocalContext
-  | Info.ofTermInfo i  => i.lctx
-  | Info.ofFieldInfo i => i.lctx
-  | _                  => LocalContext.empty
+  | Info.ofTermInfo i     => i.lctx
+  | Info.ofFieldInfo i    => i.lctx
+  | Info.ofOmissionInfo i => i.lctx
+  | _                     => LocalContext.empty
 
 def Info.pos? (i : Info) : Option String.Pos :=
   i.stx.getPos? (canonicalOnly := true)
@@ -210,14 +212,15 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
 
 def Info.type? (i : Info) : MetaM (Option Expr) :=
   match i with
-  | Info.ofTermInfo ti => Meta.inferType ti.expr
-  | Info.ofFieldInfo fi => Meta.inferType fi.val
+  | Info.ofTermInfo ti     => Meta.inferType ti.expr
+  | Info.ofFieldInfo fi    => Meta.inferType fi.val
+  | Info.ofOmissionInfo oi => Meta.inferType oi.expr
   | _ => return none
 
 def Info.docString? (i : Info) : MetaM (Option String) := do
   let env ← getEnv
   match i with
-  | Info.ofTermInfo ti =>
+  | .ofTermInfo ti =>
     if let some n := ti.expr.constName? then
       return ← findDocString? env n
   | .ofFieldInfo fi => return ← findDocString? env fi.projName
@@ -227,6 +230,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     if let some decl := (← getOptionDecls).find? oi.optionName then
       return decl.descr
     return none
+  | .ofOmissionInfo _ => return none -- Do not display the docstring of ⋯ for omitted terms
   | _ => pure ()
   if let some ei := i.toElabInfo? then
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
@@ -370,12 +374,14 @@ partial def InfoTree.hasSorry : InfoTree → IO Bool :=
 where go ci?
   | .context ci t => go (ci.mergeIntoOuter? ci?) t
   | .node i cs =>
-    if let (some ci, .ofTermInfo ti) := (ci?, i) then do
+    match ci?, i with
+    | some ci, .ofTermInfo ti
+    | some ci, .ofOmissionInfo { toTermInfo := ti } => do
       let expr ← ti.runMetaM ci (instantiateMVars ti.expr)
       return expr.hasSorry
       -- we assume that `cs` are subterms of `ti.expr` and
       -- thus do not have to be checked as well
-    else
+    | _, _ =>
       cs.anyM (go ci?)
   | _ => return false
 

tests/lean/run/deepTerms.lean

@@ -0,0 +1,34 @@
+/-!
+# Testing the `pp.deepTerms false` option
+
+Implemented in PR #3201.
+-/
+
+set_option pp.deepTerms false
+set_option pp.deepTerms.threshold 8
+
+/-!
+Subterms of terms with depth <= pp.deepTerms.threshold are not omitted
+-/
+#check Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ
+
+/-!
+Shallow subterms (subterms with depth <= pp.deepTerms.threshold/4) of terms with
+depth > pp.deepTerms.threshold are not omitted
+-/
+#check Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ
+
+/-!
+Deep subterms of terms with depth > pp.deepTerms.threshold are omitted
+-/
+#check Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ
+
+/-!
+Nothing is omitted in short lists
+-/
+#check [1, 2, 3, 4, 5, 6, 7, 8]
+
+/-!
+In longer lists, the tail is omitted
+-/
+#check [1, 2, 3, 4, 5, 6, 7, 8, 9]

tests/lean/run/deepTerms.lean.expected.out

@@ -0,0 +1,6 @@
+Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))) : Nat
+Nat.succ
+  (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))))) : Nat
+Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ ⋯)))))))) : Nat
+[1, 2, 3, 4, 5, 6, 7, 8] : List Nat
+[1, 2, 3, 4, 5, 6, 7, 8, ⋯] : List Nat