Implementing a custom rewrite

Stream: lean4

[Vladimir Gladstein]

Hey! I am defining my own rewrite tactic srw, the simplified version of which would be just a regular rw where lemmas are listed not in square brackets, but just one by one.
The idea how I am going to implement that is:
having:

srw a b at l

I want it to be equivalent to

rw [a] at l; rw [b] at l

In other words, my elaboration function for srw (show below) takes a sequence of lemmas rs, and a location l, and

1. first pairs each lemma with a location l, yielding a syntax of category srwRuleLoc
2. then for each srwRuleLoc it elaborates it by calling an original rw (implemented in elab_rules)

The implementation is shown below:

declare_syntax_cat srwRule
declare_syntax_cat srwRules
declare_syntax_cat srwRuleLoc
declare_syntax_cat srwRulesLoc
syntax (name:= srwRule) term:max : srwRule
syntax srwRule  (location)? : srwRuleLoc
syntax (ppSpace colGt (srwRule))* : srwRules
syntax (name:= srwRulesLoc) (ppSpace colGt (srwRuleLoc))* : srwRulesLoc
syntax (name := srw) "srw" srwRules (location)? : tactic

-- rewriting a term with location
elab_rules : tactic
  | `(srwRuleLoc| $t:term $l:location ?) =>
      try do
        evalTactic $ <- `(tactic| rw [$t:term] $(l)?)
      catch | ex => throwErrorAt t ex.toMessageData

-- having an object of category `srwRule and a location, return `srwRuleLoc
def insertLocation (l : Option (TSyntax `Lean.Parser.Tactic.location)) (x : TSyntax `srwRule) : MacroM Syntax := do
  if x.raw.isOfKind `srwRule then
        let y <- `(srwRuleLoc| $(⟨x.raw.setKind `srwRule⟩):srwRule $l:location ?)
        return y.raw
  else return x.raw

-- elaborate each rewrite term one by one
elab "srw" rs:srwRules l:(location)? : tactic =>
  match rs with
  | `(srwRules| $[$rs] *) => do
    let rs <- rs.mapM (liftMacroM $ insertLocation l ·)
   for r in rs do evalTactic rs
  | _ => throwError ""

example : (True /\ False) /\ (True /\ True) = False := by
  srw true_and true_and -- the goal doesn't update withinh each rewrite separately

The problem with this code is that goal doesn't update within each rewrite rule. I guess this is because evalTactic will srwRuleLoc syntax with the context info, but not srwRule.

What would be the better way to fix it without changing elab_rules?
There is a reason why I want to treat each rule as a separate rewrite (In future, I want to specify a location for each rewrite separately). And the there is a reason why I don't want to add withTacticInfoContext t do to elab_rules (I want it to be extensible, such that if someone else wants to extend it they would not have to think about annotations)