From fdc64def1b7322450e4704db47cb754b3246431d Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 14 Feb 2024 08:58:36 +1100 Subject: [PATCH] feat: upstream 'Try this:' widgets (#3266) There is a test file in Std that should later be reunited with this code. --------- Co-authored-by: Sebastian Ullrich --- src/Lean/Meta/Tactic.lean | 1 + src/Lean/Meta/Tactic/TryThis.lean | 585 ++++++++++++++++++ .../completionOption.lean.expected.out | 44 ++ 3 files changed, 630 insertions(+) create mode 100644 src/Lean/Meta/Tactic/TryThis.lean diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean index bedd0800fc..d4ef86fd02 100644 --- a/src/Lean/Meta/Tactic.lean +++ b/src/Lean/Meta/Tactic.lean @@ -22,6 +22,7 @@ import Lean.Meta.Tactic.Simp import Lean.Meta.Tactic.AuxLemma import Lean.Meta.Tactic.SplitIf import Lean.Meta.Tactic.Split +import Lean.Meta.Tactic.TryThis import Lean.Meta.Tactic.Cleanup import Lean.Meta.Tactic.Unfold import Lean.Meta.Tactic.Rename diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean new file mode 100644 index 0000000000..f7d3142c4a --- /dev/null +++ b/src/Lean/Meta/Tactic/TryThis.lean @@ -0,0 +1,585 @@ +/- +Copyright (c) 2021 Gabriel Ebner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner, Mario Carneiro, Thomas Murrills +-/ +import Lean.Server.CodeActions +import Lean.Widget.UserWidget +import Lean.Data.Json.Elab + +/-- Gets the LSP range from a `String.Range`. -/ +def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range := + { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop } + + +/-! +# "Try this" support + +This implements a mechanism for tactics to print a message saying `Try this: `, +where `` is a link to a replacement tactic. Users can either click on the link +in the suggestion (provided by a widget), or use a code action which applies the suggestion. +-/ +namespace Lean.Meta.Tactic.TryThis + +open Lean Elab PrettyPrinter Meta Server RequestM + +/-! # Raw widget -/ + +/-- +This is a widget which is placed by `TryThis.addSuggestion` and `TryThis.addSuggestions`. + +When placed by `addSuggestion`, it says `Try this: ` +where `` is a link which will perform the replacement. + +When placed by `addSuggestions`, it says: +``` +Try these: +``` +* `` +* `` +* `` +* ... + +where `` is a link which will perform the replacement. +-/ +@[widget_module] def tryThisWidget : Widget.Module where + javascript := " +import * as React from 'react'; +import { EditorContext } from '@leanprover/infoview'; +const e = React.createElement; +export default function ({ pos, suggestions, range, header, isInline, style }) { + const editorConnection = React.useContext(EditorContext) + const defStyle = style || { + className: 'link pointer dim', + style: { color: 'var(--vscode-textLink-foreground)' } + } + + // Construct the children of the HTML element for a given suggestion. + function makeSuggestion({ suggestion, preInfo, postInfo, style }) { + function onClick() { + editorConnection.api.applyEdit({ + changes: { [pos.uri]: [{ range, newText: suggestion }] } + }) + } + return [ + preInfo, + e('span', { onClick, title: 'Apply suggestion', ...style || defStyle }, suggestion), + postInfo + ] + } + + // Choose between an inline 'Try this'-like display and a list-based 'Try these'-like display. + let inner = null + if (isInline) { + inner = e('div', { className: 'ml1' }, + e('pre', { className: 'font-code pre-wrap' }, header, makeSuggestion(suggestions[0]))) + } else { + inner = e('div', { className: 'ml1' }, + e('pre', { className: 'font-code pre-wrap' }, header), + e('ul', { style: { paddingInlineStart: '20px' } }, suggestions.map(s => + e('li', { className: 'font-code pre-wrap' }, makeSuggestion(s))))) + } + return e('details', { open: true }, + e('summary', { className: 'mv2 pointer' }, 'Suggestions'), + inner) +}" + +/-! # Code action -/ + +/-- A packet of information about a "Try this" suggestion +that we store in the infotree for the associated code action to retrieve. -/ +structure TryThisInfo : Type where + /-- The textual range to be replaced by one of the suggestions. -/ + range : Lsp.Range + /-- + A list of suggestions for the user to choose from. + Each suggestion may optionally come with an override for the code action title. + -/ + suggestionTexts : Array (String × Option String) + /-- The prefix to display before the code action for a "Try this" suggestion if no custom code + action title is provided. If not provided, `"Try this: "` is used. -/ + codeActionPrefix? : Option String + deriving TypeName + +/-- +This is a code action provider that looks for `TryThisInfo` nodes and supplies a code action to +apply the replacement. +-/ +@[code_action_provider] def tryThisProvider : CodeActionProvider := fun params snap => do + let doc ← readDoc + pure <| snap.infoTree.foldInfo (init := #[]) fun _ctx info result => Id.run do + let .ofCustomInfo { stx, value } := info | result + let some { range, suggestionTexts, codeActionPrefix? } := + value.get? TryThisInfo | result + let some stxRange := stx.getRange? | result + let stxRange := doc.meta.text.utf8RangeToLspRange stxRange + unless stxRange.start.line ≤ params.range.end.line do return result + unless params.range.start.line ≤ stxRange.end.line do return result + let mut result := result + for h : i in [:suggestionTexts.size] do + let (newText, title?) := suggestionTexts[i]'h.2 + let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText + result := result.push { + eager.title := title + eager.kind? := "quickfix" + -- Only make the first option preferred + eager.isPreferred? := if i = 0 then true else none + eager.edit? := some <| .ofTextEdit doc.versionedIdentifier { range, newText } + } + result + +/-! # Formatting -/ + +/-- Yields `(indent, column)` given a `FileMap` and a `String.Range`, where `indent` is the number +of spaces by which the line that first includes `range` is initially indented, and `column` is the +column `range` starts at in that line. -/ +def getIndentAndColumn (map : FileMap) (range : String.Range) : Nat × Nat := + let start := map.source.findLineStart range.start + let body := map.source.findAux (· ≠ ' ') range.start start + ((body - start).1, (range.start - start).1) + +/-- Replace subexpressions like `?m.1234` with `?_` so it can be copy-pasted. -/ +partial def replaceMVarsByUnderscores [Monad m] [MonadQuotation m] + (s : Syntax) : m Syntax := + s.replaceM fun s => do + let `(?$id:ident) := s | pure none + if id.getId.hasNum || id.getId.isInternal then `(?_) else pure none + +/-- Delaborate `e` into syntax suitable for use by `refine`. -/ +def delabToRefinableSyntax (e : Expr) : MetaM Term := + return ⟨← replaceMVarsByUnderscores (← delab e)⟩ + +/-- +An option allowing the user to customize the ideal input width. Defaults to 100. +This option controls output format when +the output is intended to be copied back into a lean file -/ +register_option format.inputWidth : Nat := { + /- The default maximum width of an ideal line in source code. -/ + defValue := 100 + descr := "ideal input width" +} + +/-- Get the input width specified in the options -/ +def getInputWidth (o : Options) : Nat := format.inputWidth.get o + +/-! # `Suggestion` data -/ + +-- TODO: we could also support `Syntax` and `Format` +/-- Text to be used as a suggested replacement in the infoview. This can be either a `TSyntax kind` +for a single `kind : SyntaxNodeKind` or a raw `String`. + +Instead of using constructors directly, there are coercions available from these types to +`SuggestionText`. -/ +inductive SuggestionText where + /-- `TSyntax kind` used as suggested replacement text in the infoview. Note that while `TSyntax` + is in general parameterized by a list of `SyntaxNodeKind`s, we only allow one here; this + unambiguously guides pretty-printing. -/ + | tsyntax {kind : SyntaxNodeKind} : TSyntax kind → SuggestionText + /-- A raw string to be used as suggested replacement text in the infoview. -/ + | string : String → SuggestionText + deriving Inhabited + +instance : ToMessageData SuggestionText where + toMessageData + | .tsyntax stx => stx + | .string s => s + +instance {kind : SyntaxNodeKind} : CoeHead (TSyntax kind) SuggestionText where + coe := .tsyntax + +instance : Coe String SuggestionText where + coe := .string + +namespace SuggestionText + +/-- Pretty-prints a `SuggestionText` as a `Format`. If the `SuggestionText` is some `TSyntax kind`, +we use the appropriate pretty-printer; strings are coerced to `Format`s as-is. -/ +def pretty : SuggestionText → CoreM Format + | .tsyntax (kind := kind) stx => ppCategory kind stx + | .string text => return text + +/- Note that this is essentially `return (← s.pretty).prettyExtra w indent column`, but we +special-case strings to avoid converting them to `Format`s and back, which adds indentation after each newline. -/ +/-- Pretty-prints a `SuggestionText` as a `String` and wraps with respect to the pane width, +indentation, and column, via `Format.prettyExtra`. If `w := none`, then +`w := getInputWidth (← getOptions)` is used. Raw `String`s are returned as-is. -/ +def prettyExtra (s : SuggestionText) (w : Option Nat := none) + (indent column : Nat := 0) : CoreM String := + match s with + | .tsyntax (kind := kind) stx => do + let w ← match w with | none => do pure <| getInputWidth (← getOptions) | some n => pure n + return (← ppCategory kind stx).pretty w indent column + | .string text => return text + +end SuggestionText + +/-- +Style hooks for `Suggestion`s. See `SuggestionStyle.error`, `.warning`, `.success`, `.value`, +and other definitions here for style presets. This is an arbitrary `Json` object, with the following +interesting fields: +* `title`: the hover text in the suggestion link +* `className`: the CSS classes applied to the link +* `style`: A `Json` object with additional inline CSS styles such as `color` or `textDecoration`. +-/ +def SuggestionStyle := Json deriving Inhabited, ToJson + +/-- Style as an error. By default, decorates the text with an undersquiggle; providing the argument +`decorated := false` turns this off. -/ +def SuggestionStyle.error (decorated := true) : SuggestionStyle := + let style := if decorated then + json% { + -- The VS code error foreground theme color (`--vscode-errorForeground`). + color: "var(--vscode-errorForeground)", + textDecoration: "underline wavy var(--vscode-editorError-foreground) 1pt" + } + else json% { color: "var(--vscode-errorForeground)" } + json% { className: "pointer dim", style: $style } + +/-- Style as a warning. By default, decorates the text with an undersquiggle; providing the +argument `decorated := false` turns this off. -/ +def SuggestionStyle.warning (decorated := true) : SuggestionStyle := + if decorated then + json% { + -- The `.gold` CSS class, which the infoview uses when e.g. building a file. + className: "gold pointer dim", + style: { textDecoration: "underline wavy var(--vscode-editorWarning-foreground) 1pt" } + } + else json% { className: "gold pointer dim" } + +/-- Style as a success. -/ +def SuggestionStyle.success : SuggestionStyle := + -- The `.information` CSS class, which the infoview uses on successes. + json% { className: "information pointer dim" } + +/-- Style the same way as a hypothesis appearing in the infoview. -/ +def SuggestionStyle.asHypothesis : SuggestionStyle := + json% { className: "goal-hyp pointer dim" } + +/-- Style the same way as an inaccessible hypothesis appearing in the infoview. -/ +def SuggestionStyle.asInaccessible : SuggestionStyle := + json% { className: "goal-inaccessible pointer dim" } + +/-- Draws the color from a red-yellow-green color gradient with red at `0.0`, yellow at `0.5`, and +green at `1.0`. Values outside the range `[0.0, 1.0]` are clipped to lie within this range. + +With `showValueInHoverText := true` (the default), the value `t` will be included in the `title` of +the HTML element (which appears on hover). -/ +def SuggestionStyle.value (t : Float) (showValueInHoverText := true) : SuggestionStyle := + let t := min (max t 0) 1 + json% { + className: "pointer dim", + -- interpolates linearly from 0º to 120º with 95% saturation and lightness + -- varying around 50% in HSL space + style: { color: $(s!"hsl({(t * 120).round} 95% {60 * ((t - 0.5)^2 + 0.75)}%)") }, + title: $(if showValueInHoverText then s!"Apply suggestion ({t})" else "Apply suggestion") + } + +/-- Holds a `suggestion` for replacement, along with `preInfo` and `postInfo` strings to be printed +immediately before and after that suggestion, respectively. It also includes an optional +`MessageData` to represent the suggestion in logs; by default, this is `none`, and `suggestion` is +used. -/ +structure Suggestion where + /-- Text to be used as a replacement via a code action. -/ + suggestion : SuggestionText + /-- Optional info to be printed immediately before replacement text in a widget. -/ + preInfo? : Option String := none + /-- Optional info to be printed immediately after replacement text in a widget. -/ + postInfo? : Option String := none + /-- Optional style specification for the suggestion. If `none` (the default), the suggestion is + styled as a text link. Otherwise, the suggestion can be styled as: + * a status: `.error`, `.warning`, `.success` + * a hypothesis name: `.asHypothesis`, `.asInaccessible` + * a variable color: `.value (t : Float)`, which draws from a red-yellow-green gradient, with red + at `0.0` and green at `1.0`. + + See `SuggestionStyle` for details. -/ + style? : Option SuggestionStyle := none + /-- How to represent the suggestion as `MessageData`. This is used only in the info diagnostic. + If `none`, we use `suggestion`. Use `toMessageData` to render a `Suggestion` in this manner. -/ + messageData? : Option MessageData := none + /-- How to construct the text that appears in the lightbulb menu from the suggestion text. If + `none`, we use `fun ppSuggestionText => "Try this: " ++ ppSuggestionText`. Only the pretty-printed + `suggestion : SuggestionText` is used here. -/ + toCodeActionTitle? : Option (String → String) := none + deriving Inhabited + +/-- Converts a `Suggestion` to `Json` in `CoreM`. We need `CoreM` in order to pretty-print syntax. + +This also returns a `String × Option String` consisting of the pretty-printed text and any custom +code action title if `toCodeActionTitle?` is provided. + +If `w := none`, then `w := getInputWidth (← getOptions)` is used. +-/ +def Suggestion.toJsonAndInfoM (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) : + CoreM (Json × String × Option String) := do + let text ← s.suggestion.prettyExtra w indent column + let mut json := [("suggestion", (text : Json))] + if let some preInfo := s.preInfo? then json := ("preInfo", preInfo) :: json + if let some postInfo := s.postInfo? then json := ("postInfo", postInfo) :: json + if let some style := s.style? then json := ("style", toJson style) :: json + return (Json.mkObj json, text, s.toCodeActionTitle?.map (· text)) + +/- If `messageData?` is specified, we use that; otherwise (by default), we use `toMessageData` of +the suggestion text. -/ +instance : ToMessageData Suggestion where + toMessageData s := s.messageData?.getD (toMessageData s.suggestion) + +instance : Coe SuggestionText Suggestion where + coe t := { suggestion := t } + +/-- Delaborate `e` into a suggestion suitable for use by `refine`. -/ +def delabToRefinableSuggestion (e : Expr) : MetaM Suggestion := + return { suggestion := ← delabToRefinableSyntax e, messageData? := e } + +/-! # Widget hooks -/ + +/-- Core of `addSuggestion` and `addSuggestions`. Whether we use an inline display for a single +element or a list display is controlled by `isInline`. -/ +private def addSuggestionCore (ref : Syntax) (suggestions : Array Suggestion) + (header : String) (isInline : Bool) (origSpan? : Option Syntax := none) + (style? : Option SuggestionStyle := none) + (codeActionPrefix? : Option String := none) : CoreM Unit := do + if let some range := (origSpan?.getD ref).getRange? then + let map ← getFileMap + -- FIXME: this produces incorrect results when `by` is at the beginning of the line, i.e. + -- replacing `tac` in `by tac`, because the next line will only be 2 space indented + -- (less than `tac` which starts at column 3) + let (indent, column) := getIndentAndColumn map range + let suggestions ← suggestions.mapM (·.toJsonAndInfoM (indent := indent) (column := column)) + let suggestionTexts := suggestions.map (·.2) + let suggestions := suggestions.map (·.1) + let ref := Syntax.ofRange <| ref.getRange?.getD range + let range := map.utf8RangeToLspRange range + pushInfoLeaf <| .ofCustomInfo { + stx := ref + value := Dynamic.mk + { range, suggestionTexts, codeActionPrefix? : TryThisInfo } + } + Widget.savePanelWidgetInfo (hash tryThisWidget.javascript) ref + (props := return json% { + suggestions: $suggestions, + range: $range, + header: $header, + isInline: $isInline, + style: $style? + }) + +/-- Add a "try this" suggestion. This has three effects: + +* An info diagnostic is displayed saying `Try this: ` +* A widget is registered, saying `Try this: ` with a link on `` to apply + the suggestion +* A code action is added, which will apply the suggestion. + +The parameters are: +* `ref`: the span of the info diagnostic +* `s`: a `Suggestion`, which contains + * `suggestion`: the replacement text; + * `preInfo?`: an optional string shown immediately after the replacement text in the widget + message (only) + * `postInfo?`: an optional string shown immediately after the replacement text in the widget + message (only) + * `style?`: an optional `Json` object used as the value of the `style` attribute of the + suggestion text's element (not the whole suggestion element). + * `messageData?`: an optional message to display in place of `suggestion` in the info diagnostic + (only). The widget message uses only `suggestion`. If `messageData?` is `none`, we simply use + `suggestion` instead. + * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the + pretty-printed suggestion text into the code action text which appears in the lightbulb menu. + If `none`, we simply prepend `"Try This: "` to the suggestion text. +* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`. + If not provided it defaults to `ref`. +* `header`: a string that begins the display. By default, it is `"Try this: "`. +* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the + suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used. +-/ +def addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := none) + (header : String := "Try this: ") (codeActionPrefix? : Option String := none) : MetaM Unit := do + logInfoAt ref m!"{header}{s}" + addSuggestionCore ref #[s] header (isInline := true) origSpan? + (codeActionPrefix? := codeActionPrefix?) + +/-- Add a list of "try this" suggestions as a single "try these" suggestion. This has three effects: + +* An info diagnostic is displayed saying `Try these: ` +* A widget is registered, saying `Try these: ` with a link on each + `` to apply the suggestion +* A code action for each suggestion is added, which will apply the suggestion. + +The parameters are: +* `ref`: the span of the info diagnostic +* `suggestions`: an array of `Suggestion`s, which each contain + * `suggestion`: the replacement text; + * `preInfo?`: an optional string shown immediately after the replacement text in the widget + message (only) + * `postInfo?`: an optional string shown immediately after the replacement text in the widget + message (only) + * `style?`: an optional `Json` object used as the value of the `style` attribute of the + suggestion text's element (not the whole suggestion element). + * `messageData?`: an optional message to display in place of `suggestion` in the info diagnostic + (only). The widget message uses only `suggestion`. If `messageData?` is `none`, we simply use + `suggestion` instead. + * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the + pretty-printed suggestion text into the code action text which appears in the lightbulb menu. + If `none`, we simply prepend `"Try This: "` to the suggestion text. +* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`. + If not provided it defaults to `ref`. +* `header`: a string that precedes the list. By default, it is `"Try these:"`. +* `style?`: a default style for all suggestions which do not have a custom `style?` set. +* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all + suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is + used. +-/ +def addSuggestions (ref : Syntax) (suggestions : Array Suggestion) + (origSpan? : Option Syntax := none) (header : String := "Try these:") + (style? : Option SuggestionStyle := none) + (codeActionPrefix? : Option String := none) : MetaM Unit := do + if suggestions.isEmpty then throwErrorAt ref "no suggestions available" + let msgs := suggestions.map toMessageData + let msgs := msgs.foldl (init := MessageData.nil) (fun msg m => msg ++ m!"\n• " ++ m) + logInfoAt ref m!"{header}{msgs}" + addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix? + +private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion := do + let stx ← delabToRefinableSyntax e + let mvars ← getMVars e + let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx) + let messageData? := if mvars.isEmpty then m!"exact {e}" else m!"refine {e}" + let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else + let mut str := "\nRemaining subgoals:" + for g in mvars do + -- TODO: use a MessageData.ofExpr instead of rendering to string + let e ← PrettyPrinter.ppExpr (← instantiateMVars (← g.getType)) + str := str ++ Format.pretty ("\n⊢ " ++ e) + pure str + pure { suggestion, postInfo?, messageData? } + +/-- Add an `exact e` or `refine e` suggestion. + +The parameters are: +* `ref`: the span of the info diagnostic +* `e`: the replacement expression +* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`. + If not provided it defaults to `ref`. +* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after + `Remaining subgoals:` +* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the + suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used. +-/ +def addExactSuggestion (ref : Syntax) (e : Expr) + (origSpan? : Option Syntax := none) (addSubgoalsMsg := false) + (codeActionPrefix? : Option String := none): MetaM Unit := do + addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg e) + (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?) + +/-- Add `exact e` or `refine e` suggestions. + +The parameters are: +* `ref`: the span of the info diagnostic +* `es`: the array of replacement expressions +* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`. + If not provided it defaults to `ref`. +* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after + `Remaining subgoals:` +* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all + suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is + used. +-/ +def addExactSuggestions (ref : Syntax) (es : Array Expr) + (origSpan? : Option Syntax := none) (addSubgoalsMsg := false) + (codeActionPrefix? : Option String := none) : MetaM Unit := do + let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg + addSuggestions ref suggestions (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?) + +/-- Add a term suggestion. + +The parameters are: +* `ref`: the span of the info diagnostic +* `e`: the replacement expression +* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`. + If not provided it defaults to `ref`. +* `header`: a string which precedes the suggestion. By default, it's `"Try this: "`. +* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the + suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used. +-/ +def addTermSuggestion (ref : Syntax) (e : Expr) + (origSpan? : Option Syntax := none) (header : String := "Try this: ") + (codeActionPrefix? : Option String := none) : MetaM Unit := do + addSuggestion ref (← delabToRefinableSuggestion e) (origSpan? := origSpan?) (header := header) + (codeActionPrefix? := codeActionPrefix?) + +/-- Add term suggestions. + +The parameters are: +* `ref`: the span of the info diagnostic +* `es`: an array of the replacement expressions +* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`. + If not provided it defaults to `ref`. +* `header`: a string which precedes the list of suggestions. By default, it's `"Try these:"`. +* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all + suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is + used. +-/ +def addTermSuggestions (ref : Syntax) (es : Array Expr) + (origSpan? : Option Syntax := none) (header : String := "Try these:") + (codeActionPrefix? : Option String := none) : MetaM Unit := do + addSuggestions ref (← es.mapM delabToRefinableSuggestion) + (origSpan? := origSpan?) (header := header) (codeActionPrefix? := codeActionPrefix?) + +open Lean Elab Elab.Tactic PrettyPrinter Meta + +/-- Add a suggestion for `have h : t := e`. -/ +def addHaveSuggestion (ref : Syntax) (h? : Option Name) (t? : Option Expr) (e : Expr) + (origSpan? : Option Syntax := none) : TermElabM Unit := do + let estx ← delabToRefinableSyntax e + let prop ← isProp (← inferType e) + let tac ← if let some t := t? then + let tstx ← delabToRefinableSyntax t + if prop then + match h? with + | some h => `(tactic| have $(mkIdent h) : $tstx := $estx) + | none => `(tactic| have : $tstx := $estx) + else + `(tactic| let $(mkIdent (h?.getD `_)) : $tstx := $estx) + else + if prop then + match h? with + | some h => `(tactic| have $(mkIdent h) := $estx) + | none => `(tactic| have := $estx) + else + `(tactic| let $(mkIdent (h?.getD `_)) := $estx) + addSuggestion ref tac origSpan? + +open Lean.Parser.Tactic +open Lean.Syntax + +/-- Add a suggestion for `rw [h₁, ← h₂] at loc`. -/ +def addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool)) + (type? : Option Expr := none) (loc? : Option Expr := none) + (origSpan? : Option Syntax := none) : + TermElabM Unit := do + let rules_stx := TSepArray.ofElems <| ← rules.toArray.mapM fun ⟨e, symm⟩ => do + let t ← delabToRefinableSyntax e + if symm then `(rwRule| ← $t:term) else `(rwRule| $t:term) + let tac ← do + let loc ← loc?.mapM fun loc => do `(location| at $(← delab loc):term) + `(tactic| rw [$rules_stx,*] $(loc)?) + + -- We don't simply write `let mut tacMsg := m!"{tac}"` here + -- but instead rebuild it, so that there are embedded `Expr`s in the message, + -- thus giving more information in the hovers. + -- Perhaps in future we will have a better way to attach elaboration information to + -- `Syntax` embedded in a `MessageData`. + let mut tacMsg := + let rulesMsg := MessageData.sbracket <| MessageData.joinSep + (rules.map fun ⟨e, symm⟩ => (if symm then "← " else "") ++ m!"{e}") ", " + if let some loc := loc? then + m!"rw {rulesMsg} at {loc}" + else + m!"rw {rulesMsg}" + let mut extraMsg := "" + if let some type := type? then + tacMsg := tacMsg ++ m!"\n-- {type}" + extraMsg := extraMsg ++ s!"\n-- {← PrettyPrinter.ppExpr type}" + addSuggestion ref (s := { suggestion := tac, postInfo? := extraMsg, messageData? := tacMsg }) + origSpan? diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out index 0bdc0109fc..8b3036f5ff 100644 --- a/tests/lean/interactive/completionOption.lean.expected.out +++ b/tests/lean/interactive/completionOption.lean.expected.out @@ -24,6 +24,17 @@ "label": "format.indent", "kind": 10, "detail": "(2), indentation"}, + {"textEdit": + {"replace": + {"start": {"line": 1, "character": 11}, + "end": {"line": 1, "character": 17}}, + "newText": "format.inputWidth", + "insert": + {"start": {"line": 1, "character": 11}, + "end": {"line": 1, "character": 17}}}, + "label": "format.inputWidth", + "kind": 10, + "detail": "(100), ideal input width"}, {"textEdit": {"replace": {"start": {"line": 1, "character": 11}, @@ -85,6 +96,17 @@ "label": "format.indent", "kind": 10, "detail": "(2), indentation"}, + {"textEdit": + {"replace": + {"start": {"line": 4, "character": 11}, + "end": {"line": 4, "character": 20}}, + "newText": "format.inputWidth", + "insert": + {"start": {"line": 4, "character": 11}, + "end": {"line": 4, "character": 20}}}, + "label": "format.inputWidth", + "kind": 10, + "detail": "(100), ideal input width"}, {"textEdit": {"replace": {"start": {"line": 4, "character": 11}, @@ -228,6 +250,17 @@ "label": "format.indent", "kind": 10, "detail": "(2), indentation"}, + {"textEdit": + {"replace": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 17}}, + "newText": "format.inputWidth", + "insert": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 17}}}, + "label": "format.inputWidth", + "kind": 10, + "detail": "(100), ideal input width"}, {"textEdit": {"replace": {"start": {"line": 13, "character": 11}, @@ -289,6 +322,17 @@ "label": "format.indent", "kind": 10, "detail": "(2), indentation"}, + {"textEdit": + {"replace": + {"start": {"line": 16, "character": 11}, + "end": {"line": 16, "character": 18}}, + "newText": "format.inputWidth", + "insert": + {"start": {"line": 16, "character": 11}, + "end": {"line": 16, "character": 18}}}, + "label": "format.inputWidth", + "kind": 10, + "detail": "(100), ideal input width"}, {"textEdit": {"replace": {"start": {"line": 16, "character": 11},