From deab1ebc56cb1b347fa05f4033aab22cbed26568 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 17 Apr 2022 08:46:08 -0700
Subject: [PATCH] feat: add `save` tactic

It is a more convenient way of creating checkpoints.
---
 src/Init/Notation.lean                  |  2 ++
 src/Lean/Elab/Tactic/BuiltinTactic.lean | 36 ++++++++++++++++++++++++-
 2 files changed, 37 insertions(+), 1 deletion(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 65ad31d401..83ff845c16 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -599,6 +599,8 @@ syntax (name := fail) "fail " (str)? : tactic
 
 syntax (name := checkpoint) "checkpoint " tacticSeq : tactic
 
+macro (name := save) "save" : tactic => `(skip)
+
 end Tactic
 
 namespace Attr
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 55b0158651..1f695bf4b0 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -24,9 +24,43 @@ open Meta
 @[builtinTactic paren] def evalParen : Tactic := fun stx =>
   evalTactic stx[1]
 
+def isCheckpointableTactic (arg : Syntax) : TacticM Bool := do
+  -- TODO: make it parametric
+  let kind := arg.getKind
+  return kind == ``Lean.Parser.Tactic.save
+
+partial def addCheckpoints (args : Array Syntax) : TacticM (Array Syntax) := do
+  -- if (← readThe Term.Context).tacticCache? |>.isSome then
+  if (← args.anyM fun arg => isCheckpointableTactic arg[0]) then
+    let argsNew ← go 0 #[] #[]
+    return argsNew
+  return args
+where
+  push (acc : Array Syntax) (result : Array Syntax) : Array Syntax :=
+    if acc.isEmpty then
+      result
+    else
+      let ref := acc.back
+      let accSeq := mkNode ``Lean.Parser.Tactic.tacticSeq1Indented #[mkNullNode acc]
+      let checkpoint := mkNode ``Lean.Parser.Tactic.checkpoint #[mkAtomFrom ref "checkpoint", accSeq]
+      result.push (mkNode groupKind #[checkpoint, mkNullNode])
+
+  go (i : Nat) (acc : Array Syntax) (result : Array Syntax) : TacticM (Array Syntax) := do
+    if h : i < args.size then
+      let arg := args.get ⟨i, h⟩
+      if (← isCheckpointableTactic arg[0]) then
+        -- `argNew` is `arg` as singleton sequence. The idea is to make sure it does not satisfy `isCheckpointableTactic` anymore
+        let argNew := arg.setArg 0 (mkNullNode #[arg[0]])
+        let acc := acc.push argNew
+        go (i+1) #[] (push acc result)
+      else
+        go (i+1) (acc.push arg) result
+    else
+      return result ++ acc
+
 /- Evaluate `many (group (tactic >> optional ";")) -/
 def evalManyTacticOptSemi (stx : Syntax) : TacticM Unit := do
-  stx.forArgsM fun seqElem => do
+  for seqElem in (← addCheckpoints stx.getArgs) do
     evalTactic seqElem[0]
     saveTacticInfoForToken seqElem[1] -- add TacticInfo node for `;`