I’ve built a bit of concrete syntax for ‘object files’, being files packing up the results of elaboration, which live in some kind of framework. The syntax is quite simple
FrameObject := UId Frame
Frame :=
- {FrameObject}Frame
- (UId : Term)Frame
- FrameThing
FrameThing :=
- ⇒ Term : Term
- —
- …
FrameThing accounts for definitions and modules respectively, with holes, datatype bits and such to come in a while. Frame equips these things with parametrization and subobjects. The point is that the subobjects are local yet visible and that common parameters are shared. Note that, provided objects at each level have distinct names, a sequence of UId and a sequence of Term determine at most one thing.
An object file should contain a sequence of FrameObject. We can nest object files if we add a ‘File’ production to FrameThing.
What I need to do now is to implement the construction of the semantic objects from this syntax. With that done, several fronts open simultaneously…