From f577b4c6e64b0f823ac91b7c67eef6b30f3862cf Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Mon, 21 Jun 2021 11:29:47 -0700
Subject: [PATCH] experiment: tactic tracing

---
 src/Lean/Elab/Tactic/Basic.lean           | 53 +++++++++++++++++++++--
 src/Lean/PrettyPrinter/Formatter.lean     |  3 +-
 src/Lean/PrettyPrinter/Parenthesizer.lean |  3 +-
 3 files changed, 53 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 29d88dc98443..21ee57398014 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -15,9 +15,14 @@ import Lean.Meta.Tactic.Subst
 import Lean.Elab.Util
 import Lean.Elab.Term
 import Lean.Elab.Binders
+import Lean.PrettyPrinter.Formatter
+import Lean.PrettyPrinter.Parenthesizer
+import Std.Data.HashMap
+
+open Std (HashMap)
 
 namespace Lean.Elab
-open Meta
+open Meta PrettyPrinter
 
 /- Assign `mvarId := sorry` -/
 def admitGoal (mvarId : MVarId) : MetaM Unit :=
@@ -39,7 +44,8 @@ structure Context where
   main : MVarId
 
 structure State where
-  goals : List MVarId
+  goals   : List MVarId
+  history : HashMap (List MVarId) Syntax := {}
   deriving Inhabited
 
 structure SavedState where
@@ -68,6 +74,44 @@ def getUnsolvedGoals : TacticM (List MVarId) := do
   pruneSolvedGoals
   getGoals
 
+partial def clearTacticSeqs : Syntax → TacticM Syntax
+  | Syntax.node k args => do
+    if k == `Lean.Parser.Tactic.tacticSeq then
+      `(?_)
+    else
+      Syntax.node k (← args.mapM clearTacticSeqs)
+  | stx => stx
+
+partial def clearSyntheticHoles : Syntax → TacticM Syntax
+  | Syntax.node k args => do
+    if k == `Lean.Parser.Term.syntheticHole then
+      `(?_)
+    else
+      Syntax.node k (← args.mapM clearSyntheticHoles)
+  | stx => stx
+
+--   (Term.syntheticHole "?" (Term.hole "_")))))
+def recordHistory (stx : Syntax) : TacticM Unit := do
+  if (stx.getKind == `Lean.Parser.Tactic.case) then return ()
+  let gs ← getUnsolvedGoals
+  -- This is a bad idea, because lot's of silly actions will dominate
+  -- if (← get).history.contains gs then return ()
+  let stx ← clearTacticSeqs stx
+  let stx ← clearSyntheticHoles stx
+  modify fun s => { s with history := s.history.insert gs stx }
+
+def printHistory : TacticM Unit := do
+  for (gs, stx) in (← get).history.toList do
+    let msgData := goalsToMessageData [gs.head!]
+    let msgData ← addMessageContext msgData
+    println! "--- START ---"
+    println! "[GOAL]"
+    println! "{← msgData.toString}"
+    println! "[Tactic]"
+    -- println! "{stx}"
+    println! "{← formatTactic (← parenthesizeTactic stx)}"
+    println! "--- END ---"
+
 @[inline] private def TacticM.runCore (x : TacticM α) (ctx : Context) (s : State) : TermElabM (α × State) :=
   x ctx |>.run s
 
@@ -90,7 +134,7 @@ def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) :=
        else
          throw ex
    try
-     aux.runCore' { main := mvarId } { goals := [mvarId] }
+     (aux <* printHistory).runCore' { main := mvarId } { goals := [mvarId] }
    finally
      modify fun s => { s with syntheticMVars := savedSyntheticMVars }
 
@@ -183,7 +227,8 @@ mutual
           | evalFns => evalTacticUsing s stx evalFns
       | _ => throwError m!"unexpected tactic{indentD stx}"
 
-  partial def evalTactic (stx : Syntax) : TacticM Unit :=
+  partial def evalTactic (stx : Syntax) : TacticM Unit := do
+    recordHistory stx
     withTacticInfoContext stx (evalTacticAux stx)
 
 end
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index a15741c69427..533bb21aae51 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -483,8 +483,9 @@ def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
       pure $ Format.fill $ st.stack.get! 0)
     (fun _ => throwError "format: uncaught backtrack exception")
 
-def formatTerm := format $ categoryParser.formatter `term
+def formatTerm    := format $ categoryParser.formatter `term
 def formatCommand := format $ categoryParser.formatter `command
+def formatTactic  := format $ categoryParser.formatter `tactic
 
 builtin_initialize registerTraceClass `PrettyPrinter.format;
 
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index b7de8dd704c0..43f8f4df73ff 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -543,8 +543,9 @@ def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax :
       pure st.stxTrav.cur)
     (fun _ => throwError "parenthesize: uncaught backtrack exception")
 
-def parenthesizeTerm := parenthesize $ categoryParser.parenthesizer `term 0
+def parenthesizeTerm    := parenthesize $ categoryParser.parenthesizer `term 0
 def parenthesizeCommand := parenthesize $ categoryParser.parenthesizer `command 0
+def parenthesizeTactic  := parenthesize $ categoryParser.parenthesizer `tactic 0
 
 builtin_initialize registerTraceClass `PrettyPrinter.parenthesize