### Binding-Time Analysis

The purpose of binding-time analysis is to factor the program into the
generating extension and the residual code. The analysis is described
here as an abstract interpretation [NN?], with binding times as
abstract values. It may be more efficient to implement as a type
inference [Henglein91].

The analysis starts with a root language code structure and the
binding times of its arguments. The simplest binding times are static
(`S`

) and dynamic (`D`

). Static arguments are available to the
generated compiler, and are thus considered `program'; dynamic
arguments appear as arguments to the code returned by the compiler.

Since there are no infinite ascending chains in the binding-time
lattice, termination of cogen is guaranteed.

The set of binding times (the lattice) is described in five steps,
each elaborates the previous in order to capture more static
information.

- simple
- pairs
- first-order jumps and constants
- higher order jumps
- spines

The final, formal definition of the binding times:

`bt` ::= `S`

| `D`

| (cons `bt` `bt` `cp` `is-clo` `is-sure`) | (const `v`)
`cp` ::= `instruction`
`is-clo` ::= `boolean`
`is-sure` ::= `boolean`
`v` ::= `any-value`

I haven't finished the formal definition of the ordering of the
lattice. Here's a first approximation:

(const `v`) < `S`

< (cons `a` `d` ...) < `D`

(cons `a1` `d1` `cp1` ...) <= (cons `a2` `d2` `cp2` ...) <==>
`a1` <= `a2` and `d1` <= d2 and cp1 = cp2