More better documentation tomorrow, but I’ve hacked up the abstract syntax and operational semantics of a framework for definitions, holes and modules with parameters. I’ve implemented a parser from a textual format. The abstract syntax uses long names and is fully λ-lifted, whilst the concrete syntax is suitably localised. The code is a bit of a mess, but I’m too tired to tidy it now. I hasten to add that I haven’t got a checker for object files, just a somewhat trusting reader. Of course, in a lazy language, you can cache the semantics on loading the text as long as you promise not to use it until you’ve checked the corresponding syntax…
I’m doing a bit of a tidy now. This code is fairly essentially monadic, so I’m cleaning it up with the assistance of some Monad transformers…
Email is a distraction, so I’ve switched it off. If you need me, phone me…
Much tider now. I also fixed a bug I introduced last night into DeBruijn.lhs. See if you can spot it…