chore: split out Expr.getMVarDependencies from MVarId.getMVarDependencies

src/Lean/Meta/CollectMVars.lean

@@ -50,39 +50,50 @@ def getMVarsAtDecl (d : Declaration) : MetaM (Array MVarId) := do
   let (_, s) ← (collectMVarsAtDecl d).run {}
   pure s.result
 
+end Lean.Meta
+
+open Lean Meta
+
+mutual
+
+/-- Auxiliary definition for `getMVarDependencies`. -/
+private partial def addMVars (e : Expr) (includeDelayed := false) : StateRefT (Std.HashSet MVarId) MetaM Unit := do
+  let mvars ← getMVars e
+  let mut s ← get
+  set ({} : Std.HashSet MVarId) -- Ensure that `s` is not shared.
+  for mvarId in mvars do
+    if ← pure includeDelayed <||> notM (mvarId.isDelayedAssigned) then
+      s := s.insert mvarId
+  set s
+  mvars.forM go
+
+/-- Auxiliary definition for `getMVarDependencies`. -/
+private partial def go (mvarId : MVarId) (includeDelayed := false) : StateRefT (Std.HashSet MVarId) MetaM Unit :=
+  withIncRecDepth do
+    let mdecl ← mvarId.getDecl
+    addMVars mdecl.type includeDelayed
+    for ldecl in mdecl.lctx do
+      addMVars ldecl.type includeDelayed
+      if let (some val) := ldecl.value? then
+        addMVars val includeDelayed
+    if let (some ass) ← getDelayedMVarAssignment? mvarId then
+      let pendingMVarId := ass.mvarIdPending
+      if ← notM pendingMVarId.isAssignedOrDelayedAssigned then
+        modify (·.insert pendingMVarId)
+      go pendingMVarId includeDelayed
+
+end
+
 /--
 Collect the metavariables which `mvarId` depends on. These are the metavariables
 which appear in the type and local context of `mvarId`, as well as the
 metavariables which *those* metavariables depend on, etc.
 -/
-partial def _root_.Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed := false) :
+def Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed := false) :
     MetaM (Std.HashSet MVarId) :=
-  (·.snd) <$> (go mvarId).run {}
-where
-  /-- Auxiliary definition for `getMVarDependencies`. -/
-  addMVars (e : Expr) : StateRefT (Std.HashSet MVarId) MetaM Unit := do
-    let mvars ← getMVars e
-    let mut s ← get
-    set ({} : Std.HashSet MVarId) -- Ensure that `s` is not shared.
-    for mvarId in mvars do
-      if ← pure includeDelayed <||> notM (mvarId.isDelayedAssigned) then
-        s := s.insert mvarId
-    set s
-    mvars.forM go
+  (·.snd) <$> (go mvarId includeDelayed).run {}
 
-  /-- Auxiliary definition for `getMVarDependencies`. -/
-  go (mvarId : MVarId) : StateRefT (Std.HashSet MVarId) MetaM Unit :=
-    withIncRecDepth do
-      let mdecl ← mvarId.getDecl
-      addMVars mdecl.type
-      for ldecl in mdecl.lctx do
-        addMVars ldecl.type
-        if let (some val) := ldecl.value? then
-          addMVars val
-      if let (some ass) ← getDelayedMVarAssignment? mvarId then
-        let pendingMVarId := ass.mvarIdPending
-        if ← notM pendingMVarId.isAssignedOrDelayedAssigned then
-          modify (·.insert pendingMVarId)
-        go pendingMVarId
-
-end Lean.Meta
+/-- Collect the metavariables appearing in the expression `e`,
+including metavariables in the type or local context of any such metavariables, etc. -/
+def Lean.Expr.getMVarDependencies (e : Expr) (includeDelayed := false) : MetaM (Std.HashSet MVarId) := do
+  (·.snd) <$> (addMVars e includeDelayed).run {}