Lean4
/-- Return the Interfaces for rewriting `e`, both filtered and unfiltered. -/
def getRewriteInterfaces (e : Expr) (occ : Option Nat) (loc : Option Name) (except : Option FVarId)
(range : Lsp.Range) : MetaM (Array (Array RewriteInterface × Kind) × Array (Array RewriteInterface × Kind)) := do
let mut filtr := #[]
let mut all := #[]
for rewrites in ← getHypothesisRewrites e except do
let rewrites ← rewrites.mapM fun (rw, fvarId) => rw.toInterface (.inr fvarId) occ loc range
all := all.push (rewrites, .hypothesis)
filtr := filtr.push (← filterRewrites e rewrites (·.replacement) (·.makesNewMVars), .hypothesis)
for rewrites in ← getModuleRewrites e do
let rewrites ← rewrites.mapM fun (rw, name) => rw.toInterface (.inl name) occ loc range
all := all.push (rewrites, .fromFile)
filtr := filtr.push (← filterRewrites e rewrites (·.replacement) (·.makesNewMVars), .fromFile)
for rewrites in ← getImportRewrites e do
let rewrites ← rewrites.mapM fun (rw, name) => rw.toInterface (.inl name) occ loc range
all := all.push (rewrites, .fromCache)
filtr := filtr.push (← filterRewrites e rewrites (·.replacement) (·.makesNewMVars), .fromCache)
return (filtr, all)
