From d1c0dc376fce10d1abe8d7576c2673626f828706 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 30 Oct 2023 14:44:06 -0700
Subject: [PATCH] feat: Print metavariable name in goal

---
 Pantograph/Protocol.lean |  5 +++--
 Pantograph/Serial.lean   |  7 ++++---
 Test/Common.lean         |  1 +
 Test/Integration.lean    |  1 +
 Test/Proofs.lean         | 16 +++++++++-------
 5 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index e379782..fd790bb 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -54,8 +54,9 @@ structure Variable where
   value?: Option Expression := .none
   deriving Lean.ToJson
 structure Goal where
-  /-- String case id -/
-  caseName?: Option String  := .none
+  name: String := ""
+  /-- Name of the metavariable -/
+  userName?: Option String  := .none
   /-- Is the goal in conversion mode -/
   isConversion: Bool        := false
   /-- target expression type -/
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 615d9b9..a46c2c7 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -168,7 +168,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
   }
 
 /-- Adapted from ppGoal -/
-def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
       : MetaM Protocol.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
@@ -229,7 +229,8 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
           | false => ppVar localDecl
         return var::acc
     return {
-      caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
+      name := of_name goal.name,
+      userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
       isConversion := isLHSGoal? mvarDecl.type |>.isSome,
       target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
@@ -246,7 +247,7 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt
   goals.mapM fun goal => do
     match state.mctx.findDecl? goal with
     | .some mvarDecl =>
-      let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
+      let serializedGoal ← serialize_goal options goal mvarDecl (parentDecl? := parentDecl?)
       pure serializedGoal
     | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
diff --git a/Test/Common.lean b/Test/Common.lean
index 3e52932..f74e6a2 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -7,6 +7,7 @@ namespace Protocol
 def Goal.devolatilize (goal: Goal): Goal :=
   {
     goal with
+    name := "",
     vars := goal.vars.map removeInternalAux,
   }
   where removeInternalAux (v: Variable): Variable :=
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 6400cca..0420a29 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -84,6 +84,7 @@ def test_malformed_command : IO LSpec.TestSeq :=
   ]
 def test_tactic : IO LSpec.TestSeq :=
   let goal: Protocol.Goal := {
+    name := "_uniq.10",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
     vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
   }
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index a726627..c08ecb2 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -66,9 +66,9 @@ def startProof (start: Start): TestM (Option GoalState) := do
 
 def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
-def buildGoal (nameType: List (String × String)) (target: String) (caseName?: Option String := .none): Protocol.Goal :=
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
   {
-    caseName?,
+    userName?,
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
       userName := x.fst,
@@ -293,13 +293,13 @@ def proof_or_comm: TestM Unit := do
   return ()
   where
     typeProp: Protocol.Expression := { pp? := .some "Prop" }
-    branchGoal (caseName name: String): Protocol.Goal := {
-      caseName? := .some caseName,
+    branchGoal (caseName varName: String): Protocol.Goal := {
+      userName? := .some caseName,
       target := { pp? := .some "q ∨ p" },
       vars := #[
         { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
         { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
-        { userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
+        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
       ]
     }
 
@@ -352,9 +352,11 @@ def proof_proposition_generation: TestM Unit := do
       return ()
   addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[
-      buildGoal [] "?fst" (caseName? := .some "snd"),
-      buildGoal [] "Prop" (caseName? := .some "fst")
+      buildGoal [] "?fst" (userName? := .some "snd"),
+      buildGoal [] "Prop" (userName? := .some "fst")
       ])
+  if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
+    addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
 
   let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with