"Try this" code action and tactic suggestions

This implements a mechanism for tactics to print a message saying Try this: <suggestion>, where <suggestion> 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.

Raw widget

def Lean.Meta.Tactic.TryThis.tryThisWidget : Widget.Module

This is a widget which is placed by TryThis.addSuggestion and TryThis.addSuggestions.

When placed by addSuggestion, it says Try this: <replacement> where <replacement> is a link which will perform the replacement.

When placed by addSuggestions, it says:

Try these:

• <replacement1>
• <replacement2>
• <replacement3>
• ...

where <replacement*> is a link which will perform the replacement.

Code action

def Lean.Meta.Tactic.TryThis.tryThisProvider : Server.CodeActionProvider

This is a code action provider that looks for TryThisInfo nodes and supplies a code action to apply the replacement.

Formatting

def Lean.Meta.Tactic.TryThis.delabToRefinableSyntax (e : Expr) : MetaM Term

Delaborate e into syntax suitable for use by refine.

def Lean.Meta.Tactic.TryThis.delabToRefinableSuggestion (e : Expr) : MetaM Suggestion

Delaborate e into a suggestion suitable for use by refine.

def Lean.Meta.Tactic.TryThis.addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := none) (header : String := "Try this: ") (codeActionPrefix? : Option String := none) : MetaM Unit

Add a "try this" suggestion. This has three effects:

• An info diagnostic is displayed saying Try this: <suggestion>
• A widget is registered, saying Try this: <suggestion> with a link on <suggestion> 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 Lean.Meta.Tactic.TryThis.addSuggestions (ref : Syntax) (suggestions : Array Suggestion) (origSpan? : Option Syntax := none) (header : String := "Try these:") (style? : Option SuggestionStyle := none) (codeActionPrefix? : Option String := none) : MetaM Unit

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: <list of suggestions>
• A widget is registered, saying Try these: <list of suggestions> with a link on each <suggestion> 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 Suggestions, 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.

Tactic-specific widget hooks

def Lean.Meta.Tactic.TryThis.addExactSuggestion (ref : Syntax) (e : Expr) (origSpan? : Option Syntax := none) (addSubgoalsMsg : Bool := false) (codeActionPrefix? : Option String := none) (checkState? : Option Elab.Tactic.SavedState := none) (tacticErrorAsInfo : Bool := false) : Elab.Tactic.TacticM Unit

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.
• checkState?: if passed, the tactic state in which the generated tactic will be validated, inserting expose_names if necessary.
• tacticErrorAsInfo: if true (default false), if a generated tactic is invalid (e.g., due to a pretty-printing issue), the resulting error message will be logged as an info message instead of being thrown as an error. Has no effect if checkState? is none.

def Lean.Meta.Tactic.TryThis.addExactSuggestions (ref : Syntax) (es : Array Expr) (origSpan? : Option Syntax := none) (addSubgoalsMsg : Bool := false) (codeActionPrefix? : Option String := none) (checkState? : Option Elab.Tactic.SavedState := none) (tacticErrorAsInfo : Bool := true) : Elab.Tactic.TacticM Unit

Add exact e or refine e suggestions if they can be successfully generated; for those that cannot, display messages indicating the invalid generated tactics.

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.
• checkState?: if passed, the tactic state in which the generated tactics will be validated, inserting expose_names if necessary.
• tacticErrorAsInfo: if true (default true), invalid generated tactics will log info messages instead of throwing an error. The default behavior differs from addExactSuggestion because throwing an error means that any subsequent suggestions will not be displayed. Has no effect if checkState? is none.

def Lean.Meta.Tactic.TryThis.addTermSuggestion (ref : Syntax) (e : Expr) (origSpan? : Option Syntax := none) (header : String := "Try this: ") (codeActionPrefix? : Option String := none) : MetaM Unit

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 Lean.Meta.Tactic.TryThis.addTermSuggestions (ref : Syntax) (es : Array Expr) (origSpan? : Option Syntax := none) (header : String := "Try these:") (codeActionPrefix? : Option String := none) : MetaM Unit

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 Lean.Meta.Tactic.TryThis.addHaveSuggestion (ref : Syntax) (h? : Option Name) (t? : Option Expr) (e : Expr) (origSpan? : Option Syntax := none) (checkState? : Option Elab.Tactic.SavedState := none) : Elab.Tactic.TacticM Unit

Add a suggestion for have h : t := e.

def Lean.Meta.Tactic.TryThis.addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool)) (type? : LOption Expr := LOption.undef) (loc? : Option Expr := none) (origSpan? : Option Syntax := none) (checkState? : Option Elab.Tactic.SavedState := none) : Elab.Tactic.TacticM Unit

Add a suggestion for rw [h₁, ← h₂] at loc.

Parameters:

• ref: the span of the info diagnostic
• rules: a list of arguments to rw, with the second component true if the rewrite is reversed
• type?: the goal after the suggested rewrite, .none if the rewrite closes the goal, or .undef if the resulting goal is unknown
• loc?: the hypothesis at which the rewrite is performed, or none if the goal is targeted
• origSpan?: a syntax object whose span is the actual text to be replaced by suggestion. If not provided it defaults to ref.
• checkState?: if passed, the tactic state in which the generated tactic will be validated, inserting expose_names if necessary