def
Lean.Meta.mkGeneralizationForbiddenSet
(targets : Array Lean.Expr)
(forbidden : optParam Lean.FVarIdSet ∅)
:
Equations
- Lean.Meta.mkGeneralizationForbiddenSet targets forbidden = (fun visit loop => let s := { visitedExpr := ∅, fvarSet := forbidden }; let todo := #[]; do let r ← forIn targets { fst := s, snd := todo } fun target r => let s := r.fst; let todo := r.snd; if Lean.Expr.isFVar target = true then let todo := Array.push todo (Lean.Expr.fvarId! target); do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := todo }) else do let a ← Lean.Meta.inferType target let a ← Lean.Meta.instantiateMVars a let s : Lean.CollectFVars.State := Lean.collectFVars s a pure PUnit.unit pure (ForInStep.yield { fst := s, snd := todo }) let x : MProd Lean.CollectFVars.State (Array Lean.FVarId) := r match x with | { fst := s, snd := todo } => loop (Array.toList todo) s.fvarSet) Lean.Meta.mkGeneralizationForbiddenSet.visit Lean.Meta.mkGeneralizationForbiddenSet.loop
def
Lean.Meta.mkGeneralizationForbiddenSet.visit
(fvarId : Lean.FVarId)
(todo : List Lean.FVarId)
(s : Lean.FVarIdSet)
:
Equations
- Lean.Meta.mkGeneralizationForbiddenSet.visit fvarId todo s = do let localDecl ← Lean.Meta.getLocalDecl fvarId let a ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) let s' : Lean.CollectFVars.State := Lean.collectFVars { visitedExpr := ∅, fvarSet := ∅ } a let _do_jp : Lean.CollectFVars.State → PUnit → Lean.MetaM (List Lean.FVarId × Lean.FVarIdSet) := fun s' y => let todo := todo; let s := s; do let r ← let col := s'.fvarSet; forIn col { fst := s, snd := todo } fun fvarId r => let s := r.fst; let todo := r.snd; if Std.RBTree.contains s fvarId = true then do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := todo }) else let todo := fvarId :: todo; let s := Std.RBTree.insert s fvarId; do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := todo }) let x : MProd Lean.FVarIdSet (List Lean.FVarId) := r match x with | { fst := s, snd := todo } => pure (todo, s) match Lean.LocalDecl.value? localDecl with | some val => do let a ← Lean.Meta.instantiateMVars val let s' : Lean.CollectFVars.State := Lean.collectFVars s' a let y ← pure PUnit.unit _do_jp s' y | x => do let y ← pure PUnit.unit _do_jp s' y
partial def
Lean.Meta.mkGeneralizationForbiddenSet.loop
(todo : List Lean.FVarId)
(s : Lean.FVarIdSet)
:
Equations
- Lean.Meta.getFVarSetToGeneralize targets forbidden = let s := Array.foldl (fun s target => if Lean.Expr.isFVar target = true then Std.RBTree.insert s (Lean.Expr.fvarId! target) else s) ∅ targets 0 (Array.size targets); let r := ∅; do let a ← Lean.getLCtx let r ← let col := a; forIn col { fst := s, snd := r } fun localDecl r => let s := r.fst; let r := r.snd; if Std.RBTree.contains forbidden (Lean.LocalDecl.fvarId localDecl) = true then do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := r }) else if (Lean.LocalDecl.isAuxDecl localDecl || Lean.BinderInfo.isInstImplicit (Lean.LocalDecl.binderInfo localDecl)) = true then do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := r }) else do let a ← Lean.getMCtx if (Lean.MetavarContext.findLocalDeclDependsOn a localDecl fun fvarId => Std.RBTree.contains s fvarId) = true then let r := Std.RBTree.insert r (Lean.LocalDecl.fvarId localDecl); let s := Std.RBTree.insert s (Lean.LocalDecl.fvarId localDecl); do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := r }) else do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := r }) let x : MProd Lean.FVarIdSet Lean.FVarIdSet := r match x with | { fst := s, snd := r } => pure r
def
Lean.Meta.getFVarsToGeneralize
(targets : Array Lean.Expr)
(forbidden : optParam Lean.FVarIdSet ∅)
:
Equations
- Lean.Meta.getFVarsToGeneralize targets forbidden = do let forbidden ← Lean.Meta.mkGeneralizationForbiddenSet targets forbidden let s ← Lean.Meta.getFVarSetToGeneralize targets forbidden Lean.Meta.sortFVarIds (Std.RBTree.toArray s)