Merge pull request 'feat: Query arbitrary assignment in goal' (#47) from goal/relation into dev

Reviewed-on: #47

Pantograph/Goal.lean

@@ -225,6 +225,10 @@ protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
   let expr := goalState.mctx.eAssignment.find! parent
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr
+protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
+  let expr ← goalState.mctx.eAssignment.find? mvar
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  return expr
 
 
 end Pantograph

Pantograph/Protocol.lean

@@ -243,7 +243,7 @@ structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parent?: Option Expression := .none
+  parent?: Option Expression
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL

Test/Integration.lean

@@ -97,6 +97,12 @@ def test_tactic : IO LSpec.TestSeq :=
        goals? := #[goal1],
      }:
       Protocol.GoalTacticResult)),
+    subroutine_step "goal.print"
+      [("stateId", .num 1)]
+     (Lean.toJson ({
+       parent? := .some { pp? := .some "fun x => ?m.11 x" },
+     }:
+      Protocol.GoalPrintResult)),
     subroutine_step "goal.tactic"
       [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      (Lean.toJson ({