Modeling nested scoping

Problem

How to model nested scoping in stack graphs? The problematic pattern is illustrated by the following lambda term:

(\x\y.x) t t'

The question is what the stack graph model is that ensures the result of this whole term is t.

This problem occurs in dynamic languages with nested functions where we model data flow (e.g., JavaScript & Python), as well as in static languages with nested type abstractions (i.e., TypeScript & Java).

MWE

I created a minimal(-ish) working example using JavaScript that illustrates this problem, which can be found in tree-sitter-code-nav/tree/mwe-nested-scoping. The JavaScript rules are stripped down to set that implements a lambda calculus. The examples directory contains several examples of different cases. The file id.js defines an id function, which works as expected. The file const.js defines a cnst function with a nested function which exhibits the problem. For comparison, there is also nested-calls.js, which does a regular function call from a function body.

The JavaScript program exhibiting the problem:

let o1 = {a:{}};
let o2 = {b:{}};

let cnst = function (x) {
    return function (y) {
        return x;
    }
}

cnst(o1)(o2).a;

The ccorresponding stack graph:

Discussion

The core of the problem is that this kind of scoping results in two consecutive scoped pop nodes. The second pop replaces the scope stack coming from the first pop, which is lost. However, because the inner function can see the enclosing function, a reference the parameter of the outer function (y in our example) steps out of its own scope into the surrounding scope. In this surrounding scope, the the scope stack from the first push should be used for any jumps, instead of the scope stack resulting from the pop of the inner function.

In the MWE, the point where we step out of the inner scope is marked by a DROP-ONE node (here in the rules). However, this does not have the intended behavior. It pops the top of the scope stack, but it should instead restore the outer scope stack somehow.

Possible Solution

I have sketched my idea of using a stack of scope stacks, instead of a single stack. The top of that scope stack stack behaves as the current scope stack, but the remainder of the scope stack stack is captured on push and restored on jump, so that we always restore the complete context as it was at the push. A drop simply drops the top, going to the scope context as it was before the last push (which corresponds to stepping out of the scope of the nested function into the enclosing function).

Edit: Instead of scope stack stack, I am now calling it a scope context, which contains scope stacks.

Stack graph rules: stack-graphs.pdf

Rules applied to the example to illustrate the effect during resolution: paths-for-example.pdf

github / stack-graphs