feat: upstream addHaveSuggestion and addRewriteSuggestion (leanprover…

…-community#210)

Co-authored-by: Mario Carneiro <[email protected]>

Std.lean

@@ -75,6 +75,7 @@ import Std.Lean.PersistentHashMap
 import Std.Lean.PersistentHashSet
 import Std.Lean.Position
 import Std.Lean.SMap
+import Std.Lean.Syntax
 import Std.Lean.System.IO
 import Std.Lean.Tactic
 import Std.Lean.TagAttribute

Std/Lean/Syntax.lean

@@ -0,0 +1,30 @@
+/-
+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.Syntax
+
+/-!
+# Helper functions for working with typed syntaxes.
+-/
+
+namespace Lean
+
+/--
+Applies the given function to every subsyntax.
+
+Like `Syntax.replaceM` but for typed syntax.
+(Note there are no guarantees of type correctness here.)
+-/
+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

@@ -9,6 +9,7 @@ import Std.Lean.Name
 import Std.Lean.Format
 import Std.Lean.Position
 import Std.Data.Json
+import Std.Lean.Syntax
 
 /-!
 # "Try this" support
@@ -523,3 +524,61 @@ def addTermSuggestions (ref : Syntax) (es : Array Expr)
     (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 Std.Tactic.TryThis
+
+/-- 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?