feat: merge RunCmd and RunTac, add by_elab (#361)

Author: digama0

Mathlib.lean

@@ -102,7 +102,6 @@ import Mathlib.Tactic.Replace
 import Mathlib.Tactic.RestateAxiom
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.RunCmd
-import Mathlib.Tactic.RunTac
 import Mathlib.Tactic.Sat.FromLRAT
 import Mathlib.Tactic.SeqFocus
 import Mathlib.Tactic.Set

Mathlib/Data/List/Basic.lean

@@ -687,7 +687,7 @@ theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
     if h₁ : n < length l₁ then by
       rw [get?_eq_get, get?_eq_get, h n h₁ (by rwa [←hl])]
     else by
-      have h₁ := le_of_not_gt h₁
+      have h₁ := le_of_not_lt h₁
       rw [get?_len_le h₁, get?_len_le]; rwa [← hl]
 
 theorem modifyNthTail_id : ∀ n (l : List α), l.modifyNthTail id n = l

Mathlib/Mathport/Syntax.lean

@@ -195,7 +195,6 @@ syntax caseArg := binderIdent,+ (" :" (ppSpace (ident <|> "_"))+)?
   (" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
 /- E -/ syntax (name := symm) "symm" : tactic
 /- E -/ syntax (name := trans) "trans" (ppSpace colGt term)? : tactic
-/- B -/ syntax (name := acRfl') "ac_rfl" : tactic
 /- B -/ syntax (name := cc) "cc" : tactic
 
 -- builtin unfold only accepts single ident

Mathlib/Tactic/Conv.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-import Mathlib.Tactic.RunTac
+import Mathlib.Tactic.RunCmd
 
 /-!
 Additional `conv` tactics.

Mathlib/Tactic/RunCmd.lean

@@ -1,22 +1,61 @@
 /-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Copyright (c) 2018 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
+Authors: Sebastian Ullrich, Mario Carneiro
 -/
-import Lean
+import Lean.Elab.SyntheticMVars
 import Mathlib.Util.TermUnsafe
 
 /-!
-Define a `run_cmd a; b` command which executes code in `CommandElabM Unit`.
-This is almost the same as `#eval show CommandElabM Unit from do a; b`,
-except that it doesn't print an empty diagnostic.
+Defines commands to compile and execute a command / term / tactic on the spot:
+
+* `run_cmd doSeq` command which executes code in `CommandElabM Unit`.
+  This is almost the same as `#eval show CommandElabM Unit from do doSeq`,
+  except that it doesn't print an empty diagnostic.
+
+* `run_tac doSeq` tactic which executes code in `TacticM Unit`.
+
+* `by_elab doSeq` term which executes code in `TermElabM Expr` to produce an expression.
 -/
 
-namespace Lean.Parser.Command
-open Meta Elab Command Term
+namespace Mathlib.RunCmd
+open Lean Meta Elab Command Term Tactic
 
+/--
+The `run_cmd doSeq` command executes code in `CommandElabM Unit`.
+This is almost the same as `#eval show CommandElabM Unit from do doSeq`,
+except that it doesn't print an empty diagnostic.
+-/
 elab (name := runCmd) "run_cmd " elems:doSeq : command => do
   ← liftTermElabM <|
     unsafe evalTerm (CommandElabM Unit)
       (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
       (← `(discard do $elems))
+
+/-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
+elab (name := runTac) "run_tac" e:doSeq : tactic => do
+  ← unsafe evalTerm (TacticM Unit) (mkApp (mkConst ``TacticM) (mkConst ``Unit))
+    (← `(discard do $e))
+
+/--
+* The `by_elab doSeq` expression runs the `doSeq` as a `TermElabM Expr` to
+  synthesize the expression.
+* `by_elab fun expectedType? => do doSeq` receives the expected type (an `Option Expr`)
+  as well.
+-/
+syntax (name := byElab) "by_elab" doSeq : term
+
+/-- Elaborator for `by_elab`. -/
+@[termElab byElab] def elabRunElab : TermElab := fun
+| `(by_elab $cmds:doSeq), expectedType? => do
+  if let `(Lean.Parser.Term.doSeq| $e:term) := cmds then
+    if e matches `(Lean.Parser.Term.doSeq| fun $_* => $_) then
+      let tac ← unsafe evalTerm
+        (Option Expr → TermElabM Expr)
+        (Lean.mkForall `x .default
+          (mkApp (mkConst ``Option) (mkConst ``Expr))
+          (mkApp (mkConst ``TermElabM) (mkConst ``Expr))) e
+      return ← tac expectedType?
+  (← unsafe evalTerm (TermElabM Expr) (mkApp (mkConst ``TermElabM) (mkConst ``Expr))
+    (← `(do $cmds)))
+| _, _ => throwUnsupportedSyntax

Mathlib/Tactic/RunTac.lean

@@ -439,7 +439,6 @@
  ["docBlame", "Mathlib.ExtendedBinder.«term∀ᵉ_,_»"],
  ["docBlame", "Mathlib.ExtendedBinder.«term∃__,_»"],
  ["docBlame", "Mathlib.ExtendedBinder.«term∃ᵉ_,_»"],
- ["docBlame", "Mathlib.RunTac.tacticRun_tac_"],
  ["docBlame", "Mathlib.Tactic.haveLetCore"],
  ["docBlame", "Mathlib.Tactic.renameArg"],
  ["docBlame", "Mathlib.Tactic.set"],

scripts/nolints.json

@@ -0,0 +1,11 @@
+import Lean.Elab.Tactic.ElabTerm
+import Mathlib.Tactic.RunCmd
+
+open Lean Elab Tactic
+
+example : True := by
+  run_tac
+    evalApplyLikeTactic MVarId.apply (← `(True.intro))
+
+example : True := by_elab
+  Term.elabTerm (← `(True.intro)) none