feat: upstream addHaveSuggestion and addRewriteSuggestion

Std.lean

@@ -81,6 +81,7 @@ import Std.Lean.Parser
 import Std.Lean.PersistentHashMap
 import Std.Lean.PersistentHashSet
 import Std.Lean.Position
+import Std.Lean.Syntax
 import Std.Lean.Tactic
 import Std.Lean.TagAttribute
 import Std.Linter

Std/Lean/Syntax.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+import Lean
+
+/-!
+# Helper functions for working with typed syntaxes.
+-/
+
+namespace Lean
+
+/--
+Applies the given function to every subsyntax.
+
+Like `Syntax.replaceM` but for typed syntax.
+-/
+def TSyntax.replaceM [Monad M] (f : Syntax → M (Option Syntax)) (stx : TSyntax k) : M (TSyntax k) :=
+  .mk <$> stx.1.replaceM f
+
+/--
+Constructs a typed separated array from elements.
+The given array does not include the separators.
+
+Like `Syntax.SepArray.ofElems` but for typed syntax.
+-/
+def Syntax.TSepArray.ofElems {sep} (elems : Array (TSyntax k)) : TSepArray k sep :=
+  .mk (SepArray.ofElems (sep := sep) elems).1

Std/Tactic/TryThis.lean

@@ -1,13 +1,14 @@
 /-
 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
+Authors: Gabriel Ebner, Mario Carneiro, Scott Morrison
 -/
 import Lean.Server.CodeActions
 import Lean.Widget.UserWidget
 import Std.Lean.Name
 import Std.Lean.Format
 import Std.Lean.Position
+import Std.Lean.Syntax
 
 /-!
 # "Try this" support
@@ -147,3 +148,57 @@ def addTermSuggestion (ref : Syntax) (e : Expr)
     (origSpan? : Option Syntax := none) : TermElabM Unit := do
   addSuggestion ref (← delabToRefinableSyntax e)
     (suggestionForMessage? := e) (origSpan? := origSpan?)
+
+open Lean Elab Elab.Tactic PrettyPrinter Meta Std.Tactic.TryThis
+
+/-- Add a suggestion for `have : t := e`. -/
+def addHaveSuggestion (ref : Syntax) (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
+      `(tactic| have : $tstx := $estx)
+    else
+      `(tactic| let this : $tstx := $estx)
+  else
+    if prop then
+      `(tactic| have := $estx)
+    else
+      `(tactic| let this := $estx)
+  addSuggestion ref tac none 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 attached 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 tac (suggestionForMessage? := tacMsg)
+    (extraMsg := extraMsg) (origSpan? := origSpan?)