feat: Tactic steps now include used constants (#59)

* modify tactic info to emit used constants * refactor * update tests
leanprover-community · Nov 1, 2024 · 65f1337 · 65f1337
1 parent adbbfcb
commit 65f1337
Show file tree

Hide file tree

Showing 6 changed files with 37 additions and 14 deletions.
diff --git a/REPL/JSON.lean b/REPL/JSON.lean
@@ -103,15 +103,17 @@ structure Tactic where
   goals : String
   tactic : String
   proofState : Option Nat
+  usedConstants : Array Name
 deriving ToJson, FromJson
 
 /-- Construct the JSON representation of a Lean tactic. -/
-def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Tactic :=
+def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat) (usedConstants : Array Name) : Tactic :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
     goals,
     tactic,
-    proofState }
+    proofState,
+    usedConstants }
 
 /--
 A response to a Lean command.

diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean
@@ -111,6 +111,12 @@ def isSubstantive (t : TacticInfo) : Bool :=
   | some ``Lean.Parser.Tactic.paren => false
   | _ => true
 
+def getUsedConstantsAsSet (t : TacticInfo) : NameSet :=
+  t.goalsBefore
+    |>.filterMap t.mctxAfter.getExprAssignmentCore?
+    |>.map Expr.getUsedConstantsAsSet
+    |>.foldl .union .empty
+
 end Lean.Elab.TacticInfo
 
 namespace Lean.Elab.InfoTree
@@ -206,11 +212,16 @@ def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Posit
   (t.findSorryTermNodes.map fun ⟨i, ctx⟩ =>
     (ctx, .term i.lctx i.expectedType?, stxRange ctx.fileMap i.stx))
 
-def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × Position × Position) :=
-  (t.findTacticNodes.map fun ⟨i, ctx⟩ =>
+def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × Position × Position × Array Name) :=
     -- HACK: creating a child ngen
-     ({ ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, i.stx, i.goalsBefore,
-       stxRange ctx.fileMap i.stx))
+  t.findTacticNodes.map fun ⟨i, ctx⟩ => 
+    let range := stxRange ctx.fileMap i.stx 
+    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, 
+      i.stx, 
+      i.goalsBefore, 
+      range.fst, 
+      range.snd, 
+      i.getUsedConstantsAsSet.toArray )
 
 
 end Lean.Elab.InfoTree

diff --git a/REPL/Main.lean b/REPL/Main.lean
@@ -116,12 +116,12 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
 
 def tactics (trees : List InfoTree) : M m (List Tactic) :=
   trees.bind InfoTree.tactics |>.mapM
-    fun ⟨ctx, stx, goals, pos, endPos⟩ => do
+    fun ⟨ctx, stx, goals, pos, endPos, ns⟩ => do
       let proofState := some (← ProofSnapshot.create ctx none none goals)
       let goals := s!"{(← ctx.ppGoals goals)}".trim
       let tactic := Format.pretty (← ppTactic ctx stx)
       let proofStateId ← proofState.mapM recordProofSnapshot
-      return Tactic.of goals tactic pos endPos proofStateId
+      return Tactic.of goals tactic pos endPos proofStateId ns
 
 /-- Record a `ProofSnapshot` and generate a JSON response for it. -/
 def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) :

diff --git a/test/all_tactics.expected.out b/test/all_tactics.expected.out
@@ -1,10 +1,12 @@
 {"tactics":
- [{"tactic": "have t := 37",
+ [{"usedConstants": ["instOfNatNat", "Nat", "OfNat.ofNat", "letFun"],
+   "tactic": "have t := 37",
    "proofState": 0,
    "pos": {"line": 1, "column": 18},
    "goals": "⊢ Nat",
    "endPos": {"line": 1, "column": 30}},
-  {"tactic": "exact t",
+  {"usedConstants": [],
+   "tactic": "exact t",
    "proofState": 1,
    "pos": {"line": 1, "column": 32},
    "goals": "t : Nat ⊢ Nat",

diff --git a/test/calc.expected.out b/test/calc.expected.out
@@ -1,15 +1,21 @@
 {"tactics":
- [{"tactic": "calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
+ [{"usedConstants":
+   ["Trans.trans", "instOfNatNat", "instTransEq", "Nat", "OfNat.ofNat", "Eq"],
+   "tactic": "calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
    "proofState": 2,
    "pos": {"line": 1, "column": 22},
    "goals": "⊢ 3 = 5",
    "endPos": {"line": 3, "column": 19}},
-  {"tactic": "sorry",
+  {"usedConstants":
+   ["sorryAx", "instOfNatNat", "Nat", "OfNat.ofNat", "Bool.false", "Eq"],
+   "tactic": "sorry",
    "proofState": 3,
    "pos": {"line": 2, "column": 14},
    "goals": "⊢ 3 = 4",
    "endPos": {"line": 2, "column": 19}},
-  {"tactic": "sorry",
+  {"usedConstants":
+   ["sorryAx", "instOfNatNat", "Nat", "OfNat.ofNat", "Bool.false", "Eq"],
+   "tactic": "sorry",
    "proofState": 4,
    "pos": {"line": 3, "column": 14},
    "goals": "⊢ 4 = 5",

diff --git a/test/file.expected.out b/test/file.expected.out
@@ -1,5 +1,7 @@
 {"tactics":
- [{"tactic": "exact rfl",
+ [{"usedConstants":
+   ["f", "g", "instHAdd", "HAdd.hAdd", "Nat", "instAddNat", "rfl"],
+   "tactic": "exact rfl",
    "proofState": 0,
    "pos": {"line": 5, "column": 29},
    "goals": "⊢ f + g = 39",