refactor: use Simp.Context instead of Config+SimpLemmas+CongrLemmas

src/Lean/Elab/Tactic/Simp.lean

@@ -12,11 +12,11 @@ import Lean.Meta.Tactic.Replace
 namespace Lean.Elab.Tactic
 open Meta
 
-def simpTarget (config : Meta.Simp.Config) (simpLemmas : SimpLemmas) (congrLemmas : CongrLemmas) : TacticM Unit := do
+def simpTarget (ctx : Simp.Context) : TacticM Unit := do
   let (g, gs) ← getMainGoal
   withMVarContext g do
     let target ← instantiateMVars (← getMVarDecl g).type
-    let r ← simp target config simpLemmas congrLemmas
+    let r ← simp target ctx
     match r.proof? with
     | some proof => setGoals ((← replaceTargetEq g r.expr proof) :: gs)
     | none => setGoals ((← replaceTargetDefEq g r.expr) :: gs)
@@ -25,28 +25,28 @@ def simpTarget (config : Meta.Simp.Config) (simpLemmas : SimpLemmas) (congrLemma
 -- TODO: issues: self simplification
 -- TODO: add new assertion with simplified result and clear old ones after simplifying all locals
 
-def simpLocalDeclFVarId (config : Meta.Simp.Config) (simpLemmas : SimpLemmas) (congrLemmas : CongrLemmas) (fvarId : FVarId) : TacticM Unit := do
+def simpLocalDeclFVarId (ctx : Simp.Context) (fvarId : FVarId) : TacticM Unit := do
   let (g, gs) ← getMainGoal
   withMVarContext g do
     let localDecl ← getLocalDecl fvarId
-    let r ← simp localDecl.type config simpLemmas congrLemmas
+    let r ← simp localDecl.type ctx
     match r.proof? with
     | some proof =>
       setGoals ((← replaceLocalDecl g fvarId r.expr proof).mvarId :: gs)
     | none => setGoals ((← changeLocalDecl g fvarId r.expr (checkDefEq := false)) :: gs)
 
-def simpLocalDecl (config : Meta.Simp.Config) (simpLemmas : SimpLemmas) (congrLemmas : CongrLemmas) (userName : Name) : TacticM Unit :=
+def simpLocalDecl (ctx : Simp.Context) (userName : Name) : TacticM Unit :=
   withMainMVarContext do
     let localDecl ← getLocalDeclFromUserName userName
-    simpLocalDeclFVarId config simpLemmas congrLemmas localDecl.fvarId
+    simpLocalDeclFVarId ctx localDecl.fvarId
 
-def simpAll (config : Meta.Simp.Config) (simpLemmas : SimpLemmas) (congrLemmas : CongrLemmas) : TacticM Unit := do
-  let worked ← «try» (simpTarget config simpLemmas congrLemmas)
+def simpAll (ctx : Simp.Context) : TacticM Unit := do
+  let worked ← «try» (simpTarget ctx)
   withMainMVarContext do
     let mut worked := worked
     -- We must traverse backwards because `replaceLocalDecl` uses the revert/intro idiom
     for fvarId in (← getLCtx).getFVarIds.reverse do
-      worked := worked || (← «try» <| simpLocalDeclFVarId config simpLemmas congrLemmas fvarId)
+      worked := worked || (← «try» <| simpLocalDeclFVarId ctx fvarId)
     unless worked do
       let (mvarId, _) ← getMainGoal
       throwTacticEx `simp mvarId "failed to simplify"
@@ -73,38 +73,36 @@ def elabSimpConfig (optConfig : Syntax) : TermElabM Meta.Simp.Config := do
       let c ← Term.elabTermEnsuringType optConfig[0] (Lean.mkConst ``Meta.Simp.Config)
       evalSimpConfig (← instantiateMVars c)
 
+/-- Elaborate extra simp lemmas provided to `simp`. `stx` is of the `simpLemma,*` -/
+private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Context := do
+  if stx.isNone then
+    return ctx
+  else
+    /-
+    syntax simpPre := "↓"
+    syntax simpPost := "↑"
+    syntax simpLemma := (simpPre <|> simpPost)? term
+     -/
+    let (g, _) ← getMainGoal
+    withMVarContext g do
+      let mut lemmas := ctx.simpLemmas
+      for simpLemma in stx[1].getSepArgs do
+        let post :=
+          if simpLemma[0].isNone then
+            true
+          else
+            simpLemma[0][0].getKind == ``Parser.Tactic.simpPost
+        let term ← elabTerm simpLemma[1] none true
+        lemmas ← lemmas.add term post
+      return { ctx with simpLemmas := lemmas }
+
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
-  let simpLemmas ← mkSimpLemmas stx[1]
-  let congrLemmas ← getCongrLemmas
-  let config ← elabSimpConfig stx[2]
+  let ctx ← elabSimpLemmas stx[1] { config := (← elabSimpConfig stx[2]), simpLemmas := (← getSimpLemmas), congrLemmas := (← getCongrLemmas) }
   let loc := expandOptLocation stx[3]
   match loc with
-  | Location.target => simpTarget config simpLemmas congrLemmas
-  | Location.localDecls userNames => userNames.forM (simpLocalDecl config simpLemmas congrLemmas)
-  | Location.wildcard => simpAll config simpLemmas congrLemmas
+  | Location.target => simpTarget ctx
+  | Location.localDecls userNames => userNames.forM (simpLocalDecl ctx)
+  | Location.wildcard => simpAll ctx
   tryExactTrivial
-where
-  mkSimpLemmas (stx : Syntax) := do
-    let lemmas ← getSimpLemmas
-    if stx.isNone then
-      return lemmas
-    else
-      /-
-      syntax simpPre := "↓"
-      syntax simpPost := "↑"
-      syntax simpLemma := (simpPre <|> simpPost)? term
-       -/
-      let (g, _) ← getMainGoal
-      withMVarContext g do
-        let mut lemmas := lemmas
-        for simpLemma in stx[1].getSepArgs do
-          let post :=
-            if simpLemma[0].isNone then
-              true
-            else
-              simpLemma[0][0].getKind == ``Parser.Tactic.simpPost
-          let term ← elabTerm simpLemma[1] none true
-          lemmas ← lemmas.add term post
-        return lemmas
 
 end Lean.Elab.Tactic

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -163,6 +163,7 @@ where
 
   /- Try to rewrite `e` children using the given congruence lemma -/
   tryCongrLemma? (c : CongrLemma) (e : Expr) : M (Option Result) := withNewMCtxDepth do
+    trace[Meta.Tactic.simp.congr]! "{c.theoremName}, {e}"
     let info ← getConstInfo c.theoremName
     let lemma := mkConst c.theoremName (← info.levelParams.mapM fun _ => mkFreshLevelMVar)
     let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType lemma)
@@ -178,10 +179,13 @@ where
           if (← processCongrHypothesis x) then
             modified := true
         catch _ =>
+          trace[Meta.Tactic.simp.congr]! "processCongrHypothesis {c.theoremName} failed {← inferType x}"
           return none
       unless modified do
+        trace[Meta.Tactic.simp.congr]! "{c.theoremName} not modified"
         return none
       unless (← synthesizeArgs c.theoremName xs bis (← read).discharge?) do
+        trace[Meta.Tactic.simp.congr]! "{c.theoremName} synthesizeArgs failed"
         return none
       let eNew ← instantiateMVars rhs
       let proof ← instantiateMVars (mkAppN lemma xs)
@@ -285,16 +289,16 @@ where
       modify fun s => { s with cache := s.cache.insert e r }
     return r
 
-def main (e : Expr) (config : Config := {}) (methods : Methods := {}) (simpLemmas : SimpLemmas := {}) (congrLemmas : CongrLemmas := {}) : MetaM Result := do
+def main (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Result := do
   withReducible do
-    simp e methods { config := config, simpLemmas := simpLemmas, congrLemmas := congrLemmas } |>.run' {}
+    simp e methods ctx |>.run' {}
 
 end Simp
 
-def simp (e : Expr) (config : Simp.Config := {}) (simpLemmas : SimpLemmas := {}) (congrLemmas : CongrLemmas := {}) : MetaM Simp.Result := do
+def simp (e : Expr) (ctx : Simp.Context) : MetaM Simp.Result := do
   let discharge? (e : Expr) : SimpM (Option Expr) := return none -- TODO: use simp, and add config option
   let pre  := (Simp.preDefault · discharge?)
   let post := (Simp.postDefault · discharge?)
-  Simp.main e (config := config) (methods := { pre := pre, post := post, discharge? := discharge? }) (simpLemmas := simpLemmas) (congrLemmas := congrLemmas)
+  Simp.main e ctx (methods := { pre := pre, post := post, discharge? := discharge? })
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -19,9 +19,9 @@ abbrev Cache := ExprMap Result
 
 structure Context where
   config      : Config
-  parent?     : Option Expr := none
   simpLemmas  : SimpLemmas
   congrLemmas : CongrLemmas
+  parent?     : Option Expr := none
 
 structure State where
   cache    : Cache := {}