Merge pull request leanprover#147 from leanprover/aggregate-at

feat: add `at _` location option to `sym_aggregate`

Tactics/Aggregate.lean

@@ -12,23 +12,39 @@ open Lean Meta Elab.Tactic
 namespace Sym
 
 /-- Given an array of (non-)effects hypotheses, aggregate these effects by
-`simp`ing the main goals -/
-def aggregate (axHyps : Array LocalDecl) : TacticM Unit :=
+`simp`ing at the specified location -/
+def aggregate (axHyps : Array LocalDecl) (location : Location) : TacticM Unit :=
   let msg := m!"aggregating (non-)effects"
   withTraceNode `Tactic.sym (fun _ => pure msg) <| do
     trace[Tactic.sym] "using hypotheses: {axHyps.map (·.toExpr)}"
 
     let (ctx, simprocs) ← LNSymSimpContext
         (config := {decide := true, failIfUnchanged := false})
         (decls := axHyps)
-    let goal? ← LNSymSimp (← getMainGoal) ctx simprocs
-    replaceMainGoal goal?.toList
 
+    withLocation location
+      (fun hyp => do
+        trace[Tactic.sym] "aggregating at {Expr.fvar hyp}"
+        let goal ← LNSymSimp (← getMainGoal) ctx simprocs hyp
+        replaceMainGoal goal.toList
+      )
+      (do
+        trace[Tactic.sym] "aggregating at the goal"
+        let goal ← LNSymSimp (← getMainGoal) ctx simprocs
+        replaceMainGoal goal.toList
+      )
+      (fun _ => pure ())
+
+open Parser.Tactic (location) in
 /--
 `sym_aggregate` will search for all local hypotheses of the form
   `r ?fld ?state = _` or `∀ f ..., r ?fld ?state = _`,
-and use those hypotheses to simplify the goal -/
-elab "sym_aggregate" : tactic => withMainContext do
+and use those hypotheses to simplify the goal
+
+`sym_aggregate at ...` will use those same hypotheses to simplify at the
+specified locations, using the same syntax as `simp at ...`
+-/
+elab "sym_aggregate" loc:(location)? : tactic => withMainContext do
   let msg := m!"aggregating local (non-)effect hypotheses"
   withTraceNode `Tactic.sym (fun _ => pure msg) <| do
     let lctx ← getLCtx
@@ -44,18 +60,21 @@ elab "sym_aggregate" : tactic => withMainContext do
       return mkApp (mkConst ``CheckSPAlignment) state
 
     let axHyps ←
-      lctx.foldlM (init := #[]) fun axHyps decl => do
-        forallTelescope decl.type <| fun _ type => do
-          trace[Tactic.sym] "checking {decl.toExpr} with type {type}"
-          let expectedRead ← expectedRead
-          let expectedAlign ← expectedAlign
-          if ← isDefEq type expectedRead then
-            trace[Tactic.sym] "{Lean.checkEmoji} match for {expectedRead}"
-            return axHyps.push decl
-          else if ← isDefEq type expectedAlign then
-            trace[Tactic.sym] "{Lean.checkEmoji} match for {expectedAlign}"
-            return axHyps.push decl
-          else
-            trace[Tactic.sym] "{Lean.crossEmoji} no match"
-            return axHyps
-    aggregate axHyps
+      withTraceNode `Tactic.sym (fun _ => pure m!"searching for effect hypotheses") <|
+        lctx.foldlM (init := #[]) fun axHyps decl => do
+          forallTelescope decl.type <| fun _ type => do
+            trace[Tactic.sym] "checking {decl.toExpr} with type {type}"
+            let expectedRead ← expectedRead
+            let expectedAlign ← expectedAlign
+            if ← isDefEq type expectedRead then
+              trace[Tactic.sym] "{Lean.checkEmoji} match for {expectedRead}"
+              return axHyps.push decl
+            else if ← isDefEq type expectedAlign then
+              trace[Tactic.sym] "{Lean.checkEmoji} match for {expectedAlign}"
+              return axHyps.push decl
+            else
+              trace[Tactic.sym] "{Lean.crossEmoji} no match"
+              return axHyps
+
+    let loc := (loc.map expandLocation).getD (.targets #[] true)
+    aggregate axHyps loc