Changes in cbneed spec.
Changes in cbneed spec.

I realized that there is a potential problem with the abstract state
space: function appplication expressions |@F| are generated at runtime.
This isn't a huge problem because these generated expresssions are a
combination of 1) a function application from the source and 2) a binder
supplied at runtime. This does indeed result in a finite state space,
but it isn't linear in program points, rather it's quadratic. Clearly
something isn't quite right.

I discovered this when I went to give unique identifiers to program
points; I wasn't able to use freshly generated integers for the
dynamically created expressions. At best I would need to use a product
of source location and a binder as the identifier for these dynamically
generated expressions.

This caused me to rethink my allocation strategy. In the old design, ref
cells carried around with them the name they would use to allocate
results that flow out of them. This seemed okay, but cause the problem
mentioned above.

The solution (and I think the right design) is for |@F| and |CASE| forms
to have two unique identifiers: one when that expression is reached, and
one for the expression when it is used as a continuation. Because of
this, the same binder needs to be used when these are turned into
continuations. As a result, the binder associated with |REF| values
before is now assocaited with |@F| and |CASE| expressions, and the state
space for control expressions can now be represented as a single
globally unique integer generated up front.

Now to implement it...

davdar/maam,FranklinChen/maam