feat: add optional config parser to rewrite tactics

src/Init/Conv.lean

@@ -29,7 +29,7 @@ syntax (name := ext) "ext " (colGt ident)* : conv
 syntax (name := change) "change " term : conv
 syntax (name := delta) "delta " ident : conv
 syntax (name := pattern) "pattern " term : conv
-syntax (name := rewrite) "rewrite " rwRuleSeq : conv
+syntax (name := rewrite) "rewrite " (config)? rwRuleSeq : conv
 syntax (name := erewrite) "erewrite " rwRuleSeq : conv
 syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
 syntax (name := simpMatch) "simpMatch " : conv

src/Init/Notation.lean

@@ -334,27 +334,22 @@ syntax (name := changeWith) "change " term " with " term (location)? : tactic
 syntax rwRule    := ("←" <|> "<-")? term
 syntax rwRuleSeq := "[" rwRule,+,? "]"
 
-syntax (name := rewriteSeq) "rewrite " rwRuleSeq (location)? : tactic
-syntax (name := erewriteSeq) "erewrite " rwRuleSeq (location)? : tactic
+syntax (name := rewriteSeq) "rewrite " (config)? rwRuleSeq (location)? : tactic
 
-syntax (name := rwSeq) "rw " rwRuleSeq (location)? : tactic
-syntax (name := erwSeq) "erw " rwRuleSeq (location)? : tactic
+syntax (name := rwSeq) "rw " (config)? rwRuleSeq (location)? : tactic
 
 def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Syntax := do
   -- We show the `rfl` state on `]`
-  let seq   := stx[1]
+  let seq   := stx[2]
   let rbrak := seq[2]
   -- Replace `]` token with one without position information in the expanded tactic
   let seq   := seq.setArg 2 (mkAtom "]")
-  let tac   := stx.setKind kind |>.setArg 0 (mkAtomFrom stx atom) |>.setArg 1 seq
+  let tac   := stx.setKind kind |>.setArg 0 (mkAtomFrom stx atom) |>.setArg 2 seq
   `(tactic| $tac; try (withReducible rfl%$rbrak))
 
 @[macro rwSeq] def expandRwSeq : Macro :=
   rwWithRfl ``Lean.Parser.Tactic.rewriteSeq "rewrite"
 
-@[macro erwSeq] def expandERwSeq : Macro :=
-  rwWithRfl ``Lean.Parser.Tactic.erewriteSeq "erewrite"
-
 syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
 
 syntax (name := injections) "injections" : tactic

src/Lean/Elab/Tactic/Conv/Rewrite.lean

@@ -10,18 +10,13 @@ import Lean.Elab.Tactic.Conv.Basic
 namespace Lean.Elab.Tactic.Conv
 open Meta
 
-def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx =>
-  withRWRulesSeq stx[0] stx[1] fun symm term => do
+@[builtinTactic Lean.Parser.Tactic.Conv.rewrite] def evalRewrite : Tactic := fun stx => do
+  let config ← Tactic.elabRewriteConfig stx[1]
+  withRWRulesSeq stx[0] stx[2] fun symm term => do
     Term.withSynthesize <| withMainContext do
       let e ← elabTerm term none true
-      let r ← rewrite (← getMainGoal) (← getLhs) e symm (config := { transparency := mode })
+      let r ← rewrite (← getMainGoal) (← getLhs) e symm (config := config)
       updateLhs r.eNew r.eqProof
       replaceMainGoal ((← getMainGoal) :: r.mvarIds)
 
-@[builtinTactic Lean.Parser.Tactic.Conv.rewrite] def evalRewrite : Tactic :=
-  evalRewriteCore TransparencyMode.instances
-
-@[builtinTactic Lean.Parser.Tactic.Conv.erewrite] def evalERewrite : Tactic :=
-  evalRewriteCore TransparencyMode.default
-
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Rewrite.lean

@@ -8,21 +8,22 @@ import Lean.Meta.Tactic.Replace
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Location
+import Lean.Elab.Tactic.Config
 namespace Lean.Elab.Tactic
 open Meta
 
-def rewriteTarget (stx : Syntax) (symm : Bool) (mode : TransparencyMode) : TacticM Unit := do
+def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do
   Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
-    let r ← rewrite (← getMainGoal) (← getMainTarget) e symm (config := { transparency := mode })
+    let r ← rewrite (← getMainGoal) (← getMainTarget) e symm (config := config)
     let mvarId' ← replaceTargetEq (← getMainGoal) r.eNew r.eqProof
     replaceMainGoal (mvarId' :: r.mvarIds)
 
-def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (mode : TransparencyMode) : TacticM Unit := do
+def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do
   Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
     let localDecl ← getLocalDecl fvarId
-    let rwResult ← rewrite (← getMainGoal) localDecl.type e symm (config := { transparency := mode })
+    let rwResult ← rewrite (← getMainGoal) localDecl.type e symm (config := config)
     let replaceResult ← replaceLocalDecl (← getMainGoal) fvarId rwResult.eNew rwResult.eqProof
     replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
 
@@ -44,18 +45,15 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
         let term := rule[1]
         x symm term
 
-def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => do
-  let loc   := expandOptLocation stx[2]
-  withRWRulesSeq stx[0] stx[1] fun symm term => do
+declare_config_elab elabRewriteConfig Rewrite.Config
+
+@[builtinTactic Lean.Parser.Tactic.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
+  let cfg ← elabRewriteConfig stx[1]
+  let loc   := expandOptLocation stx[3]
+  withRWRulesSeq stx[0] stx[2] fun symm term => do
     withLocation loc
-      (rewriteLocalDecl term symm · mode)
-      (rewriteTarget term symm mode)
+      (rewriteLocalDecl term symm · cfg)
+      (rewriteTarget term symm cfg)
       (throwTacticEx `rewrite . "did not find instance of the pattern in the current goal")
 
-@[builtinTactic Lean.Parser.Tactic.rewriteSeq] def evalRewriteSeq : Tactic :=
-  evalRewriteCore TransparencyMode.instances
-
-@[builtinTactic Lean.Parser.Tactic.erewriteSeq] def evalERewriteSeq : Tactic :=
-  evalRewriteCore TransparencyMode.default
-
 end Lean.Elab.Tactic

src/Std/Data/HashMap.lean

@@ -12,7 +12,8 @@ def HashMapBucket (α : Type u) (β : Type v) :=
 
 def HashMapBucket.update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) : HashMapBucket α β :=
   ⟨ data.val.uset i d h,
-    by erw [Array.size_set]; exact data.property ⟩
+    by conv => lhs; apply Array.size_set
+       apply data.property ⟩
 
 structure HashMapImp (α : Type u) (β : Type v) where
   size       : Nat

src/Std/Data/HashSet.lean

@@ -11,7 +11,8 @@ def HashSetBucket (α : Type u) :=
 
 def HashSetBucket.update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) : HashSetBucket α :=
   ⟨ data.val.uset i d h,
-    by erw [Array.size_set]; exact data.property ⟩
+    by conv => lhs; apply Array.size_set
+       apply data.property ⟩
 
 structure HashSetImp (α : Type u) where
   size       : Nat