James C and I are trying to make some progress on this hierarchical proof state lark. The new file EcceThump.lhs is our working file, but it will eventually get renamed, reorganised etc. Our new data structure seems a little cleaner than the previous one, which I find reassuring. I expect we’ll get quite a lot of this file by cut-paste-refactor from various versions of Ecce.lhs we have lying around. I’ve already ported the resolver from my previous abortive attempt at this. Correspondingly, I’ve been able to write something which claims to be a ‘loader’, inserting a new chunk of proof state (in concrete syntax) at the current cursor. It just trusts the supplier, rather than typechecking anything.
Next up, I’ll be porting the Christener and writing some sort of crude display mechanism, so we can see what we’re doing. Then it’ll be time to write some operations which actually do intros and claim/let in a typechecked manner. After that, we need to implement (anti-)refinement and update-propagation. I’ve already installed some dependency book-keeping, so we’ll see how that goes.