Lean4
/-- The main implementation of the flexible linter. -/
def flexibleLinter : Linter where
run :=
withSetOptionIn fun _stx => do
unless getLinterValue linter.flexible (← getLinterOptions) && (← getInfoState).enabled do
return
if (← MonadState.get).messages.hasErrors then
return
let trees ← getInfoTrees
let x :=
trees.map
(extractCtxAndGoals (fun _ => true))
-- `stains` records pairs `(location, mvar)`, where
-- * `location` is either a hypothesis or the main goal modified by a flexible tactic and
-- * `mvar` is the metavariable containing the modified location
let mut stains : Array ((FVarId × MVarId) × (Stained × Syntax)) := #[]
let mut msgs : Array (Syntax × Syntax × Stained) := #[]
for d in x do
for (s, ctx0, ctx1, mvs0, mvs1) in d do
let skind := s.getKind
if stoppers.contains skind then
continue
let shouldStain? := flexible? s && mvs1.length == mvs0.length
for d in getStained! s do
if shouldStain? then
for currMVar1 in mvs1 do
let lctx1 := (ctx1.decls.findD currMVar1 default).lctx
let locsAfter := d.toFMVarId currMVar1 lctx1
stains := stains ++ locsAfter.map (fun l ↦ (l, (d, s)))
else
let stained_in_syntax := if usesGoal? skind then (toStained s).insert d else toStained s
if !flexible.contains skind then
for currMv0 in mvs0 do
let lctx0 := (ctx0.decls.findD currMv0 default).lctx
let mut foundFvs : Std.HashSet (FVarId × MVarId) := { }
for st in stained_in_syntax do
for d in st.toFMVarId currMv0 lctx0 do
if !foundFvs.contains d then
foundFvs := foundFvs.insert d
for l in foundFvs do
if let some (_stdLoc, (st, kind)) := stains.find? (Prod.fst · == l) then
msgs :=
msgs.push
(s, kind, st)
-- tactics often change the name of the current `MVarId`, so we migrate the `FvarId`s
-- in the "old" `mvars` to the "same" `FVarId` in the "new" `mvars`
let mut new : Array ((FVarId × MVarId) × (Stained × Syntax)) := .empty
for (fv, (stLoc, kd)) in stains do
let psisted := reallyPersist #[fv] mvs0 mvs1 ctx0 ctx1
if psisted == #[] && mvs1 != [] then
new := new.push (fv, (stLoc, kd))
dbg_trace "lost {((fv.1.name, fv.2.name), stLoc, kd)}"
for p in psisted do
new := new.push (p, (stLoc, kd))
stains := new
for (s, stainStx, d) in msgs do
Linter.logLint linter.flexible stainStx m! "'{stainStx }' is a flexible tactic modifying '{d}'…"
logInfoAt s m! "… and '{s }' uses '{d}'!"
