|
|
|---|
|
|
|
|---|
Representation of the FGL interpreter stack.
FGL stores the stack of its interpreter as a nested stobj
A major-stack is a nonempty list of major-frame objects. Each such frame represents an entirely new scope for variables such as a function definition or rewrite rule application. Each major-frame contains some debugging info, a variable bindings alist, and a minor-stack, which is a nonempty list of minor-frame objects. Each minor frame represents a lambda body within the larger context of the major frame. It has its own bindings and debugging info, as well as a list of scratch objects representing arguments to be passed to subsequent function calls.
The distinction between major and minor stack frames is subtle, especially given ACL2's insistence that lambdas bind all the variables found in their bodies. The difference is that in FGL, when we encounter a lambda nesting, we preprocess it so as to ignore variables that are re-bound to themselves, instead keeping the current bindings and only adding to them. On the other hand, when we apply a rewrite rule we enter a completely new namespace where initially only the variables of the unifying substitution are bound. This lazy binding of lambdas allows us to support syntax-bind by allowing us to leave variables unbound until they are used in a nontrivial way: that is, passed into a function or bound to a different variable in a lambda.