Lean4
/-- `reallyPersist` converts an array of pairs `(fvar, mvar)` to another array of the same type. -/
def reallyPersist (fmvars : Array (FVarId × MVarId)) (mvs0 mvs1 : List MVarId) (ctx0 ctx1 : MetavarContext) :
Array (FVarId × MVarId) :=
Id.run
(do
-- split the input `fmvars` into
-- * the `active` ones, whose `mvar` appears in `mvs0` and
-- * the `inert` ones, the rest.
-- `inert` gets copied unchanged, while we transform `active`
let (active, inert) := fmvars.partition fun (_, mv) => mvs0.contains mv
let mut new := #[]
for (fvar, mvar) in active do -- for each `active` pair `(fvar, mvar)`
match ctx0.decls.find? mvar with -- check if `mvar` is managed by `ctx0` (it should be)
| none => -- the `mvar` is not managed by `ctx0`: no change
new := new.push (fvar, mvar)
| some mvDecl0 => -- the `mvar` *is* managed by `ctx0`: push the pair `(fvar, mvar)` through
for mv1 in mvs1 do -- for each new `MVarId` in `mvs1`
match ctx1.decls.find? mv1 with -- check if `mv1` is managed by `ctx1` (it should be)
| none =>
dbg_trace"'really_persist' could this happen?"
default
| some mvDecl1 => -- we found a "new" declaration
let persisted_fv := persistFVars fvar mvDecl0.lctx mvDecl1.lctx
new := new.push (persisted_fv, mv1)
return inert ++ new)
