From d7c95907804dcb673dd6b8f208af4369b65bed4f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 5 Nov 2024 14:37:06 -0800
Subject: [PATCH] feat: Extract used constants from invocation

---
 Pantograph/Frontend/Elab.lean | 15 ++++++++++++++-
 Pantograph/Protocol.lean      |  3 +++
 Test/Integration.lean         | 12 +++++++-----
 3 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 6245877..ceecfae 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -122,6 +122,13 @@ protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
 protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
   t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
 
+protected def usedConstants (t: TacticInvocation) : NameSet :=
+  let info := t.info
+  info.goalsBefore
+    |>.filterMap info.mctxAfter.getExprAssignmentCore?
+    |>.map Expr.getUsedConstantsAsSet
+    |>.foldl .union .empty
+
 end TacticInvocation
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@@ -158,7 +165,13 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
     let tactic ← invocation.ctx.runMetaM {} do
       let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
       return t.pretty
-    return { goalBefore, goalAfter, tactic }
+    let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
+    return {
+      goalBefore,
+      goalAfter,
+      tactic,
+      usedConstants,
+    }
 
 structure InfoWithContext where
   info: Elab.Info
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 2ba073e..86a7b4d 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -298,6 +298,9 @@ structure InvokedTactic where
   goalBefore: String
   goalAfter: String
   tactic: String
+
+  -- List of used constants
+  usedConstants: Array String
   deriving Lean.ToJson
 
 structure CompilationUnit where
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 413ed1c..9fb86b7 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -167,8 +167,8 @@ example : ∀ (p: Prop), p → p := by
 
 def test_frontend_process : Test :=
   [
-    let file := "example : ∀ (p: Prop), p → p := by\n  intro p h\n  exact h"
-    let goal1 := "p : Prop\nh : p\n⊢ p"
+    let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
+    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
     step "frontend.process"
       [
         ("file", .str file),
@@ -180,14 +180,16 @@ def test_frontend_process : Test :=
          boundary := (0, file.utf8ByteSize),
          invocations? := .some [
            {
-             goalBefore := "⊢ ∀ (p : Prop), p → p",
+             goalBefore := "⊢ ∀ (p q : Prop), p → p ∨ q",
              goalAfter := goal1,
-             tactic := "intro p h",
+             tactic := "intro p q h",
+             usedConstants := #[],
            },
            {
              goalBefore := goal1 ,
              goalAfter := "",
-             tactic := "exact h",
+             tactic := "exact Or.inl h",
+             usedConstants := #["Or.inl"],
            },
          ]
        }],