From 651afa75f4cb8cbd10c77247e055177c5adeed56 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 2 Aug 2024 19:49:11 -0700
Subject: [PATCH] feat: Filter in `visibleFVarsOfMVar`

---
 Pantograph/Condensed.lean | 14 +++++++++++---
 Pantograph/Goal.lean      | 10 +++++++---
 2 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 8b5c313..1db3c62 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -66,11 +66,19 @@ def elabState (levelNames: Array Name): Elab.Term.State := {
 
 end Condensed
 
+-- Get the list of visible (by default) free variables from a goal
+@[export pantograph_visible_fvars_of_mvar]
+protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
+  let mvarDecl ← mctx.findDecl? mvarId
+  let lctx := mvarDecl.lctx
+  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
+    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
+    | none      => r
+
 @[export pantograph_to_condensed_goal_m]
 def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
-  let options : Protocol.Options := {}
-  let ppAuxDecls       := options.printAuxDecls
-  let ppImplDetailHyps := options.printImplementationDetailHyps
+  let ppAuxDecls     := Meta.pp.auxDecls.get (← getOptions)
+  let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
   let mvarDecl ← mvarId.getDecl
   let lctx     := mvarDecl.lctx
   let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 0e87a12..ccb7a3d 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -69,10 +69,14 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
 
-@[export pantograph_goal_state_fvar_names_of_goal]
-protected def GoalState.fvarNamesOfGoal (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do
+-- Get the list of visible free variables from a goal
+@[export pantograph_goal_state_visible_fvars]
+protected def GoalState.visibleFVars (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do
   let mvarDecl ← state.mctx.findDecl? mvarId
-  return mvarDecl.lctx.getFVarIds
+  let lctx := mvarDecl.lctx
+  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
+    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
+    | none      => r
 
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState