From cd0be38bb4a78b8ec5619e6cf51feaf85725c70f Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 31 Jan 2024 18:28:29 +0100 Subject: [PATCH] feat: elidible subterms (#3201) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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.
InfoView with pp.deepTerms set to false (click to show image) ![image](https://github.com/leanprover/lean4/assets/10852073/f6df8b2c-d769-41c8-821e-efd0af23ccfa)
### 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ₖ, ⋯]`. --- RELEASES.md | 2 + src/Init/NotationExtra.lean | 24 ++++++- src/Lean/Elab/InfoTree/Main.lean | 5 ++ src/Lean/Elab/InfoTree/Types.lean | 10 +++ src/Lean/PrettyPrinter/Delaborator/Basic.lean | 72 ++++++++++++++++--- .../PrettyPrinter/Delaborator/Options.lean | 12 ++++ .../Server/FileWorker/WidgetRequests.lean | 17 +++-- src/Lean/Server/InfoUtils.lean | 22 +++--- tests/lean/run/deepTerms.lean | 34 +++++++++ tests/lean/run/deepTerms.lean.expected.out | 6 ++ 10 files changed, 180 insertions(+), 24 deletions(-) create mode 100644 tests/lean/run/deepTerms.lean create mode 100644 tests/lean/run/deepTerms.lean.expected.out diff --git a/RELEASES.md b/RELEASES.md index 2b75b7ab7f..66ffbef1c0 100644 --- a/RELEASES.md +++ b/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 --------- diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index fb9c75d078..239a7fc80c 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -170,6 +170,20 @@ 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 | `($(_)) => `(()) @@ -177,9 +191,13 @@ syntax (name := calcTactic) "calc" calcSteps : tactic | `($(_)) => `([]) @[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,*]) diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index 1171194ab9..b861ed6df7 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/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. diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index 855bb08b9f..f7eca68b2f 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/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 diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 4ee0d04c08..576a84dd90 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/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,10 +220,10 @@ 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), @@ -227,11 +231,60 @@ where 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 diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean index c9d5e0a384..4b3f5be6c1 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Options.lean +++ b/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 diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean index 2c7fa57884..1719985962 100644 --- a/src/Lean/Server/FileWorker/WidgetRequests.lean +++ b/src/Lean/Server/FileWorker/WidgetRequests.lean @@ -53,11 +53,12 @@ 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 { @@ -65,6 +66,12 @@ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup) 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 diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 28a4a2b90a..93aff6edfa 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/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 diff --git a/tests/lean/run/deepTerms.lean b/tests/lean/run/deepTerms.lean new file mode 100644 index 0000000000..0d0fa1d76d --- /dev/null +++ b/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] diff --git a/tests/lean/run/deepTerms.lean.expected.out b/tests/lean/run/deepTerms.lean.expected.out new file mode 100644 index 0000000000..c3c4204351 --- /dev/null +++ b/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