Three things on the slate this week
- Datatypes for OTT: the current implementation loses canonicity if you use the notion of datatype from the pre-OTT days, so we need to bring this up to date. Peter Morris and I have a plan bearing a certain resemblance to what’s going on in the Indexed Containers paper; we also have a longer term plan, with an even stronger resemblance to the same, but that’s another story.
- Hierarchical proof state for Ecce: my Oleg theory of holes has the annoying problem that objects only have private subobjects (within so-called ‘guesses’); subobjects which need to be visible get λ-lifted and exported to the global context, resulting in a flattening of the elaboration tree, a loss of sharing, you name it. Just do a proof-state dump in Epigram 1 (META-RET, then look in *Epigram-bin*) if you don’t know what I’m talking about. So the plan is to do away with guesses in favour of hierarchically stored but fully λ-lifted holes and definitions. With a twist: we use a relative mode of naming, omitting the parameters held in common between reference and referent. So although these things are globally global, locally they look local. Oh, wait and see…
- Dummy elaborator for high-level source code. Joel has refactored the grammar and the parser; Peter has refactored the scoper; we just need to reassemble the pieces we had before and we have a basis to build a real UI. We might have the beginnings of a non-dummy elaborator soon enough too.