Lean4
/-- Get all metavariables which `mvarId` depends on. These are the metavariables
which occur in the target or local context or delayed assignment (if any) of
`mvarId`, plus the metavariables which occur in these metavariables, etc.
-/
partial def getUnassignedGoalMVarDependencies (mvarId : MVarId) : MetaM (Std.HashSet MVarId) :=
return (← go mvarId |>.run { }).snd
where
/-- auxiliary function for `getUnassignedGoalMVarDependencies` -/
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
unless ← mvarId.isDelayedAssigned do
s := s.insert mvarId
set s
mvars.forM go
/-- auxiliary function for `getUnassignedGoalMVarDependencies` -/
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
unless ← pendingMVarId.isAssigned <||> pendingMVarId.isDelayedAssigned do
modify (·.insert pendingMVarId)
go pendingMVarId
