We sat in James’s garden, drank bad espresso, and enjoyed the nice weather. We also spent some time talking about the state Epigram was in.
* There appears to be a scoper. It works – i.e. compiles and delivers coloured IORefs.
* TODO Cache scope stack at each node. This should be trivial modification as we’re parametric in the labelling of recursive subnodes. We still need to write something to turn coloured IORefs into coloured Strings, which Joel can render.
* The hierarchical proof state is in pieces on pieces on Conor’s floor. Conor really wants to rethink things before working this out further.
* DONE Name resolution and christening works (more or less).
* TODO Navigation and update of hierarchical datastructure needs serious work.
* TODO Commit mechanism for updating meta variables
* Joel’s been messing about with Gtk2hs. He hopes to have something that at least renders concrete syntax by next week.
* How should we organise representation of terms to perform efficient updates?
We may want to design a drop-in replacement for terms in the proof state. We do not want to change values, just the terms. The replacement should support cheap update actions and convert easily between the actual terms. It’s a nice separable job for Wouter.
Once the proof state has been updated, we can work on the theorem prover layer.
Plan of action
James and Conor should work on proof state manipulations.
Peter should continue working on data types.
Edwin was here last meeting. He went away having some clue about the Term data
type. Compilation would be a good thing to have, but requires him having a fair amount of time.