The "extended ancestors" generator, with a proof of correctness

[Edward K. Ream]

This post discusses a beautiful generator created by Vitalije Milosevic. This generator quickly yields what I call all the "extended ancestors" of a vnode v. Two time-sensitive routines, g.getLanguageFromAncestorAtFileNode, and v.setAllAncestorAtFileNodesDirty use this generator.

In this post I'll discuss the generator and outline of a proof of correctness.

The generator

Here is the latest form of the generator:

v = << vnode whose ancestors are to be discovered >>
seen = set([v.context.hiddenRootNode])

def v_and_parents(v):
    if v in seen:
        return
    seen.add(v)
    yield v
    for parent_v in v.parents:
        if parent_v not in seen:
            yield from v_and_parents(parent_v)

The generator yields all vnodes that are extended ancestors of v:

- all vnodes that are ancestors of v itself,

- all ancestors of any node v_c that is a clone of any ancestor of v.

This generator handles clones elegantly: if v_c is a clone, the v_c.parents array will contain more than one vnode.

I tweaked this generator while working on PR #2321. I added the "seen" set and related logic.

Proof of correctness

The proof must show that:

1.  the generator yields all extended ancestors of v.

2. the generator will terminate.

Part 1 is guaranteed because if v_c is a clone, the generators will include all (direct) ancestors of v_c in the search.

Part 2 is guaranteed because the seen set ensures that the generator examines vnodes at most once. In fact, the generator would terminate without the seen logic, but it might yield vnodes more than once.

History

I recently "rediscovered" this generator while working on g.getLanguageFromAncestorAtFileNode. See PR #2314.  My new code was similarly fast, but much less elegant because it didn't use a generator.

I then wondered whether I could speed up v.setAllAncestorAtFileNodesDirty using the same idea.  Heh!  Vitalije had done the job better!  So I used Vitalije's generator in g.getLanguageFromAncestorAtFileNode.

Finally, I added the "seen" logic to both generators.

Summary

g.getLanguageFromAncestorAtFileNode and v.setAllAncestorAtFileNodesDirty owe their speed to this beautiful generator.  Thank you, Виталије Милошевић.

Edward