From 8c82302acaade273e564d0246476291d2816ce66 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 12 Sep 2021 18:09:19 -0700
Subject: [PATCH] refactor: add `config` syntax and macro for boilerplate code

---
 src/Init/Notation.lean           |  7 +++++--
 src/Lean/Elab/Tactic/Config.lean | 24 ++++++++++++++++++++++++
 src/Lean/Elab/Tactic/Simp.lean   | 28 ++++++++--------------------
 3 files changed, 37 insertions(+), 22 deletions(-)
 create mode 100644 src/Lean/Elab/Tactic/Config.lean

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 63d4861505..bdda844f90 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -320,6 +320,9 @@ macro "admit" : tactic => `(exact sorry)
 macro "sorry" : tactic => `(exact sorry)
 macro "inferInstance" : tactic => `(exact inferInstance)
 
+/- Optional configuration option for tactics -/
+syntax config := ("(" &"config" " := " term ")")
+
 syntax locationWildcard := "*"
 syntax locationHyp      := (colGt ident)+ ("⊢" <|> "|-")? -- TODO: delete
 syntax locationTargets  := (colGt ident)+ ("⊢" <|> "|-")?
@@ -361,8 +364,8 @@ syntax simpPost  := "↑"
 syntax simpLemma := (simpPre <|> simpPost)? ("←" <|> "<-")? term
 syntax simpErase := "-" ident
 syntax simpStar  := "*"
-syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
-syntax (name := simpAll) "simp_all " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic
+syntax (name := simp) "simp " (config)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
+syntax (name := simpAll) "simp_all " (config)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic
 
 /--
   Delta expand the given definition.
diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean
new file mode 100644
index 0000000000..2a14f47119
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Config.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.SyntheticMVars
+
+namespace Lean.Elab.Tactic
+open Meta
+macro "declare_config_elab" elabName:ident type:ident : command =>
+ `(unsafe def evalUnsafe (e : Expr) : TermElabM $type :=
+    Term.evalExpr $type ``$type e
+   @[implementedBy evalUnsafe] constant eval (e : Expr) : TermElabM $type
+   def $elabName (optConfig : Syntax) : TermElabM $type := do
+     if optConfig.isNone then
+       return { : $type }
+     else
+       withoutModifyingState <| withLCtx {} {} <| Term.withSynthesize do
+         let c ← Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``$type)
+         eval (← instantiateMVars c)
+  )
+
+end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 5976314565..fdc02c5892 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -4,39 +4,27 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Simp
+import Lean.Meta.Tactic.Replace
+import Lean.Elab.BuiltinNotation
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Location
-import Lean.Meta.Tactic.Replace
-import Lean.Elab.BuiltinNotation
+import Lean.Elab.Tactic.Config
 
 namespace Lean.Elab.Tactic
 open Meta
 
-unsafe def evalSimpConfigUnsafe (e : Expr) : TermElabM Meta.Simp.Config :=
-  Term.evalExpr Meta.Simp.Config ``Meta.Simp.Config e
-@[implementedBy evalSimpConfigUnsafe] constant evalSimpConfig (e : Expr) : TermElabM Meta.Simp.Config
-
-unsafe def evalSimpConfigCtxUnsafe (e : Expr) : TermElabM Meta.Simp.ConfigCtx :=
-  Term.evalExpr Meta.Simp.ConfigCtx ``Meta.Simp.ConfigCtx e
-@[implementedBy evalSimpConfigCtxUnsafe] constant evalSimpConfigCtx (e : Expr) : TermElabM Meta.Simp.ConfigCtx
+declare_config_elab elabSimpConfigCore    Meta.Simp.Config
+declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
 
 /-
   `optConfig` is of the form `("(" "config" ":=" term ")")?`
   If `ctx == false`, the argument is assumed to have type `Meta.Simp.Config`, and `Meta.Simp.ConfigCtx` otherwise. -/
 def elabSimpConfig (optConfig : Syntax) (ctx : Bool) : TermElabM Meta.Simp.Config := do
-  if optConfig.isNone then
-    if ctx then
-      return { : Meta.Simp.ConfigCtx }.toConfig
-    else
-      return {}
+  if ctx then
+    return (← elabSimpConfigCtxCore optConfig).toConfig
   else
-    withoutModifyingState <| withLCtx {} {} <| Term.withSynthesize do
-      let c ← Term.elabTermEnsuringType optConfig[3] (Lean.mkConst (if ctx then ``Meta.Simp.ConfigCtx else ``Meta.Simp.Config))
-      if ctx then
-        return (← evalSimpConfigCtx (← instantiateMVars c)).toConfig
-      else
-        evalSimpConfig (← instantiateMVars c)
+    elabSimpConfigCore optConfig
 
 private def addDeclToUnfoldOrLemma (lemmas : Meta.SimpLemmas) (e : Expr) (post : Bool) (inv : Bool) : MetaM Meta.SimpLemmas := do
   if e.isConst then