Scoping traverses concrete syntax, threading some effects:
- reading the scope, being (concretely) an alist of strings to namerefs; what is its abstract interface?
- generating new namerefs, due either to an explicit binding (in a pattern or a shadow), or to an implicit binding (a previously unseen name in an lhs or a sig)
- accumulating the set of new namerefs, when we see a name which is not in an explicit binding position, we should look it up if we can and generate a new nameref if not; we must accumulate the set of these names so we can add them to the relevant shadow; this way, the elaborator will know exactly where everything is to be bound
- building imperative syntax trees: we may as well get our node identifiers from the ref supplier; also, we can equip trees with backpointers, and possibly other editor-related gubbins
Scoping will also need to generate binary applications, handling any weird operators we might allow. I’ll have a stab at the datatype of nodes in a bit.
What could be the exact format to exchange the information between Epigram and external editors? Could it be XML?
I’m planning to specify a Haskell-level interface: datatypes and functionality which are delivered to and required of an external editor. Anyone writing such an editor would thus need to write at least a little Haskell to turn this into some kind of command-response interface. There is no reason why such a command-response interface should not use XML as its interchange format (given suitably serialisable datatypes). So packing up Epigram as some kind of server communicating in XML will be possible, but not compulsory.