Reworking Pterodactyl’s program elaboration [01KJ]

I thought I was being clever with my approach to elaborating Epigram-style program trees, but I am seeing that I really should have hewed more closely to the presentation of Elaborating Inductive Definitions. The “clever” thing I did was have the elaborator environment keep track of what amounts to a program label in the sense of Epigram, and append stack frames to it when entering the subgoals of negative introduction rules. This is a bit brittle, because it forces a coupling between the use of introduction rules and the shape of user-defined programming problems that is unlikely to hold true in the future. In particular, I think this approach will break down very quickly when I begin allowing things like goal generalisation, etc.

I tentatively think that the elaborator should not keep track of the programming label as part of its local state, and the interaction with programming labels should be restricted to the specific refinement rules for program trees, just as in Figure 6 of Elaborating Inductive Definitions.

Another place where I have probably erred is in treating each clause of a program tree as a separate declaration (a unit of incrementality). I think that instead these should be treated as a single hierarchical declaration. In the future it could be a good idea to incrementalise this, and I think it can be done on top of a simpler hierarchical declaration. Trying to do all this at once is flying too close to the sun.

In short, I believe I should retreat a bit and implement almost exactly what is written in Elaborating Inductive Definitions.